id_whiskerLeft_symm — Mathlib

English

The left unitor of a composite factors through the left unitor of the first factor and the associator with the second.

Русский

Левый уитор композиции разлагается через левый уитор первого факторa и ассоциатор со вторым.

LaTeX

$$$ (λ_{f g})^{hom} = (α_{\\mathbf{1}_A} f g)^{-1} \\; ≫ \\; (λ_f)^{hom} ◁ g $$$

Lean4

theorem id_whiskerLeft_symm {f g : a ⟶ b} (η : f ⟶ g) : η = (λ_ f).inv ≫ 𝟙 a ◁ η ≫ (λ_ g).hom := by simp

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