rightUnitor_inv_naturality — Mathlib

English

Naturality of the right unitor: for f: X ⟶ X', f ≫ ρ_{X'}^{-1} = ρ_X^{-1} ≫ f ▷ ⊗.

Русский

Естественность правой единичной стрелки: для f: X ⟶ X', выполняется f ≫ ρ_{X'}^{-1} = ρ_X^{-1} ∘ f ▷ 1.

LaTeX

$$$ f \circ (\rho_{X'})^{-1} = (\rho_X)^{-1} \circ f \triangleright (\mathrm{tensorUnit}). $$$

Lean4

@[reassoc]
theorem rightUnitor_inv_naturality {X X' : C} (f : X ⟶ X') : f ≫ (ρ_ X').inv = (ρ_ X).inv ≫ f ▷ _ := by simp

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