Cocharacter lattices of tori

The geometric cocharacter lattice, its dual comparison, Galois action, and evaluation pairing are defined for every group of multiplicative type in TauCeti.Algebra.AlgebraicGroup.MultiplicativeType.Cocharacter. This file specializes that API to tori and uses the finite freeness of their character lattices to prove perfectness, finite freeness, and rank equality for their cocharacter lattices.

Main declarations

• TauCeti.TorusCommHopfAlgCat.toMultiplicativeTypeCommHopfAlgCat: a torus regarded as a group of multiplicative type.
• TauCeti.TorusCommHopfAlgCat.instCharacterCocharacterPairingIsPerfPair: the character-- cocharacter pairing of a torus is perfect.
• TauCeti.TorusCommHopfAlgCat.cocharacterLattice_module_free and TauCeti.TorusCommHopfAlgCat.cocharacterLattice_module_finite: the cocharacter lattice is finite free over ℤ.

References

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

@[reducible, inline]

noncomputable abbrev TauCeti.TorusCommHopfAlgCat.toMultiplicativeTypeCommHopfAlgCat {k : Type u} [Field k] (T : TorusCommHopfAlgCat k) : MultiplicativeTypeCommHopfAlgCat k

A torus regarded as a group of multiplicative type.

Equations

• T.toMultiplicativeTypeCommHopfAlgCat = { obj := T.obj, property := ⋯ }

instance TauCeti.TorusCommHopfAlgCat.instCharacterCocharacterPairingIsPerfPair {k : Type u} [Field k] (T : TorusCommHopfAlgCat k) : T.toMultiplicativeTypeCommHopfAlgCat.characterCocharacterPairing.IsPerfPair

The character--cocharacter pairing of a torus is perfect.

theorem TauCeti.TorusCommHopfAlgCat.cocharacterLattice_module_free {k : Type u} [Field k] (T : TorusCommHopfAlgCat k) : Module.Free ℤ T.toMultiplicativeTypeCommHopfAlgCat.cocharacterLattice

The cocharacter lattice of a torus is free over the integers.

theorem TauCeti.TorusCommHopfAlgCat.cocharacterLattice_module_finite {k : Type u} [Field k] (T : TorusCommHopfAlgCat k) : Module.Finite ℤ T.toMultiplicativeTypeCommHopfAlgCat.cocharacterLattice

The cocharacter lattice of a torus is finitely generated over the integers.

theorem TauCeti.TorusCommHopfAlgCat.finrank_cocharacterLattice_eq_characterLattice {k : Type u} [Field k] (T : TorusCommHopfAlgCat k) : Module.finrank ℤ T.toMultiplicativeTypeCommHopfAlgCat.cocharacterLattice = Module.finrank ℤ (CommHopfAlgCat.additiveCharacterGroup T.obj.obj)

The character and cocharacter lattices of a torus have the same rank.

theorem TauCeti.TorusCommHopfAlgCat.exists_cocharacterLattice_linearEquiv {k : Type u} [Field k] (T : TorusCommHopfAlgCat k) : ∃ (n : ℕ), Nonempty (T.toMultiplicativeTypeCommHopfAlgCat.cocharacterLattice ≃ₗ[ℤ] Fin n → ℤ)

A torus cocharacter lattice is noncanonically a finite-rank free abelian group.