counit_tensorObj_tensorObj_left — Mathlib

English

Same as above for a left-associated triple tensor: the counit on ((CoalgCat.of R M ⊗ CoalgCat.of R N) ⊗ CoalgCat.of R P) coincides with the standard counit on M ⊗_R N ⊗_R P.

Русский

Аналогично слева в ассоциированном тройном тензоре: коулит на ((CoalgCat.of R M ⊗ CoalgCat.of R N) ⊗ CoalgCat.of R P) совпадает со стандартным на M ⊗_R N ⊗_R P.

LaTeX

$$$\operatorname{counit} (R := R) (A := ((\mathrm{CoalgCat.of R M} \otimes \mathrm{CoalgCat.of R N}) \otimes \mathrm{CoalgCat.of R P} : \mathrm{CoalgCat R})) = \,\operatorname{counit} (A := (M \otimes[R] N) \otimes[R] P)$$$

Lean4

theorem counit_tensorObj_tensorObj_left :
    Coalgebra.counit (R := R) (A := ((CoalgCat.of R M ⊗ CoalgCat.of R N) ⊗ CoalgCat.of R P : CoalgCat R)) =
      Coalgebra.counit (A := (M ⊗[R] N) ⊗[R] P) :=
  by
  rw [ofComonObjCoalgebraStruct_counit]
  simp [TensorProduct.counit_def, TensorProduct.AlgebraTensorModule.rid_eq_rid, ← lid_eq_rid]
  rfl

Похожие утверждения