## Stream: general

### Topic: Field of 4 elements

#### Kenny Lau (Feb 22 2019 at 22:17):

Does the field of 4 elements have its place in mathlib? I am using it in my little project as a ring that is not generated by 1, and the decidability was quite useful; if I PR my use case to mathlib, do I need to replace it by a more "regular" ring such as ZxZ or Z[X]?

#### Kenny Lau (Feb 22 2019 at 22:20):

@[derive decidable_eq]
inductive F4 : Type | z | o | a | b

namespace F4

instance : fintype F4 :=
{ elems := {z, o, a, b},
complete := λ x, by cases x; simp }

def add : F4 → F4 → F4
| z x := x
| x z := x
| o o := z
| o a := b
| o b := a
| a o := b
| a a := z
| a b := o
| b o := a
| b a := o
| b b := z

def mul : F4 → F4 → F4
| z x := z
| x z := z
| o x := x
| x o := x
| a a := b
| a b := o
| b a := o
| b b := a

def inv : F4 → F4
| z := z
| o := o
| a := b
| b := a

instance : discrete_field F4 :=
by refine
zero := z,
neg := id,
mul := mul,
one := o,
inv := inv,
has_decidable_eq := F4.decidable_eq,
.. }; tactic.exact_dec_trivial

end F4


#### Chris Hughes (Feb 22 2019 at 22:50):

You can prove discrete_field constructively for adjoin_root using euclidean division I guess, or just for finite fields using a search.

#### Kevin Buzzard (Feb 22 2019 at 23:09):

I think there's a place in mathlib for the field with q elements, and one could define it as the splitting field of X^q-X over Z/pZ if q is a power of p

#### Kenny Lau (Feb 22 2019 at 23:09):

yeah but specifically 4 elements

insert q= 4?

#### Kenny Lau (Feb 22 2019 at 23:41):

that seems too much work for something not with that purpose

#### Mario Carneiro (Feb 22 2019 at 23:42):

but this seems like a lot of case analysis for a more abstract thing

#### Mario Carneiro (Feb 22 2019 at 23:43):

If you just need to know a field with 4 elements exists, that's definitely part of a more general theorem

#### Kenny Lau (Feb 22 2019 at 23:44):

no I just want a simple ring that is not generated by 1

#### Kenny Lau (Feb 22 2019 at 23:44):

simple as in not complicated

#### Mario Carneiro (Feb 22 2019 at 23:44):

ring? How about zmod 2 x zmod 2

#### Mario Carneiro (Feb 22 2019 at 23:45):

or rat or real

#### Kenny Lau (Feb 22 2019 at 23:48):

and you need to be able to prove that it is not generated by 1

#### Mario Carneiro (Feb 22 2019 at 23:48):

sqrt 2 is not in Q

#### Kenny Lau (Feb 22 2019 at 23:50):

sqrt 2 is easier than 1/2?

#### Mario Carneiro (Feb 22 2019 at 23:51):

I wasn't sure which "generated" you meant. 1/2 works too

#### Mario Carneiro (Feb 22 2019 at 23:51):

I recall Kevin looking for a short proof that 1/2 is not an integer. I think noting it has denominator 2 works

or 0 < 1/2 <1

#### Kenny Lau (Feb 22 2019 at 23:52):

lemme try that later

#### Kevin Buzzard (Feb 22 2019 at 23:59):

Q is not generated by 1 because Z is a subring and 1/2 is not an integer

#### Kevin Buzzard (Feb 23 2019 at 00:01):

The complexes are not generated by 1 because the reals are a subring and i is not real, maybe that's easier

#### Kenny Lau (Feb 23 2019 at 00:01):

yeah but are they in mathlib?

#### Mario Carneiro (Feb 23 2019 at 00:03):

We usually don'r state such theorems explicitly, but sqrt 2 not in Q is an exception

oh brilliant

#### Mario Carneiro (Feb 23 2019 at 00:03):

i not real also sound like a good candidate

#### Kevin Buzzard (Feb 23 2019 at 00:03):

You mean the fact that the reals are a subring? Everything else is. Why do you want examples anyway? It's theorems we need :-)

#### Mario Carneiro (Feb 23 2019 at 00:04):

That's my point. Most of these are just "examples" so they don't go in mathlib

#### Kevin Buzzard (Feb 23 2019 at 00:04):

Lack of examples makes maths UG example sheets harder to do

#### Mario Carneiro (Feb 23 2019 at 00:04):

There are a few cases of examples that are actually useful for theorems, and I think having simple things like this is good

#### Mario Carneiro (Feb 23 2019 at 00:05):

that's a good thing, it means the kids can't cheat :)

#### Mario Carneiro (Feb 23 2019 at 00:06):

I consider example making part of the educator's job

#### Kenny Lau (Feb 23 2019 at 01:05):

we have theorems about irrational numbers but not rational numbers?

#### Kenny Lau (Feb 23 2019 at 01:09):

thanks, sqrt 2 worked like a charm! @Mario Carneiro

#### Kenny Lau (Feb 23 2019 at 01:09):

theorem is_supported_pure {p} {s : set α} : is_supported (pure p) s ↔ p ∈ s :=
suffices is_supported (pure p) s → p ∈ s, from ⟨this, λ hps, ring.subset_closure ⟨p, hps, rfl⟩⟩,
assume hps : is_supported (pure p) s, begin
classical,
have : ∀ x, is_supported x s → ∃ q : ℚ, lift (λ q, if q ∈ s then 0 else real.sqrt 2) x = ↑q,
{ intros x hx, refine ring.in_closure.rec_on hx _ _ _ _,
{ use 1, rw [lift_one, rat.cast_one] },
{ use -1, rw [lift_neg, lift_one, rat.cast_neg, rat.cast_one], },
{ rintros _ ⟨z, hzs, rfl⟩ _ _, use 0, rw [lift_mul, lift_of, if_pos hzs, zero_mul, rat.cast_zero] },
{ rintros x y ⟨q, hq⟩ ⟨r, hr⟩, use q+r, rw [lift_add, hq, hr, rat.cast_add] } },
specialize this (of p) hps, rw [lift_of] at this, split_ifs at this, { exact h },
exfalso, exact irr_sqrt_two this
end


#### Mario Carneiro (Feb 23 2019 at 01:10):

what is is_supported pure?

#### Kenny Lau (Feb 23 2019 at 01:11):

def is_supported (x : free_comm_ring α) (s : set α) : Prop :=
x ∈ ring.closure (of '' s)


Last updated: May 13 2021 at 19:20 UTC