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] :
            (inv e).left = inv e.left
            @[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] :
            theorem CategoryTheory.Comma.left_hom_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] :
            theorem CategoryTheory.Comma.inv_left_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} (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) :
              (leftIso α).hom = α.hom.left
              @[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) :
              (leftIso α).inv = α.inv.left
              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_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.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) :
                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) :
                X Y

                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_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_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_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
                  @[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
                  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_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_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
                    @[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_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
                    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_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) :
                      (mapFst α β).hom.app X = CategoryStruct.id (F₁.obj X.left)
                      @[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) :
                      (mapFst α β).inv.app X = CategoryStruct.id (F₁.obj X.left)
                      @[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) :
                          ((mapLeft R l).obj X).right = X.right
                          @[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✝) :
                          ((mapLeft R l).map f).right = f.right
                          @[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_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_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_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_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_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_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) :
                                @[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_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) :
                                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_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_unitIso_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} (i : L₁ L₂) (X : Comma L₁ R) :
                                  @[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_counitIso_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} (i : L₁ L₂) (X : Comma L₂ R) :
                                  @[simp]
                                  theorem CategoryTheory.Comma.mapLeftIso_unitIso_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} (i : L₁ L₂) (X : Comma L₁ R) :
                                  @[simp]
                                  theorem CategoryTheory.Comma.mapLeftIso_counitIso_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} (i : L₁ L₂) (X : Comma L₂ R) :
                                  @[simp]
                                  theorem CategoryTheory.Comma.mapLeftIso_counitIso_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} (i : L₁ L₂) (X : Comma L₂ R) :
                                  @[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_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_counitIso_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} (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_unitIso_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} (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]
                                  theorem CategoryTheory.Comma.mapLeftIso_unitIso_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} (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✝) :
                                  @[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) :
                                  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✝) :
                                    ((mapRight L r).map f).right = f.right
                                    @[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₁) :
                                    ((mapRight L r).obj X).left = X.left
                                    @[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_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₁) :
                                    ((mapRight L r).obj X).right = X.right
                                    @[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✝) :
                                    ((mapRight L r).map f).left = f.left

                                    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_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₁) :
                                        @[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_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_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₁) :
                                        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_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₁) :
                                          @[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_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₁) :
                                          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_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]
                                            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_counitIso_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} (i : R₁ R₂) (X : Comma L R₂) :
                                            @[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_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_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_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_unitIso_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} (i : R₁ R₂) (X : Comma L R₁) :
                                            @[simp]
                                            theorem CategoryTheory.Comma.mapRightIso_unitIso_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} (i : R₁ R₂) (X : Comma L R₁) :
                                            @[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_counitIso_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} (i : R₁ R₂) (X : Comma L R₂) :
                                            @[simp]
                                            theorem CategoryTheory.Comma.mapRightIso_unitIso_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} (i : R₁ R₂) (X : Comma L R₁) :
                                            @[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_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]
                                            theorem CategoryTheory.Comma.mapRightIso_unitIso_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} (i : R₁ R₂) (X : Comma L R₁) :
                                            @[simp]
                                            theorem CategoryTheory.Comma.mapRightIso_counitIso_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} (i : R₁ R₂) (X : Comma L R₂) :
                                            @[simp]
                                            theorem CategoryTheory.Comma.mapRightIso_counitIso_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} (i : R₁ R₂) (X : Comma L R₂) :
                                            @[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_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_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_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
                                              @[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

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

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

                                                          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_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 := }
                                                                  @[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 }

                                                                  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_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 }
                                                                        @[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 := }

                                                                        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]
                                                                              @[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))
                                                                              @[simp]