counit_tensorObj — Mathlib

English

For coalgebras M and N over R, the counit of the tensor product CoalgCat.of R M ⊗ CoalgCat.of R N equals the standard counit on the ordinary tensor M ⊗_R N.

Русский

Для коалгебр M и N над R копулус (коначающий элемент) тензора CoalgCat.of R M ⊗ CoalgCat.of R N совпадает с обычным коулитом на тензоре M ⊗_R N.

LaTeX

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

Lean4

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

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