Subobjects #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

There is a coercion from subobject X back to the ambient category C (using choice to pick a representative), and for P : subobject X, P.arrow : (P : C) ⟶ X is the inclusion morphism.

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 and prove their basic properties and relationships. These are all easy consequences of the earlier development of the corresponding functors for mono_over.

The subobjects of X form a preorder making them into a category. We have X ≤ Y if and only if X.arrow factors through Y.arrow: see of_le/of_le_mk/of_mk_le/of_mk_le_mk and le_of_comm. Similarly, to show that two subobjects are equal, we can supply an isomorphism between the underlying objects that commutes with the arrows (eq_of_comm).

See also

• category_theory.subobject.factor_thru : an API describing factorization of morphisms through subobjects.
• category_theory.subobject.lattice : the lattice structures on subobjects.

Notes #

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

Implementation note #

Currently we describe pullback, map, etc., as functors. It may be better to just say that they are monotone functions, and even avoid using categorical language entirely when describing subobject X. (It's worth keeping this in mind in future use; it should be a relatively easy change here if it looks preferable.)

Relation to pseudoelements #

There is a separate development of pseudoelements in category_theory.abelian.pseudoelements, as a quotient (but not by isomorphism) of over X.

When a morphism f has an image, the image represents the same pseudoelement. In a category with images pseudoelements X could be constructed as a quotient of mono_over X. In fact, in an abelian category (I'm not sure in what generality beyond that), pseudoelements X agrees with subobject X, but we haven't developed this in mathlib yet.

We now construct the subobject lattice for X : C, as the quotient by isomorphisms of mono_over X.

Since mono_over X is a thin category, we use thin_skeleton to take the quotient.

Essentially all the structure defined above on mono_over X descends to subobject X, with morphisms becoming inequalities, and isomorphisms becoming equations.