inv_η — Mathlib

English

The inverse image of the left unitor is given by a specific composition of μ, η and tensoration maps, as described by the monoidal structure.

Русский

Обратный образ левого унитора описывается через композицию μ, η и соответствующих тензорных отображений.

LaTeX

$$$$ F(\\lambda_X)^{-1} = (\\lambda_{F X})^{-1} \\circ (\\varepsilon F \\triangleright F X) \\circ \\mu F (\\mathbf{1}_C, X) $$$$

Lean4

@[simp]
theorem inv_η : CategoryTheory.inv (η F) = ε F := by rw [← εIso_hom, ← Iso.comp_inv_eq_id, εIso_inv, IsIso.inv_hom_id]

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