comul_counit_hom — Mathlib

English

For f: M → Z, the composite Δ[M] followed by (f ⊗ ε[M]) equals f composed with the inverse right unitor on Z.

Русский

Для f: M → Z композиция Δ[M] затем (f ⊗ ε[M]) равна f затем обратный правый юнитор над Z.

LaTeX

$$$\Delta[M] \\;≫ \\; (f \\otimes ε[M]) = f \\;≫ \\; (\\rho_Z)^{-1}$$$

Lean4

@[reassoc (attr := simp)]
theorem comul_counit_hom {Z : C} (f : M ⟶ Z) : Δ[M] ≫ (f ⊗ₘ ε[M]) = f ≫ (ρ_ Z).inv := by
  rw [rightUnitor_inv_naturality, tensorHom_def', comul_counit_assoc]

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