map_epi — Mathlib

English

If f: W → Y and g: X → Z are epimorphisms, then biprod.map f g is epi.

Русский

Если f: W → Y и g: X → Z являются эпиморфизмами, то biprod.map f g является эпиморфизмом.

LaTeX

$$$\mathrm{Epi}(\mathrm{biprod.map} f g)$$$

Lean4

instance map_epi {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Epi f] [Epi g] [HasBinaryBiproduct W X]
    [HasBinaryBiproduct Y Z] : Epi (biprod.map f g) :=
  by
  rw [show biprod.map f g = (biprod.isoCoprod _ _).hom ≫ coprod.map f g ≫ (biprod.isoCoprod _ _).inv by aesop]
  infer_instance

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