triangle_assoc_comp_left_inv — Mathlib

English

The left triangle identity expresses a symmetry of the left unitor with the associator. For any f: a → b and g: b → c, the equation f ◁ (λ_ g)^{-1} ≫ α_f(g, I_b)^{−1} equals (ρ_f)^{−1} ◁ g.

Русский

Левое тождество треугольника выражает симметрию между левым уитером и ассоциатором: для любых f: a → b и g: b → c выполняется равенство f ◁ (λ_g)^{-1} ≫ α_f(g, I_b)^{-1} = (ρ_f)^{-1} ▷ g.

LaTeX

$$$ f \\triangleleft (\\lambda_g)^{-1} \\; \\circ \\; (\\alpha_f(g, \\mathbf{1}_b))^{-1} = (\\rho_f)^{-1} \\triangleright g $$$

Lean4

@[reassoc (attr := simp)]
theorem triangle_assoc_comp_left_inv (f : a ⟶ b) (g : b ⟶ c) : f ◁ (λ_ g).inv ≫ (α_ f (𝟙 b) g).inv = (ρ_ f).inv ▷ g :=
  by simp [← cancel_mono ((ρ_ f).hom ▷ g)]

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