Artin–Schreier extensions

A root of X ^ p - X - u in characteristic p generates a Galois extension whose automorphisms translate the root by elements of the prime field. If u is not of the form w ^ p - w in the base field, the extension has degree p and its Galois group is the additive group of ZMod p. This supplies the field-theoretic input for the ramification theory of Artin–Schreier covers.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Proposition 3.7.8.
• Mathlib: Subfield.splits_bot and IsGalois.card_aut_eq_finrank.

theorem TauCeti.ArtinSchreier.splits {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {u : K} {y : L} (hy : y ^ p - y = (algebraMap K L) u) : (Polynomial.map (algebraMap K L) (Polynomial.X ^ p - Polynomial.X - Polynomial.C u)).Splits

An Artin–Schreier polynomial splits in any field containing one of its roots.

theorem TauCeti.ArtinSchreier.isSplittingField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {u : K} {y : L} (hy : y ^ p - y = (algebraMap K L) u) (hgen : K⟮y⟯ = ⊤) : Polynomial.IsSplittingField K L (Polynomial.X ^ p - Polynomial.X - Polynomial.C u)

A field generated by an Artin–Schreier root is its polynomial's splitting field.

theorem TauCeti.ArtinSchreier.isGalois {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {u : K} {y : L} (hy : y ^ p - y = (algebraMap K L) u) (hgen : K⟮y⟯ = ⊤) : IsGalois K L

A generated Artin–Schreier extension is Galois, including the trivial case.

noncomputable def TauCeti.ArtinSchreier.translationHom {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {u : K} {y : L} (hy : y ^ p - y = (algebraMap K L) u) : Gal(L/K) →* Multiplicative (ZMod p)

The translation character sends an automorphism to the prime-field displacement of the chosen Artin–Schreier root. The multiplicative type tag matches composition in Gal.

Equations

• TauCeti.ArtinSchreier.translationHom hy = { toFun := fun (σ : Gal(L/K)) => Multiplicative.ofAdd (TauCeti.ArtinSchreier.translation✝ hy σ), map_one' := ⋯, map_mul' := ⋯ }

theorem TauCeti.ArtinSchreier.aut_apply_eq_add_translationHom {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {u : K} {y : L} (hy : y ^ p - y = (algebraMap K L) u) (σ : Gal(L/K)) : σ y = y + (Multiplicative.toAdd ((translationHom hy) σ)).cast

The translation character computes the action on the chosen root.

theorem TauCeti.ArtinSchreier.translationHom_injective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {u : K} {y : L} (hy : y ^ p - y = (algebraMap K L) u) (hgen : K⟮y⟯ = ⊤) : Function.Injective ⇑(translationHom hy)

An automorphism of a generated Artin–Schreier extension is determined by its translation of the generator.

theorem TauCeti.ArtinSchreier.isCyclic {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {u : K} {y : L} (hy : y ^ p - y = (algebraMap K L) u) (hgen : K⟮y⟯ = ⊤) : IsCyclic Gal(L/K)

Every generated Artin–Schreier extension has a cyclic Galois group.

theorem TauCeti.ArtinSchreier.finrank_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {u : K} {y : L} (hy : y ^ p - y = (algebraMap K L) u) (hgen : K⟮y⟯ = ⊤) (hu : ∀ (w : K), w ^ p - w ≠ u) : Module.finrank K L = p

A nontrivial Artin–Schreier class gives an extension of degree exactly p.

noncomputable def TauCeti.ArtinSchreier.autEquivZmod {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {u : K} {y : L} (hy : y ^ p - y = (algebraMap K L) u) (hgen : K⟮y⟯ = ⊤) (hu : ∀ (w : K), w ^ p - w ≠ u) : Gal(L/K) ≃* Multiplicative (ZMod p)

For a nontrivial Artin–Schreier class, every prime-field translation occurs as a unique automorphism.

Equations

• TauCeti.ArtinSchreier.autEquivZmod hy hgen hu = MulEquiv.ofBijective (TauCeti.ArtinSchreier.translationHom hy) ⋯

@[simp]

theorem TauCeti.ArtinSchreier.autEquivZmod_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {u : K} {y : L} (hy : y ^ p - y = (algebraMap K L) u) (hgen : K⟮y⟯ = ⊤) (hu : ∀ (w : K), w ^ p - w ≠ u) (σ : Gal(L/K)) : (autEquivZmod hy hgen hu) σ = (translationHom hy) σ

The Galois-group equivalence is the translation character of the chosen root.

@[simp]

theorem TauCeti.ArtinSchreier.autEquivZmod_symm_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] {u : K} {y : L} (hy : y ^ p - y = (algebraMap K L) u) (hgen : K⟮y⟯ = ⊤) (hu : ∀ (w : K), w ^ p - w ≠ u) (c : Multiplicative (ZMod p)) : ((autEquivZmod hy hgen hu).symm c) y = y + (Multiplicative.toAdd c).cast

The inverse Galois-group equivalence translates the generator by its argument.