Documentation

Mathlib.CategoryTheory.Comma

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

  • left : A
  • right : B
  • hom : L.obj s.left R.obj s.right

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.

Instances For
    Equations
    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
    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

    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
      • One or more equations did not get rendered due to their size.
      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
            @[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).inv.right = r.inv
            @[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).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).inv.left = l.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).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
            Instances For

              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

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

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

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

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