The monoid algebra of a product is the tensor product of monoid algebras

For two monoids G and H, the canonical map single (g, h) 1 ↦ single g 1 ⊗ₜ single h 1 is an isomorphism of R-bialgebras R[G × H] ≃ₐc[R] R[G] ⊗[R] R[H].

The bialgebra isomorphism is promoted from the standard algebra maps: the lift of the group-like monoid hom (g, h) ↦ single g 1 ⊗ₜ single h 1 one way, and the tensor-product universal map of the two inclusions R[G] → R[G × H], R[H] → R[G × H] (themselves MonoidAlgebra.mapDomainAlgHom of MonoidHom.inl/MonoidHom.inr) the other way. The public API keeps only the bialgebra equivalence and its generator formulas.

This is generic monoid-algebra API used by the diagonalizable-group product calculation.

Main definitions

• TauCeti.MonoidAlgebra.prodTensorBialgEquiv: the bialgebra isomorphism R[G × H] ≃ₐc[R] R[G] ⊗[R] R[H].

References

The tensor-product bialgebra structure and Algebra.TensorProduct.lift are from Mathlib's Mathlib.RingTheory.Bialgebra.TensorProduct and Mathlib.RingTheory.TensorProduct.Maps; the monoid-algebra bialgebra structure and MonoidAlgebra.mapDomainAlgHom are from Mathlib.RingTheory.Bialgebra.MonoidAlgebra and Mathlib.Algebra.MonoidAlgebra.Basic.

noncomputable def TauCeti.MonoidAlgebra.prodTensorBialgEquiv (R : Type u) [CommSemiring R] {G : Type v} {H : Type w} [Monoid G] [Monoid H] : MonoidAlgebra R (G × H) ≃ₐc[R] TensorProduct R (MonoidAlgebra R G) (MonoidAlgebra R H)

The monoid algebra of a product is the tensor product of monoid algebras, as a bialgebra isomorphism.

Equations

• TauCeti.MonoidAlgebra.prodTensorBialgEquiv R = BialgEquiv.ofAlgEquiv (TauCeti.MonoidAlgebra.prodTensorAlgEquiv✝ R) ⋯ ⋯

@[simp]

theorem TauCeti.MonoidAlgebra.prodTensorBialgEquiv_single (R : Type u) [CommSemiring R] {G : Type v} {H : Type w} [Monoid G] [Monoid H] (g : G) (h : H) : (prodTensorBialgEquiv R) (MonoidAlgebra.single (g, h) 1) = MonoidAlgebra.single g 1 ⊗ₜ[R] MonoidAlgebra.single h 1

The forward product bialgebra equivalence sends the generator indexed by (g, h) to the pure tensor of the two factor generators.

@[simp]

theorem TauCeti.MonoidAlgebra.prodTensorBialgEquiv_symm_tmul_single (R : Type u) [CommSemiring R] {G : Type v} {H : Type w} [Monoid G] [Monoid H] (g : G) (h : H) : (prodTensorBialgEquiv R).symm (MonoidAlgebra.single g 1 ⊗ₜ[R] MonoidAlgebra.single h 1) = MonoidAlgebra.single (g, h) 1

The inverse product bialgebra equivalence sends a pure tensor of factor generators to the generator indexed by their product pair.