Galois

Results named in Tau Ceti's TauCeti.FieldTheory.Galois modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremArtin's theorem#

M is finite over the field fixed by a finite group of automorphisms.

Mathlib has this for FixedPoints.subfield H M; the fixed field of the Galois correspondence is the same subfield, and this is the instance on that form, with no hypothesis on M / K.

IntermediateField.finiteDimensional_fixedField.{u_1, u_2} {K : Type u_1} {M : Type u_2} [Field K]
  [Field M] [Algebra K M] (H : Subgroup Gal(M/K)) [Finite ↥H] :
  FiniteDimensional (↥(IntermediateField.fixedField H)) M

Lean

Formalized in Tau Ceti as IntermediateField.finiteDimensional_fixedField.

Other forms

Artin's theorem. Formalized in Tau Ceti as IntermediateField.isGalois_fixedField.

IntermediateField.isGalois_fixedField.{u_1, u_2} {K : Type u_1} {M : Type u_2} [Field K] [Field M]
  [Algebra K M] (H : Subgroup Gal(M/K)) [Finite ↥H] : IsGalois (↥(IntermediateField.fixedField H)) M

Artin's theorem, degree form. Formalized in Tau Ceti as IntermediateField.finrank_fixedField_eq_natCard.

IntermediateField.finrank_fixedField_eq_natCard.{u_1, u_2} {K : Type u_1} {M : Type u_2} [Field K]
  [Field M] [Algebra K M] (H : Subgroup Gal(M/K)) [Finite ↥H] :
  Module.finrank (↥(IntermediateField.fixedField H)) M = Nat.card ↥H

Sources

• Tau Ceti documentation: IntermediateField.finiteDimensional_fixedField
• Source of IntermediateField.finiteDimensional_fixedField in TauCeti/FieldTheory/Galois/FixedField.lean

LeanIntermediateField.finiteDimensional_fixedField · IntermediateField.isGalois_fixedField · IntermediateField.finrank_fixedField_eq_natCard

Used by 19

Used byThe Hurwitz bound (Stichtenoth, Exercise 3.18) · Hilbert reciprocity · Local reciprocity for the Weil group · The global class formation · The global invariant · The global invariant is injective · The Kummer case of global existence (Milne VII, Lemma 9.3) · The local class formation · The local invariant · Existence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · The cyclotomic normalization of the local Artin map of a finite extension of ℚ_p · The relative discriminant coefficient of a fixed field from double cosets · The Chebotarev density theorem · The fixed-field Frobenius fiber count · Weighted Chebotarev for abelian extensions · Tate's duality on an open subgroup acting trivially on μₙ · The Kronecker–Weber theorem · The Kummer case of the second fundamental inequality · The finite level of the generator theorem (NSW, proof of (7.4.1))

DefinitionThe fundamental theorem of Galois theory in the ambient model#

For a normal extension E/F the closed subgroups of Gal(E/F) correspond, inclusion-reversingly, to the intermediate fields of the separable closure separableClosure F E / F; an intermediate field of E outside the separable closure has the same fixing subgroup as its separable part.

TauCeti.intermediateFieldEquivClosedSubgroup.{u_1, u_2} {F : Type u_1} {E : Type u_2} [Field F]
  [Field E] [Algebra F E] [Normal F E] :
  IntermediateField F ↥(separableClosure F E) ≃o (ClosedSubgroup Gal(E/F))ᵒᵈ

Lean

Formalized in Tau Ceti as TauCeti.intermediateFieldEquivClosedSubgroup.

Sources

• Tau Ceti documentation: TauCeti.intermediateFieldEquivClosedSubgroup
• Source of TauCeti.intermediateFieldEquivClosedSubgroup in TauCeti/FieldTheory/Galois/AbsoluteGaloisGroup/Basic.lean

LeanTauCeti.intermediateFieldEquivClosedSubgroup

TheoremHilbert's Theorem 90 for cyclic extensions#

If g generates Gal(L/K) and the unit x of L has norm one, then x = g y / y for a unit y of L.

TauCeti.exists_smul_div_eq_of_norm_eq_one.{u_1, u_2} {K : Type u_1} {L : Type u_2} [Field K]
  [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {g : Gal(L/K)}
  (hg : ∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers g) {x : Lˣ} (hx : (Algebra.norm K) ↑x = 1) :
  ∃ y, g • y / y = x

Lean

Formalized in Tau Ceti as TauCeti.exists_smul_div_eq_of_norm_eq_one.

Sources

• Tau Ceti documentation: TauCeti.exists_smul_div_eq_of_norm_eq_one
• Source of TauCeti.exists_smul_div_eq_of_norm_eq_one in TauCeti/FieldTheory/Galois/Hilbert90.lean

LeanTauCeti.exists_smul_div_eq_of_norm_eq_one

Used by 1

Used byHasse--Arf in prime degree

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.