associativity_inv — Mathlib

English

Describes how δ composes with δ after whiskering on the right, reflecting associativity of δ.

Русский

Описывает компоновку δ с δ после отводки справа, отражая ассоциативность δ.

LaTeX

$$$δ F (X ⊗ Y) Z \\circ δ F X Y \\triangleright F.obj Z = F.map (α_{X Y Z})^{hom} \\circ δ F X (Y ⊗ Z) \\circ F.obj X ◁ δ F Y Z \\circ (α_{F X F Y F Z})^{-1}$$$

Lean4

@[reassoc (attr := simp)]
theorem associativity_inv (X Y Z : C) :
    δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv =
      F.map (α_ X Y Z).inv ≫ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z :=
  by
  rw [← Category.assoc, Iso.comp_inv_eq, Category.assoc, Category.assoc, associativity, ← Category.assoc, ← F.map_comp,
    Iso.inv_hom_id, F.map_id, id_comp]

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