The four elements of a field of order four

A root ω of X² + X + 1 labels the four elements as 0, 1, ω, ω². The explicit enumeration supports finite calculations over this alphabet without choosing another model of the field. Squaring exchanges the two roots in characteristic two.

Additively, a field of four elements is the Klein four-group: zmodTwoProdAddEquiv sends (a, b) : ZMod 2 × ZMod 2 to a + bω, so that the three nonzero elements 1, ω, ω² correspond to (1, 0), (0, 1) and (1, 1). The absolute trace to the prime field is z ↦ z + z².

theorem TauCeti.card_galoisField_two_two [Fintype (GaloisField 2 2)] : Fintype.card (GaloisField 2 2) = 4

The Galois field of order four has four elements, independently of its enumeration.

theorem TauCeti.sq_add_self_add_one_eq_zero {F : Type u_1} [Field F] [Finite F] (hF : Nat.card F = 4) {ω : F} (h0 : ω ≠ 0) (h1 : ω ≠ 1) : ω ^ 2 + ω + 1 = 0

Every element other than zero and one in a field of order four is a root of X² + X + 1.

theorem TauCeti.sq_sq_add_sq_add_one_eq_zero {R : Type u_2} [CommSemiring R] [CharP R 2] {ω : R} (hω : ω ^ 2 + ω + 1 = 0) : (ω ^ 2) ^ 2 + ω ^ 2 + 1 = 0

Squaring preserves roots of X² + X + 1 in characteristic two.

theorem TauCeti.exists_sq_add_self_add_one_eq_zero_of_card_eq_four {F : Type u_1} [Field F] [Finite F] (hF : Nat.card F = 4) : ∃ (ω : F), ω ^ 2 + ω + 1 = 0

Every field of order four contains a root of X² + X + 1.

The additive group of a field of order four

noncomputable def TauCeti.zmodTwoProdAddEquiv {F : Type u_1} [Field F] [Finite F] (hF : Nat.card F = 4) {ω : F} (hω : ω ^ 2 + ω + 1 = 0) : ZMod 2 × ZMod 2 ≃+ F

A field of order four is additively the Klein four-group: given a root ω of X² + X + 1, the pair (a, b) of residues modulo two corresponds to a + bω.

Equations

• TauCeti.zmodTwoProdAddEquiv hF hω = AddEquiv.ofBijective ((TauCeti.zmodTwoHom✝ hF 1).coprod (TauCeti.zmodTwoHom✝ hF ω)) ⋯

theorem TauCeti.zmodTwoProdAddEquiv_apply {F : Type u_1} [Field F] [Finite F] (hF : Nat.card F = 4) {ω : F} (hω : ω ^ 2 + ω + 1 = 0) (a b : ZMod 2) : (zmodTwoProdAddEquiv hF hω) (a, b) = ↑a.val + ↑b.val * ω

The additive identification sends (a, b) to a + bω, using the canonical representatives of a and b.

@[simp]

theorem TauCeti.zmodTwoProdAddEquiv_apply_one_zero {F : Type u_1} [Field F] [Finite F] (hF : Nat.card F = 4) {ω : F} (hω : ω ^ 2 + ω + 1 = 0) : (zmodTwoProdAddEquiv hF hω) (1, 0) = 1

The additive identification sends the first generator to 1.

@[simp]

theorem TauCeti.zmodTwoProdAddEquiv_apply_zero_one {F : Type u_1} [Field F] [Finite F] (hF : Nat.card F = 4) {ω : F} (hω : ω ^ 2 + ω + 1 = 0) : (zmodTwoProdAddEquiv hF hω) (0, 1) = ω

The additive identification sends the second generator to ω.

@[simp]

theorem TauCeti.zmodTwoProdAddEquiv_apply_one_one {F : Type u_1} [Field F] [Finite F] (hF : Nat.card F = 4) {ω : F} (hω : ω ^ 2 + ω + 1 = 0) : (zmodTwoProdAddEquiv hF hω) (1, 1) = ω ^ 2

The additive identification sends the diagonal generator to ω².

@[simp]

theorem TauCeti.zmodTwoProdAddEquiv_symm_one {F : Type u_1} [Field F] [Finite F] (hF : Nat.card F = 4) {ω : F} (hω : ω ^ 2 + ω + 1 = 0) : (zmodTwoProdAddEquiv hF hω).symm 1 = (1, 0)

The inverse additive identification sends 1 to the first generator.

@[simp]

theorem TauCeti.zmodTwoProdAddEquiv_symm_root {F : Type u_1} [Field F] [Finite F] (hF : Nat.card F = 4) {ω : F} (hω : ω ^ 2 + ω + 1 = 0) : (zmodTwoProdAddEquiv hF hω).symm ω = (0, 1)

The inverse additive identification sends ω to the second generator.

@[simp]

theorem TauCeti.zmodTwoProdAddEquiv_symm_root_sq {F : Type u_1} [Field F] [Finite F] (hF : Nat.card F = 4) {ω : F} (hω : ω ^ 2 + ω + 1 = 0) : (zmodTwoProdAddEquiv hF hω).symm (ω ^ 2) = (1, 1)

The inverse additive identification sends ω² to the diagonal generator.

noncomputable def TauCeti.finFourEquiv {F : Type u_1} [Field F] [Finite F] (hF : Nat.card F = 4) {ω : F} (hω : ω ^ 2 + ω + 1 = 0) : Fin 4 ≃ F

Label a field of four elements by 0, 1, ω, ω², in that order.

Equations

• TauCeti.finFourEquiv hF hω = (Equiv.ofBijective ![(0, 0), (1, 0), (0, 1), (1, 1)] TauCeti.finFourEquiv._proof_1✝).trans (TauCeti.zmodTwoProdAddEquiv hF hω).toEquiv

@[simp]

theorem TauCeti.finFourEquiv_apply {F : Type u_1} [Field F] [Finite F] (hF : Nat.card F = 4) {ω : F} (hω : ω ^ 2 + ω + 1 = 0) (i : Fin 4) : (finFourEquiv hF hω) i = ![0, 1, ω, ω ^ 2] i

The four-element labelling evaluates to the displayed tuple.

theorem TauCeti.univ_eq_zero_one_root_sq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : Nat.card F = 4) {ω : F} (hω : ω ^ 2 + ω + 1 = 0) : Finset.univ = {0, 1, ω, ω ^ 2}

The four elements of a field of order four, labelled by a root of X² + X + 1.

theorem TauCeti.algebraMap_trace_eq_add_sq_of_natCard_eq_four {F : Type u_1} [Field F] [Finite F] [Algebra (ZMod 2) F] (hF : Nat.card F = 4) (z : F) : (algebraMap (ZMod 2) F) ((Algebra.trace (ZMod 2) F) z) = z + z ^ 2

The absolute trace of a field of order four to its prime field is z ↦ z + z².