Bialgebra maps and base change for tensor products

This file packages the canonical inclusions into and projections out of a tensor product of bialgebras as bialgebra morphisms, and records their action on pure tensors. The projections are obtained by applying the counit to the other tensor factor.

Scalar extension also commutes with tensor products of bialgebras. The resulting bialgebra equivalence upgrades TauCeti.Algebra.TensorProduct.baseChangeTensorAlgEquiv and records its action on pure tensors in both directions.

The underlying algebra equivalence upgrades Mathlib's TensorProduct.AlgebraTensorModule.distribBaseChange. The bialgebra comparison supplies the product/base-change identification for coordinate rings of direct products of affine group schemes.

The tensor-product bialgebra structure and its unit isomorphisms are from Mathlib's Mathlib.RingTheory.Bialgebra.TensorProduct.

noncomputable def TauCeti.Bialgebra.TensorProduct.includeLeft {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] : H₁ →ₐc[R] TensorProduct R H₁ H₂

The left inclusion x ↦ x ⊗ₜ 1 of a bialgebra into a tensor product of bialgebras, packaged as a bialgebra morphism. It is the unit R →ₐc[R] H₂ tensored on the right with H₁, precomposed with the right-unit isomorphism H₁ ≃ₐc[R] H₁ ⊗[R] R.

Equations

• TauCeti.Bialgebra.TensorProduct.includeLeft = (Bialgebra.TensorProduct.map (BialgHom.id R H₁) (Bialgebra.unitBialgHom R H₂)).comp (Bialgebra.TensorProduct.rid R R H₁).symm.toBialgHom

noncomputable def TauCeti.Bialgebra.TensorProduct.includeRight {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] : H₂ →ₐc[R] TensorProduct R H₁ H₂

The right inclusion y ↦ 1 ⊗ₜ y of a bialgebra into a tensor product of bialgebras, packaged as a bialgebra morphism. It is the unit R →ₐc[R] H₁ tensored on the left with H₂, precomposed with the left-unit isomorphism H₂ ≃ₐc[R] R ⊗[R] H₂.

Equations

• TauCeti.Bialgebra.TensorProduct.includeRight = (Bialgebra.TensorProduct.map (Bialgebra.unitBialgHom R H₁) (BialgHom.id R H₂)).comp (Bialgebra.TensorProduct.lid R H₂).symm.toBialgHom

@[simp]

theorem TauCeti.Bialgebra.TensorProduct.includeLeft_apply {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] (x : H₁) : includeLeft x = x ⊗ₜ[R] 1

@[simp]

theorem TauCeti.Bialgebra.TensorProduct.includeRight_apply {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] (y : H₂) : includeRight y = 1 ⊗ₜ[R] y

@[simp]

theorem TauCeti.Bialgebra.TensorProduct.includeLeft_toAlgHom {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] : ↑includeLeft = Algebra.TensorProduct.includeLeft

@[simp]

theorem TauCeti.Bialgebra.TensorProduct.includeRight_toAlgHom {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] : ↑includeRight = Algebra.TensorProduct.includeRight

noncomputable def TauCeti.Bialgebra.TensorProduct.projectLeft {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] : TensorProduct R H₁ H₂ →ₐc[R] H₁

The left projection H₁ ⊗[R] H₂ → H₁, given on pure tensors by x ⊗ₜ y ↦ ε(y) • x, as a bialgebra morphism.

Equations

• TauCeti.Bialgebra.TensorProduct.projectLeft = (Bialgebra.TensorProduct.rid R R H₁).toBialgHom.comp (Bialgebra.TensorProduct.map (BialgHom.id R H₁) (Bialgebra.counitBialgHom R H₂))

noncomputable def TauCeti.Bialgebra.TensorProduct.projectRight {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] : TensorProduct R H₁ H₂ →ₐc[R] H₂

The right projection H₁ ⊗[R] H₂ → H₂, given on pure tensors by x ⊗ₜ y ↦ ε(x) • y, as a bialgebra morphism.

Equations

• TauCeti.Bialgebra.TensorProduct.projectRight = (Bialgebra.TensorProduct.lid R H₂).toBialgHom.comp (Bialgebra.TensorProduct.map (Bialgebra.counitBialgHom R H₁) (BialgHom.id R H₂))

@[simp]

theorem TauCeti.Bialgebra.TensorProduct.projectLeft_tmul {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] (x : H₁) (y : H₂) : projectLeft (x ⊗ₜ[R] y) = CoalgebraStruct.counit y • x

@[simp]

theorem TauCeti.Bialgebra.TensorProduct.projectRight_tmul {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] (x : H₁) (y : H₂) : projectRight (x ⊗ₜ[R] y) = CoalgebraStruct.counit x • y

@[simp]

theorem TauCeti.Bialgebra.TensorProduct.projectLeft_comp_includeLeft {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] : projectLeft.comp includeLeft = BialgHom.id R H₁

The left projection is a retraction of the left inclusion.

@[simp]

theorem TauCeti.Bialgebra.TensorProduct.projectRight_comp_includeRight {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Bialgebra R H₁] [Bialgebra R H₂] : projectRight.comp includeRight = BialgHom.id R H₂

The right projection is a retraction of the right inclusion.

noncomputable def TauCeti.Bialgebra.TensorProduct.baseChangeTensorBialgEquiv (k : Type u) (K : Type w) [CommSemiring k] [CommSemiring K] [Algebra k K] (H : Type v) (L : Type x) [Semiring H] [Semiring L] [Bialgebra k H] [Bialgebra k L] : TensorProduct k K (TensorProduct k H L) ≃ₐc[K] TensorProduct K (TensorProduct k K H) (TensorProduct k K L)

Base change commutes with tensor products of bialgebras.

The underlying algebra equivalence distributes scalar extension across a tensor product. This bundling records that it also preserves the counit and comultiplication. For commutative Hopf algebras, it is contravariantly the canonical identification (G × H)_K ≅ G_K × H_K of affine groups.

Equations

• TauCeti.Bialgebra.TensorProduct.baseChangeTensorBialgEquiv k K H L = BialgEquiv.ofAlgEquiv (TauCeti.Algebra.TensorProduct.baseChangeTensorAlgEquiv k K H L) ⋯ ⋯

@[simp]

theorem TauCeti.Bialgebra.TensorProduct.baseChangeTensorBialgEquiv_toAlgEquiv (k : Type u) (K : Type w) [CommSemiring k] [CommSemiring K] [Algebra k K] (H : Type v) (L : Type x) [Semiring H] [Semiring L] [Bialgebra k H] [Bialgebra k L] : (baseChangeTensorBialgEquiv k K H L).toAlgEquiv = Algebra.TensorProduct.baseChangeTensorAlgEquiv k K H L

The algebra equivalence underlying the product/base-change bialgebra equivalence.

@[simp]

theorem TauCeti.Bialgebra.TensorProduct.baseChangeTensorBialgEquiv_tmul (k : Type u) (K : Type w) [CommSemiring k] [CommSemiring K] [Algebra k K] (H : Type v) (L : Type x) [Semiring H] [Semiring L] [Bialgebra k H] [Bialgebra k L] (s : K) (h : H) (l : L) : (baseChangeTensorBialgEquiv k K H L) (s ⊗ₜ[k] (h ⊗ₜ[k] l)) = s ⊗ₜ[k] h ⊗ₜ[K] (1 ⊗ₜ[k] l)

On a pure tensor, the product/base-change equivalence puts the scalar in the first base-changed factor.

@[simp]

theorem TauCeti.Bialgebra.TensorProduct.baseChangeTensorBialgEquiv_symm_tmul (k : Type u) (K : Type w) [CommSemiring k] [CommSemiring K] [Algebra k K] (H : Type v) (L : Type x) [Semiring H] [Semiring L] [Bialgebra k H] [Bialgebra k L] (s t : K) (h : H) (l : L) : (baseChangeTensorBialgEquiv k K H L).symm (s ⊗ₜ[k] h ⊗ₜ[K] (t ⊗ₜ[k] l)) = (s * t) ⊗ₜ[k] (h ⊗ₜ[k] l)

The inverse product/base-change equivalence multiplies the two scalar coefficients.