English
The pushout along the LE inclusion A ⟶ A' with A' = largerSubobject hG A exists in the generatingMonomorphisms family.
Русский
Pushout вдоль включения A ⟶ A' c largerSubobject hG A существует в семье generatingMonomorphisms.
LaTeX
$$$(generatingMonomorphisms G).pushouts (A.ofLE A' h.le)$$$
Lean4
theorem pushouts_ofLE_le_largerSubobject (A : Subobject X) :
(generatingMonomorphisms G).pushouts (Subobject.ofLE _ _ (le_largerSubobject hG A)) :=
by
by_cases hA : A = ⊤
· subst hA
have := (Subobject.isIso_arrow_iff_eq_top (largerSubobject hG (⊤ : Subobject X))).2 (by simp)
exact
(MorphismProperty.arrow_mk_iso_iff _
(Arrow.isoMk (asIso (Subobject.arrow _)) (asIso (Subobject.arrow _)) (by simp))).2
(isomorphisms_le_pushouts_generatingMonomorphisms G (𝟙 X) (MorphismProperty.isomorphisms.infer_property _))
· refine (MorphismProperty.arrow_mk_iso_iff _ ?_).1 (exists_larger_subobject hG A hA).choose_spec.choose_spec
exact Arrow.isoMk (Iso.refl _) (Subobject.isoOfEq _ _ ((by simp [largerSubobject, dif_neg hA])))
