triangle_assoc_comp_left_inv — Mathlib

English

In a monoidal category, the left inverse triangle identity relates X whiskered with (λ_Y)^{-1} and the inverse of the associator; equivalently, (X ◁ (λ_Y)^{-1}) ≫ α_{X,I,Y}^{-1} = (ρ_X)^{-1} whiskered by Y.

Русский

В моноидальной категории левый член треугольника связывает X, инвертированную левую единицу и обратный ассоциатор; то есть (X ◁ (λ_Y)^{-1}) ≫ α_{X,I,Y}^{-1} = (ρ_X)^{-1} ◁ Y.

LaTeX

$$$(X \\triangleleft (\\lambda_Y)^{-1}) \\;\\circ\\; α_{X, \\mathbf{1}, Y}^{-1} = (\\rho_X)^{-1} \\;\\triangleright\\; Y$$$

Lean4

@[reassoc (attr := simp)]
theorem triangle_assoc_comp_left_inv (X Y : C) : (X ◁ (λ_ Y).inv) ≫ (α_ X (𝟙_ C) Y).inv = (ρ_ X).inv ▷ Y := by
  simp [← cancel_mono ((ρ_ X).hom ▷ Y)]

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