id_whiskerLeft_symm — Mathlib

English

Identity whisker left symmetry: f = λ_X^{-1} ∘ 1_C ◁ f ∘ λ_X'^{hom}.

Русский

Симметрия левого whisker с тождественным: f = λ_X^{-1} ∘ 1_C ◁ f ∘ λ_{X'}^{hom}.

LaTeX

$$$ f = (\lambda_X)^{-1} \circ \mathrm{Id}_C \triangleleft f \circ (\lambda_{X'})^{\mathrm{hom}}. $$$

Lean4

@[reassoc]
theorem id_whiskerLeft_symm {X X' : C} (f : X ⟶ X') : f = (λ_ X).inv ≫ 𝟙_ C ◁ f ≫ (λ_ X').hom := by
  simp only [id_whiskerLeft, assoc, inv_hom_id, comp_id, inv_hom_id_assoc]

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