isIso_coprod — Mathlib

English

If f: W → Y and g: X → Z are epis, and W ⨿ X and Y ⨿ Z exist as binary coproducts, then the map coprod.map f g is an epimorphism; in particular, if f and g are isos, coprod.map f g is an isomorphism.

Русский

Если f и g являются эпиморфизмами, то coprod.map f g является эпиморфизмом; если f,g — изоморфизмы, coprod.map f g — изоморфизм.

LaTeX

$$$\text{If } f: W\to Y, g: X\to Z,\; f,g\;\text{epimorphisms},\; coprod.map f g \;\text{is epi};\;\text{moreover if } f,g\text{ are iso, then } coprod.map f g\cong id.$$$

Lean4

instance isIso_coprod {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) [IsIso f]
    [IsIso g] : IsIso (coprod.map f g) :=
  (coprod.mapIso (asIso f) (asIso g)).isIso_hom

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