Documentation

Mathlib.CategoryTheory.Subobject.MonoOver

Monomorphisms over a fixed object #

As preparation for defining Subobject X, we set up the theory for MonoOver X := { f : Over X // Mono f.hom}.

Here MonoOver 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 yet a partial order.

Subobject X will be defined as the skeletalization of MonoOver X.

We provide

Notes #

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

def CategoryTheory.MonoOver {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) :
Type (max u₁ v₁)

The category of monomorphisms into X as a full subcategory of the over category. This isn't skeletal, so it's not a partial order.

Later we define Subobject X as the quotient of this by isomorphisms.

Instances For

    Construct a MonoOver X.

    Instances For

      The inclusion from monomorphisms over X to morphisms over X.

      Instances For
        @[inline, reducible]

        Convenience notation for the underlying arrow of a monomorphism over X.

        Instances For

          The category of monomorphisms over X is a thin category, which makes defining its skeleton easy.

          @[inline, reducible]

          Convenience constructor for a morphism in monomorphisms over X.

          Instances For

            Convenience constructor for an isomorphism in monomorphisms over X.

            Instances For

              If f : MonoOver X, then mk' f.arrow is of course just f, but not definitionally, so we package it as an isomorphism.

              Instances For

                Lift a functor between over categories to a functor between MonoOver categories, given suitable evidence that morphisms are taken to monomorphisms.

                Instances For

                  Isomorphic functors Over Y ⥤ Over X lift to isomorphic functors MonoOver Y ⥤ MonoOver X.

                  Instances For

                    Monomorphisms over an object f : Over A in an over category are equivalent to monomorphisms over the source of f.

                    Instances For

                      When C has pullbacks, a morphism f : X ⟶ Y induces a functor MonoOver Y ⥤ MonoOver X, by pulling back a monomorphism along f.

                      Instances For

                        We can map monomorphisms over X to monomorphisms over Y by post-composition with a monomorphism f : X ⟶ Y.

                        Instances For
                          @[simp]
                          theorem CategoryTheory.MonoOver.map_obj_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X Y) [CategoryTheory.Mono f] (g : CategoryTheory.MonoOver X) :
                          ((CategoryTheory.MonoOver.map f).obj g).obj.left = g.obj.left

                          Isomorphic objects have equivalent MonoOver categories.

                          Instances For

                            An equivalence of categories e between C and D induces an equivalence between MonoOver X and MonoOver (e.functor.obj X) whenever X is an object of C.

                            Instances For

                              The MonoOver Y for the image inclusion for a morphism f : X ⟶ Y.

                              Instances For

                                Taking the image of a morphism gives a functor Over X ⥤ MonoOver X.

                                Instances For

                                  MonoOver.image : Over X ⥤ MonoOver X is left adjoint to MonoOver.forget : MonoOver X ⥤ Over X

                                  Instances For

                                    Forgetting that a monomorphism over X is a monomorphism, then taking its image, is the identity functor.

                                    Instances For

                                      In the case where f is not a monomorphism but C has images, we can still take the "forward map" under it, which agrees with mono_over.map f.

                                      Instances For