Documentation

TauCeti.Algebra.Bialgebra.SymmetricAlgebra.BaseChange

Base change of symmetric bialgebras #

For a commutative semiring extension k → K and a k-module M, scalar extension of the symmetric bialgebra on M is canonically the symmetric bialgebra on the scalar extension of M:

K ⊗[k] SymmetricAlgebra k M ≃ₐc[K] SymmetricAlgebra K (K ⊗[k] M).

The equivalence preserves the counit and comultiplication and is characterized in both directions on pure-tensor generators.

This supplies the coordinate-bialgebra calculation used by the additive-group worked example in the ReductiveGroups roadmap's Layer 0 base-change milestone.

Main declarations #

References #

The construction follows W. C. Waterhouse, Introduction to Affine Group Schemes, §1. It uses Mathlib's AlgHom.liftEquiv, _root_.SymmetricAlgebra.lift, and BialgEquiv.ofAlgEquiv, together with the bialgebra structures from Mathlib.RingTheory.Bialgebra.SymmetricAlgebra and Mathlib.RingTheory.Bialgebra.TensorProduct.

source
noncomputable def TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv {k : Type u} {K : Type v} {M : Type w} [CommSemiring k] [CommSemiring K] [Algebra k K] [AddCommMonoid M] [Module k M] :
TensorProduct k K (SymmetricAlgebra k M) ≃ₐc[K] SymmetricAlgebra K (TensorProduct k K M)

Symmetric bialgebras commute with scalar extension.

The equivalence sends s ⊗ ι(m) to the generator ι(s ⊗ m) of the symmetric algebra on the scalar-extended module.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv_tmul_ι {k : Type u} {K : Type v} {M : Type w} [CommSemiring k] [CommSemiring K] [Algebra k K] [AddCommMonoid M] [Module k M] (s : K) (m : M) :
    scalarTensorBialgEquiv (s ⊗ₜ[k] (SymmetricAlgebra.ι k M) m) = (SymmetricAlgebra.ι K (TensorProduct k K M)) (s ⊗ₜ[k] m)

    The scalar-extension equivalence sends s ⊗ ι(m) to ι(s ⊗ m).

    source
    @[simp]
    theorem TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv_symm_ι_tmul {k : Type u} {K : Type v} {M : Type w} [CommSemiring k] [CommSemiring K] [Algebra k K] [AddCommMonoid M] [Module k M] (s : K) (m : M) :
    scalarTensorBialgEquiv.symm ((SymmetricAlgebra.ι K (TensorProduct k K M)) (s ⊗ₜ[k] m)) = s ⊗ₜ[k] (SymmetricAlgebra.ι k M) m

    The inverse scalar-extension equivalence sends the generator indexed by s ⊗ m to s ⊗ ι(m).

    source
    @[simp]
    theorem TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv_tmul_one {k : Type u} {K : Type v} {M : Type w} [CommSemiring k] [CommSemiring K] [Algebra k K] [AddCommMonoid M] [Module k M] (s : K) :
    scalarTensorBialgEquiv (s ⊗ₜ[k] 1) = (algebraMap K (SymmetricAlgebra K (TensorProduct k K M))) s

    The scalar-extension equivalence identifies the scalar copy of K on both sides.

    source
    theorem LinearMap.scalarTensorBialgEquiv_comp_map {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) :
    (↑TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv.toAlgEquiv).comp (Algebra.TensorProduct.map (AlgHom.id S S) (SymmetricAlgebra.map R f)) = (SymmetricAlgebra.map S (baseChange S f)).comp ↑TauCeti.SymmetricAlgebra.scalarTensorBialgEquiv.toAlgEquiv

    The scalar-extension comparison commutes with maps induced by linear maps.