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 .

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_hom {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {Y : T} (f : Y X) :
    @[simp]
    theorem CategoryTheory.Over.mk_left {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_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
          @[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

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

                                        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
                                            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_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
                                                  @[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
                                                  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_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
                                                      @[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
                                                      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