Contragredient duality of integral Galois lattices

Integral duals preserve finite freeness and continuity of the Galois action. Evaluation into the double dual exhibits this contravariant functor as an equivalence. This is the lattice duality relating the character and cocharacter classifications of tori.

@[reducible, inline]

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

The integral dual of a Galois lattice, with its contragredient action.

Equations

• M.dual = { obj := M.obj.dual, property := ⋯ }

@[simp]

theorem TauCeti.GaloisLatticeCat.dual_obj {k : Type u} [Field k] (M : GaloisLatticeCat k) : M.dual.obj = M.obj.dual

The representation underlying the dual lattice is the contragredient representation.

@[implicit_reducible]

noncomputable def TauCeti.GaloisLatticeCat.dualFunctor {k : Type u} [Field k] : CategoryTheory.Functor (GaloisLatticeCat k)ᵒᵖ (GaloisLatticeCat k)

Contragredient duality as a functor on integral Galois lattices.

Equations

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

@[simp]

theorem TauCeti.GaloisLatticeCat.dualFunctor_obj_obj {k : Type u} [Field k] (M : (GaloisLatticeCat k)ᵒᵖ) : (dualFunctor.obj M).obj = (Opposite.unop M).obj.dual

The representation underlying the contragredient functor.

@[simp]

theorem TauCeti.GaloisLatticeCat.dualFunctor_map_hom {k : Type u} [Field k] {M N : (GaloisLatticeCat k)ᵒᵖ} (f : M ⟶ N) : (dualFunctor.map f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (Rep.dualMap f.unop.hom) (CategoryTheory.eqToHom ⋯))

The map part of contragredient duality, in the underlying representation category.

noncomputable def TauCeti.GaloisLatticeCat.doubleDualIso {k : Type u} [Field k] (M : GaloisLatticeCat k) : M ≅ dualFunctor.obj (Opposite.op (dualFunctor.obj (Opposite.op M)))

Evaluation identifies a Galois lattice with its double dual.

Equations

• M.doubleDualIso = id ((TauCeti.galoisLatticeProperty k).isoMk M.obj.doubleDualIso)

@[simp]

theorem TauCeti.GaloisLatticeCat.doubleDualIso_hom_hom {k : Type u} [Field k] (M : GaloisLatticeCat k) : M.doubleDualIso.hom.hom = CategoryTheory.CategoryStruct.comp M.obj.doubleDualIso.hom (CategoryTheory.eqToHom ⋯)

On underlying representations, the double-dual identification is evaluation.

theorem TauCeti.GaloisLatticeCat.doubleDualIso_naturality {k : Type u} [Field k] {M N : GaloisLatticeCat k} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp f N.doubleDualIso.hom = CategoryTheory.CategoryStruct.comp M.doubleDualIso.hom (dualFunctor.map (dualFunctor.map f.op).op)

Evaluation into the double dual is natural in the lattice.

theorem TauCeti.GaloisLatticeCat.doubleDualIso_naturality_assoc {k : Type u} [Field k] {M N : GaloisLatticeCat k} (f : M ⟶ N) {Z : GaloisLatticeCat k} (h : dualFunctor.obj (Opposite.op (dualFunctor.obj (Opposite.op N))) ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp N.doubleDualIso.hom h) = CategoryTheory.CategoryStruct.comp M.doubleDualIso.hom (CategoryTheory.CategoryStruct.comp (dualFunctor.map (dualFunctor.map f.op).op) h)

Evaluation into the double dual is natural in the lattice.

instance TauCeti.GaloisLatticeCat.dualFunctor_isEquivalence {k : Type u} [Field k] : dualFunctor.IsEquivalence

The contragredient functor is an equivalence.