whiskerLeft_hom_inv' — Mathlib

English

If f: Y → Z is an isomorphism, then X ◁ f.hom ≫ X ◁ f.inv = 𝟙 (X ⊗ Z).

Русский

Если f: Y → Z — изоморфизм, то X ◁ f.hom ≫ X ◁ f.inv = 𝟙 (X ⊗ Z).

LaTeX

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

Lean4

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

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