English
Symmetric variant: if t is a pushout cocone for (f,g) with f epi, then t.inl is epi.
Русский
Симметрично: если t — пушпокойон для (f,g) и f — эпиморфизм, то t.inl эпиморфизм.
LaTeX
$$$(\\forall C, \\forall X,Y,Z, f:X\\to Y, g:X\\to Z)(\\IsColimit\\ t)\\ (\\Epi\\ f)\\Rightarrow \\Epi\\ t.inl$$
Lean4
/-- Suppose `f` and `g` are two morphisms with a common domain and `s` is a colimit cocone over the
diagram formed by `f` and `g`. Suppose `f` and `g` both factor through an epimorphism `h` via
`x` and `y`, respectively. Then `s` is also a colimit cocone over the diagram formed by `x` and
`y`. -/
def isColimitOfFactors (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) [Epi h] (x : W ⟶ Y) (y : W ⟶ Z) (hhx : h ≫ x = f)
(hhy : h ≫ y = g) (s : PushoutCocone f g) (hs : IsColimit s) :
have reassoc₁ : h ≫ x ≫ inl s = f ≫ inl s := by -- Porting note: working around reassoc
rw [← Category.assoc]; apply congrArg (· ≫ inl s) hhx
have reassoc₂ : h ≫ y ≫ inr s = g ≫ inr s := by rw [← Category.assoc]; apply congrArg (· ≫ inr s) hhy
IsColimit
(PushoutCocone.mk _ _
(show x ≫ s.inl = y ≫ s.inr from (cancel_epi h).1 <| by rw [reassoc₁, reassoc₂, s.condition])) :=
PushoutCocone.isColimitAux' _ fun t =>
⟨hs.desc (PushoutCocone.mk t.inl t.inr <| by rw [← hhx, ← hhy, Category.assoc, Category.assoc, t.condition]),
⟨hs.fac _ WalkingSpan.left, hs.fac _ WalkingSpan.right, fun hr hr' =>
by
apply PushoutCocone.IsColimit.hom_ext hs
· simp only [PushoutCocone.mk_inl, PushoutCocone.mk_inr] at hr hr' ⊢
simp only [hr]
symm
exact hs.fac _ WalkingSpan.left
· simp only [PushoutCocone.mk_inl, PushoutCocone.mk_inr] at hr hr' ⊢
simp only [hr']
symm
exact hs.fac _ WalkingSpan.right⟩⟩
