epi_coprod_to_pushout — Mathlib

English

If HasPushout f g and Epi f, then pushout.inr is epi (duplicate).

Русский

Если существует пушпокойон f,g и f эпиморфизм, то pushout.inr эпиморфизм (повтор).

LaTeX

$$$\\operatorname{Epi}(\\mathrm{pushout.inr}\\ f\\ g)$$$

Lean4

/-- The map `X ⨿ Y ⟶ X ⨿[Z] Y` is epi. -/
instance epi_coprod_to_pushout {C : Type*} [Category C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g]
    [HasBinaryCoproduct Y Z] : Epi (coprod.desc (pushout.inl f g) (pushout.inr f g)) :=
  ⟨fun {W} i₁ i₂ h => by
    ext
    · simpa using congrArg (fun f => coprod.inl ≫ f) h
    · simpa using congrArg (fun f => coprod.inr ≫ f) h⟩

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