tensor_isIso — Mathlib

English

If f and g are morphisms with f and g isomorphisms, then f ⊗ₘ g is an isomorphism.

Русский

Если f и g являются морфизмами, обратимыми, то их тензор f ⊗ₘ g также является изоморфизмом.

LaTeX

$$$ \text{If } f: W \to X,\ g: Y \to Z \text{ with } IsIso f, IsIso g, \text{ then } IsIso (f \otimes_m g).$$$

Lean4

instance tensor_isIso {W X Y Z : C} (f : W ⟶ X) [IsIso f] (g : Y ⟶ Z) [IsIso g] : IsIso (f ⊗ₘ g) :=
  (asIso f ⊗ᵢ asIso g).isIso_hom

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