Field of 4 elements

Stream: general

[Kenny Lau]

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]

@[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
{ add := add,
  zero := z,
  neg := id,
  mul := mul,
  one := o,
  inv := inv,
  has_decidable_eq := F4.decidable_eq,
  .. }; tactic.exact_dec_trivial

end F4

[Chris Hughes]

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

[Kevin Buzzard]

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]

yeah but specifically 4 elements

[Mario Carneiro]

insert q= 4?

[Kenny Lau]

that seems too much work for something not with that purpose

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

simple as in not complicated

[Mario Carneiro]

ring? How about zmod 2 x zmod 2

[Mario Carneiro]

or rat or real

[Kenny Lau]

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

[Mario Carneiro]

sqrt 2 is not in Q

[Kenny Lau]

sqrt 2 is easier than 1/2?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

or 0 < 1/2 <1

[Kenny Lau]

lemme try that later

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

yeah but are they in mathlib?

[Mario Carneiro]

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

[Kenny Lau]

oh brilliant

[Mario Carneiro]

i not real also sound like a good candidate

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Lack of examples makes maths UG example sheets harder to do

[Mario Carneiro]

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]

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

[Mario Carneiro]

I consider example making part of the educator's job

[Kenny Lau]

we have theorems about irrational numbers but not rational numbers?

[Kenny Lau]

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

[Kenny Lau]

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]

what is is_supported pure?

[Kenny Lau]

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