counit_comul_hom — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem counit_comul_hom {Z : C} (f : M ⟶ Z) : Δ[M] ≫ (ε[M] ⊗ₘ f) = f ≫ (λ_ Z).inv := by
  rw [leftUnitor_inv_naturality, tensorHom_def, counit_comul_assoc]

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