The diagonal torus attached to a weighted basis

A basis b : Basis ι R M and a family of units w : ι → Rˣ determine the automorphism of M scaling the i-th basis vector by w i. Letting w range over all such families realizes the group ι → Rˣ — the R-points of the split torus 𝔾ₘ^ι — inside the automorphism group of M.

Weights cut this down to a torus of smaller rank. A weight function wt : ι → κ → ℤ assigns to each basis vector a character of 𝔾ₘ^κ, and evaluating those characters at a point s : κ → Rˣ gives the family of units the diagonal automorphism is built from. The resulting homomorphism TauCeti.basisWeightTorus is the split maximal torus of a Chevalley group written in a weight basis of an admissible lattice, and TauCeti.basisDiagonal_apply_of_repr_eq_zero is the statement that it acts on a weight vector by the corresponding character — which is what makes the conjugation formula against a root subgroup come out.

Fixing the weight instead of the point turns a character into a homomorphism TauCeti.weightChar on the points of the torus, which is the form in which a weight indexes a joint eigenspace. Whether that indexing is faithful depends on the coefficients: over 𝔽₂ the torus has a single point, so every weight gives the trivial character, while over an infinite field distinct weights stay distinct (TauCeti.weightChar_injective).

Main definitions

• TauCeti.torusCharacter: the value at s : κ → Rˣ of the character μ : κ → ℤ of 𝔾ₘ^κ.
• TauCeti.weightChar: that character with the weight fixed, as a homomorphism on the points of the torus.
• TauCeti.weylReflectTorusPoint: the multiplicative reflection of split-torus points dual to a reflection of their character lattice.
• TauCeti.basisDiagonal: the automorphism scaling each basis vector by a prescribed unit.
• TauCeti.basisDiagonalHom: the resulting homomorphism from ι → Rˣ.
• TauCeti.basisWeightTorus: the homomorphism from κ → Rˣ determined by a weight function.

Main results

• TauCeti.basisDiagonal_apply_of_repr_eq_zero: a diagonal automorphism acts by a single scalar on any vector whose coordinates are supported where that scalar is attained.
• TauCeti.basisWeightTorus_apply_of_repr_eq_zero: the special case for a weight vector.
• TauCeti.conj_basisWeightTorus_of_map_basis: a compatible monomial basis automorphism conjugates represented torus points by coordinate reindexing.
• TauCeti.map_basisWeightTorus_range_conj_of_map_basis: such an automorphism normalizes the represented weight torus.
• TauCeti.mul_inv_weylReflectTorusPoint: a point divided by its reflection is supported at the reflecting coordinate, with value there the root character.
• TauCeti.torusCharacter_weylReflectTorusPoint: evaluation at a reflected point agrees with evaluation of the reflected character.
• TauCeti.exists_torusCharacter_eq_of_sum_mul_eq_one: a weight whose coordinates have a ℤ-linear combination equal to one takes every unit as a value.
• TauCeti.weightChar_injective: over an infinite field, distinct weights give distinct characters of the torus; TauCeti.weightChar_injective_of_algebraRat specializes this to fields that are ℚ-algebras.
• TauCeti.eq_of_span_eq_top_of_torusCharacter_eq: dually, weights generating the whole character lattice separate the points of the torus, over any coefficient ring.
• TauCeti.basisDiagonalHom_injective and TauCeti.basisWeightTorus_injective: a diagonal automorphism determines its scaling units, so spanning weights make the represented weight torus a monomorphism.

References

• J. C. Jantzen, Representations of Algebraic Groups, II.1.
• R. W. Carter, Simple Groups of Lie Type, §4.4, §7.1, and §12.2.

Characters of a split torus

def TauCeti.torusCharacter {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] (s : κ → Rˣ) (μ : κ → ℤ) : Rˣ

The value at the point s of the character μ of the split torus 𝔾ₘ^κ, namely ∏ j, s j ^ μ j. Weights of a representation are exactly such characters, so this is the scalar by which a torus point acts on a weight vector.

Equations

• TauCeti.torusCharacter s μ = ∏ j : κ, s j ^ μ j

theorem TauCeti.torusCharacter_def {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] (s : κ → Rˣ) (μ : κ → ℤ) : torusCharacter s μ = ∏ j : κ, s j ^ μ j

A split-torus character evaluates as the product of its coordinate powers.

@[simp]

theorem TauCeti.torusCharacter_mulEquivArrowCongr {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] (σ : Equiv.Perm κ) (s : κ → Rˣ) (μ : κ → ℤ) : torusCharacter ((MulEquiv.arrowCongr σ (MulEquiv.refl Rˣ)) s) μ = torusCharacter s (μ ∘ ⇑σ)

Evaluating a character at a point reindexed by σ is the same as precomposing the character with σ.

@[simp]

theorem TauCeti.torusCharacter_equivFunOnFinite {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] (s : κ → Rˣ) (m : κ →₀ ℤ) : torusCharacter s (Finsupp.equivFunOnFinite m) = m.prod fun (i : κ) (z : ℤ) => s i ^ z

Writing a finite-support exponent vector as a function identifies its character value with the corresponding finitely supported product.

@[simp]

theorem TauCeti.torusCharacter_zero {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] (s : κ → Rˣ) : torusCharacter s 0 = 1

The trivial character takes the value one at every point.

theorem TauCeti.torusCharacter_add {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] (s : κ → Rˣ) (μ ν : κ → ℤ) : torusCharacter s (μ + ν) = torusCharacter s μ * torusCharacter s ν

Characters multiply when weights are added.

theorem TauCeti.torusCharacter_sum {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] {ι : Type u_2} (s : κ → Rˣ) (t : Finset ι) (μ : ι → κ → ℤ) : torusCharacter s (∑ i ∈ t, μ i) = ∏ i ∈ t, torusCharacter s (μ i)

Evaluating a finite sum of characters is the product of their evaluations.

theorem TauCeti.torusCharacter_nsmul {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] (s : κ → Rˣ) (μ : κ → ℤ) (n : ℕ) : torusCharacter s (n • μ) = torusCharacter s μ ^ n

Scaling a weight by a natural number raises its value to that power.

theorem TauCeti.torusCharacter_neg {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] (s : κ → Rˣ) (μ : κ → ℤ) : torusCharacter s (-μ) = (torusCharacter s μ)⁻¹

Negating a weight inverts the value of its character.

theorem TauCeti.torusCharacter_sub {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] (s : κ → Rˣ) (μ ν : κ → ℤ) : torusCharacter s (μ - ν) = torusCharacter s μ / torusCharacter s ν

Subtracting weights divides the values of their characters.

theorem TauCeti.torusCharacter_zsmul {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] (s : κ → Rˣ) (μ : κ → ℤ) (z : ℤ) : torusCharacter s (z • μ) = torusCharacter s μ ^ z

Scaling a weight by an integer raises its value to that integer power.

@[simp]

theorem TauCeti.torusCharacter_one {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] (μ : κ → ℤ) : torusCharacter 1 μ = 1

Every character takes the value one at the identity point.

theorem TauCeti.torusCharacter_mul {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] (s t : κ → Rˣ) (μ : κ → ℤ) : torusCharacter (s * t) μ = torusCharacter s μ * torusCharacter t μ

A character is a homomorphism on the points of the torus.

@[simp]

theorem TauCeti.torusCharacter_mulSingle {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] [DecidableEq κ] (c : κ) (z : Rˣ) (μ : κ → ℤ) : torusCharacter (Pi.mulSingle c z) μ = z ^ μ c

At a point supported on the single coordinate c, a character is the μ c-th power of the value there: the other coordinates contribute the factor 1.

@[simp]

theorem TauCeti.torusCharacter_single {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] [DecidableEq κ] (s : κ → Rˣ) (c : κ) (z : ℤ) : torusCharacter s (Pi.single c z) = s c ^ z

The character of the weight z • e_c is the z-th power of the c-th coordinate.

theorem TauCeti.exists_torusCharacter_eq_of_sum_mul_eq_one {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] {μ m : κ → ℤ} (hm : ∑ j : κ, μ j * m j = 1) (u : Rˣ) : ∃ (s : κ → Rˣ), torusCharacter s μ = u

A unimodular weight is surjective on points. If the coordinates of μ have a ℤ-linear combination equal to one, then every unit is the value of the character μ at some point of the torus: the point whose j-th coordinate is u ^ m j works, because the character collapses the resulting product of powers to u ^ ∑ j, μ j * m j.

The hypothesis says that the coordinates of μ are setwise coprime. It is needed: the weight 2 on a rank-one torus attains only the squares.

Reflections of split-torus points

def TauCeti.weylReflectTorusPoint {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] [DecidableEq κ] (α : κ → ℤ) (c : κ) : (κ → Rˣ) →* κ → Rˣ

The multiplicative reflection s_α on points of the split torus 𝔾ₘ^κ. Here c is the Cartan index of the coroot α^∨; the reflection divides the c-th coordinate of a point s by the value α(s) and leaves the others unchanged.

Equations

• TauCeti.weylReflectTorusPoint α c = { toFun := fun (s : κ → Rˣ) => s * Pi.mulSingle c (TauCeti.torusCharacter s α)⁻¹, map_one' := ⋯, map_mul' := ⋯ }

theorem TauCeti.weylReflectTorusPoint_apply {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] [DecidableEq κ] (α : κ → ℤ) (c : κ) (s : κ → Rˣ) : (weylReflectTorusPoint α c) s = s * Pi.mulSingle c (torusCharacter s α)⁻¹

The reflected torus point as a coordinatewise product.

@[simp]

theorem TauCeti.weylReflectTorusPoint_apply_same {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] [DecidableEq κ] (α : κ → ℤ) (c : κ) (s : κ → Rˣ) : (weylReflectTorusPoint α c) s c = s c * (torusCharacter s α)⁻¹

At the coroot coordinate, the reflected point is divided by the root character.

@[simp]

theorem TauCeti.weylReflectTorusPoint_apply_of_ne {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] [DecidableEq κ] (α : κ → ℤ) {c j : κ} (hcj : j ≠ c) (s : κ → Rˣ) : (weylReflectTorusPoint α c) s j = s j

Away from the coroot coordinate, the reflected point is unchanged.

theorem TauCeti.mul_inv_weylReflectTorusPoint {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] [DecidableEq κ] (α : κ → ℤ) (c : κ) (s : κ → Rˣ) : s * ((weylReflectTorusPoint α c) s)⁻¹ = Pi.mulSingle c (torusCharacter s α)

A point divided by its reflection is supported at the reflecting coordinate. The reflection changes only the c-th coordinate, dividing it by the value α(s), so the quotient is the point with c-th coordinate α(s) and all others 1.

@[simp]

theorem TauCeti.torusCharacter_weylReflectTorusPoint {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] [DecidableEq κ] (α : κ → ℤ) (c : κ) (s : κ → Rˣ) (μ : κ → ℤ) : torusCharacter ((weylReflectTorusPoint α c) s) μ = torusCharacter s (μ - μ c • α)

The reflected point computes the reflected character. The character μ takes at the reflected point the value that μ - μ(c) α, the reflection s_α μ, takes at the original one.

theorem TauCeti.weylReflectTorusPoint_weylReflectTorusPoint {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] [DecidableEq κ] (α : κ → ℤ) {c : κ} (hαc : α c = 2) (s : κ → Rˣ) : (weylReflectTorusPoint α c) ((weylReflectTorusPoint α c) s) = s

The reflection of points is an involution, as soon as the root takes the value two at its own coroot.

def TauCeti.torusCharacterHom {ι : Type u} {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] (wt : ι → κ → ℤ) : (κ → Rˣ) →* ι → Rˣ

The family of characters attached to a weight function, as a homomorphism from the points of the split torus 𝔾ₘ^κ to families of units indexed by the basis.

Equations

• TauCeti.torusCharacterHom wt = { toFun := fun (s : κ → Rˣ) (i : ι) => TauCeti.torusCharacter s (wt i), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.torusCharacterHom_apply {ι : Type u} {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] (wt : ι → κ → ℤ) (s : κ → Rˣ) (i : ι) : (torusCharacterHom wt) s i = torusCharacter s (wt i)

The value of the weight-character homomorphism at a point and a basis index.

theorem TauCeti.map_torusCharacter {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] {S : Type u_2} [CommRing S] (φ : R →+* S) (s : κ → Rˣ) (μ : κ → ℤ) : (Units.map ↑φ) (torusCharacter s μ) = torusCharacter (fun (j : κ) => (Units.map ↑φ) (s j)) μ

Torus characters are natural in the ring of values.

A character as a homomorphism of torus points

def TauCeti.weightChar {κ : Type v} (R : Type w) [CommRing R] [Fintype κ] (μ : κ → ℤ) : (κ → Rˣ) →* Rˣ

The character μ of the split torus 𝔾ₘ^κ read as a homomorphism (κ → Rˣ) →* Rˣ: the value TauCeti.torusCharacter s μ with the weight μ fixed and the point s varying. This is the form in which a weight indexes a joint eigenspace of the torus.

Equations

• TauCeti.weightChar R μ = { toFun := fun (s : κ → Rˣ) => TauCeti.torusCharacter s μ, map_one' := ⋯, map_mul' := ⋯ }

theorem TauCeti.weightChar_apply {κ : Type v} (R : Type w) [CommRing R] [Fintype κ] (μ : κ → ℤ) (s : κ → Rˣ) : (weightChar R μ) s = torusCharacter s μ

A weight character evaluates as the split-torus character of its weight, with the arguments in the order the weight-space API uses. Every arithmetic property of TauCeti.weightChar reduces through this to the TauCeti.torusCharacter lemmas.

@[simp]

theorem TauCeti.weightChar_zero {κ : Type v} (R : Type w) [CommRing R] [Fintype κ] : weightChar R 0 = 1

The trivial weight gives the trivial character.

theorem TauCeti.weightChar_add {κ : Type v} (R : Type w) [CommRing R] [Fintype κ] (μ ν : κ → ℤ) : weightChar R (μ + ν) = weightChar R μ * weightChar R ν

Weights add as characters multiply.

@[simp]

theorem TauCeti.weightChar_single {κ : Type v} (R : Type w) [CommRing R] [Fintype κ] [DecidableEq κ] (c : κ) (s : κ → Rˣ) : (weightChar R (Pi.single c 1)) s = s c

The character of Pi.single c 1 is the c-th coordinate: this is the weight carried by the c-th basis vector of a weight basis.

theorem TauCeti.weightChar_const {κ : Type v} (R : Type w) [CommRing R] [Fintype κ] (z : ℤ) (s : κ → Rˣ) : (weightChar R fun (x : κ) => z) s = (∏ j : κ, s j) ^ z

The character of a constant weight is a power of the product of the coordinates.

Separating weights

theorem TauCeti.weightChar_injective {κ : Type v} [Fintype κ] {K : Type u_2} [Field K] [Infinite K] : Function.Injective (weightChar K)

Distinct weights give distinct characters of the split torus, over an infinite field. Some hypothesis on the coefficients is needed: over 𝔽₂ the torus 𝔾ₘ^κ has a single point and every weight gives the trivial character. A field of characteristic zero is infinite (CharZero.infinite), so that case is a specialisation.

theorem TauCeti.weightChar_injective_of_algebraRat {κ : Type v} [Fintype κ] (k : Type u_2) [Field k] [Algebra ℚ k] : Function.Injective (weightChar k)

The weight characters of a field that is a ℚ-algebra separate weights: such a field has characteristic zero, hence infinitely many elements.

Separating torus points

theorem TauCeti.eq_of_span_eq_top_of_torusCharacter_eq {ι : Type u} {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] {wt : ι → κ → ℤ} (hwt : Submodule.span ℤ (Set.range wt) = ⊤) {s t : κ → Rˣ} (h : ∀ (i : ι), torusCharacter s (wt i) = torusCharacter t (wt i)) : s = t

Spanning weights separate the points of the split torus. If a family of characters generates the whole character lattice κ → ℤ, then two points at which every one of them takes the same value are equal.

This and TauCeti.weightChar_injective separate in opposite variables, and their hypotheses are not comparable: here the family of weights is asked to be plentiful and the coefficient ring is arbitrary, there a single pair of weights is separated at the cost of an infinite field.

theorem TauCeti.torusCharacterHom_injective {ι : Type u} {κ : Type v} {R : Type w} [CommRing R] [Fintype κ] {wt : ι → κ → ℤ} (hwt : Submodule.span ℤ (Set.range wt) = ⊤) : Function.Injective ⇑(torusCharacterHom wt)

Spanning weights make the family of characters of the split torus injective on points.

Diagonal automorphisms

noncomputable def TauCeti.basisDiagonal {ι : Type u} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis ι R M) (w : ι → Rˣ) : M ≃ₗ[R] M

The automorphism of M scaling the i-th vector of the basis b by the unit w i.

Equations

• TauCeti.basisDiagonal b w = b.equiv (b.unitsSMul w) (Equiv.refl ι)

@[simp]

theorem TauCeti.basisDiagonal_basis {ι : Type u} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis ι R M) (w : ι → Rˣ) (i : ι) : (basisDiagonal b w) (b i) = ↑(w i) • b i

The defining action of a diagonal automorphism on a basis vector.

theorem TauCeti.basisDiagonal_intertwine_of_map_basis {ι : Type u} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis ι R M) (v w : ι → Rˣ) (c : ι → R) (τ : ι → ι) (θ : M ≃ₗ[R] M) (hθ : ∀ (i : ι), θ (b i) = c i • b (τ i)) (hvw : ∀ (i : ι), w (τ i) = v i) : θ * basisDiagonal b v = basisDiagonal b w * θ

A basis automorphism acting by scalar multiples intertwines diagonal automorphisms whose diagonal entries correspond under the induced basis-index map.

theorem TauCeti.conj_basisDiagonal_of_map_basis {ι : Type u} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis ι R M) (v w : ι → Rˣ) (c : ι → R) (τ : ι → ι) (θ : M ≃ₗ[R] M) (hθ : ∀ (i : ι), θ (b i) = c i • b (τ i)) (hvw : ∀ (i : ι), w (τ i) = v i) : θ * basisDiagonal b v * θ⁻¹ = basisDiagonal b w

Conjugating a diagonal automorphism by a compatible basis automorphism acting by scalar multiples reindexes its diagonal entries.

@[simp]

theorem TauCeti.basisDiagonal_one {ι : Type u} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis ι R M) : basisDiagonal b 1 = 1

The diagonal automorphism attached to the constant family 1 is the identity.

theorem TauCeti.basisDiagonal_mul {ι : Type u} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis ι R M) (w v : ι → Rˣ) : basisDiagonal b (w * v) = basisDiagonal b w * basisDiagonal b v

Diagonal automorphisms multiply pointwise in the family of scaling units.

noncomputable def TauCeti.basisDiagonalHom {ι : Type u} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis ι R M) : (ι → Rˣ) →* M ≃ₗ[R] M

The diagonal automorphisms as a homomorphism from the group of families of units.

Equations

• TauCeti.basisDiagonalHom b = { toFun := TauCeti.basisDiagonal b, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.basisDiagonalHom_apply {ι : Type u} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis ι R M) (w : ι → Rˣ) : (basisDiagonalHom b) w = basisDiagonal b w

The homomorphism of diagonal automorphisms evaluates to TauCeti.basisDiagonal.

theorem TauCeti.basisDiagonalHom_injective {ι : Type u} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis ι R M) : Function.Injective ⇑(basisDiagonalHom b)

A diagonal automorphism determines its scaling units: reading off the i-th coordinate of the image of the i-th basis vector recovers the i-th unit.

theorem TauCeti.repr_basisDiagonal {ι : Type u} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis ι R M) (w : ι → Rˣ) (m : M) (i : ι) : (b.repr ((basisDiagonal b w) m)) i = ↑(w i) * (b.repr m) i

A diagonal automorphism scales each coordinate by its corresponding unit.

theorem TauCeti.basisDiagonal_inv {ι : Type u} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis ι R M) (w : ι → Rˣ) : (basisDiagonal b w)⁻¹ = basisDiagonal b w⁻¹

Inverting a diagonal automorphism inverts each of its diagonal entries.

theorem TauCeti.toMatrix_basisDiagonal {ι : Type u} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R M) (w : ι → Rˣ) : (LinearMap.toMatrix b b) ↑(basisDiagonal b w) = Matrix.diagonal fun (i : ι) => ↑(w i)

The matrix of a diagonal basis automorphism in that basis is the diagonal matrix of its scaling units.

theorem TauCeti.basisDiagonal_apply_of_repr_eq_zero {ι : Type u} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis ι R M) (w : ι → Rˣ) {c : Rˣ} {m : M} (hm : ∀ (i : ι), w i ≠ c → (b.repr m) i = 0) : (basisDiagonal b w) m = ↑c • m

A diagonal automorphism scales by a single unit any vector whose coordinates vanish outside the basis vectors carrying that unit. Applied to a weight basis, this says that a torus point acts on a weight vector by the value of the corresponding character.

The torus of a weighted basis

noncomputable def TauCeti.basisWeightTorus {ι : Type u} {κ : Type v} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] [Fintype κ] (b : Module.Basis ι R M) (wt : ι → κ → ℤ) : (κ → Rˣ) →* M ≃ₗ[R] M

The split torus of rank κ acting on M through a weight function on a basis: the point s acts on the i-th basis vector by the value at s of the character wt i.

This is how the split maximal torus of a Chevalley group acts on an admissible lattice written in a weight basis.

Equations

• TauCeti.basisWeightTorus b wt = (TauCeti.basisDiagonalHom b).comp (TauCeti.torusCharacterHom wt)

theorem TauCeti.basisWeightTorus_apply {ι : Type u} {κ : Type v} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] [Fintype κ] (b : Module.Basis ι R M) (wt : ι → κ → ℤ) (s : κ → Rˣ) : (basisWeightTorus b wt) s = basisDiagonal b fun (i : ι) => torusCharacter s (wt i)

The weight torus at a point is the diagonal automorphism scaling by the weight characters.

@[simp]

theorem TauCeti.basisWeightTorus_basis {ι : Type u} {κ : Type v} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] [Fintype κ] (b : Module.Basis ι R M) (wt : ι → κ → ℤ) (s : κ → Rˣ) (i : ι) : ((basisWeightTorus b wt) s) (b i) = ↑(torusCharacter s (wt i)) • b i

A torus point scales the i-th basis vector by the value at it of the character wt i.

theorem TauCeti.basisWeightTorus_intertwine_of_map_basis {ι : Type u} {κ : Type v} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] [Fintype κ] (b : Module.Basis ι R M) (wt : ι → κ → ℤ) (τ : ι → ι) (σ : Equiv.Perm κ) (θ : M ≃ₗ[R] M) (c : ι → R) (hθ : ∀ (i : ι), θ (b i) = c i • b (τ i)) (hwt : ∀ (i : ι) (j : κ), wt (τ i) (σ j) = wt i j) (s : κ → Rˣ) : θ * (basisWeightTorus b wt) s = (basisWeightTorus b wt) ((MulEquiv.arrowCongr σ (MulEquiv.refl Rˣ)) s) * θ

A basis automorphism acting by scalar multiples whose basis-index map is compatible with a coordinate permutation intertwines each represented torus point with its reindexing. The basis-index map is only a function because the proof does not need its bijectivity.

theorem TauCeti.conj_basisWeightTorus_of_map_basis {ι : Type u} {κ : Type v} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] [Fintype κ] (b : Module.Basis ι R M) (wt : ι → κ → ℤ) (τ : ι → ι) (σ : Equiv.Perm κ) (θ : M ≃ₗ[R] M) (c : ι → R) (hθ : ∀ (i : ι), θ (b i) = c i • b (τ i)) (hwt : ∀ (i : ι) (j : κ), wt (τ i) (σ j) = wt i j) (s : κ → Rˣ) : θ * (basisWeightTorus b wt) s * θ⁻¹ = (basisWeightTorus b wt) ((MulEquiv.arrowCongr σ (MulEquiv.refl Rˣ)) s)

Conjugating a represented weight-torus point by a compatible basis automorphism reindexes that point. This is the normalizer form of basisWeightTorus_intertwine_of_map_basis.

theorem TauCeti.map_basisWeightTorus_range_conj_of_map_basis {ι : Type u} {κ : Type v} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] [Fintype κ] (b : Module.Basis ι R M) (wt : ι → κ → ℤ) (τ : ι → ι) (σ : Equiv.Perm κ) (θ : M ≃ₗ[R] M) (c : ι → R) (hθ : ∀ (i : ι), θ (b i) = c i • b (τ i)) (hwt : ∀ (i : ι) (j : κ), wt (τ i) (σ j) = wt i j) : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj θ)) (basisWeightTorus b wt).range = (basisWeightTorus b wt).range

A compatible basis symmetry acting by scalar multiples normalizes the represented weight torus. Conjugation by θ maps its range onto itself by reindexing torus points through σ.

theorem TauCeti.basisWeightTorus_apply_of_repr_eq_zero {ι : Type u} {κ : Type v} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] [Fintype κ] (b : Module.Basis ι R M) (wt : ι → κ → ℤ) (s : κ → Rˣ) {μ : κ → ℤ} {m : M} (hm : ∀ (i : ι), wt i ≠ μ → (b.repr m) i = 0) : ((basisWeightTorus b wt) s) m = ↑(torusCharacter s μ) • m

A torus point acts on a weight vector by the value of the corresponding character.

theorem TauCeti.basisWeightTorus_injective {ι : Type u} {κ : Type v} {R : Type w} {M : Type u_1} [CommRing R] [AddCommGroup M] [Module R M] [Fintype κ] (b : Module.Basis ι R M) {wt : ι → κ → ℤ} (hwt : Submodule.span ℤ (Set.range wt) = ⊤) : Function.Injective ⇑(basisWeightTorus b wt)

Spanning weights make the represented weight torus a monomorphism: distinct points of 𝔾ₘ^κ then act by distinct automorphisms of M.