counit_tensorObj_tensorObj_right — Mathlib

English

For coalgebras M, N, P over R, the counit of the tensor product CoalgCat.of R M ⊗ (CoalgCat.of R N ⊗ CoalgCat.of R P) equals the standard counit on M ⊗_R (N ⊗_R P).

Русский

Для коалгебр M, N, P над R каулит тензорного объекта справа совпадает с обычным коулитом на 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_right :
    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

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