Documentation

TauCeti.Algebra.AlgebraicGroup.SplitTorus.CharacterLattice

Character lattices of split tori #

The intrinsic character lattice of a split torus is its defining finite-rank free abelian group, and its absolute-Galois action is trivial.

Main declarations #

References #

See J. S. Milne, Algebraic Groups (2017), Definition 12.17.

source
noncomputable def TauCeti.SplitTorus.characterLatticeEquiv (k : Type u) [Field k] (σ : Type u) [Finite σ] :
CommHopfAlgCat.additiveCharacterGroup (DiagonalizableGroup.coordinateRing k (characterGroup σ)).obj ≃+ (σ →₀ ℤ)

The additive character lattice of a split-torus presentation is its defining finite-rank free ℤ-module.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.SplitTorus.ofAdd_characterLatticeEquiv_apply (k : Type u) [Field k] (σ : Type u) [Finite σ] (x : CommHopfAlgCat.additiveCharacterGroup (DiagonalizableGroup.coordinateRing k (characterGroup σ)).obj) :
    Multiplicative.ofAdd ((characterLatticeEquiv k σ) x) = (DiagonalizableGroup.geometricCharacterGroupEquiv k (characterGroup σ)) (Additive.toMul x)

    The split-torus lattice equivalence sends a character to the additive form of its diagonalizable-group character.

    source
    @[simp]
    theorem TauCeti.SplitTorus.characterLatticeEquiv_apply_eq_iff (k : Type u) [Field k] (σ : Type u) [Finite σ] (x : CommHopfAlgCat.additiveCharacterGroup (DiagonalizableGroup.coordinateRing k (characterGroup σ)).obj) (m : σ →₀ ℤ) :
    (characterLatticeEquiv k σ) x = m ↔ (MonoidAlgebra.scalarTensorBialgEquiv k (AlgebraicClosure k)) ↑(Additive.toMul x) = MonoidAlgebra.single (Multiplicative.ofAdd m) 1

    A split-torus character corresponds to m exactly when base change identifies its underlying group-like element with the standard monomial indexed by Multiplicative.ofAdd m.

    source
    @[simp]
    theorem TauCeti.SplitTorus.characterLatticeEquiv_symm_apply_toMul_val (k : Type u) [Field k] (σ : Type u) [Finite σ] (m : σ →₀ ℤ) :
    ↑(Additive.toMul ((characterLatticeEquiv k σ).symm m)) = 1 ⊗ₜ[k] MonoidAlgebra.single (Multiplicative.ofAdd m) 1

    The inverse split-torus character corresponding to m is the standard monomial indexed by Multiplicative.ofAdd m in the scalar-extended coordinate ring.

    source
    @[simp]
    theorem TauCeti.SplitTorus.smul_characterLattice_eq_self (k : Type u) [Field k] (σ : Type u) [Finite σ] (γ : Field.absoluteGaloisGroup k) (x : CommHopfAlgCat.additiveCharacterGroup (DiagonalizableGroup.coordinateRing k (characterGroup σ)).obj) :
    γ • x = x

    The absolute-Galois action on the character lattice of a split torus is trivial.