whiskerRight_id_symm — Mathlib

English

Symmetry of whiskering with tensor unit on the right: f = ρ_X^{-1} ∘ f ▷ 1 ∘ ρ_Y^{hom}.

Русский

Симметрия правого whisker с тензорной единицей: f = ρ_X^{-1} ∘ f ▷ 1 ∘ ρ_Y^{hom}.

LaTeX

$$$ f = (\rho_X)^{-1} \circ (f \triangleright \mathrm{Id}_{\mathbb{1}}) \circ (\rho_Y)^{\mathrm{hom}}. $$$

Lean4

@[reassoc]
theorem whiskerRight_id_symm {X Y : C} (f : X ⟶ Y) : f = (ρ_ X).inv ≫ f ▷ 𝟙_ C ≫ (ρ_ Y).hom := by simp

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