δ_comp_δ_whiskerRight — Mathlib

English

The naturality of δ with the associator and tensor product is captured by a commutative diagram.

Русский

Естественность δ в отношении ассоциатора и тензорного произведения выражается в диаграмме, которая коммутирует.

LaTeX

$$$δ F X (Y ⊗ Z) \\circ δ F (X ⊗ Y) Z = δ F X Y ∘ δ F (X Y) Z$$$

Lean4

@[reassoc]
theorem δ_comp_δ_whiskerRight (X Y Z : C) :
    δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z =
      F.map (α_ X Y Z).hom ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv :=
  by rw [← associativity_assoc, Iso.hom_inv_id, Category.comp_id]

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