mathlib3

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

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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>