English
In a Grothendieck abelian category, with X as above and F: J ⥤ MonoOver X, the subobject corresponding to the colimit f is the supremum of the subobjects coming from each j, i.e., Subobject.mk f = ⨆ j, Subobject.mk (F.obj j).obj.hom.
Русский
В абелевой категории Гротендикта подмножество, соответствующее колимиту f, является верхней границей подмножеств, порожденных каждого j: Subobject.mk f = ⨆ j, Subobject.mk (F.obj j).obj.hom.
LaTeX
$$$\mathrm{Subobject.mk}(f) = \big \vee_{j \in J} \mathrm{Subobject.mk}((F.obj j).obj.hom)$$$
Lean4
/-- If `C` is a Grothendieck abelian category, `X : C`, if `F : J ⥤ MonoOver X` is a
functor from a filtered category `J`, the colimit of `F` (computed in `C`) gives
a subobject of `F` which is a supremum of the subobjects corresponding to
the objects in the image of the functor `F`. -/
theorem subobjectMk_of_isColimit_eq_iSup :
haveI := mono_of_isColimit_monoOver F hc f hf
Subobject.mk f = ⨆ j, Subobject.mk (F.obj j).obj.hom :=
by
haveI := mono_of_isColimit_monoOver F hc f hf
apply le_antisymm
· rw [le_iSup_iff]
intro s H
induction s using Subobject.ind with
| _ g
let c' : Cocone (F ⋙ MonoOver.forget _ ⋙ Over.forget _) :=
Cocone.mk _
{ app j := Subobject.ofMkLEMk _ _ (H j)
naturality j j'
f := by
dsimp
simpa only [← cancel_mono g, Category.assoc, Subobject.ofMkLEMk_comp, Category.comp_id] using
MonoOver.w (F.map f) }
exact
Subobject.mk_le_mk_of_comm (hc.desc c')
(hc.hom_ext (fun j ↦ by rw [hc.fac_assoc c' j, hf, Subobject.ofMkLEMk_comp]))
· rw [iSup_le_iff]
intro j
exact Subobject.mk_le_mk_of_comm (c.ι.app j) (hf j)
