Supremum in `Subobject` as a colimit

Stream: Is there code for X?

[Adam Topaz]

Do we have some API to view supremums in Subobject X (cf. docs#CategoryTheory.Subobject ) as colimits? (dually, infimums as limits.) Well, this requires some additional assumptions on the category and/or the supremum itself.

[Scott Morrison]

Related: https://mathoverflow.net/questions/426901/given-a-hookrightarrow-x-and-b-hookrightarrow-x-with-trivial-intersection

[Adam Topaz]

Thanks! The main case I’m working with is an abelian category satisfying AB5. In this case the supr of a directed subset of subobjects should be the colimit.

[Adam Topaz]

But anyway, it seems that there is essentially no infrastructure in mathlib currently for such assertions

[Adam Topaz]

FWIW, here's what I have so far:

import Mathlib

open CategoryTheory Limits

variable {C : Type u} [Category.{v} C] [HasCoproducts C] [WellPowered C] [HasImages C]
variable {X : C} (E : Set (Subobject X))

@[simps]
noncomputable def diagram : E ⥤ C where
  obj := (·)
  map := (Subobject.ofLE _ _ ·.le)

@[simps]
noncomputable def cocone : Cocone (diagram E) where
  pt := X
  ι := { app := fun ⟨e,_⟩ => e.arrow }

noncomputable
def subobject [HasColimit (diagram E)] [Mono (colimit.desc _ (cocone E))] : Subobject X :=
  .mk (colimit.desc _ (cocone E))

lemma foo [HasColimit (diagram E)] [Mono (colimit.desc _ (cocone E))] :
    subobject E = sSup E := by
  apply le_antisymm
  · fapply Subobject.mk_le_of_comm
    · exact colimit.desc _ ⟨_, fun ⟨e, he⟩ => Subobject.ofLE _ _ (le_sSup he), by aesop_cat⟩
    · ext
      simp
  · apply sSup_le
    intro e he
    fapply Subobject.le_mk_of_comm
    · exact colimit.ι (diagram E) ⟨e,he⟩
    · simp