map_epi — Mathlib

English

If f: W → Y and g: X → Z are epis and W ⨿ X and Y ⨿ Z exist as binary coproducts, then coprod.map f g is an epi.

Русский

Если f,g — эпиморфизмы, то coprod.map f g — эпиморфизм.

LaTeX

$$$\text{If } f,g \text{ are epis } coprod.map f g \text{ is epi}.$$$

Lean4

instance map_epi {C : Type*} [Category C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Epi f] [Epi g] [HasBinaryCoproduct W X]
    [HasBinaryCoproduct Y Z] : Epi (coprod.map f g) :=
  ⟨fun i₁ i₂ h => by
    ext
    · rw [← cancel_epi f]
      simpa using congr_arg (fun f => coprod.inl ≫ f) h
    · rw [← cancel_epi g]
      simpa using congr_arg (fun f => coprod.inr ≫ f) h⟩

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