The split torus and its functor of points

The split torus on an index type σ is the diagonalizable group D(M) of the free abelian group M = Multiplicative (σ →₀ ℤ); its character lattice is σ →₀ ℤ, the free ℤ-module on σ. Concretely it is Spec R[Multiplicative (σ →₀ ℤ)], and for σ = Fin n it is the rank-n split torus 𝔾ₘⁿ.

This file computes its functor of points: for every commutative R-algebra A, the convolution group of R-algebra homomorphisms R[Multiplicative (σ →₀ ℤ)] →ₐ[R] A is the product group σ → Aˣ (with Fin n → Aˣ = (Aˣ)ⁿ in the finite-rank case), under pointwise multiplication. The equivalence sends a point to its values on the standard characters ofAdd (single i 1), equivalently the basis monomials single (ofAdd (single i 1)) 1.

This combines two existing pieces: the diagonalizable-group points calculation TauCeti.DiagonalizableGroup.pointsMulEquiv, computing the points of D(M) as the character group M →* Aˣ, and the free-abelian-group universal property TauCeti.freeAbelianCharEquiv, identifying characters of Multiplicative (σ →₀ ℤ) with families σ → Aˣ.

This is a worked-example check for the reductive-groups roadmap (ReductiveGroups/README.md in TauCetiRoadmap), Layer 4 ("Tori: split ... the character lattice X*(T)") together with the Layer 0 functor-of-points calculation, in the same spirit as the existing multiplicative group 𝔾ₘ, roots of unity μ_n, and diagonalizable group D(G).

Main definitions

• TauCeti.SplitTorus.characterGroup: the finitely generated character group of a finite-rank split torus.
• TauCeti.SplitTorus.pointsMulEquiv: the multiplicative equivalence from the convolution group of A-points of the rank-σ split torus to σ → Aˣ.
• TauCeti.SplitTorus.pointsMulEquiv_eq_freeAbelianCharEquiv: this equivalence factors through the free-abelian character equivalence.
• TauCeti.SplitTorus.pointsMulEquiv_apply_coe: a point is sent to its values on the standard generators single (ofAdd (single i 1)) 1.
• TauCeti.SplitTorus.pointsMulEquiv_mapValue: the points equivalence is natural in the value algebra.

References

The diagonalizable-group points calculation is Tau Ceti's DiagonalizableGroup.pointsMulEquiv; the free-abelian-group character identification is TauCeti.freeAbelianCharEquiv, which reuses Mathlib's Finsupp.liftAddHom and zmultiplesHom.

instance TauCeti.SplitTorus.instFGMultiplicativeFinsuppInt {sigma : Type u} [Finite sigma] : Group.FG (Multiplicative (sigma →₀ ℤ))

A finite-rank free character lattice, written multiplicatively, is finitely generated.

@[reducible, inline]

noncomputable abbrev TauCeti.SplitTorus.characterGroup (sigma : Type u) [Finite sigma] : FGCommGrpCat

The finitely generated character group of the split torus indexed by sigma.

Equations

• TauCeti.SplitTorus.characterGroup sigma = TauCeti.FGCommGrpCat.of (Multiplicative (sigma →₀ ℤ))

noncomputable def TauCeti.SplitTorus.pointsMulEquiv {R : Type u} {A : Type v} {σ : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] : WithConv (MonoidAlgebra R (Multiplicative (σ →₀ ℤ)) →ₐ[R] A) ≃* (σ → Aˣ)

The functor of points of the rank-σ split torus D(Multiplicative (σ →₀ ℤ)): for every commutative R-algebra A, the convolution group of R-algebra maps out of R[Multiplicative (σ →₀ ℤ)] is the product group σ → Aˣ, under pointwise multiplication.

Equations

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

theorem TauCeti.SplitTorus.pointsMulEquiv_eq_freeAbelianCharEquiv {R : Type u} {A : Type v} {σ : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] (f : WithConv (MonoidAlgebra R (Multiplicative (σ →₀ ℤ)) →ₐ[R] A)) : pointsMulEquiv f = freeAbelianCharEquiv (DiagonalizableGroup.pointsMulEquiv f)

The split-torus points equivalence is the free-abelian character equivalence applied to the underlying diagonalizable-group character.

@[simp]

theorem TauCeti.SplitTorus.pointsMulEquiv_apply_coe {R : Type u} {A : Type v} {σ : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] (f : WithConv (MonoidAlgebra R (Multiplicative (σ →₀ ℤ)) →ₐ[R] A)) (i : σ) : ↑(pointsMulEquiv f i) = f.ofConv (MonoidAlgebra.single (Multiplicative.ofAdd (Finsupp.single i 1)) 1)

The points equivalence reads off the value of a point on the i-th standard generator single (ofAdd (single i 1)) 1 of R[Multiplicative (σ →₀ ℤ)].

@[simp]

theorem TauCeti.SplitTorus.pointsMulEquiv_symm_apply {R : Type u} {A : Type v} {σ : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] (c : σ → Aˣ) : pointsMulEquiv.symm c = WithConv.toConv (DiagonalizableGroup.point (freeAbelianCharEquiv.symm c))

The inverse points equivalence sends a family c : σ → Aˣ to the point extending the character of Multiplicative (σ →₀ ℤ) determined by c.

theorem TauCeti.SplitTorus.pointsMulEquiv_symm_apply_single {R : Type u} {A : Type v} {σ : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] (c : σ → Aˣ) (i : σ) : (pointsMulEquiv.symm c).ofConv (MonoidAlgebra.single (Multiplicative.ofAdd (Finsupp.single i 1)) 1) = ↑(c i)

The inverse points equivalence sends a coordinate family to the point taking the i-th standard generator to the i-th coordinate.

theorem TauCeti.SplitTorus.pointsMulEquiv_mapValue {R : Type u} {A : Type v} {σ : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] {B : Type u_1} [CommSemiring B] [Algebra R B] (φ : A →ₐ[R] B) (f : WithConv (MonoidAlgebra R (Multiplicative (σ →₀ ℤ)) →ₐ[R] A)) (i : σ) : pointsMulEquiv ((AlgHom.mapValue φ) f) i = (Units.map ↑φ.toRingHom) (pointsMulEquiv f i)

The split-torus points equivalence is natural in the value algebra: post-composing a point with an R-algebra map φ : A →ₐ[R] B sends each coordinate through the induced map on units.

theorem TauCeti.SplitTorus.mapValue_pointsMulEquiv_symm_apply {R : Type u} {A : Type v} {σ : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] {B : Type u_1} [CommSemiring B] [Algebra R B] (φ : A →ₐ[R] B) (c : σ → Aˣ) : (AlgHom.mapValue φ) (pointsMulEquiv.symm c) = pointsMulEquiv.symm fun (i : σ) => (Units.map ↑φ.toRingHom) (c i)

Naturality of the inverse split-torus points equivalence in the value algebra.