Duals of integral Galois lattices

The contragredient representation on the integral dual of a Galois lattice is again a Galois lattice. Continuity is proved using a finite basis: the pointwise stabilizer of that basis is an open subgroup, and it fixes every linear functional under the contragredient action.

Main declaration

• TauCeti.galoisLatticeProperty_dual: the integral dual of a Galois lattice, with its contragredient action, is a Galois lattice.
• TauCeti.galoisLatticeProperty_contragredient: transport the contragredient action across a linear equivalence with an integral dual.

References

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

theorem TauCeti.galoisLatticeProperty_contragredient {k V : Type u} [Field k] [AddCommGroup V] [Module.Free ℤ V] [Module.Finite ℤ V] {W : Type u} [AddCommGroup W] [Module ℤ W] (ρ : Representation ℤ (Field.absoluteGaloisGroup k) V) (τ : Representation ℤ (Field.absoluteGaloisGroup k) W) (e : W ≃ₗ[ℤ] Module.Dual ℤ V) (he : ∀ (σ : Field.absoluteGaloisGroup k) (w : W) (x : V), (e ((τ σ) w)) x = (e w) ((ρ σ⁻¹) x)) (hopen : ∀ (x : V), IsOpen {σ : Field.absoluteGaloisGroup k | (ρ σ) x = x}) : galoisLatticeProperty k (Rep.of τ)

A representation identified equivariantly with the contragredient of a Galois lattice is itself a Galois lattice. This form lets a construction retain its intrinsic carrier rather than replacing it by an integral dual.

theorem TauCeti.galoisLatticeProperty_dual {k V : Type u} [Field k] [AddCommGroup V] [Module.Free ℤ V] [Module.Finite ℤ V] (ρ : Representation ℤ (Field.absoluteGaloisGroup k) V) (hopen : ∀ (x : V), IsOpen {σ : Field.absoluteGaloisGroup k | (ρ σ) x = x}) : galoisLatticeProperty k (Rep.of ρ.dual)

The contragredient representation on the integral dual of a Galois lattice is again a Galois lattice.