hom_inv_whiskerRight' — Mathlib

English

For f: X → Y isomorphism and Z, f.hom ▷ Z ≫ inv f ▷ Z = 𝟙 (X ⊗ Z).

Русский

Для f: X → Y изоморфизм, и Z: f.hom ▷ Z ≫ inv f ▷ Z = 𝟙 (X ⊗ Z).

LaTeX

$$$ f.hom \\triangleright Z \\circ (\\mathrm{inv} f) \\triangleright Z = 𝟙 (X \\otimes Z) $$$

Lean4

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

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