Lean4
/-- Let `X : C` be an object in a Grothendieck abelian category,
`F : J ⥤ MonoOver X` a functor from a filtered category, `c` a cocone for
the composition `F ⋙ MonoOver.forget _ : J ⥤ Over X`. We assume
that `c.pt.hom : c.pt.left ⟶ X` is a monomorphism and that the corresponding
subobject of `X` is the supremum of the subobjects given by `(F.obj j).obj.hom`,
then `c` becomes a colimit cocone after the application of
the forget functor `Over X ⥤ C`. (See also `subobjectMk_of_isColimit_eq_iSup`.) -/
noncomputable def isColimitMapCoconeOfSubobjectMkEqISup [IsFiltered J] (c : Cocone (F ⋙ MonoOver.forget _))
[Mono c.pt.hom] (h : Subobject.mk c.pt.hom = ⨆ j, Subobject.mk (F.obj j).obj.hom) :
IsColimit ((Over.forget _).mapCocone c) :=
by
let f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
colimit.desc _
(Cocone.mk X
{ app j := (F.obj j).obj.hom
naturality {j j'} g := by simp [MonoOver.forget] })
haveI := mono_of_isColimit_monoOver F (colimit.isColimit _) f (by simp [f])
have := subobjectMk_of_isColimit_eq_iSup F (colimit.isColimit _) f (by simp [f])
rw [← h] at this
refine IsColimit.ofIsoColimit (colimit.isColimit _) (Cocones.ext (Subobject.isoOfMkEqMk _ _ this) (fun j ↦ ?_))
rw [← cancel_mono (c.pt.hom)]
dsimp
rw [Category.assoc, Subobject.ofMkLEMk_comp, Over.w]
apply colimit.ι_desc
