feat(category_theory/subobject): the semilattice_inf/sup of subobjects (#6278)

The lattice of subobjects

We define subobject X as the quotient (by isomorphisms) of mono_over X := {f : over X // mono f.hom}. Here mono_over X is a thin category (a pair of objects has at most one morphism between them), so we can think of it as a preorder. However as it is not skeletal, it is not a partial order. We provide

• def pullback [has_pullbacks C] (f : X ⟶ Y) : subobject Y ⥤ subobject X
• def map (f : X ⟶ Y) [mono f] : subobject X ⥤ subobject Y
• def «exists» [has_images C] (f : X ⟶ Y) : subobject X ⥤ subobject Y (each first at the level of mono_over), and prove their basic properties and relationships. We also provide the semilattice_inf_top (subobject X) instance when [has_pullback C], and the semilattice_inf (subobject X) instance when [has_images C] [has_finite_coproducts C].

Notes

This development originally appeared in Bhavik Mehta's "Topos theory for Lean" repository, and was ported to mathlib by Scott Morrison.