Separable action fields of Galois lattices

The continuous absolute-Galois action on an integral Galois lattice factors through the automorphism group of the finite normal field GaloisLatticeCat.actionField. Over an imperfect base that field need not itself be separable. This file replaces it by its maximal separable subextension.

The original action field is purely inseparable over this subextension. Consequently restriction induces an isomorphism between their automorphism groups: an automorphism of the action field is uniquely determined on the separable subextension, and every automorphism of the latter extends by normality. Transporting the lattice action across this isomorphism gives a realization over a finite Galois extension of the base field.

Main declarations

• TauCeti.GaloisLatticeCat.separableActionField: the maximal separable subextension of the finite normal action field.
• TauCeti.GaloisLatticeCat.actionFieldGalEquivSeparableActionField: restriction identifies the two automorphism groups.
• TauCeti.GaloisLatticeCat.separableActionFieldRepresentation: the lattice action by the automorphism group of the finite Galois action field.
• TauCeti.GaloisLatticeCat.separableActionFieldRepresentation_comp_restriction: pulling this action back to the absolute Galois group recovers the original representation.

References

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

This supplies the finite Galois splitting field needed before constructing the semilinear descent datum on the split coordinate Hopf algebra in Layer 4, "Tori: split and non-split", of the ReductiveGroups roadmap.

@[instance_reducible]

noncomputable def TauCeti.GaloisLatticeCat.separableActionFieldStoredModule {k : Type u} [Field k] (M : GaloisLatticeCat k) : Module ℤ ↑M.obj

The module structure stored in the bundled representation.

Equations

• M.separableActionFieldStoredModule = M.obj.hV2

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

The maximal separable subextension of the finite normal action field of a Galois lattice.

Equations

• M.separableActionField = separableClosure k ↥M.actionField

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

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

instance TauCeti.GaloisLatticeCat.instIsGaloisSeparableActionField {k : Type u} [Field k] (M : GaloisLatticeCat k) : IsGalois k ↥M.separableActionField

The separable action field is a finite Galois extension of the base field.

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

Restriction from the original action field to its maximal separable subextension.

Equations

• M.actionFieldGalToSeparableActionField = AlgEquiv.restrictNormalHom ↥M.separableActionField

noncomputable def TauCeti.GaloisLatticeCat.actionFieldGalEquivSeparableActionField {k : Type u} [Field k] (M : GaloisLatticeCat k) : Gal(↥M.actionField/k) ≃* Gal(↥M.separableActionField/k)

Restriction identifies the automorphism group of the finite normal action field with that of its finite Galois separable subextension. This is separableClosureRestrictEquiv for the normal extension actionField M / k, forgetting its continuity.

Equations

• M.actionFieldGalEquivSeparableActionField = (TauCeti.separableClosureRestrictEquiv k ↥M.actionField).toMulEquiv

@[simp]

theorem TauCeti.GaloisLatticeCat.actionFieldGalEquivSeparableActionField_apply {k : Type u} [Field k] (M : GaloisLatticeCat k) (sigma : Gal(↥M.actionField/k)) : M.actionFieldGalEquivSeparableActionField sigma = M.actionFieldGalToSeparableActionField sigma

The isomorphism of automorphism groups is restriction to the separable action field.

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

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

Equations

• M.separableActionFieldToActionQuotient = M.actionFieldToActionQuotient.comp M.actionFieldGalEquivSeparableActionField.symm.toMonoidHom

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

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

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

Restriction of an absolute Galois automorphism to the separable action field, through the original action field.

Equations

• M.separableActionFieldRestriction = M.actionFieldGalEquivSeparableActionField.toMonoidHom.comp M.actionFieldRestriction

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

Restriction from the absolute Galois group onto the separable action field is surjective.

@[simp]

theorem TauCeti.GaloisLatticeCat.separableActionFieldToActionQuotient_restrict {k : Type u} [Field k] (M : GaloisLatticeCat k) (sigma : Field.absoluteGaloisGroup k) : M.separableActionFieldToActionQuotient (M.separableActionFieldRestriction sigma) = ↑sigma

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

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

The representation of the finite Galois action field obtained from the original action-field representation through the restriction isomorphism.

Equations

• M.separableActionFieldRepresentation = MonoidHom.comp M.actionQuotientRepresentation M.separableActionFieldToActionQuotient

@[simp]

theorem TauCeti.GaloisLatticeCat.separableActionFieldRepresentation_restrict_apply {k : Type u} [Field k] (M : GaloisLatticeCat k) (sigma : Field.absoluteGaloisGroup k) (x : ↑M.obj) : (M.separableActionFieldRepresentation (M.separableActionFieldRestriction sigma)) x = (M.obj.ρ sigma) x

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

theorem TauCeti.GaloisLatticeCat.separableActionFieldRepresentation_comp_restriction {k : Type u} [Field k] (M : GaloisLatticeCat k) : MonoidHom.comp M.separableActionFieldRepresentation M.separableActionFieldRestriction = M.obj.ρ

The original absolute-Galois representation is the pullback of the representation over the finite Galois separable action field.

theorem TauCeti.GaloisLatticeCat.separableActionFieldRepresentation_ker {k : Type u} [Field k] (M : GaloisLatticeCat k) : MonoidHom.ker M.separableActionFieldRepresentation = M.separableActionFieldToActionQuotient.ker

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