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

structure CategoryTheory.Comma {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) :
Type (max u₁ u₂ v₃)

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
    structure CategoryTheory.CommaMorphism {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} (X Y : Comma L R) :
    Type (max v₁ v₂)

    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
      theorem CategoryTheory.CommaMorphism.ext {A : Type u₁} {inst✝ : Category.{v₁, u₁} A} {B : Type u₂} {inst✝¹ : Category.{v₂, u₂} B} {T : Type u₃} {inst✝² : Category.{v₃, u₃} T} {L : Functor A T} {R : Functor B T} {X Y : Comma L R} {x y : CommaMorphism X Y} (left : x.left = y.left) (right : x.right = y.right) :
      x = y
      @[simp]
      theorem CategoryTheory.CommaMorphism.w_assoc {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y : Comma L R} (self : CommaMorphism X Y) {Z : T} (h : R.obj Y.right Z) :
      theorem CategoryTheory.Comma.hom_ext {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y : Comma L R} (f g : X Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) :
      f = g
      @[simp]
      theorem CategoryTheory.Comma.comp_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y Z : Comma L R} {f : X Y} {g : Y Z} :
      @[simp]
      theorem CategoryTheory.Comma.comp_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y Z : Comma L R} {f : X Y} {g : Y Z} :
      def CategoryTheory.Comma.fst {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) :
      Functor (Comma L R) A

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

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.Comma.fst_obj {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L R) :
        (fst L R).obj X = X.left
        @[simp]
        theorem CategoryTheory.Comma.fst_map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) {X✝ Y✝ : Comma L R} (f : X✝ Y✝) :
        (fst L R).map f = f.left
        def CategoryTheory.Comma.snd {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) :
        Functor (Comma L R) B

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

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.Comma.snd_obj {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L R) :
          (snd L R).obj X = X.right
          @[simp]
          theorem CategoryTheory.Comma.snd_map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) {X✝ Y✝ : Comma L R} (f : X✝ Y✝) :
          (snd L R).map f = f.right
          def CategoryTheory.Comma.natTrans {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) :
          (fst L R).comp L (snd L R).comp R

          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.natTrans_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L R) :
            (natTrans L R).app X = X.hom
            @[simp]
            theorem CategoryTheory.Comma.eqToHom_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X Y : Comma L R) (H : X = Y) :
            @[simp]
            theorem CategoryTheory.Comma.eqToHom_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X Y : Comma L R) (H : X = Y) :
            instance CategoryTheory.Comma.instIsIsoLeft {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y : Comma L R} (e : X Y) [IsIso e] :
            instance CategoryTheory.Comma.instIsIsoRight {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y : Comma L R} (e : X Y) [IsIso e] :
            @[simp]
            theorem CategoryTheory.Comma.inv_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y : Comma L R} (e : X Y) [IsIso e] :
            @[simp]
            theorem CategoryTheory.Comma.inv_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L : Functor A T} {R : Functor B T} {X Y : Comma L R} (e : X Y) [IsIso e] :
            def CategoryTheory.Comma.leftIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L₁ : Functor A T} {R₁ : Functor B T} {X Y : Comma L₁ R₁} (α : X Y) :

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

            Equations
            Instances For
              @[simp]
              theorem CategoryTheory.Comma.leftIso_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L₁ : Functor A T} {R₁ : Functor B T} {X Y : Comma L₁ R₁} (α : X Y) :
              @[simp]
              theorem CategoryTheory.Comma.leftIso_inv {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L₁ : Functor A T} {R₁ : Functor B T} {X Y : Comma L₁ R₁} (α : X Y) :
              def CategoryTheory.Comma.rightIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L₁ : Functor A T} {R₁ : Functor B T} {X Y : Comma L₁ R₁} (α : X Y) :

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

              Equations
              Instances For
                @[simp]
                theorem CategoryTheory.Comma.rightIso_inv {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L₁ : Functor A T} {R₁ : Functor B T} {X Y : Comma L₁ R₁} (α : X Y) :
                @[simp]
                theorem CategoryTheory.Comma.rightIso_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L₁ : Functor A T} {R₁ : Functor B T} {X Y : Comma L₁ R₁} (α : X Y) :
                def CategoryTheory.Comma.isoMk {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {L₁ : Functor A T} {R₁ : Functor B T} {X Y : Comma L₁ R₁} (l : X.left Y.left) (r : X.right Y.right) (h : CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryStruct.comp X.hom (R₁.map r.hom) := by aesop_cat) :

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

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

                  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
                    @[simp]
                    theorem CategoryTheory.Comma.map_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') {X Y : Comma L R} (φ : X Y) :
                    ((map α β).map φ).right = F₂.map φ.right
                    @[simp]
                    theorem CategoryTheory.Comma.map_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') (X : Comma L R) :
                    ((map α β).obj X).left = F₁.obj X.left
                    @[simp]
                    theorem CategoryTheory.Comma.map_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') (X : Comma L R) :
                    ((map α β).obj X).right = F₂.obj X.right
                    @[simp]
                    theorem CategoryTheory.Comma.map_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') (X : Comma L R) :
                    @[simp]
                    theorem CategoryTheory.Comma.map_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') {X Y : Comma L R} (φ : X Y) :
                    ((map α β).map φ).left = F₁.map φ.left
                    instance CategoryTheory.Comma.faithful_map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') [F₁.Faithful] [F₂.Faithful] :
                    (map α β).Faithful
                    instance CategoryTheory.Comma.full_map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') [F.Faithful] [F₁.Full] [F₂.Full] [IsIso α] [IsIso β] :
                    (map α β).Full
                    instance CategoryTheory.Comma.essSurj_map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') [F₁.EssSurj] [F₂.EssSurj] [F.Full] [IsIso α] [IsIso β] :
                    (map α β).EssSurj
                    instance CategoryTheory.Comma.isEquivalenceMap {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') [F₁.IsEquivalence] [F₂.IsEquivalence] [F.Faithful] [F.Full] [IsIso α] [IsIso β] :
                    @[simp]
                    theorem CategoryTheory.Comma.map_fst {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') :
                    (map α β).comp (fst L' R') = (fst L R).comp F₁

                    The equality between map α β ⋙ fst L' R' and fst L R ⋙ F₁, where α : F₁ ⋙ L' ⟶ L ⋙ F.

                    def CategoryTheory.Comma.mapFst {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') :
                    (map α β).comp (fst L' R') (fst L R).comp F₁

                    The isomorphism between map α β ⋙ fst L' R' and fst L R ⋙ F₁, where α : F₁ ⋙ L' ⟶ L ⋙ F.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem CategoryTheory.Comma.mapFst_inv_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') (X : Comma L R) :
                      @[simp]
                      theorem CategoryTheory.Comma.mapFst_hom_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') (X : Comma L R) :
                      @[simp]
                      theorem CategoryTheory.Comma.map_snd {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') :
                      (map α β).comp (snd L' R') = (snd L R).comp F₂

                      The equality between map α β ⋙ snd L' R' and snd L R ⋙ F₂, where β : R ⋙ F ⟶ F₂ ⋙ R'.

                      def CategoryTheory.Comma.mapSnd {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') :
                      (map α β).comp (snd L' R') (snd L R).comp F₂

                      The isomorphism between map α β ⋙ snd L' R' and snd L R ⋙ F₂, where β : R ⋙ F ⟶ F₂ ⋙ R'.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem CategoryTheory.Comma.mapSnd_inv_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') (X : Comma L R) :
                        @[simp]
                        theorem CategoryTheory.Comma.mapSnd_hom_app {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {A' : Type u₄} [Category.{v₄, u₄} A'] {B' : Type u₅} [Category.{v₅, u₅} B'] {T' : Type u₆} [Category.{v₆, u₆} T'] {L : Functor A T} {R : Functor B T} {L' : Functor A' T'} {R' : Functor B' T'} {F₁ : Functor A A'} {F₂ : Functor B B'} {F : Functor T T'} (α : F₁.comp L' L.comp F) (β : R.comp F F₂.comp R') (X : Comma L R) :
                        def CategoryTheory.Comma.mapLeft {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l : L₁ L₂) :
                        Functor (Comma L₂ R) (Comma L₁ R)

                        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
                          @[simp]
                          theorem CategoryTheory.Comma.mapLeft_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l : L₁ L₂) (X : Comma L₂ R) :
                          @[simp]
                          theorem CategoryTheory.Comma.mapLeft_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l : L₁ L₂) (X : Comma L₂ R) :
                          ((mapLeft R l).obj X).left = X.left
                          @[simp]
                          theorem CategoryTheory.Comma.mapLeft_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l : L₁ L₂) {X✝ Y✝ : Comma L₂ R} (f : X✝ Y✝) :
                          @[simp]
                          theorem CategoryTheory.Comma.mapLeft_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l : L₁ L₂) (X : Comma L₂ R) :
                          @[simp]
                          theorem CategoryTheory.Comma.mapLeft_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l : L₁ L₂) {X✝ Y✝ : Comma L₂ R} (f : X✝ Y✝) :
                          ((mapLeft R l).map f).left = f.left

                          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
                            def CategoryTheory.Comma.mapLeftComp {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ L₃ : Functor A T} (l : L₁ L₂) (l' : L₂ L₃) :

                            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
                              @[simp]
                              theorem CategoryTheory.Comma.mapLeftComp_hom_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ L₃ : Functor A T} (l : L₁ L₂) (l' : L₂ L₃) (X : Comma L₃ R) :
                              @[simp]
                              theorem CategoryTheory.Comma.mapLeftComp_inv_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ L₃ : Functor A T} (l : L₁ L₂) (l' : L₂ L₃) (X : Comma L₃ R) :
                              @[simp]
                              theorem CategoryTheory.Comma.mapLeftComp_hom_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ L₃ : Functor A T} (l : L₁ L₂) (l' : L₂ L₃) (X : Comma L₃ R) :
                              @[simp]
                              theorem CategoryTheory.Comma.mapLeftComp_inv_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ L₃ : Functor A T} (l : L₁ L₂) (l' : L₂ L₃) (X : Comma L₃ R) :
                              def CategoryTheory.Comma.mapLeftEq {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l l' : L₁ L₂) (h : l = l') :

                              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
                                @[simp]
                                theorem CategoryTheory.Comma.mapLeftEq_inv_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l l' : L₁ L₂) (h : l = l') (X : Comma L₂ R) :
                                @[simp]
                                theorem CategoryTheory.Comma.mapLeftEq_inv_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l l' : L₁ L₂) (h : l = l') (X : Comma L₂ R) :
                                @[simp]
                                theorem CategoryTheory.Comma.mapLeftEq_hom_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l l' : L₁ L₂) (h : l = l') (X : Comma L₂ R) :
                                @[simp]
                                theorem CategoryTheory.Comma.mapLeftEq_hom_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (l l' : L₁ L₂) (h : l = l') (X : Comma L₂ R) :
                                def CategoryTheory.Comma.mapLeftIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ L₂) :
                                Comma L₁ R Comma L₂ R

                                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
                                  @[simp]
                                  theorem CategoryTheory.Comma.mapLeftIso_inverse_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ L₂) {X✝ Y✝ : Comma L₂ R} (f : X✝ Y✝) :
                                  @[simp]
                                  theorem CategoryTheory.Comma.mapLeftIso_inverse_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ L₂) (X : Comma L₂ R) :
                                  @[simp]
                                  theorem CategoryTheory.Comma.mapLeftIso_inverse_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ L₂) (X : Comma L₂ R) :
                                  @[simp]
                                  theorem CategoryTheory.Comma.mapLeftIso_functor_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ L₂) (X : Comma L₁ R) :
                                  @[simp]
                                  theorem CategoryTheory.Comma.mapLeftIso_functor_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ L₂) (X : Comma L₁ R) :
                                  @[simp]
                                  theorem CategoryTheory.Comma.mapLeftIso_functor_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ L₂) {X✝ Y✝ : Comma L₁ R} (f : X✝ Y✝) :
                                  @[simp]
                                  theorem CategoryTheory.Comma.mapLeftIso_inverse_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ L₂) {X✝ Y✝ : Comma L₂ R} (f : X✝ Y✝) :
                                  @[simp]
                                  @[simp]
                                  @[simp]
                                  theorem CategoryTheory.Comma.mapLeftIso_inverse_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ L₂) (X : Comma L₂ R) :
                                  @[simp]
                                  theorem CategoryTheory.Comma.mapLeftIso_functor_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ L₂) (X : Comma L₁ R) :
                                  @[simp]
                                  theorem CategoryTheory.Comma.mapLeftIso_functor_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (R : Functor B T) {L₁ L₂ : Functor A T} (i : L₁ L₂) {X✝ Y✝ : Comma L₁ R} (f : X✝ Y✝) :
                                  def CategoryTheory.Comma.mapRight {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r : R₁ R₂) :
                                  Functor (Comma L R₁) (Comma L R₂)

                                  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
                                    @[simp]
                                    theorem CategoryTheory.Comma.mapRight_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r : R₁ R₂) {X✝ Y✝ : Comma L R₁} (f : X✝ Y✝) :
                                    @[simp]
                                    theorem CategoryTheory.Comma.mapRight_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r : R₁ R₂) (X : Comma L R₁) :
                                    @[simp]
                                    theorem CategoryTheory.Comma.mapRight_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r : R₁ R₂) (X : Comma L R₁) :
                                    @[simp]
                                    theorem CategoryTheory.Comma.mapRight_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r : R₁ R₂) {X✝ Y✝ : Comma L R₁} (f : X✝ Y✝) :
                                    @[simp]
                                    theorem CategoryTheory.Comma.mapRight_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r : R₁ R₂) (X : Comma L R₁) :

                                    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
                                      def CategoryTheory.Comma.mapRightComp {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ R₃ : Functor B T} (r : R₁ R₂) (r' : R₂ R₃) :

                                      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
                                        @[simp]
                                        theorem CategoryTheory.Comma.mapRightComp_hom_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ R₃ : Functor B T} (r : R₁ R₂) (r' : R₂ R₃) (X : Comma L R₁) :
                                        @[simp]
                                        theorem CategoryTheory.Comma.mapRightComp_hom_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ R₃ : Functor B T} (r : R₁ R₂) (r' : R₂ R₃) (X : Comma L R₁) :
                                        @[simp]
                                        theorem CategoryTheory.Comma.mapRightComp_inv_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ R₃ : Functor B T} (r : R₁ R₂) (r' : R₂ R₃) (X : Comma L R₁) :
                                        @[simp]
                                        theorem CategoryTheory.Comma.mapRightComp_inv_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ R₃ : Functor B T} (r : R₁ R₂) (r' : R₂ R₃) (X : Comma L R₁) :
                                        def CategoryTheory.Comma.mapRightEq {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r r' : R₁ R₂) (h : r = r') :

                                        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
                                          @[simp]
                                          theorem CategoryTheory.Comma.mapRightEq_hom_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r r' : R₁ R₂) (h : r = r') (X : Comma L R₁) :
                                          @[simp]
                                          theorem CategoryTheory.Comma.mapRightEq_inv_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r r' : R₁ R₂) (h : r = r') (X : Comma L R₁) :
                                          @[simp]
                                          theorem CategoryTheory.Comma.mapRightEq_inv_app_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r r' : R₁ R₂) (h : r = r') (X : Comma L R₁) :
                                          @[simp]
                                          theorem CategoryTheory.Comma.mapRightEq_hom_app_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (r r' : R₁ R₂) (h : r = r') (X : Comma L R₁) :
                                          def CategoryTheory.Comma.mapRightIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ R₂) :
                                          Comma L R₁ Comma L R₂

                                          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
                                            @[simp]
                                            theorem CategoryTheory.Comma.mapRightIso_functor_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ R₂) {X✝ Y✝ : Comma L R₁} (f : X✝ Y✝) :
                                            @[simp]
                                            theorem CategoryTheory.Comma.mapRightIso_inverse_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ R₂) (X : Comma L R₂) :
                                            @[simp]
                                            theorem CategoryTheory.Comma.mapRightIso_inverse_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ R₂) {X✝ Y✝ : Comma L R₂} (f : X✝ Y✝) :
                                            @[simp]
                                            theorem CategoryTheory.Comma.mapRightIso_inverse_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ R₂) (X : Comma L R₂) :
                                            @[simp]
                                            @[simp]
                                            theorem CategoryTheory.Comma.mapRightIso_functor_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ R₂) (X : Comma L R₁) :
                                            @[simp]
                                            theorem CategoryTheory.Comma.mapRightIso_inverse_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ R₂) (X : Comma L R₂) :
                                            @[simp]
                                            @[simp]
                                            theorem CategoryTheory.Comma.mapRightIso_functor_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ R₂) (X : Comma L R₁) :
                                            @[simp]
                                            theorem CategoryTheory.Comma.mapRightIso_inverse_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ R₂) {X✝ Y✝ : Comma L R₂} (f : X✝ Y✝) :
                                            @[simp]
                                            theorem CategoryTheory.Comma.mapRightIso_functor_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ R₂) {X✝ Y✝ : Comma L R₁} (f : X✝ Y✝) :
                                            @[simp]
                                            theorem CategoryTheory.Comma.mapRightIso_functor_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) {R₁ R₂ : Functor B T} (i : R₁ R₂) (X : Comma L R₁) :
                                            def CategoryTheory.Comma.preLeft {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (F : Functor C A) (L : Functor A T) (R : Functor B T) :
                                            Functor (Comma (F.comp L) R) (Comma L R)

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

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              @[simp]
                                              theorem CategoryTheory.Comma.preLeft_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (F : Functor C A) (L : Functor A T) (R : Functor B T) {X✝ Y✝ : Comma (F.comp L) R} (f : X✝ Y✝) :
                                              ((preLeft F L R).map f).right = f.right
                                              @[simp]
                                              theorem CategoryTheory.Comma.preLeft_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (F : Functor C A) (L : Functor A T) (R : Functor B T) {X✝ Y✝ : Comma (F.comp L) R} (f : X✝ Y✝) :
                                              ((preLeft F L R).map f).left = F.map f.left
                                              @[simp]
                                              theorem CategoryTheory.Comma.preLeft_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (F : Functor C A) (L : Functor A T) (R : Functor B T) (X : Comma (F.comp L) R) :
                                              ((preLeft F L R).obj X).right = X.right
                                              @[simp]
                                              theorem CategoryTheory.Comma.preLeft_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (F : Functor C A) (L : Functor A T) (R : Functor B T) (X : Comma (F.comp L) R) :
                                              ((preLeft F L R).obj X).left = F.obj X.left
                                              @[simp]
                                              theorem CategoryTheory.Comma.preLeft_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (F : Functor C A) (L : Functor A T) (R : Functor B T) (X : Comma (F.comp L) R) :
                                              ((preLeft F L R).obj X).hom = X.hom

                                              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
                                                instance CategoryTheory.Comma.instFullCompPreLeft {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (F : Functor C A) (L : Functor A T) (R : Functor B T) [F.Full] :
                                                (preLeft F L R).Full

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

                                                def CategoryTheory.Comma.preRight {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (F : Functor C B) (R : Functor B T) :
                                                Functor (Comma L (F.comp R)) (Comma L R)

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

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[simp]
                                                  theorem CategoryTheory.Comma.preRight_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (F : Functor C B) (R : Functor B T) {X✝ Y✝ : Comma L (F.comp R)} (f : X✝ Y✝) :
                                                  ((preRight L F R).map f).right = F.map f.right
                                                  @[simp]
                                                  theorem CategoryTheory.Comma.preRight_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (F : Functor C B) (R : Functor B T) (X : Comma L (F.comp R)) :
                                                  ((preRight L F R).obj X).right = F.obj X.right
                                                  @[simp]
                                                  theorem CategoryTheory.Comma.preRight_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (F : Functor C B) (R : Functor B T) {X✝ Y✝ : Comma L (F.comp R)} (f : X✝ Y✝) :
                                                  ((preRight L F R).map f).left = f.left
                                                  @[simp]
                                                  theorem CategoryTheory.Comma.preRight_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (F : Functor C B) (R : Functor B T) (X : Comma L (F.comp R)) :
                                                  ((preRight L F R).obj X).hom = X.hom
                                                  @[simp]
                                                  theorem CategoryTheory.Comma.preRight_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (F : Functor C B) (R : Functor B T) (X : Comma L (F.comp R)) :
                                                  ((preRight L F R).obj X).left = X.left

                                                  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
                                                    instance CategoryTheory.Comma.instFullCompPreRight {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (F : Functor C B) (R : Functor B T) [F.Full] :
                                                    (preRight L F R).Full

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

                                                    def CategoryTheory.Comma.post {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) :
                                                    Functor (Comma L R) (Comma (L.comp F) (R.comp F))

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

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[simp]
                                                      theorem CategoryTheory.Comma.post_obj_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) (X : Comma L R) :
                                                      ((post L R F).obj X).left = X.left
                                                      @[simp]
                                                      theorem CategoryTheory.Comma.post_map_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) {X✝ Y✝ : Comma L R} (f : X✝ Y✝) :
                                                      ((post L R F).map f).right = f.right
                                                      @[simp]
                                                      theorem CategoryTheory.Comma.post_obj_right {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) (X : Comma L R) :
                                                      ((post L R F).obj X).right = X.right
                                                      @[simp]
                                                      theorem CategoryTheory.Comma.post_obj_hom {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) (X : Comma L R) :
                                                      ((post L R F).obj X).hom = F.map X.hom
                                                      @[simp]
                                                      theorem CategoryTheory.Comma.post_map_left {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) {X✝ Y✝ : Comma L R} (f : X✝ Y✝) :
                                                      ((post L R F).map f).left = f.left
                                                      def CategoryTheory.Comma.postIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) :

                                                      Comma.post 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
                                                        instance CategoryTheory.Comma.instFaithfulCompPost {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) :
                                                        (post L R F).Faithful
                                                        instance CategoryTheory.Comma.instEssSurjCompPostOfFull {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] {C : Type u₄} [Category.{v₄, u₄} C] (L : Functor A T) (R : Functor B T) (F : Functor T C) [F.Full] :
                                                        (post L R F).EssSurj

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

                                                        The canonical functor from the product of two categories to the comma category of their respective functors into Discrete PUnit.

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

                                                          Taking the comma category of two functors into Discrete PUnit results in something is equivalent to their product.

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

                                                            Taking the comma category of a functor into A ⥤ Discrete PUnit and the identity Discrete PUnit ⥤ Discrete PUnit results in a category equivalent to A.

                                                            Equations
                                                            Instances For

                                                              Taking the comma category of the identity Discrete PUnit ⥤ Discrete PUnit and a functor B ⥤ Discrete PUnit results in a category equivalent to B.

                                                              Equations
                                                              Instances For

                                                                The canonical functor from Comma L R to (Comma R.op L.op)ᵒᵖ.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  @[simp]
                                                                  theorem CategoryTheory.Comma.opFunctor_obj {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L R) :
                                                                  (opFunctor L R).obj X = Opposite.op { left := Opposite.op X.right, right := Opposite.op X.left, hom := Opposite.op X.hom }
                                                                  @[simp]
                                                                  theorem CategoryTheory.Comma.opFunctor_map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) {X✝ Y✝ : Comma L R} (f : X✝ Y✝) :
                                                                  (opFunctor L R).map f = Opposite.op { left := Opposite.op f.right, right := Opposite.op f.left, w := }

                                                                  Composing the leftOp of opFunctor L R with fst L.op R.op is naturally isomorphic to snd L R.

                                                                  Equations
                                                                  Instances For

                                                                    Composing the leftOp of opFunctor L R with snd L.op R.op is naturally isomorphic to fst L R.

                                                                    Equations
                                                                    Instances For

                                                                      The canonical functor from Comma L.op R.op to (Comma R L)ᵒᵖ.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem CategoryTheory.Comma.unopFunctor_map {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) {X✝ Y✝ : Comma L.op R.op} (f : X✝ Y✝) :
                                                                        (unopFunctor L R).map f = Opposite.op { left := f.right.unop, right := f.left.unop, w := }
                                                                        @[simp]
                                                                        theorem CategoryTheory.Comma.unopFunctor_obj {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) (X : Comma L.op R.op) :
                                                                        (unopFunctor L R).obj X = Opposite.op { left := Opposite.unop X.right, right := Opposite.unop X.left, hom := X.hom.unop }

                                                                        Composing unopFunctor L R with (fst L R).op is isomorphic to snd L.op R.op.

                                                                        Equations
                                                                        Instances For

                                                                          Composing unopFunctor L R with (snd L R).op is isomorphic to fst L.op R.op.

                                                                          Equations
                                                                          Instances For

                                                                            The canonical equivalence between Comma L R and (Comma R.op L.op)ᵒᵖ.

                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              @[simp]
                                                                              theorem CategoryTheory.Comma.opEquiv_unitIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) :
                                                                              (opEquiv L R).unitIso = NatIso.ofComponents (fun (X : Comma L R) => Iso.refl ((Functor.id (Comma L R)).obj X))