inv_hom_whiskerRight — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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