Finite action fields of Galois lattices

The continuous action of the absolute Galois group on a Galois lattice factors through a finite quotient. This file realizes that factorization over an actual finite normal subextension of the chosen algebraic closure. Its fixing subgroup lies in the kernel of the lattice action, so the action descends to the automorphism group of the subextension.

Over an imperfect base the chosen normal extension need not be separable, and no Galois claim is made. Passing to a finite separable splitting field is a later refinement. The finite normal field constructed here is the field-theoretic bridge needed before descending a split torus from the algebraic closure, in Layer 4, "Tori: split and non-split", of the ReductiveGroups roadmap.

Main declarations

• TauCeti.GaloisLatticeCat.actionField: a finite normal subextension whose fixing subgroup acts trivially on the lattice.
• TauCeti.GaloisLatticeCat.actionFieldToActionQuotient: the surjective map from the field's automorphism group to the finite quotient acting faithfully on the lattice.
• TauCeti.GaloisLatticeCat.actionFieldRepresentation: the resulting action of the finite automorphism group.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 12.23 and Corollary 12.24.

noncomputable def TauCeti.GaloisLatticeCat.actionField {k : Type u} [Field k] (M : GaloisLatticeCat k) : IntermediateField k (AlgebraicClosure k)

A finite normal subextension of the algebraic closure through whose automorphism group the action on a Galois lattice factors.

Equations

• M.actionField = ⋯.choose

instance TauCeti.GaloisLatticeCat.instFiniteDimensionalActionField {k : Type u} [Field k] (M : GaloisLatticeCat k) : FiniteDimensional k ↥M.actionField

The action field is finite-dimensional over the base field.

instance TauCeti.GaloisLatticeCat.instNormalActionField {k : Type u} [Field k] (M : GaloisLatticeCat k) : Normal k ↥M.actionField

The action field is normal over the base field.

theorem TauCeti.GaloisLatticeCat.actionField_fixingSubgroup_le_ker {k : Type u} [Field k] (M : GaloisLatticeCat k) : M.actionField.fixingSubgroup ≤ MonoidHom.ker M.obj.ρ

Every absolute Galois automorphism fixing the action field acts trivially on the lattice.

noncomputable def TauCeti.GaloisLatticeCat.actionFieldRestriction {k : Type u} [Field k] (M : GaloisLatticeCat k) : Field.absoluteGaloisGroup k →* Gal(↥M.actionField/k)

Restriction of an absolute Galois automorphism to the action field.

Equations

• M.actionFieldRestriction = id (AlgEquiv.restrictNormalHom ↥M.actionField)

@[simp]

theorem TauCeti.GaloisLatticeCat.actionFieldRestriction_apply {k : Type u} [Field k] (M : GaloisLatticeCat k) (σ : Field.absoluteGaloisGroup k) (a : ↥M.actionField) : ↑((M.actionFieldRestriction σ) a) = ↑σ ↑a

Restriction to the action field agrees with the original automorphism on its elements.

theorem TauCeti.GaloisLatticeCat.actionFieldRestriction_surjective {k : Type u} [Field k] (M : GaloisLatticeCat k) : Function.Surjective ⇑M.actionFieldRestriction

Restriction to the action field is surjective.

theorem TauCeti.GaloisLatticeCat.actionFieldRestriction_ker_le {k : Type u} [Field k] (M : GaloisLatticeCat k) : M.actionFieldRestriction.ker ≤ MonoidHom.ker M.obj.ρ

The kernel of restriction to the action field acts trivially on the lattice.

noncomputable def TauCeti.GaloisLatticeCat.actionFieldToActionQuotient {k : Type u} [Field k] (M : GaloisLatticeCat k) : Gal(↥M.actionField/k) →* M.actionQuotient

The automorphism group of the action field maps to the faithful finite quotient acting on the lattice.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GaloisLatticeCat.actionFieldToActionQuotient_restrict {k : Type u} [Field k] (M : GaloisLatticeCat k) (σ : Field.absoluteGaloisGroup k) : M.actionFieldToActionQuotient (M.actionFieldRestriction σ) = ↑σ

Restriction to the action field followed by the quotient map is the original class in the action quotient.

theorem TauCeti.GaloisLatticeCat.actionFieldToActionQuotient_surjective {k : Type u} [Field k] (M : GaloisLatticeCat k) : Function.Surjective ⇑M.actionFieldToActionQuotient

The map from the action field's automorphism group to the action quotient is surjective.

noncomputable def TauCeti.GaloisLatticeCat.actionFieldRepresentation {k : Type u} [Field k] (M : GaloisLatticeCat k) : Representation ℤ Gal(↥M.actionField/k) ↑M.obj

The representation of the action field's finite automorphism group obtained by descending the absolute-Galois action.

Equations

• M.actionFieldRepresentation = MonoidHom.comp M.actionQuotientRepresentation M.actionFieldToActionQuotient

@[simp]

theorem TauCeti.GaloisLatticeCat.actionFieldRepresentation_restrict_apply {k : Type u} [Field k] (M : GaloisLatticeCat k) (σ : Field.absoluteGaloisGroup k) (x : ↑M.obj) : (M.actionFieldRepresentation (M.actionFieldRestriction σ)) x = (M.obj.ρ σ) x

Restricting an absolute Galois automorphism to the action field and then acting on the lattice recovers the original action.

theorem TauCeti.GaloisLatticeCat.actionFieldRepresentation_comp_restriction {k : Type u} [Field k] (M : GaloisLatticeCat k) : MonoidHom.comp M.actionFieldRepresentation M.actionFieldRestriction = M.obj.ρ

The original absolute-Galois representation is the pullback of the action-field representation along restriction.

theorem TauCeti.GaloisLatticeCat.actionFieldRepresentation_ker {k : Type u} [Field k] (M : GaloisLatticeCat k) : MonoidHom.ker M.actionFieldRepresentation = M.actionFieldToActionQuotient.ker

An automorphism of the action field acts trivially on the lattice exactly when it maps to the identity in the faithful action quotient.