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].


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

Estimated changes