Documentation

Mathlib.CategoryTheory.Comma.Basic

Comma categories #

A comma category is a construction in category theory, which builds a category out of two functors with a common codomain. Specifically, for functors L : A ⥤ T and R : B ⥤ T, an object in Comma L R is a morphism hom : L.obj left ⟶ R.obj right for some objects left : A and right : B, and a morphism in Comma L R between hom : L.obj left ⟶ R.obj right and hom' : L.obj left' ⟶ R.obj right' is a commutative square

L.obj left  ⟶  L.obj left'
      |               |
  hom |               | hom'
      ↓               ↓
R.obj right ⟶  R.obj right',

where the top and bottom morphism come from morphisms left ⟶ left' and right ⟶ right', respectively.

Main definitions #

References #

Tags #

comma, slice, coslice, over, under, arrow

The objects of the comma category are triples of an object left : A, an object right : B and a morphism hom : L.obj left ⟶ R.obj right.

  • left : A
  • right : B
  • hom : L.obj self.left R.obj self.right
Instances For
    Equations
    theorem CategoryTheory.CommaMorphism.ext {A : Type u₁} :
    ∀ {inst : CategoryTheory.Category.{v₁, u₁} A} {B : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} B} {T : Type u₃} {inst_2 : CategoryTheory.Category.{v₃, u₃} T} {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L R} (x y : CategoryTheory.CommaMorphism X Y), x.left = y.leftx.right = y.rightx = y
    theorem CategoryTheory.CommaMorphism.ext_iff {A : Type u₁} :
    ∀ {inst : CategoryTheory.Category.{v₁, u₁} A} {B : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} B} {T : Type u₃} {inst_2 : CategoryTheory.Category.{v₃, u₃} T} {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L R} (x y : CategoryTheory.CommaMorphism X Y), x = y x.left = y.left x.right = y.right

    A morphism between two objects in the comma category is a commutative square connecting the morphisms coming from the two objects using morphisms in the image of the functors L and R.

    Instances For
      Equations
      theorem CategoryTheory.Comma.hom_ext {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {X : CategoryTheory.Comma L R} {Y : CategoryTheory.Comma L R} (f : X Y) (g : X Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) :
      f = g

      The functor sending an object X in the comma category to X.left.

      Equations
      Instances For

        The functor sending an object X in the comma category to X.right.

        Equations
        Instances For

          We can interpret the commutative square constituting a morphism in the comma category as a natural transformation between the functors fst ⋙ L and snd ⋙ R from the comma category to T, where the components are given by the morphism that constitutes an object of the comma category.

          Equations
          Instances For

            Extract the isomorphism between the left objects from an isomorphism in the comma category.

            Equations
            Instances For

              Extract the isomorphism between the right objects from an isomorphism in the comma category.

              Equations
              Instances For
                @[simp]
                theorem CategoryTheory.Comma.isoMk_hom_left {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T} {R₁ : CategoryTheory.Functor B T} {X : CategoryTheory.Comma L₁ R₁} {Y : CategoryTheory.Comma L₁ R₁} (l : X.left Y.left) (r : X.right Y.right) (h : autoParam (CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom)) _auto✝) :
                (CategoryTheory.Comma.isoMk l r h).hom.left = l.hom
                @[simp]
                theorem CategoryTheory.Comma.isoMk_inv_left {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T} {R₁ : CategoryTheory.Functor B T} {X : CategoryTheory.Comma L₁ R₁} {Y : CategoryTheory.Comma L₁ R₁} (l : X.left Y.left) (r : X.right Y.right) (h : autoParam (CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom)) _auto✝) :
                (CategoryTheory.Comma.isoMk l r h).inv.left = l.inv
                @[simp]
                theorem CategoryTheory.Comma.isoMk_inv_right {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T} {R₁ : CategoryTheory.Functor B T} {X : CategoryTheory.Comma L₁ R₁} {Y : CategoryTheory.Comma L₁ R₁} (l : X.left Y.left) (r : X.right Y.right) (h : autoParam (CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom)) _auto✝) :
                (CategoryTheory.Comma.isoMk l r h).inv.right = r.inv
                @[simp]
                theorem CategoryTheory.Comma.isoMk_hom_right {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T} {R₁ : CategoryTheory.Functor B T} {X : CategoryTheory.Comma L₁ R₁} {Y : CategoryTheory.Comma L₁ R₁} (l : X.left Y.left) (r : X.right Y.right) (h : autoParam (CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom)) _auto✝) :
                (CategoryTheory.Comma.isoMk l r h).hom.right = r.hom
                def CategoryTheory.Comma.isoMk {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T} {R₁ : CategoryTheory.Functor B T} {X : CategoryTheory.Comma L₁ R₁} {Y : CategoryTheory.Comma L₁ R₁} (l : X.left Y.left) (r : X.right Y.right) (h : autoParam (CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom)) _auto✝) :
                X Y

                Construct an isomorphism in the comma category given isomorphisms of the objects whose forward directions give a commutative square.

                Equations
                • CategoryTheory.Comma.isoMk l r h = { hom := { left := l.hom, right := r.hom, w := h }, inv := { left := l.inv, right := r.inv, w := }, hom_inv_id := , inv_hom_id := }
                Instances For
                  @[simp]
                  theorem CategoryTheory.Comma.map_map_right {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u_1} {B' : Type u_2} {T' : Type u_3} [CategoryTheory.Category.{u_4, u_1} A'] [CategoryTheory.Category.{u_5, u_2} B'] [CategoryTheory.Category.{u_6, u_3} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') {X : CategoryTheory.Comma L R} {Y : CategoryTheory.Comma L R} (φ : X Y) :
                  ((CategoryTheory.Comma.map α β).map φ).right = F₂.map φ.right
                  @[simp]
                  theorem CategoryTheory.Comma.map_obj_left {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u_1} {B' : Type u_2} {T' : Type u_3} [CategoryTheory.Category.{u_4, u_1} A'] [CategoryTheory.Category.{u_5, u_2} B'] [CategoryTheory.Category.{u_6, u_3} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') (X : CategoryTheory.Comma L R) :
                  ((CategoryTheory.Comma.map α β).obj X).left = F₁.obj X.left
                  @[simp]
                  theorem CategoryTheory.Comma.map_obj_right {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u_1} {B' : Type u_2} {T' : Type u_3} [CategoryTheory.Category.{u_4, u_1} A'] [CategoryTheory.Category.{u_5, u_2} B'] [CategoryTheory.Category.{u_6, u_3} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') (X : CategoryTheory.Comma L R) :
                  ((CategoryTheory.Comma.map α β).obj X).right = F₂.obj X.right
                  @[simp]
                  theorem CategoryTheory.Comma.map_map_left {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u_1} {B' : Type u_2} {T' : Type u_3} [CategoryTheory.Category.{u_4, u_1} A'] [CategoryTheory.Category.{u_5, u_2} B'] [CategoryTheory.Category.{u_6, u_3} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') {X : CategoryTheory.Comma L R} {Y : CategoryTheory.Comma L R} (φ : X Y) :
                  ((CategoryTheory.Comma.map α β).map φ).left = F₁.map φ.left

                  The functor Comma L R ⥤ Comma L' R' induced by three functors F₁, F₂, F and two natural transformations F₁ ⋙ L' ⟶ L ⋙ F and R ⋙ F ⟶ F₂ ⋙ R'.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    instance CategoryTheory.Comma.faithful_map {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u_1} {B' : Type u_2} {T' : Type u_3} [CategoryTheory.Category.{u_4, u_1} A'] [CategoryTheory.Category.{u_5, u_2} B'] [CategoryTheory.Category.{u_6, u_3} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') [F₁.Faithful] [F₂.Faithful] :
                    (CategoryTheory.Comma.map α β).Faithful
                    Equations
                    • =
                    instance CategoryTheory.Comma.full_map {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u_1} {B' : Type u_2} {T' : Type u_3} [CategoryTheory.Category.{u_5, u_1} A'] [CategoryTheory.Category.{u_6, u_2} B'] [CategoryTheory.Category.{u_4, u_3} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') [F.Faithful] [F₁.Full] [F₂.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] :
                    Equations
                    • =
                    instance CategoryTheory.Comma.essSurj_map {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u_1} {B' : Type u_2} {T' : Type u_3} [CategoryTheory.Category.{u_4, u_1} A'] [CategoryTheory.Category.{u_5, u_2} B'] [CategoryTheory.Category.{u_6, u_3} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') [F₁.EssSurj] [F₂.EssSurj] [F.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] :
                    (CategoryTheory.Comma.map α β).EssSurj
                    Equations
                    • =
                    noncomputable instance CategoryTheory.Comma.isEquivalenceMap {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {A' : Type u_1} {B' : Type u_2} {T' : Type u_3} [CategoryTheory.Category.{u_4, u_1} A'] [CategoryTheory.Category.{u_5, u_2} B'] [CategoryTheory.Category.{u_6, u_3} T'] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'} {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') [F₁.IsEquivalence] [F₂.IsEquivalence] [F.Faithful] [F.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β] :
                    (CategoryTheory.Comma.map α β).IsEquivalence
                    Equations
                    • =

                    A natural transformation L₁ ⟶ L₂ induces a functor Comma L₂ R ⥤ Comma L₁ R.

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

                      The functor Comma L R ⥤ Comma L R induced by the identity natural transformation on L is naturally isomorphic to the identity functor.

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

                        The functor Comma L₁ R ⥤ Comma L₃ R induced by the composition of two natural transformations l : L₁ ⟶ L₂ and l' : L₂ ⟶ L₃ is naturally isomorphic to the composition of the two functors induced by these natural transformations.

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

                          Two equal natural transformations L₁ ⟶ L₂ yield naturally isomorphic functors Comma L₁ R ⥤ Comma L₂ R.

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

                            A natural isomorphism L₁ ≅ L₂ induces an equivalence of categories Comma L₁ R ≌ Comma L₂ R.

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

                              A natural transformation R₁ ⟶ R₂ induces a functor Comma L R₁ ⥤ Comma L R₂.

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

                                The functor Comma L R ⥤ Comma L R induced by the identity natural transformation on R is naturally isomorphic to the identity functor.

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

                                  The functor Comma L R₁ ⥤ Comma L R₃ induced by the composition of the natural transformations r : R₁ ⟶ R₂ and r' : R₂ ⟶ R₃ is naturally isomorphic to the composition of the functors induced by these natural transformations.

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

                                    Two equal natural transformations R₁ ⟶ R₂ yield naturally isomorphic functors Comma L R₁ ⥤ Comma L R₂.

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

                                      A natural isomorphism R₁ ≅ R₂ induces an equivalence of categories Comma L R₁ ≌ Comma L R₂.

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

                                        The functor (F ⋙ L, R) ⥤ (L, R)

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

                                          Comma.preLeft is a particular case of Comma.map, but with better definitional properties.

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

                                            If F is an equivalence, then so is preLeft F L R.

                                            Equations
                                            • =

                                            The functor (F ⋙ L, R) ⥤ (L, R)

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

                                              Comma.preRight is a particular case of Comma.map, but with better definitional properties.

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

                                                If F is an equivalence, then so is preRight L F R.

                                                Equations
                                                • =

                                                The functor (L, R) ⥤ (L ⋙ F, R ⋙ F)

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