left_unitality_inv — Mathlib

English

For a lax monoidal functor F and object X, the inverse left unitor composed with the unit morphism and μ realizes the action of F on the left unit via the comparison with the mapped left unitor on X.

Русский

Для слабомономодального функторa F и объекта X обратный левый унитор, сопоставленный с единичным морфизмом и μ, реализует отображение левого единичного тождественного через отображение F левого унитора на X.

LaTeX

$$$(\\lambda_{F X})^{-1} \\;\\circ \\big( \\varepsilon_F \\triangleright F X \\big) \\circ μ_{\\mathbb{1},X}^F \;=\; F.map (\\lambda_X)^{-1}$$$

Lean4

@[reassoc (attr := simp)]
theorem left_unitality_inv (X : C) : (λ_ (F.obj X)).inv ≫ ε F ▷ F.obj X ≫ μ F (𝟙_ C) X = F.map (λ_ X).inv := by
  rw [Iso.inv_comp_eq, left_unitality, Category.assoc, Category.assoc, ← F.map_comp, Iso.hom_inv_id, F.map_id, comp_id]

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