Documentation

Mathlib.CategoryTheory.Over

Over and under categories #

Over (and under) categories are special cases of comma categories.

Tags #

Comma, Slice, Coslice, Over, Under

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

The over category has as objects arrows in T with codomain X and as morphisms commutative triangles.

See https://stacks.math.columbia.edu/tag/001G.

Equations
Instances For
    Equations
    theorem CategoryTheory.Over.OverMorphism.ext {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U : CategoryTheory.Over X} {V : CategoryTheory.Over X} {f : U V} {g : U V} (h : f.left = g.left) :
    f = g
    @[simp]
    theorem CategoryTheory.Over.mk_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} (f : Y X) :
    @[simp]
    theorem CategoryTheory.Over.mk_hom {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} (f : Y X) :

    To give an object in the over category, it suffices to give a morphism with codomain X.

    Equations
    Instances For

      We can set up a coercion from arrows with codomain X to over X. This most likely should not be a global instance, but it is sometimes useful.

      Equations
      • CategoryTheory.Over.coeFromHom = { coe := CategoryTheory.Over.mk }
      Instances For
        @[simp]
        theorem CategoryTheory.Over.coe_hom {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} (f : Y X) :
        @[simp]
        theorem CategoryTheory.Over.homMk_right_down_down {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U : CategoryTheory.Over X} {V : CategoryTheory.Over X} (f : U.left V.left) (w : autoParam (CategoryTheory.CategoryStruct.comp f V.hom = U.hom) _auto✝) :
        (_ : V.right.as = V.right.as) = (_ : V.right.as = V.right.as)

        To give a morphism in the over category, it suffices to give an arrow fitting in a commutative triangle.

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.Over.isoMk_hom_right_down_down {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f : CategoryTheory.Over X} {g : CategoryTheory.Over X} (hl : f.left g.left) (hw : autoParam (CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom) _auto✝) :
          (_ : g.right.as = g.right.as) = (_ : g.right.as = g.right.as)
          @[simp]
          theorem CategoryTheory.Over.isoMk_inv_right_down_down {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f : CategoryTheory.Over X} {g : CategoryTheory.Over X} (hl : f.left g.left) (hw : autoParam (CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom) _auto✝) :
          (_ : f.right.as = f.right.as) = (_ : f.right.as = f.right.as)
          @[simp]
          theorem CategoryTheory.Over.isoMk_inv_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f : CategoryTheory.Over X} {g : CategoryTheory.Over X} (hl : f.left g.left) (hw : autoParam (CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom) _auto✝) :
          (CategoryTheory.Over.isoMk hl).inv.left = hl.inv
          @[simp]
          theorem CategoryTheory.Over.isoMk_hom_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f : CategoryTheory.Over X} {g : CategoryTheory.Over X} (hl : f.left g.left) (hw : autoParam (CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom) _auto✝) :
          (CategoryTheory.Over.isoMk hl).hom.left = hl.hom

          Construct an isomorphism in the over category given isomorphisms of the objects whose forward direction gives a commutative triangle.

          Equations
          Instances For

            The natural cocone over the forgetful functor Over X ⥤ T with cocone point X.

            Equations
            Instances For
              @[simp]
              theorem CategoryTheory.Over.map_obj_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} {f : X Y} {U : CategoryTheory.Over X} :
              ((CategoryTheory.Over.map f).obj U).left = U.left
              @[simp]
              theorem CategoryTheory.Over.map_map_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} {f : X Y} {U : CategoryTheory.Over X} {V : CategoryTheory.Over X} {g : U V} :
              ((CategoryTheory.Over.map f).map g).left = g.left

              Mapping by the identity morphism is just the identity functor.

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

                Mapping by the composite morphism f ≫ g is the same as mapping by f then by g.

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

                  The identity over X is terminal.

                  Equations
                  • CategoryTheory.Over.mkIdTerminal = CategoryTheory.CostructuredArrow.mkIdTerminal
                  Instances For

                    If k.left is an epimorphism, then k is an epimorphism. In other words, Over.forget X reflects epimorphisms. The converse does not hold without additional assumptions on the underlying category, see CategoryTheory.Over.epi_left_of_epi.

                    If k.left is a monomorphism, then k is a monomorphism. In other words, Over.forget X reflects monomorphisms. The converse of CategoryTheory.Over.mono_left_of_mono.

                    This lemma is not an instance, to avoid loops in type class inference.

                    If k is a monomorphism, then k.left is a monomorphism. In other words, Over.forget X preserves monomorphisms. The converse of CategoryTheory.Over.mono_of_mono_left.

                    Equations

                    Given f : Y ⟶ X, this is the obvious functor from (T/X)/f to T/Y

                    Equations
                    Instances For

                      Given f : Y ⟶ X, this is the obvious functor from T/Y to (T/X)/f

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

                        Given f : Y ⟶ X, we have an equivalence between (T/X)/f and T/Y

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

                          A functor F : T ⥤ D induces a functor Over X ⥤ Over (F.obj X) in the obvious way.

                          Equations
                          Instances For

                            Reinterpreting an F-costructured arrow F.obj d ⟶ X as an arrow over X induces a functor CostructuredArrow F X ⥤ Over X.

                            Equations
                            Instances For
                              def CategoryTheory.Under {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] (X : T) :
                              Type (max u₁ v₁)

                              The under category has as objects arrows with domain X and as morphisms commutative triangles.

                              Equations
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                theorem CategoryTheory.Under.UnderMorphism.ext {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U : CategoryTheory.Under X} {V : CategoryTheory.Under X} {f : U V} {g : U V} (h : f.right = g.right) :
                                f = g
                                @[simp]
                                theorem CategoryTheory.Under.mk_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} (f : X Y) :
                                @[simp]
                                theorem CategoryTheory.Under.mk_hom {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} (f : X Y) :

                                To give an object in the under category, it suffices to give an arrow with domain X.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem CategoryTheory.Under.homMk_left_down_down {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {U : CategoryTheory.Under X} {V : CategoryTheory.Under X} (f : U.right V.right) (w : autoParam (CategoryTheory.CategoryStruct.comp U.hom f = V.hom) _auto✝) :
                                  (_ : V.left.as = V.left.as) = (_ : V.left.as = V.left.as)

                                  To give a morphism in the under category, it suffices to give a morphism fitting in a commutative triangle.

                                  Equations
                                  Instances For

                                    Construct an isomorphism in the over category given isomorphisms of the objects whose forward direction gives a commutative triangle.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem CategoryTheory.Under.isoMk_hom_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f : CategoryTheory.Under X} {g : CategoryTheory.Under X} (hr : f.right g.right) (hw : CategoryTheory.CategoryStruct.comp f.hom hr.hom = g.hom) :
                                      (CategoryTheory.Under.isoMk hr).hom.right = hr.hom
                                      @[simp]
                                      theorem CategoryTheory.Under.isoMk_inv_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f : CategoryTheory.Under X} {g : CategoryTheory.Under X} (hr : f.right g.right) (hw : CategoryTheory.CategoryStruct.comp f.hom hr.hom = g.hom) :
                                      (CategoryTheory.Under.isoMk hr).inv.right = hr.inv

                                      The natural cone over the forgetful functor Under X ⥤ T with cone point X.

                                      Equations
                                      Instances For

                                        A morphism X ⟶ Y induces a functor Under Y ⥤ Under X in the obvious way.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem CategoryTheory.Under.map_obj_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} {f : X Y} {U : CategoryTheory.Under Y} :
                                          ((CategoryTheory.Under.map f).obj U).right = U.right
                                          @[simp]
                                          theorem CategoryTheory.Under.map_map_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} {f : X Y} {U : CategoryTheory.Under Y} {V : CategoryTheory.Under Y} {g : U V} :
                                          ((CategoryTheory.Under.map f).map g).right = g.right

                                          Mapping by the identity morphism is just the identity functor.

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

                                            Mapping by the composite morphism f ≫ g is the same as mapping by f then by g.

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

                                              The identity under X is initial.

                                              Equations
                                              • CategoryTheory.Under.mkIdInitial = CategoryTheory.StructuredArrow.mkIdInitial
                                              Instances For

                                                If k.right is a monomorphism, then k is a monomorphism. In other words, Under.forget X reflects epimorphisms. The converse does not hold without additional assumptions on the underlying category, see CategoryTheory.Under.mono_right_of_mono.

                                                If k.right is an epimorphism, then k is an epimorphism. In other words, Under.forget X reflects epimorphisms. The converse of CategoryTheory.Under.epi_right_of_epi.

                                                This lemma is not an instance, to avoid loops in type class inference.

                                                If k is an epimorphism, then k.right is an epimorphism. In other words, Under.forget X preserves epimorphisms. The converse of CategoryTheory.under.epi_of_epi_right.

                                                Equations

                                                A functor F : T ⥤ D induces a functor Under X ⥤ Under (F.obj X) in the obvious way.

                                                Equations
                                                Instances For

                                                  Reinterpreting an F-structured arrow X ⟶ F.obj d as an arrow under X induces a functor StructuredArrow X F ⥤ Under X.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem CategoryTheory.Functor.toOver_map_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [CategoryTheory.Category.{v₂, u₂} S] (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → F.obj Y X) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) :
                                                    ∀ {X Y : S} (g : X Y), ((CategoryTheory.Functor.toOver F X f h).map g).left = F.map g
                                                    @[simp]
                                                    theorem CategoryTheory.Functor.toOver_obj_left {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [CategoryTheory.Category.{v₂, u₂} S] (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → F.obj Y X) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) (Y : S) :
                                                    ((CategoryTheory.Functor.toOver F X f h).obj Y).left = F.obj Y
                                                    def CategoryTheory.Functor.toOver {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [CategoryTheory.Category.{v₂, u₂} S] (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → F.obj Y X) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) :

                                                    Given X : T, to upgrade a functor F : S ⥤ T to a functor S ⥤ Over X, it suffices to provide maps F.obj Y ⟶ X for all Y making the obvious triangles involving all F.map g commute.

                                                    Equations
                                                    Instances For
                                                      def CategoryTheory.Functor.toOverCompForget {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [CategoryTheory.Category.{v₂, u₂} S] (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → F.obj Y X) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) :

                                                      Upgrading a functor S ⥤ T to a functor S ⥤ Over X and composing with the forgetful functor Over X ⥤ T recovers the original functor.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        @[simp]
                                                        theorem CategoryTheory.Functor.toOver_comp_forget {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [CategoryTheory.Category.{v₂, u₂} S] (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → F.obj Y X) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (F.map g) (f Z) = f Y) :
                                                        @[simp]
                                                        theorem CategoryTheory.Functor.toUnder_obj_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [CategoryTheory.Category.{v₂, u₂} S] (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → X F.obj Y) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z) (Y : S) :
                                                        ((CategoryTheory.Functor.toUnder F X f h).obj Y).right = F.obj Y
                                                        @[simp]
                                                        theorem CategoryTheory.Functor.toUnder_map_right {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [CategoryTheory.Category.{v₂, u₂} S] (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → X F.obj Y) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z) :
                                                        ∀ {X Y : S} (g : X Y), ((CategoryTheory.Functor.toUnder F X f h).map g).right = F.map g
                                                        def CategoryTheory.Functor.toUnder {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [CategoryTheory.Category.{v₂, u₂} S] (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → X F.obj Y) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z) :

                                                        Given X : T, to upgrade a functor F : S ⥤ T to a functor S ⥤ Under X, it suffices to provide maps X ⟶ F.obj Y for all Y making the obvious triangles involving all F.map g commute.

                                                        Equations
                                                        Instances For

                                                          Upgrading a functor S ⥤ T to a functor S ⥤ Under X and composing with the forgetful functor Under X ⥤ T recovers the original functor.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            @[simp]
                                                            theorem CategoryTheory.Functor.toUnder_comp_forget {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {S : Type u₂} [CategoryTheory.Category.{v₂, u₂} S] (F : CategoryTheory.Functor S T) (X : T) (f : (Y : S) → X F.obj Y) (h : ∀ {Y Z : S} (g : Y Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map g) = f Z) :