whiskerLeftIso — Mathlib

English

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

Русский

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

LaTeX

$$$ \\mathrm{inv} f \\triangleright Z \\circ f \\triangleright Z = 𝟙 (Y \\otimes Z) $$$

Lean4

/-- The left whiskering of an isomorphism is an isomorphism. -/
@[simps]
def whiskerLeftIso (X : C) {Y Z : C} (f : Y ≅ Z) : X ⊗ Y ≅ X ⊗ Z
    where
  hom := X ◁ f.hom
  inv := X ◁ f.inv

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