theorem TensorProduct.map_left_up {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (f : A →ₗ[R] B) (g : C →ₗ[R] D) : TensorProduct.map f g = TensorProduct.map f LinearMap.id ∘ₗ TensorProduct.map LinearMap.id g

theorem TensorProduct.map_right_down {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (f : A →ₗ[R] B) (g : C →ₗ[R] D) : TensorProduct.map f g = TensorProduct.map f LinearMap.id ∘ₗ TensorProduct.map LinearMap.id g

Alias of TensorProduct.map_left_up.

theorem TensorProduct.map_right_up {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (f : A →ₗ[R] B) (g : C →ₗ[R] D) : TensorProduct.map f g = TensorProduct.map LinearMap.id g ∘ₗ TensorProduct.map f LinearMap.id

theorem TensorProduct.map_left_down {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (f : A →ₗ[R] B) (g : C →ₗ[R] D) : TensorProduct.map f g = TensorProduct.map LinearMap.id g ∘ₗ TensorProduct.map f LinearMap.id

Alias of TensorProduct.map_right_up.

theorem Algebra.linearMap_mul'_assoc {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : LinearMap.mul' R A ∘ₗ TensorProduct.map (LinearMap.mul' R A) LinearMap.id = LinearMap.mul' R A ∘ₗ TensorProduct.map LinearMap.id (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A)

theorem Algebra.assoc {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : LinearMap.mul' R A ∘ₗ TensorProduct.map (LinearMap.mul' R A) LinearMap.id = LinearMap.mul' R A ∘ₗ TensorProduct.map LinearMap.id (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A)

Alias of Algebra.linearMap_mul'_assoc.

theorem Algebra.assoc' {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (LinearMap.mul' R A) = LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A)

theorem Algebra.mul_comp_rTensor_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (LinearMap.mul' R A) = LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A)

Alias of Algebra.assoc'.

theorem Algebra.mul_comp_rTensor_unit {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (Algebra.linearMap R A) = ↑(TensorProduct.lid R A)

theorem Algebra.mul_comp_rTensor_unit_comp_lid_symm {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (Algebra.linearMap R A) ∘ₗ ↑(TensorProduct.lid R A).symm = LinearMap.id

theorem Algebra.mul_comp_lTensor_unit {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (Algebra.linearMap R A) = ↑(TensorProduct.rid R A)

theorem Algebra.mul_comp_lTensor_unit_comp_rid_symm {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (Algebra.linearMap R A) ∘ₗ ↑(TensorProduct.rid R A).symm = LinearMap.id

theorem counit_comp_mul_comp_rTensor_unit {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [Coalgebra R A] : Coalgebra.counit ∘ₗ LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (Algebra.linearMap R A) ∘ₗ ↑(TensorProduct.lid R A).symm = Coalgebra.counit

theorem counit_comp_mul_lTensor_unit {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [Coalgebra R A] : Coalgebra.counit ∘ₗ LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (Algebra.linearMap R A) ∘ₗ ↑(TensorProduct.rid R A).symm = Coalgebra.counit

theorem lTensor_counit_comp_comul_unit {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [Coalgebra R A] : LinearMap.lTensor A Coalgebra.counit ∘ₗ Coalgebra.comul ∘ₗ Algebra.linearMap R A = ↑(TensorProduct.rid R A).symm ∘ₗ Algebra.linearMap R A

theorem Coalgebra.rTensor_counit_comp_comul' {R : Type u_1} [CommSemiring R] {A : Type u_2} [AddCommMonoid A] [Module R A] [Coalgebra R A] : LinearMap.rTensor A Coalgebra.counit ∘ₗ Coalgebra.comul = ↑(TensorProduct.lid R A).symm

theorem TensorProduct.assoc_symm_comp_rTensor {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (x : A →ₗ[R] D) : ↑(TensorProduct.assoc R D B C).symm ∘ₗ LinearMap.rTensor (TensorProduct R B C) x = LinearMap.rTensor C (LinearMap.rTensor B x) ∘ₗ ↑(TensorProduct.assoc R A B C).symm

theorem TensorProduct.assoc_symm_comp_lTensor_lTensor {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (x : A →ₗ[R] D) : ↑(TensorProduct.assoc R B C D).symm ∘ₗ LinearMap.lTensor B (LinearMap.lTensor C x) = LinearMap.lTensor (TensorProduct R B C) x ∘ₗ ↑(TensorProduct.assoc R B C A).symm

theorem TensorProduct.rTensor_lTensor_comp_assoc_symm {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (x : A →ₗ[R] D) : LinearMap.rTensor C (LinearMap.lTensor B x) ∘ₗ ↑(TensorProduct.assoc R B A C).symm = ↑(TensorProduct.assoc R B D C).symm ∘ₗ LinearMap.lTensor B (LinearMap.rTensor C x)

theorem TensorProduct.assoc_comp_rTensor_rTensor {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (x : A →ₗ[R] D) : ↑(TensorProduct.assoc R D B C) ∘ₗ LinearMap.rTensor C (LinearMap.rTensor B x) = LinearMap.rTensor (TensorProduct R B C) x ∘ₗ ↑(TensorProduct.assoc R A B C)

theorem TensorProduct.ext_fourfold'' {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} {E : Type u_6} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [AddCommMonoid E] [Module R A] [Module R B] [Module R C] [Module R D] [Module R E] {f : TensorProduct R A (TensorProduct R B (TensorProduct R C D)) →ₗ[R] E} {g : TensorProduct R A (TensorProduct R B (TensorProduct R C D)) →ₗ[R] E} : (∀ (x : A) (y : B) (z : C) (w : D), f (x ⊗ₜ[R] y ⊗ₜ[R] z ⊗ₜ[R] w) = g (x ⊗ₜ[R] y ⊗ₜ[R] z ⊗ₜ[R] w)) → f = g

theorem TensorProduct.assoc_comp_rTensor_assoc_symm_comp_assoc_symm_comp_lTensor_assoc_symm {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] : ↑(TensorProduct.assoc R (TensorProduct R A B) C D) ∘ₗ LinearMap.rTensor D ↑(TensorProduct.assoc R A B C).symm ∘ₗ ↑(TensorProduct.assoc R A (TensorProduct R B C) D).symm ∘ₗ LinearMap.lTensor A ↑(TensorProduct.assoc R B C D).symm = ↑(TensorProduct.assoc R A B (TensorProduct R C D)).symm

theorem TensorProduct.rTensor_comp_rTensor {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (x : B →ₗ[R] C) (y : A →ₗ[R] B) : LinearMap.rTensor D x ∘ₗ LinearMap.rTensor D y = LinearMap.rTensor D (x ∘ₗ y)

theorem TensorProduct.lTensor_comp_lTensor {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (x : B →ₗ[R] C) (y : A →ₗ[R] B) : LinearMap.lTensor D x ∘ₗ LinearMap.lTensor D y = LinearMap.lTensor D (x ∘ₗ y)

theorem lid_tensor {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] : ↑(TensorProduct.lid R (TensorProduct R A B)) = LinearMap.rTensor B ↑(TensorProduct.lid R A) ∘ₗ ↑(TensorProduct.assoc R R A B).symm

theorem rTensor_comp_lTensor' {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (x : A →ₗ[R] B) (y : C →ₗ[R] D) : LinearMap.rTensor D x ∘ₗ LinearMap.lTensor A y = LinearMap.lTensor B y ∘ₗ LinearMap.rTensor C x

theorem lTensor_mul_comp_rTensor_comul_of {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] [Coalgebra R A] (h : LinearMap.lTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A Coalgebra.comul = LinearMap.rTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm ∘ₗ LinearMap.lTensor A Coalgebra.comul) : LinearMap.lTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A Coalgebra.comul = Coalgebra.comul ∘ₗ LinearMap.mul' R A

if (id ⊗ mul) (comul ⊗ id) = (mul ⊗ id) (id ⊗ comul), then (id ⊗ mul) (comul ⊗ id) = comul ∘ mul.

This is sometimes referred to as the Frobenius equations.

theorem counit_comp_mul_comp_rTensor_unit_eq_counit {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] [Coalgebra R A] : Coalgebra.counit ∘ₗ LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (Algebra.linearMap R A) = Coalgebra.counit ∘ₗ ↑(TensorProduct.lid R A)

theorem counit_comp_mul_comp_lTensor_unit_eq_counit {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] [Coalgebra R A] : Coalgebra.counit ∘ₗ LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (Algebra.linearMap R A) = Coalgebra.counit ∘ₗ ↑(TensorProduct.rid R A)

theorem rTensor_counit_comp_comul_comp_unit_eq_unit {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] [Coalgebra R A] : LinearMap.rTensor A Coalgebra.counit ∘ₗ Coalgebra.comul ∘ₗ Algebra.linearMap R A = ↑(TensorProduct.lid R A).symm ∘ₗ Algebra.linearMap R A

theorem lTensor_counit_comp_comul_comp_unit_eq_unit {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] [Coalgebra R A] : LinearMap.lTensor A Coalgebra.counit ∘ₗ Coalgebra.comul ∘ₗ Algebra.linearMap R A = ↑(TensorProduct.rid R A).symm ∘ₗ Algebra.linearMap R A

class FrobeniusAlgebra (R : Type u_3) (A : Type u_4) [CommSemiring R] [Semiring A] extends Algebra , Coalgebra , SMul , RingHom , MonoidHom , OneHom , AddMonoidHom , NonUnitalRingHom , MonoidWithZeroHom , MulHom , ZeroHom , AddHom , CoalgebraStruct : Type (max u_3 u_4)

theorem FrobeniusAlgebra.lTensor_mul_comp_rTensor_comul_commute {R : Type u_3} {A : Type u_4} : ∀ {inst : CommSemiring R} {inst_1 : Semiring A} [self : FrobeniusAlgebra R A], LinearMap.lTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A Coalgebra.comul = LinearMap.rTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm ∘ₗ LinearMap.lTensor A Coalgebra.comul

theorem FrobeniusAlgebra.lTensor_mul_comp_rTensor_comul_eq_comul_comp_mul {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [FrobeniusAlgebra R A] : LinearMap.lTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A Coalgebra.comul = Coalgebra.comul ∘ₗ LinearMap.mul' R A

theorem FrobeniusAlgebra.rTensor_mul_comp_lTensor_comul_eq_comul_comp_mul {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [FrobeniusAlgebra R A] : LinearMap.rTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm ∘ₗ LinearMap.lTensor A Coalgebra.comul = Coalgebra.comul ∘ₗ LinearMap.mul' R A

theorem FrobeniusAlgebra.rTensor_mul_comp_lTensor_comul_unit_eq_comul {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [FrobeniusAlgebra R A] : LinearMap.rTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm ∘ₗ LinearMap.lTensor A (Coalgebra.comul ∘ₗ Algebra.linearMap R A) = Coalgebra.comul ∘ₗ ↑(TensorProduct.rid R A)

theorem FrobeniusAlgebra.lTensor_mul_comp_rTensor_comul_unit {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [FrobeniusAlgebra R A] : LinearMap.lTensor A (LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A (Coalgebra.comul ∘ₗ Algebra.linearMap R A) = Coalgebra.comul ∘ₗ ↑(TensorProduct.lid R A)

theorem FrobeniusAlgebra.rTensor_counit_mul_comp_lTensor_comul {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [FrobeniusAlgebra R A] : LinearMap.rTensor A (Coalgebra.counit ∘ₗ LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm ∘ₗ LinearMap.lTensor A Coalgebra.comul = ↑(TensorProduct.lid R A).symm ∘ₗ LinearMap.mul' R A

theorem FrobeniusAlgebra.lTensor_counit_mul_comp_rTensor_comul {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [FrobeniusAlgebra R A] : LinearMap.lTensor A (Coalgebra.counit ∘ₗ LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A Coalgebra.comul = ↑(TensorProduct.rid R A).symm ∘ₗ LinearMap.mul' R A

theorem FrobeniusAlgebra.rTensor_counit_mul_comp_lTensor_comul_unit {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [FrobeniusAlgebra R A] : LinearMap.rTensor A (Coalgebra.counit ∘ₗ LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm ∘ₗ LinearMap.lTensor A (Coalgebra.comul ∘ₗ Algebra.linearMap R A) = ↑(TensorProduct.comm R A R)

"snake equations" v1

theorem FrobeniusAlgebra.lTensor_counit_mul_comp_rTensor_comul_unit {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [FrobeniusAlgebra R A] : LinearMap.lTensor A (Coalgebra.counit ∘ₗ LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A (Coalgebra.comul ∘ₗ Algebra.linearMap R A) = ↑(TensorProduct.comm R R A)

"snake equations" v2