Base change of split-torus points

The rank-σ split torus over k is the diagonalizable group D(Multiplicative (σ →₀ ℤ)), represented by the group algebra k[Multiplicative (σ →₀ ℤ)]. This file records the base-changed functor-of-points calculation: if K is a k-algebra and A is a commutative K-algebra, then the convolution group of K-algebra maps out of K ⊗[k] k[Multiplicative (σ →₀ ℤ)] is the product group σ → Aˣ.

The equivalence is the specialization of DiagonalizableGroup.baseChangePointsMulEquiv to the free abelian character group, followed by freeAbelianCharEquiv. The pointwise API reads a base-changed point on the standard coordinate characters 1 ⊗ single (ofAdd (single i 1)) 1, records the inverse evaluation, and gives the finite-rank specialization.

This advances the ReductiveGroups roadmap, Layer 0 ("Base change. K ⊗[k] A as a Hopf algebra over K") and Layer 4 ("Tori: split ... the character lattice X*(T)").

Main declarations

• TauCeti.SplitTorus.baseChangePointsMulEquiv: the multiplicative equivalence from base-changed points of the rank-σ split torus to coordinate families σ → Aˣ.
• TauCeti.SplitTorus.baseChangePointsMulEquiv_apply_coe: the equivalence reads a point on the base-changed standard coordinate generator.
• TauCeti.SplitTorus.baseChangePointsMulEquiv_symm_apply_single_one: the inverse equivalence takes each standard coordinate generator to the chosen coordinate.

References

The base-change step is Tau Ceti's DiagonalizableGroup.baseChangePointsMulEquiv, and the free-abelian character calculation is Tau Ceti's freeAbelianCharEquiv, built from Mathlib's Finsupp.liftAddHom and zmultiplesHom.

noncomputable def TauCeti.SplitTorus.baseChangePointsMulEquiv {k : Type u} {K : Type v} {A : Type w} {σ : Type w'} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] : WithConv (TensorProduct k K (MonoidAlgebra k (Multiplicative (σ →₀ ℤ))) →ₐ[K] A) ≃* (σ → Aˣ)

The A-points of the base change of the rank-σ split torus are coordinate families σ → Aˣ.

The source is the convolution group of K-algebra maps out of the base-changed Hopf algebra K ⊗[k] k[Multiplicative (σ →₀ ℤ)]; the target is the product group of units of the value algebra.

Equations

• TauCeti.SplitTorus.baseChangePointsMulEquiv = TauCeti.DiagonalizableGroup.baseChangePointsMulEquiv.trans TauCeti.freeAbelianCharEquiv

@[simp]

theorem TauCeti.SplitTorus.baseChangePointsMulEquiv_apply_coe {k : Type u} {K : Type v} {A : Type w} {σ : Type w'} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] (f : WithConv (TensorProduct k K (MonoidAlgebra k (Multiplicative (σ →₀ ℤ))) →ₐ[K] A)) (i : σ) : ↑(baseChangePointsMulEquiv f i) = f.ofConv (1 ⊗ₜ[k] MonoidAlgebra.single (Multiplicative.ofAdd (Finsupp.single i 1)) 1)

The base-changed split-torus points equivalence reads a point by evaluating it on the base-changed standard coordinate generator indexed by i.

@[simp]

theorem TauCeti.SplitTorus.baseChangePointsMulEquiv_symm_apply_tmul_single {k : Type u} {K : Type v} {A : Type w} {σ : Type w'} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] (c : σ → Aˣ) (s : K) (m : σ →₀ ℤ) (r : k) : (baseChangePointsMulEquiv.symm c).ofConv (s ⊗ₜ[k] MonoidAlgebra.single (Multiplicative.ofAdd m) r) = s • r • ↑(m.prod fun (i : σ) (n : ℤ) => c i ^ n)

The inverse base-changed split-torus points equivalence sends a pure tensor s ⊗ single (ofAdd m) r to the scalar multiple of the monomial in the chosen coordinates with exponent vector m.

theorem TauCeti.SplitTorus.baseChangePointsMulEquiv_symm_apply_single_one {k : Type u} {K : Type v} {A : Type w} {σ : Type w'} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] (c : σ → Aˣ) (i : σ) : (baseChangePointsMulEquiv.symm c).ofConv (1 ⊗ₜ[k] MonoidAlgebra.single (Multiplicative.ofAdd (Finsupp.single i 1)) 1) = ↑(c i)

The inverse base-changed split-torus points equivalence takes the standard coordinate generator indexed by i to the chosen coordinate c i.