Integral Galois lattices

An integral Galois lattice over a field is a finite free ℤ-module equipped with an action of the absolute Galois group for which every vector has an open stabilizer. This is the continuity criterion when the module carries the discrete topology.

Main declarations

• TauCeti.galoisLatticeProperty: integral representations that are finite free and have open stabilizers.
• TauCeti.GaloisLatticeCat: the corresponding full subcategory of integral representations.

References

See J. S. Milne, Algebraic Groups (2017), Definitions 12.14 and 12.17.

def TauCeti.galoisLatticeProperty (k : Type u) [Field k] : CategoryTheory.ObjectProperty (Rep ℤ (Field.absoluteGaloisGroup k))

The property of an integral representation of the absolute Galois group being a Galois lattice: its module is finite free and every vector has an open stabilizer.

Equations

• TauCeti.galoisLatticeProperty k M = ((Module.Free ℤ ↑M ∧ Module.Finite ℤ ↑M) ∧ ∀ (x : ↑M), IsOpen {sigma : Field.absoluteGaloisGroup k | (M.ρ sigma) x = x})

@[simp]

theorem TauCeti.galoisLatticeProperty_iff (k : Type u) [Field k] (M : Rep ℤ (Field.absoluteGaloisGroup k)) : galoisLatticeProperty k M ↔ (Module.Free ℤ ↑M ∧ Module.Finite ℤ ↑M) ∧ ∀ (x : ↑M), IsOpen {sigma : Field.absoluteGaloisGroup k | (M.ρ sigma) x = x}

Membership in the Galois-lattice property.

theorem TauCeti.galoisLatticeProperty_ofMulDistribMulAction (k : Type u) [Field k] (G : Type u) [CommGroup G] [MulDistribMulAction (Field.absoluteGaloisGroup k) G] [DistribMulAction (Field.absoluteGaloisGroup k) (Additive G)] [free : Module.Free ℤ (Additive G)] [finite : Module.Finite ℤ (Additive G)] (hρ : ∀ (sigma : Field.absoluteGaloisGroup k) (x : Additive G), ((Rep.ofMulDistribMulAction (Field.absoluteGaloisGroup k) G).ρ sigma) x = sigma • x) (hopen : ∀ (x : Additive G), IsOpen ↑(MulAction.stabilizer (Field.absoluteGaloisGroup k) x)) : galoisLatticeProperty k (Rep.ofMulDistribMulAction (Field.absoluteGaloisGroup k) G)

Build the Galois-lattice property for a representation induced from a multiplicative action, using the usual stabilizer formulation of continuity.

instance TauCeti.instIsClosedUnderIsomorphismsRepIntAbsoluteGaloisGroupGaloisLatticeProperty (k : Type u) [Field k] : (galoisLatticeProperty k).IsClosedUnderIsomorphisms

Being a Galois lattice is invariant under equivariant integral-linear isomorphisms.

@[reducible, inline]

abbrev TauCeti.GaloisLatticeCat (k : Type u) [Field k] : Type (u + 1)

The category of finite free integral representations of the absolute Galois group whose vectors have open stabilizers.

Equations

• TauCeti.GaloisLatticeCat k = (TauCeti.galoisLatticeProperty k).FullSubcategory

instance TauCeti.GaloisLatticeCat.instModuleFree (k : Type u) [Field k] (M : GaloisLatticeCat k) : Module.Free ℤ ↑M.obj

The integral module of a Galois lattice is free.

instance TauCeti.GaloisLatticeCat.instModuleFinite (k : Type u) [Field k] (M : GaloisLatticeCat k) : Module.Finite ℤ ↑M.obj

The integral module of a Galois lattice is finite.

theorem TauCeti.GaloisLatticeCat.isOpen_setOf_ρ_eq (k : Type u) [Field k] (M : GaloisLatticeCat k) (x : ↑M.obj) : IsOpen {sigma : Field.absoluteGaloisGroup k | (M.obj.ρ sigma) x = x}

Every vector of a Galois lattice has an open stabilizer.