Base change of monoid bialgebras

For a commutative semiring extension k → K and a commutative monoid G, scalar extension of the monoid bialgebra k[G] is canonically the monoid bialgebra K[G]:

K ⊗[k] k[G] ≃ₐc[K] K[G].

Mathlib supplies the underlying algebra equivalence as MonoidAlgebra.scalarTensorEquiv. This file records that it preserves the counit and comultiplication, hence promotes it to a bialgebra equivalence. The equivalence is natural in G. When G is a group, both sides carry their standard Hopf structures, so this is the coordinate-ring base-change identification for the diagonalizable group D(G).

This is the base-change input for the ReductiveGroups roadmap's Layer 4 development of groups of multiplicative type and non-split tori: after extension of the base field, a diagonalizable coordinate Hopf algebra remains the group algebra of the same character group.

Main declarations

• TauCeti.MonoidAlgebra.scalarTensorBialgEquiv: base change of a monoid bialgebra is the monoid bialgebra over the extended scalars.
• TauCeti.MonoidAlgebra.mapDomainBialgHom_comp_scalarTensorBialgEquiv: the equivalence is natural in the indexing monoid.

References

The underlying algebra equivalence is Mathlib's MonoidAlgebra.scalarTensorEquiv from Mathlib.RingTheory.TensorProduct.MonoidAlgebra; the bialgebra structures are from Mathlib.RingTheory.Bialgebra.MonoidAlgebra and Mathlib.RingTheory.Bialgebra.TensorProduct.

noncomputable def TauCeti.MonoidAlgebra.scalarTensorBialgEquiv (k : Type u) (K : Type v) [CommSemiring k] [CommSemiring K] [Algebra k K] {G : Type w} [CommMonoid G] : TensorProduct k K (MonoidAlgebra k G) ≃ₐc[K] MonoidAlgebra K G

Monoid bialgebras commute with base change.

This is Mathlib's algebra equivalence MonoidAlgebra.scalarTensorEquiv, promoted using the standard tensor-product and monoid-algebra coalgebra structures. For a group G, the standard Hopf structures on source and target make this the coordinate-ring base-change equivalence K ⊗[k] k[G] ≃ K[G] for the diagonalizable group D(G).

Equations

• TauCeti.MonoidAlgebra.scalarTensorBialgEquiv k K = BialgEquiv.ofAlgEquiv (MonoidAlgebra.scalarTensorEquiv k K) ⋯ ⋯

@[simp]

theorem TauCeti.MonoidAlgebra.scalarTensorBialgEquiv_tmul (k : Type u) (K : Type v) [CommSemiring k] [CommSemiring K] [Algebra k K] {G : Type w} [CommMonoid G] (s : K) (p : MonoidAlgebra k G) : (scalarTensorBialgEquiv k K) (s ⊗ₜ[k] p) = s • (MonoidAlgebra.mapAlgHom G (Algebra.ofId k K)) p

On a pure tensor, base change applies the scalar and maps the coefficients of the monoid algebra along k → K.

@[simp]

theorem TauCeti.MonoidAlgebra.scalarTensorBialgEquiv_symm_single (k : Type u) (K : Type v) [CommSemiring k] [CommSemiring K] [Algebra k K] {G : Type w} [CommMonoid G] (g : G) (s : K) : (scalarTensorBialgEquiv k K).symm (MonoidAlgebra.single g s) = s ⊗ₜ[k] MonoidAlgebra.single g 1

The inverse base-change equivalence sends a monomial over K to the corresponding pure tensor.

theorem TauCeti.MonoidAlgebra.mapDomainBialgHom_comp_scalarTensorBialgEquiv (k : Type u) (K : Type v) [CommSemiring k] [CommSemiring K] [Algebra k K] {G : Type w} {G' : Type w'} [CommMonoid G] [CommMonoid G'] (φ : G →* G') : (MonoidAlgebra.mapDomainBialgHom K φ).comp ↑(scalarTensorBialgEquiv k K) = (↑(scalarTensorBialgEquiv k K)).comp (Bialgebra.TensorProduct.map (BialgHom.id K K) (MonoidAlgebra.mapDomainBialgHom k φ))

Base change of monoid bialgebras is natural in the indexing monoid. Mapping the indices before base change gives the same bialgebra morphism as mapping them afterwards.