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.

Equations
Instances For

    Construct a MonoOver X.

    Equations
    Instances For
      Equations
      @[reducible, inline]

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

      Equations
      Instances For

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

        Equations
        • =
        @[reducible, inline]

        Convenience constructor for a morphism in monomorphisms over X.

        Equations
        Instances For
          def CategoryTheory.MonoOver.isoMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {f : CategoryTheory.MonoOver X} {g : CategoryTheory.MonoOver X} (h : f.obj.left g.obj.left) (w : autoParam (CategoryTheory.CategoryStruct.comp h.hom g.arrow = f.arrow) _auto✝) :
          f g

          Convenience constructor for an isomorphism in monomorphisms over X.

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

            Equations
            Instances For

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                MonoOver.lift commutes with composition of functors.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  MonoOver.lift preserves the identity functor.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def CategoryTheory.MonoOver.slice {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} {f : CategoryTheory.Over A} (h₁ : ∀ (g : CategoryTheory.MonoOver f), CategoryTheory.Mono (f.iteratedSliceEquiv.functor.obj ((CategoryTheory.MonoOver.forget f).obj g)).hom) (h₂ : ∀ (g : CategoryTheory.MonoOver f.left), CategoryTheory.Mono (f.iteratedSliceEquiv.inverse.obj ((CategoryTheory.MonoOver.forget f.left).obj g)).hom) :

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

                    Equations
                    • One or more equations did not get rendered due to their size.
                    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.

                      Equations
                      Instances For

                        pullback commutes with composition (up to a natural isomorphism)

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          pullback preserves the identity (up to a natural isomorphism)

                          Equations
                          Instances For

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

                            Equations
                            Instances For

                              MonoOver.map commutes with composition (up to a natural isomorphism).

                              Equations
                              • One or more equations did not get rendered due to their size.
                              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
                                Equations
                                • =
                                Equations
                                • =

                                Isomorphic objects have equivalent MonoOver categories.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                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.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    map f is left adjoint to pullback f when f is a monomorphism

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

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

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

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

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          Equations

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

                                          Equations
                                          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 MonoOver.map f.

                                            Equations
                                            Instances For

                                              When f : X ⟶ Y is a monomorphism, exists f agrees with map f.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For

                                                exists is adjoint to pullback when images exist

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For