Tensor products of coalgebras

Suppose S is an R-algebra. Given an S-coalgebra A and R-coalgebra B, we can define a natural comultiplication map Δ : A ⊗[R] B → (A ⊗[R] B) ⊗[S] (A ⊗[R] B) and counit map ε : A ⊗[R] B → S induced by the comultiplication and counit maps of A and B.

In this file we show that Δ, ε satisfy the axioms of a coalgebra, and also define other data in the monoidal structure on R-coalgebras, like the tensor product of two coalgebra morphisms as a coalgebra morphism.

In particular, when R = S we get tensor products of coalgebras, and when A = S we get the base change S ⊗[R] B as an S-coalgebra.

noncomputable instance TensorProduct.instCoalgebraStruct {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid A] [AddCommMonoid B] [Algebra R S] [Module R A] [Module S A] [Module R B] [IsScalarTower R S A] [CoalgebraStruct R B] [CoalgebraStruct S A] : CoalgebraStruct S (TensorProduct R A B)

theorem TensorProduct.comul_def {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid A] [AddCommMonoid B] [Algebra R S] [Module R A] [Module S A] [Module R B] [IsScalarTower R S A] [CoalgebraStruct R B] [CoalgebraStruct S A] : CoalgebraStruct.comul = ↑(AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) ∘ₗ AlgebraTensorModule.map CoalgebraStruct.comul CoalgebraStruct.comul

theorem TensorProduct.counit_def {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid A] [AddCommMonoid B] [Algebra R S] [Module R A] [Module S A] [Module R B] [IsScalarTower R S A] [CoalgebraStruct R B] [CoalgebraStruct S A] : CoalgebraStruct.counit = ↑(AlgebraTensorModule.rid R S S) ∘ₗ AlgebraTensorModule.map CoalgebraStruct.counit CoalgebraStruct.counit

@[simp]

theorem TensorProduct.comul_tmul {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid A] [AddCommMonoid B] [Algebra R S] [Module R A] [Module S A] [Module R B] [IsScalarTower R S A] [CoalgebraStruct R B] [CoalgebraStruct S A] (x : A) (y : B) : CoalgebraStruct.comul (x ⊗ₜ[R] y) = (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) (CoalgebraStruct.comul x ⊗ₜ[R] CoalgebraStruct.comul y)

@[simp]

theorem TensorProduct.counit_tmul {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid A] [AddCommMonoid B] [Algebra R S] [Module R A] [Module S A] [Module R B] [IsScalarTower R S A] [CoalgebraStruct R B] [CoalgebraStruct S A] (x : A) (y : B) : CoalgebraStruct.counit (x ⊗ₜ[R] y) = CoalgebraStruct.counit y • CoalgebraStruct.counit x

def TensorProduct.tacticHopf_tensor_induction_With__ : Lean.ParserDescr

hopf_tensor_induction x with x₁ x₂ attempts to replace x by x₁ ⊗ₜ x₂ via linearity. This is an implementation detail that is used to set up tensor products of coalgebras, bialgebras, and hopf algebras, and shouldn't be relied on downstream.

noncomputable instance TensorProduct.instCoalgebra {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid A] [AddCommMonoid B] [Algebra R S] [Module R A] [Module S A] [Module R B] [IsScalarTower R S A] [Coalgebra R B] [Coalgebra S A] : Coalgebra S (TensorProduct R A B)

instance TensorProduct.instIsCocomm {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [AddCommMonoid A] [AddCommMonoid B] [Algebra R S] [Module R A] [Module S A] [Module R B] [IsScalarTower R S A] [Coalgebra R B] [Coalgebra S A] [Coalgebra.IsCocomm S A] [Coalgebra.IsCocomm R B] : Coalgebra.IsCocomm S (TensorProduct R A B)

noncomputable def Coalgebra.TensorProduct.map {R : Type u_5} {S : Type u_6} {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] [Module S M] [IsScalarTower R S M] [Coalgebra S M] [Module S N] [IsScalarTower R S N] [Coalgebra S N] [Coalgebra R P] [Coalgebra R Q] (f : M →ₗc[S] N) (g : P →ₗc[R] Q) : TensorProduct R M P →ₗc[S] TensorProduct R N Q

The tensor product of two coalgebra morphisms as a coalgebra morphism.

@[simp]

theorem Coalgebra.TensorProduct.map_tmul {R : Type u_5} {S : Type u_6} {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] [Module S M] [IsScalarTower R S M] [Coalgebra S M] [Module S N] [IsScalarTower R S N] [Coalgebra S N] [Coalgebra R P] [Coalgebra R Q] (f : M →ₗc[S] N) (g : P →ₗc[R] Q) (x : M) (y : P) : (map f g) (x ⊗ₜ[R] y) = f x ⊗ₜ[R] g y

@[simp]

theorem Coalgebra.TensorProduct.map_toLinearMap {R : Type u_5} {S : Type u_6} {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] [Module S M] [IsScalarTower R S M] [Coalgebra S M] [Module S N] [IsScalarTower R S N] [Coalgebra S N] [Coalgebra R P] [Coalgebra R Q] (f : M →ₗc[S] N) (g : P →ₗc[R] Q) : ↑(map f g) = TensorProduct.AlgebraTensorModule.map ↑f ↑g

noncomputable def Coalgebra.TensorProduct.assoc (R : Type u_5) (S : Type u_6) (M : Type u_7) (N : Type u_8) (P : Type u_9) [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] [Module S M] [IsScalarTower R S M] [Coalgebra S M] [Module S N] [IsScalarTower R S N] [Coalgebra S N] [Coalgebra R P] : TensorProduct R (TensorProduct S M N) P ≃ₗc[S] TensorProduct S M (TensorProduct R N P)

The associator for tensor products of R-coalgebras, as a coalgebra equivalence.

@[simp]

theorem Coalgebra.TensorProduct.assoc_tmul {R : Type u_5} {S : Type u_6} {M : Type u_7} {N : Type u_8} {P : Type u_9} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] [Module S M] [IsScalarTower R S M] [Coalgebra S M] [Module S N] [IsScalarTower R S N] [Coalgebra S N] [Coalgebra R P] (x : M) (y : N) (z : P) : (TensorProduct.assoc R S M N P) (x ⊗ₜ[S] y ⊗ₜ[R] z) = x ⊗ₜ[S] (y ⊗ₜ[R] z)

@[simp]

theorem Coalgebra.TensorProduct.assoc_symm_tmul {R : Type u_5} {S : Type u_6} {M : Type u_7} {N : Type u_8} {P : Type u_9} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] [Module S M] [IsScalarTower R S M] [Coalgebra S M] [Module S N] [IsScalarTower R S N] [Coalgebra S N] [Coalgebra R P] (x : M) (y : N) (z : P) : (TensorProduct.assoc R S M N P).symm (x ⊗ₜ[S] (y ⊗ₜ[R] z)) = x ⊗ₜ[S] y ⊗ₜ[R] z

@[simp]

theorem Coalgebra.TensorProduct.assoc_toLinearEquiv {R : Type u_5} {S : Type u_6} {M : Type u_7} {N : Type u_8} {P : Type u_9} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] [Module S M] [IsScalarTower R S M] [Coalgebra S M] [Module S N] [IsScalarTower R S N] [Coalgebra S N] [Coalgebra R P] : ↑(TensorProduct.assoc R S M N P) = TensorProduct.AlgebraTensorModule.assoc R S S M N P

noncomputable def Coalgebra.TensorProduct.lid (R : Type u_5) (P : Type u_9) [CommSemiring R] [AddCommMonoid P] [Module R P] [Coalgebra R P] : TensorProduct R R P ≃ₗc[R] P

The base ring is a left identity for the tensor product of coalgebras, up to coalgebra equivalence.

@[simp]

theorem Coalgebra.TensorProduct.lid_toLinearEquiv {R : Type u_5} {P : Type u_9} [CommSemiring R] [AddCommMonoid P] [Module R P] [Coalgebra R P] : ↑(TensorProduct.lid R P) = _root_.TensorProduct.lid R P

@[simp]

theorem Coalgebra.TensorProduct.lid_tmul {R : Type u_5} {P : Type u_9} [CommSemiring R] [AddCommMonoid P] [Module R P] [Coalgebra R P] (r : R) (a : P) : (TensorProduct.lid R P) (r ⊗ₜ[R] a) = r • a

@[simp]

theorem Coalgebra.TensorProduct.lid_symm_apply {R : Type u_5} {P : Type u_9} [CommSemiring R] [AddCommMonoid P] [Module R P] [Coalgebra R P] (a : P) : (TensorProduct.lid R P).symm a = 1 ⊗ₜ[R] a

noncomputable def Coalgebra.TensorProduct.rid (R : Type u_5) (S : Type u_6) (M : Type u_7) [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [Coalgebra S M] : TensorProduct R M R ≃ₗc[S] M

The base ring is a right identity for the tensor product of coalgebras, up to coalgebra equivalence.

@[simp]

theorem Coalgebra.TensorProduct.rid_toLinearEquiv {R : Type u_5} {S : Type u_6} {M : Type u_7} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [Coalgebra S M] : ↑(TensorProduct.rid R S M) = TensorProduct.AlgebraTensorModule.rid R S M

@[simp]

theorem Coalgebra.TensorProduct.rid_tmul {R : Type u_5} {S : Type u_6} {M : Type u_7} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [Coalgebra S M] (r : R) (a : M) : (TensorProduct.rid R S M) (a ⊗ₜ[R] r) = r • a

@[simp]

theorem Coalgebra.TensorProduct.rid_symm_apply {R : Type u_5} {S : Type u_6} {M : Type u_7} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [Coalgebra S M] (a : M) : (TensorProduct.rid R S M).symm a = a ⊗ₜ[R] 1

@[reducible, inline]

noncomputable abbrev CoalgHom.lTensor {R : Type u_5} (M : Type u_6) {N : Type u_7} {P : Type u_8} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] (f : N →ₗc[R] P) : TensorProduct R M N →ₗc[R] TensorProduct R M P

lTensor M f : M ⊗ N →ₗc M ⊗ P is the natural coalgebra morphism induced by f : N →ₗc P.

@[reducible, inline]

noncomputable abbrev CoalgHom.rTensor {R : Type u_5} (M : Type u_6) {N : Type u_7} {P : Type u_8} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] (f : N →ₗc[R] P) : TensorProduct R N M →ₗc[R] TensorProduct R P M

rTensor M f : N ⊗ M →ₗc P ⊗ M is the natural coalgebra morphism induced by f : N →ₗc P.