Documentation

Mathlib.CategoryTheory.Comma.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) :

        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_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 hw).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 hw).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

              This section proves various equalities between functors that demonstrate, for instance, that over categories assemble into a functor mapFunctor : T ⥤ Cat.

              These equalities between functors are then converted to natural isomorphisms using eqToIso. Such natural isomorphisms could be obtained directly using Iso.refl but this method will have better computational properties, when used, for instance, in developing the theory of Beck-Chevalley transformations.

              Mapping by f and then forgetting is the same as forgetting.

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

              The functor defined by the over categories.

              Equations
              Instances For
                Equations
                • =

                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
                  • =
                  @[simp]
                  theorem CategoryTheory.Over.iteratedSliceForward_obj {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) (α : CategoryTheory.Over f) :
                  f.iteratedSliceForward.obj α = CategoryTheory.Over.mk α.hom.left
                  @[simp]
                  theorem CategoryTheory.Over.iteratedSliceForward_map {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) :
                  ∀ {X_1 Y : CategoryTheory.Over f} (κ : X_1 Y), f.iteratedSliceForward.map κ = CategoryTheory.Over.homMk κ.left.left

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem CategoryTheory.Over.iteratedSliceBackward_map {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) :
                    ∀ {X_1 Y : CategoryTheory.Over f.left} (α : X_1 Y), f.iteratedSliceBackward.map α = CategoryTheory.Over.homMk (CategoryTheory.Over.homMk α.left )

                    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
                      @[simp]
                      theorem CategoryTheory.Over.iteratedSliceEquiv_functor {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) :
                      f.iteratedSliceEquiv.functor = f.iteratedSliceForward
                      @[simp]
                      theorem CategoryTheory.Over.iteratedSliceEquiv_counitIso {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) :
                      f.iteratedSliceEquiv.counitIso = CategoryTheory.NatIso.ofComponents (fun (g : CategoryTheory.Over f.left) => CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl ((f.iteratedSliceBackward.comp f.iteratedSliceForward).obj g).left) )
                      @[simp]
                      theorem CategoryTheory.Over.iteratedSliceEquiv_inverse {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X) :
                      f.iteratedSliceEquiv.inverse = f.iteratedSliceBackward

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

                            An equivalence F induces an equivalence CostructuredArrow F X ≌ Over X.

                            Equations
                            • =
                            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_hom {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} (f : X Y) :
                              @[simp]
                              theorem CategoryTheory.Under.mk_right {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

                                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 hw).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 hw).inv.right = hr.inv

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

                                    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

                                      This section proves various equalities between functors that demonstrate, for instance, that under categories assemble into a functor mapFunctor : Tᵒᵖ ⥤ Cat.

                                      Mapping by f and then forgetting is the same as forgetting.

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

                                      The functor defined by the under categories.

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

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

                                              An equivalence F induces an equivalence StructuredArrow X F ≌ Under X.

                                              Equations
                                              • =
                                              @[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) :
                                              ((F.toOver X f h).obj Y).left = F.obj Y
                                              @[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_1 Y : S} (g : X_1 Y), ((F.toOver X f h).map g).left = F.map g
                                              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) :
                                                (F.toOver X f ).comp (CategoryTheory.Over.forget X) F

                                                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
                                                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) :
                                                  (F.toOver X f ).comp (CategoryTheory.Over.forget X) = F
                                                  @[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_1 Y : S} (g : X_1 Y), ((F.toUnder X f h).map g).right = F.map g
                                                  @[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) :
                                                  ((F.toUnder X f h).obj Y).right = F.obj Y
                                                  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
                                                    def CategoryTheory.Functor.toUnderCompForget {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) :
                                                    (F.toUnder X f ).comp (CategoryTheory.Under.forget X) F

                                                    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
                                                    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) :
                                                      (F.toUnder X f ).comp (CategoryTheory.Under.forget X) = F