triangle_assoc_comp_right_inv — Mathlib

English

In a monoidal category, the triangle identity for X and Y expresses a relation between the inverse right unitor, the associator, and the inverse left unitor; precisely, (ρ_X)^{-1} whiskered by Y composed with α_{X,I,Y} equals X whiskered with (λ_Y)^{-1}.

Русский

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

LaTeX

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

Lean4

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

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