Finite quotients acting on Galois lattices #

A finite module representation whose vectors have open stabilizers has open kernel. Indeed, the kernel is already the intersection of the stabilizers of a finite generating family. The Krull neighborhood basis then puts a finite-dimensional normal subextension's fixing subgroup inside that kernel, so the quotient of the Galois group by the kernel is finite. The original action therefore factors faithfully through a finite group.

This finite-quotient reduction is the first descent step in the classification of non-split tori: the Galois action on a torus character lattice factors through a finite Galois quotient, after which the corresponding split torus can be descended from a finite extension.

Main declarations #

Representation.isOpen_ker_of_finite: open point stabilizers imply an open kernel on a finite module.
Field.absoluteGaloisGroup.exists_finiteDimensional_normal_fixingSubgroup_le: every open subgroup of a Galois group contains the fixing subgroup of a finite-dimensional normal subextension.
TauCeti.GaloisLatticeCat.actionQuotient: the finite quotient of the absolute Galois group acting faithfully on a Galois lattice.
TauCeti.GaloisLatticeCat.actionQuotientRepresentation: the induced representation of that finite quotient.

References #

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

source

theorem Representation.isOpen_ker_of_finite {R : Type u} [Semiring R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommMonoid V] [Module R V] [Module.Finite R V] (rho : Representation R G V) (hopen : ∀ (x : V), IsOpen {g : G | (rho g) x = x}) :

IsOpen ↑(MonoidHom.ker rho)

A representation on a finite module has open kernel if every vector stabilizer is open.

It is enough to intersect the stabilizers of a finite generating family: an element fixes those generators exactly when its linear action is the identity.

source

theorem Field.absoluteGaloisGroup.exists_finiteDimensional_normal_fixingSubgroup_le {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [Normal K L] (U : Subgroup Gal(L/K)) (hU : IsOpen ↑U) :

∃ (E : IntermediateField K L), FiniteDimensional K ↥E ∧ Normal K ↥E ∧ E.fixingSubgroup ≤ U

Every open subgroup of the Galois group of a normal extension contains the fixing subgroup of a finite-dimensional normal intermediate extension.

source

theorem Field.absoluteGaloisGroup.finite_quotient_of_isOpen {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [Normal K L] (U : Subgroup Gal(L/K)) (hU : IsOpen ↑U) :

Finite (Gal(L/K) ⧸ U)

Every open subgroup of the Galois group of a normal extension has finite quotient.

source

@[instance_reducible]

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

Module ℤ ↑M.obj

The module structure stored in the bundled representation.

Equations

M.storedModule = M.obj.hV2

Instances For

source

theorem TauCeti.GaloisLatticeCat.isOpen_ker_ρ {k : Type u} [Field k] (M : GaloisLatticeCat k) :

IsOpen ↑(MonoidHom.ker M.obj.ρ)

The kernel of the absolute-Galois representation on a Galois lattice is open.

source

@[reducible, inline]

abbrev TauCeti.GaloisLatticeCat.actionQuotient {k : Type u} [Field k] (M : GaloisLatticeCat k) :

Type u

The finite quotient of the absolute Galois group that acts faithfully on a Galois lattice.

Equations

M.actionQuotient = (Field.absoluteGaloisGroup k ⧸ MonoidHom.ker M.obj.ρ)

Instances For

source

instance TauCeti.GaloisLatticeCat.instFiniteActionQuotient {k : Type u} [Field k] (M : GaloisLatticeCat k) :

Finite M.actionQuotient

The quotient of the absolute Galois group acting on a Galois lattice is finite.

source

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

Representation ℤ M.actionQuotient ↑M.obj

The representation of the finite action quotient induced by a Galois lattice. It is faithful by construction, since the quotient is by the kernel of the original action.

Equations