rightUnitor_comp_inv — Mathlib

English

Let f: a → b and g: b → c be 1-morphisms. Then the inverse of the right unitor for f ≫ g is given by the left whiskering of the inverse of the right unitor on g with f, followed by the inverse of the associator: (ρ_{f ≫ g}).inv = f ◁ (ρ_g).inv ≫ (α_{f,g,(𝟙 c)}).inv.

Русский

Пусть f: a → b и g: b → c — 1-морфизмы. Тогда обобщённый обратный правый унитор для f ≫ g задаётся как левое взвешивание обратного правого унитора к g через f, затем композиция с обратным ассоциатором: (ρ_{f ≫ g}).inv = f ◁ (ρ_g).inv ≫ (α_{f,g,(𝟙 c)}).inv.

LaTeX

$$$ (\\rho_{f \\gg g}).inv = f \\;◁\\; (\\rho_g).inv \\;\\gg\\; (\\alpha_{f,g(\\mathbb{1}_c)}).inv $$$

Lean4

@[reassoc]
theorem rightUnitor_comp_inv (f : a ⟶ b) (g : b ⟶ c) : (ρ_ (f ≫ g)).inv = f ◁ (ρ_ g).inv ≫ (α_ f g (𝟙 c)).inv := by simp

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