epimorphisms — Mathlib

English

The class of epimorphisms is stable under cobase change: given a pushout square along an epi, the corresponding right edge is epi.

Русский

Класс эпиморфизмов стабилен по cobase change: в пуш-ауте вдоль эпиморфизма правая стрелка также эпиморфизм.

LaTeX

$$$\forall X,Y,Y',S\ f,g,f',g'\, (\text{IsPushout } g f f' g')\implies (\text{Epi } f)\Rightarrow (\text{Epi } f').$$$

Lean4

instance epimorphisms : (epimorphisms C).IsStableUnderCobaseChange where
  of_isPushout {X Y Y' S f g f' g'} h
    hf := by
    have : Epi f := hf
    constructor
    intro Z f₁ f₂ h₁₂
    apply PushoutCocone.IsColimit.hom_ext h.isColimit
    · exact h₁₂
    · rw [← cancel_epi f]
      dsimp
      simp only [← reassoc_of% h.w, h₁₂]

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