English
For a non-iso mono p: X ⟶ Y, there exists a larger subobject X' of Y making a pushout of p with a monomorphism from the generating family.
Русский
Для монообразования p: X → Y не изоморфизма существует X' ⊇ X такое, что Inl X → X' вместе с монообразованием из порождающей семьи образуют pushout.
LaTeX
$$$\exists X', i, p' \; (generatingMonomorphisms G).pushouts i \wedge \neg IsIso i \wedge Mono p' \wedge i \cdot p' = p$$$
Lean4
/-- If `p : X ⟶ Y` is a monomorphism that is not an isomorphism, there exists
a subobject `X'` of `Y` containing `X` (but different from `X`) such that
the inclusion `X ⟶ X'` is a pushout of a monomorphism in the family
`generatingMonomorphisms G`. -/
theorem exists_pushouts {X Y : C} (p : X ⟶ Y) [Mono p] (hp : ¬IsIso p) :
∃ (X' : C) (i : X ⟶ X') (p' : X' ⟶ Y) (_ : (generatingMonomorphisms G).pushouts i) (_ : ¬IsIso i) (_ : Mono p'),
i ≫ p' = p :=
by
rw [hG.isDetector.isIso_iff_of_mono] at hp
simp only [coyoneda_obj_obj, coyoneda_obj_map, Set.mem_singleton_iff, forall_eq, Function.Surjective, not_forall,
not_exists] at hp
obtain ⟨f, hf⟩ := hp
refine
⟨pushout (pullback.fst p f) (pullback.snd p f), pushout.inl _ _, pushout.desc p f pullback.condition,
⟨_, _, _, (Subobject.underlyingIso _).hom ≫ pullback.fst _ _, pushout.inr _ _, ⟨Subobject.mk (pullback.snd p f)⟩,
(IsPushout.of_hasPushout (pullback.fst p f) (pullback.snd p f)).of_iso ((Subobject.underlyingIso _).symm)
(Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp) (by simp) (by simp) (by simp)⟩,
?_, ?_, by simp⟩
· intro h
rw [isIso_iff_yoneda_map_bijective] at h
obtain ⟨a, ha⟩ := (h G).2 (pushout.inr _ _)
exact hf a (by simpa using ha =≫ pushout.desc p f pullback.condition)
· exact (IsPushout.of_hasPushout _ _).mono_of_isPullback_of_mono (IsPullback.of_hasPullback p f) _ (by simp) (by simp)
