# Commit 2021-02-23 14:09 f84f5b2e

View on Github →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.