Documentation

TauCeti.Algebra.AlgebraicGroup.AdditiveGroup.BaseChange

Base change of additive groups #

The vector group attached to a k-module M is represented by the symmetric bialgebra SymmetricAlgebra k M. This file specializes the generic symmetric-bialgebra base-change equivalence to the rank-one additive group 𝔾ₐ, and records the corresponding functor-of-points calculation: if A is a commutative K-algebra, then the convolution monoid of K-algebra maps out of K ⊗[k] SymmetricAlgebra k M is the additive monoid of k-linear maps M →ₗ[k] A.

The coordinate result imported from TauCeti.Algebra.Bialgebra.SymmetricAlgebra.BaseChange transports the counit and comultiplication, hence is bialgebra-level. No separate antipode or Hopf-equivalence packaging is asserted here.

The equivalence first restricts a base-changed point along m ↦ 1 ⊗ ι(m) using AlgHom.baseChangePointsMulEquiv, then applies AdditiveGroup.pointsMulEquiv. The characteristic lemmas spell out the generator values, the inverse map on scalar multiples of generators, and the one-dimensional additive group 𝔾ₐ.

Main declarations #

References #

The coordinate-bialgebra equivalence is TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv. The generic points base-change step is Tau Ceti's AlgHom.baseChangePointsMulEquiv; the vector-group points calculation is Tau Ceti's AdditiveGroup.pointsMulEquiv. This specialization follows the API pattern of RootsOfUnityGroup.baseChangePointsMulEquiv, SplitTorus.baseChangePointsMulEquiv, and DiagonalizableGroup.baseChangePointsMulEquiv. The construction follows W. C. Waterhouse, Introduction to Affine Group Schemes, §1.

source
noncomputable def TauCeti.AdditiveGroup.gaScalarTensorBialgEquiv {k : Type u} {K : Type v} [CommSemiring k] [CommSemiring K] [Algebra k K] :
TensorProduct k K (SymmetricAlgebra k k) ≃ₐc[K] SymmetricAlgebra K K

Base change of the additive coordinate bialgebra is the additive coordinate bialgebra over the new base.

This is the rank-one specialization of TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv, transported along K ⊗[k] k ≃ K.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.AdditiveGroup.gaScalarTensorBialgEquiv_tmul_ι {k : Type u} {K : Type v} [CommSemiring k] [CommSemiring K] [Algebra k K] (s : K) (r : k) :
    gaScalarTensorBialgEquiv (s ⊗ₜ[k] (SymmetricAlgebra.ι k k) r) = s • (SymmetricAlgebra.ι K K) ((algebraMap k K) r)

    The 𝔾ₐ coordinate equivalence sends s ⊗ ι(r) to s • ι(algebraMap k K r).

    source
    @[simp]
    theorem TauCeti.AdditiveGroup.gaScalarTensorBialgEquiv_tmul_one {k : Type u} {K : Type v} [CommSemiring k] [CommSemiring K] [Algebra k K] (s : K) :
    gaScalarTensorBialgEquiv (s ⊗ₜ[k] 1) = (algebraMap K (SymmetricAlgebra K K)) s

    The 𝔾ₐ coordinate equivalence identifies the scalar copy of K on both sides.

    source
    @[simp]
    theorem TauCeti.AdditiveGroup.gaScalarTensorBialgEquiv_symm_ι {k : Type u} {K : Type v} [CommSemiring k] [CommSemiring K] [Algebra k K] (s : K) :
    gaScalarTensorBialgEquiv.symm ((SymmetricAlgebra.ι K K) s) = s ⊗ₜ[k] (SymmetricAlgebra.ι k k) 1

    The inverse 𝔾ₐ coordinate equivalence sends ι(s) to the pure tensor s ⊗ ι(1).

    source
    noncomputable def TauCeti.AdditiveGroup.baseChangePointsMulEquiv {k : Type u} {K : Type v} {A : Type w} {M : Type w'} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] [AddCommMonoid M] [Module k M] :
    WithConv (TensorProduct k K (SymmetricAlgebra k M) →ₐ[K] A) ≃* Multiplicative (M →ₗ[k] A)

    The A-points of the base change K ⊗[k] SymmetricAlgebra k M of the vector group on M are the additive monoid of k-linear maps M →ₗ[k] A.

    The source is the convolution monoid of K-algebra maps out of the base-changed bialgebra; the target is written multiplicatively as Multiplicative (M →ₗ[k] A) to match ≃*.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.AdditiveGroup.toAdd_baseChangePointsMulEquiv_apply {k : Type u} {K : Type v} {A : Type w} {M : Type w'} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] [AddCommMonoid M] [Module k M] (F : WithConv (TensorProduct k K (SymmetricAlgebra k M) →ₐ[K] A)) (m : M) :
      (Multiplicative.toAdd (baseChangePointsMulEquiv F)) m = F.ofConv (1 ⊗ₜ[k] (SymmetricAlgebra.ι k M) m)

      The base-changed vector-group points equivalence reads a point by evaluating it on the base-changed generator 1 ⊗ ι(m).

      source
      @[simp]
      theorem TauCeti.AdditiveGroup.baseChangePointsMulEquiv_symm_apply_tmul_ι {k : Type u} {K : Type v} {A : Type w} {M : Type w'} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] [AddCommMonoid M] [Module k M] (φ : Multiplicative (M →ₗ[k] A)) (s : K) (m : M) :
      (baseChangePointsMulEquiv.symm φ).ofConv (s ⊗ₜ[k] (SymmetricAlgebra.ι k M) m) = s • (Multiplicative.toAdd φ) m

      The inverse base-changed vector-group points equivalence evaluates scalar multiples of base-changed generators by scalar multiplication of the corresponding linear-map value.

      source
      theorem TauCeti.AdditiveGroup.baseChangePointsMulEquiv_symm_apply_ι {k : Type u} {K : Type v} {A : Type w} {M : Type w'} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] [AddCommMonoid M] [Module k M] (φ : Multiplicative (M →ₗ[k] A)) (m : M) :
      (baseChangePointsMulEquiv.symm φ).ofConv (1 ⊗ₜ[k] (SymmetricAlgebra.ι k M) m) = (Multiplicative.toAdd φ) m

      The inverse base-changed vector-group points equivalence takes the generator indexed by m to the value of the chosen linear map at m.

      source
      noncomputable def TauCeti.AdditiveGroup.gaBaseChangePointsMulEquiv {k : Type u} {K : Type v} [CommSemiring k] [CommSemiring K] [Algebra k K] {A : Type w} [CommSemiring A] [Algebra K A] [Algebra k A] [IsScalarTower k K A] :
      WithConv (TensorProduct k K (SymmetricAlgebra k k) →ₐ[K] A) ≃* Multiplicative A

      The base-changed one-dimensional additive group 𝔾ₐ has A-points the additive monoid of the value algebra A.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.AdditiveGroup.toAdd_gaBaseChangePointsMulEquiv {k : Type u} {K : Type v} [CommSemiring k] [CommSemiring K] [Algebra k K] {A : Type w} [CommSemiring A] [Algebra K A] [Algebra k A] [IsScalarTower k K A] (F : WithConv (TensorProduct k K (SymmetricAlgebra k k) →ₐ[K] A)) :
        Multiplicative.toAdd (gaBaseChangePointsMulEquiv F) = F.ofConv (1 ⊗ₜ[k] (SymmetricAlgebra.ι k k) 1)

        The base-changed 𝔾ₐ points equivalence reads a point by evaluating it on 1 ⊗ ι(1).

        source
        @[simp]
        theorem TauCeti.AdditiveGroup.gaBaseChangePointsMulEquiv_symm_apply_ι {k : Type u} {K : Type v} [CommSemiring k] [CommSemiring K] [Algebra k K] {A : Type w} [CommSemiring A] [Algebra K A] [Algebra k A] [IsScalarTower k K A] (a : Multiplicative A) :
        (gaBaseChangePointsMulEquiv.symm a).ofConv (1 ⊗ₜ[k] (SymmetricAlgebra.ι k k) 1) = Multiplicative.toAdd a

        The inverse base-changed 𝔾ₐ points equivalence takes the generator 1 ⊗ ι(1) to the chosen value.