English
Suppose f and g have a common codomain and g factors as a mono after an epi, and f factors through the epi part. Then every pullback of g along f yields an epi on the fst projection.
Русский
Пусть стрелки f и g имеют общую кодоморфизму и g имеет факторизацию через эпиморфизм после моно, а f факторизуется через эпимо-часть. Тогда любой пуллбаκg по f даёт эпиморфизм на fst.
LaTeX
$$$\\\\forall f,g \\\\in \\\\mathrm{Hom}, \\\\forall t: PullbackCone f g, \\\\mathrm{Epi}(t. fst) \\\\text{ under factorization conditions.}$$$
Lean4
/-- Suppose `f` and `g` are two morphisms with a common codomain and suppose we have written `g` as
an epimorphism followed by a monomorphism. If `f` factors through the mono part of this
factorization, then any pullback of `g` along `f` is an epimorphism. -/
theorem epi_fst_of_factor_thru_epi_mono_factorization (g₁ : Y ⟶ W) [Epi g₁] (g₂ : W ⟶ Z) [Mono g₂] (hg : g₁ ≫ g₂ = g)
(f' : X ⟶ W) (hf : f' ≫ g₂ = f) (t : PullbackCone f g) (ht : IsLimit t) : Epi t.fst := by
apply epi_fst_of_isLimit _ _ (PullbackCone.isLimitOfFactors f g g₂ f' g₁ hf hg t ht)
