Zulip Chat Archive

Stream: general

Topic: Field of 4 elements


view this post on Zulip 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]?

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

end F4

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Feb 22 2019 at 23:09):

yeah but specifically 4 elements

view this post on Zulip Mario Carneiro (Feb 22 2019 at 23:36):

insert q= 4?

view this post on Zulip Kenny Lau (Feb 22 2019 at 23:41):

that seems too much work for something not with that purpose

view this post on Zulip Mario Carneiro (Feb 22 2019 at 23:42):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Feb 22 2019 at 23:44):

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

view this post on Zulip Kenny Lau (Feb 22 2019 at 23:44):

simple as in not complicated

view this post on Zulip Mario Carneiro (Feb 22 2019 at 23:44):

ring? How about zmod 2 x zmod 2

view this post on Zulip Mario Carneiro (Feb 22 2019 at 23:45):

or rat or real

view this post on Zulip Kenny Lau (Feb 22 2019 at 23:48):

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

view this post on Zulip Mario Carneiro (Feb 22 2019 at 23:48):

sqrt 2 is not in Q

view this post on Zulip Kenny Lau (Feb 22 2019 at 23:50):

sqrt 2 is easier than 1/2?

view this post on Zulip Mario Carneiro (Feb 22 2019 at 23:51):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 22 2019 at 23:52):

or 0 < 1/2 <1

view this post on Zulip Kenny Lau (Feb 22 2019 at 23:52):

lemme try that later

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Feb 23 2019 at 00:01):

yeah but are they in mathlib?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Feb 23 2019 at 00:03):

oh brilliant

view this post on Zulip Mario Carneiro (Feb 23 2019 at 00:03):

i not real also sound like a good candidate

view this post on Zulip 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 :-)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 23 2019 at 00:04):

Lack of examples makes maths UG example sheets harder to do

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 23 2019 at 00:05):

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

view this post on Zulip Mario Carneiro (Feb 23 2019 at 00:06):

I consider example making part of the educator's job

view this post on Zulip Kenny Lau (Feb 23 2019 at 01:05):

we have theorems about irrational numbers but not rational numbers?

view this post on Zulip Kenny Lau (Feb 23 2019 at 01:09):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 23 2019 at 01:10):

what is is_supported pure?

view this post on Zulip 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