hom_inv_whiskerRight — Mathlib

English

A simp form of whisker_assoc: (X ◁ f) ▷ Z equals the associator relation with X, Y, Y', Z.

Русский

Упрощенная форма whisker_assoc: (X ◁ f) ▷ Z равняется отношению через ассоциатор с X, Y, Y', Z.

LaTeX

$$$ (X \\triangleleft f) \\triangleright Z = (\\alpha_{X Y Z}).hom \\circ (X \\triangleleft f \\triangleright Z) \\circ (\\alpha_{X Y' Z}).inv $$$

Lean4

@[reassoc (attr := simp)]
theorem hom_inv_whiskerRight {X Y : C} (f : X ≅ Y) (Z : C) : f.hom ▷ Z ≫ f.inv ▷ Z = 𝟙 (X ⊗ Z) := by
  rw [← comp_whiskerRight, hom_inv_id, id_whiskerRight]

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