right_unitality_inv — Mathlib

English

Analogous to the left case, the inverse right unitor composed with the unit and μ yields the mapped right unitor under F.

Русский

Аналогично левому случаю, обратный правый унитор, сочетаясь с единицей и μ, дает отображение правого унитора через F.

LaTeX

$$$(\\rho_{F X})^{-1} \\;\\circ (F X \\triangleleft \\varepsilon_F) \\circ μ_{X,\\mathbb{1}}^F \;=\; F.map (\\rho_X)^{-1}$$$

Lean4

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

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