whiskerLeft_inv_hom' — Mathlib

English

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

Русский

Для изоморфизма f: Y ≅ Z и любого X выполняется X ◁ inv f ≫ X ◁ f = 𝟙 (X ⊗ Z).

LaTeX

$$$ X \\triangleleft f^{-1} \\circ X \\triangleleft f = 𝟙 (X \\otimes Z) $$$

Lean4

@[reassoc (attr := simp)]
theorem whiskerLeft_inv_hom' (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] : X ◁ inv f ≫ X ◁ f = 𝟙 (X ⊗ Z) := by
  rw [← whiskerLeft_comp, IsIso.inv_hom_id, whiskerLeft_id]

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