whiskerLeft_inv_hom — Mathlib

English

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

Русский

Для X и изоморфизма f: Y ≅ Z выполняется X ◁ f.inv ≫ X ◁ f.hom = 𝟙 (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) : X ◁ f.inv ≫ X ◁ f.hom = 𝟙 (X ⊗ Z) := by
  rw [← whiskerLeft_comp, inv_hom_id, whiskerLeft_id]

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