Weights of the split torus as characters

The character lattice of the rank-σ split torus is σ →₀ ℤ, while a weight of a representation written in a basis is an exponent vector μ : σ → ℤ, the datum TauCeti.torusCharacter evaluates at a point. For finite σ these are the same thing, and this file records the translation:

• TauCeti.SplitTorus.weightCharacter turns an exponent vector into a character;
• TauCeti.SplitTorus.charOfPoint_weightCharacter says that evaluating that character at a point of the torus gives the monomial ∏ j, s j ^ μ j in the coordinates s of the point;
• TauCeti.SplitTorus.closure_range_weightCharacter_eq_top_iff says that a family of weights generates the character group exactly when it spans the lattice of exponent vectors.

The last statement is the hypothesis under which a diagonal representation with these weights is faithful, so it is what turns a spanning set of weights into a closed immersion of the torus.

Main declarations

• TauCeti.SplitTorus.weightCharacter: the character of 𝔾ₘ^σ with a prescribed exponent vector.

Main results

• TauCeti.SplitTorus.apply_weightCharacter: evaluation of a weight character under an arbitrary multiplicative character.
• TauCeti.SplitTorus.charOfPoint_weightCharacter: the value of a weight character at a point.
• TauCeti.SplitTorus.closure_range_weightCharacter_eq_top_iff: weights generate the character group exactly when they span the lattice of exponent vectors.

References

Milne, Algebraic Groups (2017), §12.c, describes the character lattice of a split torus.

noncomputable def TauCeti.SplitTorus.weightCharacter {σ : Type w} [Fintype σ] (μ : σ → ℤ) : Multiplicative (σ →₀ ℤ)

The character of the rank-σ split torus with exponent vector μ, that is, the Laurent monomial ∏ j, x_j ^ μ j.

Equations

• TauCeti.SplitTorus.weightCharacter μ = Multiplicative.ofAdd (Finsupp.equivFunOnFinite.symm μ)

theorem TauCeti.SplitTorus.weightCharacter_coe {σ : Type w} [Fintype σ] (f : σ →₀ ℤ) : weightCharacter ⇑f = Multiplicative.ofAdd f

A finitely supported exponent vector represents its own integral character.

@[simp]

theorem TauCeti.SplitTorus.toAdd_weightCharacter {σ : Type w} [Fintype σ] (μ : σ → ℤ) (j : σ) : (Multiplicative.toAdd (weightCharacter μ)) j = μ j

theorem TauCeti.SplitTorus.apply_weightCharacter {A : Type v} {σ : Type w} [CommRing A] [Fintype σ] (χ : Multiplicative (σ →₀ ℤ) →* Aˣ) (μ : σ → ℤ) : χ (weightCharacter μ) = torusCharacter (freeAbelianCharEquiv χ) μ

Evaluating a split-torus weight under a multiplicative character gives the corresponding monomial in the free-abelian coordinates of that character.

@[simp]

theorem TauCeti.SplitTorus.charOfPoint_weightCharacter {R : Type u} {A : Type v} {σ : Type w} [CommSemiring R] [CommRing A] [Algebra R A] [Fintype σ] (q : WithConv (MonoidAlgebra R (Multiplicative (σ →₀ ℤ)) →ₐ[R] A)) (μ : σ → ℤ) : (DiagonalizableGroup.charOfPoint q.ofConv) (weightCharacter μ) = torusCharacter (pointsMulEquiv q) μ

The value of a weight character at a point of the split torus is the corresponding monomial in the coordinates of the point.

theorem TauCeti.SplitTorus.closure_range_weightCharacter_eq_top_iff {σ : Type w} [Fintype σ] {η : Type u_1} (wt : η → σ → ℤ) : Subgroup.closure (Set.range fun (x : η) => weightCharacter (wt x)) = ⊤ ↔ Submodule.span ℤ (Set.range wt) = ⊤

A family of weights generates the character group of the split torus exactly when it spans the lattice of exponent vectors.

theorem TauCeti.SplitTorus.closure_range_weightCharacter_eq_top {σ : Type w} [Fintype σ] {η : Type u_1} (wt : η → σ → ℤ) (hwt : Submodule.span ℤ (Set.range wt) = ⊤) : Subgroup.closure (Set.range fun (x : η) => weightCharacter (wt x)) = ⊤

Spanning weights generate the character group of the split torus.