Documentation

TauCeti.Algebra.AlgebraicGroup.MultiplicativeGroup.BaseChange

Base change of multiplicative-group points #

The multiplicative group 𝔾_m over k is represented here by the Laurent-polynomial Hopf algebra k[T;T⁻¹]. This file records the base-changed functor-of-points calculation: for a k-algebra K and a commutative K-algebra A, the convolution group of K-algebra maps out of K ⊗[k] k[T;T⁻¹] is the unit group Aˣ.

The equivalence first restricts a base-changed point along f ↦ f (1 ⊗ T) using AlgHom.baseChangePointsMulEquiv, then applies the Laurent-polynomial calculation MultiplicativeGroup.pointsMulEquiv. The characteristic lemmas give the values on 1 ⊗ T and on the inverse map at pure tensors s ⊗ C r * T n.

This is the direct Laurent-polynomial 𝔾_m worked example for the ReductiveGroups roadmap, Layer 0 ("R-points as a group" and "Base change. K ⊗[k] A as a Hopf algebra over K"), alongside the more general diagonalizable and split-torus base-change APIs.

Main declarations #

References #

This reuses Tau Ceti's AlgHom.baseChangePointsMulEquiv and MultiplicativeGroup.pointsMulEquiv, which in turn build on Mathlib's tensor-product base-change adjunction and Laurent-polynomial Hopf algebra structure.

source
noncomputable def TauCeti.MultiplicativeGroup.baseChangePointsMulEquiv {k : Type u} {K : Type v} {A : 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 (LaurentPolynomial k) →ₐ[K] A) ≃* Aˣ

The A-points of the base change K ⊗[k] k[T;T⁻¹] of the multiplicative group are the unit group Aˣ.

The source is the convolution group of K-algebra maps out of the base-changed Hopf algebra. The target is the ordinary unit group of the value algebra.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.MultiplicativeGroup.baseChangePointsMulEquiv_apply {k : Type u} {K : Type v} {A : 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 (LaurentPolynomial k) →ₐ[K] A)) :
    ↑(baseChangePointsMulEquiv f) = f.ofConv (1 ⊗ₜ[k] LaurentPolynomial.T 1)

    The base-changed multiplicative-group points equivalence reads a point by evaluating it on the base-changed coordinate 1 ⊗ T.

    source
    @[simp]
    theorem TauCeti.MultiplicativeGroup.baseChangePointsMulEquiv_symm_apply_tmul_C_mul_T {k : Type u} {K : Type v} {A : Type w} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] (u : Aˣ) (s : K) (r : k) (n : ℤ) :
    (baseChangePointsMulEquiv.symm u).ofConv (s ⊗ₜ[k] (LaurentPolynomial.C r * LaurentPolynomial.T n)) = s • r • ↑(u ^ n)

    The inverse base-changed multiplicative-group points equivalence evaluates pure Laurent monomials s ⊗ C r * T n as scalar multiples of the corresponding power of the chosen unit.

    source
    @[simp]
    theorem TauCeti.MultiplicativeGroup.baseChangePointsMulEquiv_symm_apply_tmul_T {k : Type u} {K : Type v} {A : Type w} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] (u : Aˣ) (s : K) (n : ℤ) :
    (baseChangePointsMulEquiv.symm u).ofConv (s ⊗ₜ[k] LaurentPolynomial.T n) = s • ↑(u ^ n)

    The inverse base-changed multiplicative-group points equivalence evaluates pure tensors s ⊗ T n as scalar multiples of the corresponding power of the chosen unit.

    source
    theorem TauCeti.MultiplicativeGroup.baseChangePointsMulEquiv_symm_apply_T {k : Type u} {K : Type v} {A : Type w} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] (u : Aˣ) :
    (baseChangePointsMulEquiv.symm u).ofConv (1 ⊗ₜ[k] LaurentPolynomial.T 1) = ↑u

    The inverse base-changed multiplicative-group points equivalence takes 1 ⊗ T to the chosen unit.