English
Suppose f and g admit a factorization g = g1 ∘ g2 with g1 epi and g2 mono, and f factors through g2; then the fst projection of any pullback along f has mono property.
Русский
Пусть f и g допускают факторизацию g = g1 ∘ g2 с g1 эпиморфизмом и g2 моно, а f факторизуется через g2; тогда fst проекция любого pullback по f моно.
LaTeX
$$$\\\\forall f,g \\\\in \\\\mathrm{Hom}, g = g_1 \\\\circ g_2, [Epi g_1], [Mono g_2], f = g_1 \\\\circ f', t: PullbackCocone f g, \\\\Rightarrow \\\\mathrm{Mono}(t. fst).$$$
Lean4
/-- Suppose `f` and `g` are two morphisms with a common domain and suppose we have written `g` as
an epimorphism followed by a monomorphism. If `f` factors through the epi part of this
factorization, then any pushout of `g` along `f` is a monomorphism. -/
theorem mono_inl_of_factor_thru_epi_mono_factorization (f : X ⟶ Y) (g : X ⟶ Z) (g₁ : X ⟶ W) [Epi g₁] (g₂ : W ⟶ Z)
[Mono g₂] (hg : g₁ ≫ g₂ = g) (f' : W ⟶ Y) (hf : g₁ ≫ f' = f) (t : PushoutCocone f g) (ht : IsColimit t) :
Mono t.inl := by apply mono_inl_of_isColimit _ _ (PushoutCocone.isColimitOfFactors _ _ _ _ _ hf hg t ht)
