Mathlib.CategoryTheory.Comma.Basic

CategoryTheory.Comma structure

(L : A ⥤ T) (R : B ⥤ T)

Full source

/-- 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`. -/
structure Comma (L : A ⥤ T) (R : B ⥤ T) : Type max u₁ u₂ v₃ where
  /-- The left subobject -/
  left : A
  /-- The right subobject -/
  right : B
  /-- A morphism from `L.obj left` to `R.obj right` -/
  hom : L.obj left ⟶ R.obj right

Comma Category

Informal description

The comma category $\text{Comma}(L, R)$ for functors $L \colon A \to T$ and $R \colon B \to T$ consists of objects which are triples $(a, b, f)$, where $a$ is an object of $A$, $b$ is an object of $B$, and $f \colon L(a) \to R(b)$ is a morphism in $T$.

CategoryTheory.Comma.inhabited instance

[Inhabited T] : Inhabited (Comma (𝟭 T) (𝟭 T))

Full source

instance Comma.inhabited [Inhabited T] : Inhabited (Comma (𝟭 T) (𝟭 T)) where
  default :=
    { left := default
      right := default
      hom := 𝟙 default }

Inhabitedness of the Comma Category of Identity Functors

Informal description

For any category $T$ that is inhabited (i.e., contains at least one object), the comma category $\text{Comma}(1_T, 1_T)$ is also inhabited, where $1_T$ denotes the identity functor on $T$.

CategoryTheory.CommaMorphism structure

(X Y : Comma L R)

Full source

/-- 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`.
-/
@[ext]
structure CommaMorphism (X Y : Comma L R) where
  /-- Morphism on left objects -/
  left : X.left ⟶ Y.left
  /-- Morphism on right objects -/
  right : X.right ⟶ Y.right
  w : L.map left ≫ Y.hom = X.hom ≫ R.map right := by aesop_cat

Morphism in comma category

Informal description

A morphism in the comma category $\text{Comma}(L, R)$ between objects $X$ and $Y$ is a commutative square connecting the morphisms $f_X \colon L(a_X) \to R(b_X)$ and $f_Y \colon L(a_Y) \to R(b_Y)$ via morphisms $g \colon a_X \to a_Y$ in $A$ and $h \colon b_X \to b_Y$ in $B$, such that the diagram \[ \begin{array}{ccc} L(a_X) & \xrightarrow{L(g)} & L(a_Y) \\ \downarrow{f_X} & & \downarrow{f_Y} \\ R(b_X) & \xrightarrow{R(h)} & R(b_Y) \end{array} \] commutes.

CategoryTheory.CommaMorphism.inhabited instance

[Inhabited (Comma L R)] : Inhabited (CommaMorphism (default : Comma L R) default)

Full source

instance CommaMorphism.inhabited [Inhabited (Comma L R)] :
    Inhabited (CommaMorphism (default : Comma L R) default) :=
    ⟨{ left := 𝟙 _, right := 𝟙 _}⟩

Inhabitedness of Morphisms in Inhabited Comma Categories

Informal description

For any inhabited comma category $\text{Comma}(L, R)$, the type of morphisms between default objects is also inhabited.

CategoryTheory.commaCategory instance

: Category (Comma L R)

Full source

instance commaCategory : Category (Comma L R) where
  Hom X Y := CommaMorphism X Y
  id X :=
    { left := 𝟙 X.left
      right := 𝟙 X.right }
  comp f g :=
    { left := f.left ≫ g.left
      right := f.right ≫ g.right }

The Category Structure on Comma Categories

Informal description

For any functors $L \colon A \to T$ and $R \colon B \to T$, the comma category $\text{Comma}(L, R)$ forms a category where: - Objects are triples $(a, b, f)$ with $a \in A$, $b \in B$, and $f \colon L(a) \to R(b)$ a morphism in $T$. - Morphisms between $(a, b, f)$ and $(a', b', f')$ are pairs $(g, h)$ where $g \colon a \to a'$ in $A$, $h \colon b \to b'$ in $B$, making the square \[ \begin{array}{ccc} L(a) & \xrightarrow{L(g)} & L(a') \\ \downarrow{f} & & \downarrow{f'} \\ R(b) & \xrightarrow{R(h)} & R(b') \end{array} \] commute. - Composition and identities are induced by those in $A$ and $B$.

CategoryTheory.Comma.hom_ext theorem

(f g : X ⟶ Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) : f = g

Full source

@[ext]
lemma hom_ext (f g : X ⟶ Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) : f = g :=
  CommaMorphism.ext h₁ h₂

Extensionality of Morphisms in Comma Categories

Informal description

For any two morphisms $f, g \colon X \to Y$ in the comma category $\text{Comma}(L, R)$, if the left components $f_{\text{left}} = g_{\text{left}}$ and the right components $f_{\text{right}} = g_{\text{right}}$ are equal, then $f = g$.

CategoryTheory.Comma.id_left theorem

: (𝟙 X : CommaMorphism X X).left = 𝟙 X.left

Full source

@[simp]
theorem id_left : (𝟙 X : CommaMorphism X X).left = 𝟙 X.left :=
  rfl

Left Component of Identity in Comma Category is Identity

Informal description

For any object $X$ in the comma category $\text{Comma}(L,R)$, the left component of the identity morphism $\text{id}_X$ is equal to the identity morphism on the left object $X.\text{left}$ in the category $A$.

CategoryTheory.Comma.id_right theorem

: (𝟙 X : CommaMorphism X X).right = 𝟙 X.right

Full source

@[simp]
theorem id_right : (𝟙 X : CommaMorphism X X).right = 𝟙 X.right :=
  rfl

Right Component of Identity Morphism in Comma Category

Informal description

For any object $X$ in a comma category, the right component of the identity morphism $\mathrm{id}_X$ is equal to the identity morphism on the right component of $X$, i.e., $(\mathrm{id}_X)_{\mathrm{right}} = \mathrm{id}_{X_{\mathrm{right}}}$.

CategoryTheory.Comma.comp_left theorem

: (f ≫ g).left = f.left ≫ g.left

Full source

@[simp]
theorem comp_left : (f ≫ g).left = f.left ≫ g.left :=
  rfl

Left Component of Composition in Comma Category

Informal description

For any composable morphisms $f$ and $g$ in the comma category $\text{Comma}(L, R)$, the left component of their composition $(f \circ g).left$ is equal to the composition of their left components $f.left \circ g.left$ in the category $A$.

CategoryTheory.Comma.comp_right theorem

: (f ≫ g).right = f.right ≫ g.right

Full source

@[simp]
theorem comp_right : (f ≫ g).right = f.right ≫ g.right :=
  rfl

Right Component of Composition in Comma Category

Informal description

For any composable morphisms $f$ and $g$ in the comma category $\text{Comma}(L, R)$, the right component of their composition equals the composition of their right components, i.e., $(f \circ g)_{\text{right}} = f_{\text{right}} \circ g_{\text{right}}$.

CategoryTheory.Comma.fst definition

: Comma L R ⥤ A

Full source

/-- The functor sending an object `X` in the comma category to `X.left`. -/
@[simps]
def fst : CommaComma L R ⥤ A where
  obj X := X.left
  map f := f.left

First projection functor from the comma category

Informal description

The functor $\text{fst} \colon \text{Comma}(L, R) \to A$ from the comma category to the category $A$ sends each object $(a, b, f)$ to $a$ and each morphism $(g, h)$ to $g$.

CategoryTheory.Comma.snd definition

: Comma L R ⥤ B

Full source

/-- The functor sending an object `X` in the comma category to `X.right`. -/
@[simps]
def snd : CommaComma L R ⥤ B where
  obj X := X.right
  map f := f.right

Second projection functor from the comma category

Informal description

The functor $\text{snd} \colon \text{Comma}(L, R) \to B$ from the comma category to the category $B$ maps each object $(a, b, f)$ to $b$ and each morphism $(g, h)$ to $h$.

CategoryTheory.Comma.natTrans definition

: fst L R ⋙ L ⟶ snd L R ⋙ R

Full source

/-- 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. -/
@[simps]
def natTrans : fstfst L R ⋙ Lfst L R ⋙ L ⟶ snd L R ⋙ R where app X := X.hom

Natural transformation induced by objects in the comma category

Informal description

The natural transformation $\text{natTrans}$ from the composition of the first projection functor $\text{fst}$ with $L$ to the composition of the second projection functor $\text{snd}$ with $R$ in the comma category $\text{Comma}(L, R)$. For each object $X = (a, b, f)$ in $\text{Comma}(L, R)$, the component $\text{natTrans}_X$ is given by the morphism $f \colon L(a) \to R(b)$ that is part of the data of $X$.

CategoryTheory.Comma.eqToHom_left theorem

(X Y : Comma L R) (H : X = Y) : CommaMorphism.left (eqToHom H) = eqToHom (by cases H; rfl)

Full source

@[simp]
theorem eqToHom_left (X Y : Comma L R) (H : X = Y) :
    CommaMorphism.left (eqToHom H) = eqToHom (by cases H; rfl) := by
  cases H
  rfl

Left Component of Equality Morphism in Comma Category

Informal description

For any objects $X$ and $Y$ in the comma category $\text{Comma}(L, R)$ and an equality $H : X = Y$, the left component of the morphism $\text{eqToHom}(H)$ in $\text{Comma}(L, R)$ is equal to $\text{eqToHom}$ applied to the proof obtained by case analysis on $H$ (which reduces to reflexivity).

CategoryTheory.Comma.eqToHom_right theorem

(X Y : Comma L R) (H : X = Y) : CommaMorphism.right (eqToHom H) = eqToHom (by cases H; rfl)

Full source

@[simp]
theorem eqToHom_right (X Y : Comma L R) (H : X = Y) :
    CommaMorphism.right (eqToHom H) = eqToHom (by cases H; rfl) := by
  cases H
  rfl

Right Component of Equality Morphism in Comma Category

Informal description

For any objects $X$ and $Y$ in the comma category $\text{Comma}(L,R)$, given an equality $H : X = Y$, the right component of the morphism $\text{eqToHom}(H)$ in $\text{Comma}(L,R)$ is equal to $\text{eqToHom}$ applied to the proof that the right objects of $X$ and $Y$ are equal (which follows from $H$ by cases analysis and reflexivity).

CategoryTheory.Comma.instIsIsoLeft instance

[IsIso e] : IsIso e.left

Full source

instance [IsIso e] : IsIso e.left :=
  (Comma.fst L R).map_isIso e

Isomorphism in Comma Category Implies Isomorphism in Left Component

Informal description

For any morphism $e$ in the comma category $\text{Comma}(L, R)$, if $e$ is an isomorphism, then its left component $e.\text{left}$ is also an isomorphism in the category $A$.

CategoryTheory.Comma.instIsIsoRight instance

[IsIso e] : IsIso e.right

Full source

instance [IsIso e] : IsIso e.right :=
  (Comma.snd L R).map_isIso e

Right Component of an Isomorphism in Comma Category is Isomorphism

Informal description

For any morphism $e$ in the comma category $\text{Comma}(L, R)$, if $e$ is an isomorphism, then its right component $e.\text{right}$ is also an isomorphism in the category $B$.

CategoryTheory.Comma.inv_left theorem

[IsIso e] : (inv e).left = inv e.left

Full source

@[simp]
lemma inv_left [IsIso e] : (inv e).left = inv e.left := by
  apply IsIso.eq_inv_of_hom_inv_id
  rw [← Comma.comp_left, IsIso.hom_inv_id, id_left]

Inverse of Left Component in Comma Category

Informal description

For any isomorphism $e$ in the comma category $\text{Comma}(L, R)$, the left component of the inverse morphism $e^{-1}$ is equal to the inverse of the left component of $e$, i.e., $(e^{-1}).\text{left} = (e.\text{left})^{-1}$.

CategoryTheory.Comma.inv_right theorem

[IsIso e] : (inv e).right = inv e.right

Full source

@[simp]
lemma inv_right [IsIso e] : (inv e).right = inv e.right := by
  apply IsIso.eq_inv_of_hom_inv_id
  rw [← Comma.comp_right, IsIso.hom_inv_id, id_right]

Inverse of Right Component in Comma Category

Informal description

For any isomorphism $e$ in the comma category $\text{Comma}(L, R)$, the right component of the inverse morphism $e^{-1}$ is equal to the inverse of the right component of $e$, i.e., $(e^{-1})_{\text{right}} = (e_{\text{right}})^{-1}$.

CategoryTheory.Comma.left_hom_inv_right theorem

[IsIso e] : L.map (e.left) ≫ Y.hom ≫ R.map (inv e.right) = X.hom

Full source

lemma left_hom_inv_right [IsIso e] : L.map (e.left) ≫ Y.hom ≫ R.map (inv e.right) = X.hom := by
  simp

Comma Category Isomorphism Condition: $L(e_{\text{left}}) \circ Y_{\text{hom}} \circ R(e_{\text{right}}^{-1}) = X_{\text{hom}}$

Informal description

Let $L \colon A \to T$ and $R \colon B \to T$ be functors, and let $e \colon X \to Y$ be an isomorphism in the comma category $\text{Comma}(L, R)$. Then the composition \[ L(e.\text{left}) \circ Y.\text{hom} \circ R(e.\text{right}^{-1}) = X.\text{hom}, \] where $e.\text{left} \colon X.\text{left} \to Y.\text{left}$ is the left component of $e$, $e.\text{right}^{-1} \colon Y.\text{right} \to X.\text{right}$ is the inverse of the right component of $e$, and $X.\text{hom} \colon L(X.\text{left}) \to R(X.\text{right})$ and $Y.\text{hom} \colon L(Y.\text{left}) \to R(Y.\text{right})$ are the defining morphisms of $X$ and $Y$ in $\text{Comma}(L, R)$.

CategoryTheory.Comma.inv_left_hom_right theorem

[IsIso e] : L.map (inv e.left) ≫ X.hom ≫ R.map e.right = Y.hom

Full source

lemma inv_left_hom_right [IsIso e] : L.map (inv e.left) ≫ X.hom ≫ R.map e.right = Y.hom := by
  simp

Comma Category Isomorphism Condition: $L(f^{-1}) \circ X.\text{hom} \circ R(g) = Y.\text{hom}$

Informal description

For any isomorphism $e \colon X \to Y$ in the comma category $\text{Comma}(L, R)$, the composition of the following morphisms in $T$ equals the homomorphism of $Y$: \[ L(f^{-1}) \circ X.\text{hom} \circ R(g) = Y.\text{hom}, \] where $f = e.\text{left} \colon X.\text{left} \to Y.\text{left}$ is the left component of $e$, $g = e.\text{right} \colon X.\text{right} \to Y.\text{right}$ is the right component of $e$, and $f^{-1}$ is the inverse of $f$ in $A$.

CategoryTheory.Comma.leftIso definition

{X Y : Comma L₁ R₁} (α : X ≅ Y) : X.left ≅ Y.left

Full source

/-- Extract the isomorphism between the left objects from an isomorphism in the comma category. -/
@[simps!]
def leftIso {X Y : Comma L₁ R₁} (α : X ≅ Y) : X.left ≅ Y.left := (fst L₁ R₁).mapIso α

Isomorphism of left objects in a comma category

Informal description

Given an isomorphism $\alpha \colon X \cong Y$ in the comma category $\text{Comma}(L, R)$, the function extracts the isomorphism between the left objects $X.\text{left}$ and $Y.\text{left}$ in the category $A$, obtained by applying the first projection functor $\text{fst} \colon \text{Comma}(L, R) \to A$ to $\alpha$.

CategoryTheory.Comma.rightIso definition

{X Y : Comma L₁ R₁} (α : X ≅ Y) : X.right ≅ Y.right

Full source

/-- Extract the isomorphism between the right objects from an isomorphism in the comma category. -/
@[simps!]
def rightIso {X Y : Comma L₁ R₁} (α : X ≅ Y) : X.right ≅ Y.right := (snd L₁ R₁).mapIso α

Isomorphism of right objects in a comma category

Informal description

Given an isomorphism $\alpha \colon X \cong Y$ in the comma category $\text{Comma}(L, R)$, the functor $\text{snd} \colon \text{Comma}(L, R) \to B$ maps $\alpha$ to an isomorphism $X.\text{right} \cong Y.\text{right}$ in $B$.

CategoryTheory.Comma.map definition

: Comma L R ⥤ Comma L' R'

Full source

/-- 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'`. -/
@[simps]
def map : CommaComma L R ⥤ Comma L' R' where
  obj X :=
    { left := F₁.obj X.left
      right := F₂.obj X.right
      hom := α.app X.left ≫ F.map X.hom ≫ β.app X.right }
  map {X Y} φ :=
    { left := F₁.map φ.left
      right := F₂.map φ.right
      w := by
        dsimp
        rw [assoc, assoc, ← Functor.comp_map, α.naturality_assoc, ← Functor.comp_map,
          ← β.naturality]
        dsimp
        rw [← F.map_comp_assoc, ← F.map_comp_assoc, φ.w] }

Functor between comma categories induced by natural transformations

Informal description

The functor $\text{Comma}(L, R) \to \text{Comma}(L', R')$ induced by three functors $F_1 \colon A \to A'$, $F_2 \colon B \to B'$, $F \colon T \to T'$ and two natural transformations $\alpha \colon F_1 \circ L' \Rightarrow L \circ F$ and $\beta \colon R \circ F \Rightarrow F_2 \circ R'$. On objects, it maps a comma object $(a, b, f \colon L(a) \to R(b))$ to $(F_1(a), F_2(b), \alpha_a \circ F(f) \circ \beta_b \colon L'(F_1(a)) \to R'(F_2(b)))$. On morphisms, it maps a comma morphism $(g, h)$ to $(F_1(g), F_2(h))$, making the appropriate square commute via the naturality of $\alpha$ and $\beta$.

CategoryTheory.Comma.faithful_map instance

[F₁.Faithful] [F₂.Faithful] : (map α β).Faithful

Full source

instance faithful_map [F₁.Faithful] [F₂.Faithful] : (map α β).Faithful where
  map_injective {X Y} f g h := by
    ext
    · exact F₁.map_injective (congr_arg CommaMorphism.left h)
    · exact F₂.map_injective (congr_arg CommaMorphism.right h)

Faithfulness of Induced Functor on Comma Categories

Informal description

Given functors $F_1 \colon A \to A'$ and $F_2 \colon B \to B'$ that are faithful, the induced functor $\text{Comma}(L, R) \to \text{Comma}(L', R')$ between comma categories is also faithful.

CategoryTheory.Comma.full_map instance

[F.Faithful] [F₁.Full] [F₂.Full] [IsIso α] [IsIso β] : (map α β).Full

Full source

instance full_map [F.Faithful] [F₁.Full] [F₂.Full] [IsIso α] [IsIso β] : (map α β).Full where
  map_surjective {X Y} φ :=
   ⟨{ left := F₁.preimage φ.left
      right := F₂.preimage φ.right
      w := F.map_injective (by
        rw [← cancel_mono (β.app _), ← cancel_epi (α.app _), F.map_comp, F.map_comp,
          assoc, assoc]
        erw [← α.naturality_assoc, β.naturality]
        dsimp
        rw [F₁.map_preimage, F₂.map_preimage]
        simpa using φ.w) }, by aesop_cat⟩

Fullness of the Induced Functor on Comma Categories

Informal description

Given functors $F \colon T \to T'$, $F_1 \colon A \to A'$, and $F_2 \colon B \to B'$, and natural isomorphisms $\alpha \colon F_1 \circ L' \Rightarrow L \circ F$ and $\beta \colon R \circ F \Rightarrow F_2 \circ R'$, if $F$ is faithful, $F_1$ and $F_2$ are full, and $\alpha$ and $\beta$ are natural isomorphisms, then the induced functor $\text{map}(\alpha, \beta) \colon \text{Comma}(L, R) \to \text{Comma}(L', R')$ is full.

CategoryTheory.Comma.essSurj_map instance

[F₁.EssSurj] [F₂.EssSurj] [F.Full] [IsIso α] [IsIso β] : (map α β).EssSurj

Full source

instance essSurj_map [F₁.EssSurj] [F₂.EssSurj] [F.Full] [IsIso α] [IsIso β] :
    (map α β).EssSurj where
  mem_essImage X :=
    ⟨{  left := F₁.objPreimage X.left
        right := F₂.objPreimage X.right
        hom := F.preimage ((inv α).app _ ≫ L'.map (F₁.objObjPreimageIso X.left).hom ≫
          X.hom ≫ R'.map (F₂.objObjPreimageIso X.right).inv ≫ (inv β).app _) },
            ⟨isoMk (F₁.objObjPreimageIso X.left) (F₂.objObjPreimageIso X.right) (by
              dsimp
              simp only [NatIso.isIso_inv_app, Functor.comp_obj, Functor.map_preimage, assoc,
                IsIso.inv_hom_id, comp_id, IsIso.hom_inv_id_assoc]
              rw [← R'.map_comp, Iso.inv_hom_id, R'.map_id, comp_id])⟩⟩

Essential Surjectivity of the Induced Functor on Comma Categories

Informal description

Given functors $F_1 \colon A \to A'$, $F_2 \colon B \to B'$, $F \colon T \to T'$ and natural isomorphisms $\alpha \colon F_1 \circ L' \Rightarrow L \circ F$ and $\beta \colon R \circ F \Rightarrow F_2 \circ R'$, if $F_1$ and $F_2$ are essentially surjective and $F$ is full, then the induced functor $\text{map}(\alpha, \beta) \colon \text{Comma}(L, R) \to \text{Comma}(L', R')$ is essentially surjective.

CategoryTheory.Comma.isEquivalenceMap instance

[F₁.IsEquivalence] [F₂.IsEquivalence] [F.Faithful] [F.Full] [IsIso α] [IsIso β] : (map α β).IsEquivalence

Full source

noncomputable instance isEquivalenceMap
    [F₁.IsEquivalence] [F₂.IsEquivalence] [F.Faithful] [F.Full] [IsIso α] [IsIso β] :
    (map α β).IsEquivalence where

Equivalence of Comma Categories under Equivalence of Base Categories

Informal description

Given functors $F_1 \colon A \to A'$ and $F_2 \colon B \to B'$ that are equivalences of categories, and a functor $F \colon T \to T'$ that is faithful and full, along with natural isomorphisms $\alpha \colon F_1 \circ L' \Rightarrow L \circ F$ and $\beta \colon R \circ F \Rightarrow F_2 \circ R'$, the induced functor $\text{map}(\alpha, \beta) \colon \text{Comma}(L, R) \to \text{Comma}(L', R')$ is an equivalence of categories.

CategoryTheory.Comma.map_fst theorem

: map α β ⋙ fst L' R' = fst L R ⋙ F₁

Full source

/-- The equality between `map α β ⋙ fst L' R'` and `fst L R ⋙ F₁`,
where `α : F₁ ⋙ L' ⟶ L ⋙ F`. -/
@[simp]
theorem map_fst : mapmap α β ⋙ fst L' R' = fstfst L R ⋙ F₁ :=
  rfl

Commutativity of First Projection with Comma Category Mapping Functor

Informal description

Given functors $L \colon A \to T$, $R \colon B \to T$, $L' \colon A' \to T'$, $R' \colon B' \to T'$, and natural transformations $\alpha \colon F_1 \circ L' \Rightarrow L \circ F$ and $\beta \colon R \circ F \Rightarrow F_2 \circ R'$, the composition of the comma category functor $\text{map}(\alpha, \beta) \colon \text{Comma}(L, R) \to \text{Comma}(L', R')$ with the first projection functor $\text{fst}_{L', R'} \colon \text{Comma}(L', R') \to A'$ is equal to the composition of the first projection functor $\text{fst}_{L, R} \colon \text{Comma}(L, R) \to A$ with the functor $F_1 \colon A \to A'$. In other words, the following diagram of functors commutes: \[ \begin{array}{ccc} \text{Comma}(L, R) & \xrightarrow{\text{map}(\alpha, \beta)} & \text{Comma}(L', R') \\ \downarrow{\text{fst}_{L, R}} & & \downarrow{\text{fst}_{L', R'}} \\ A & \xrightarrow{F_1} & A' \end{array} \]

CategoryTheory.Comma.mapFst definition

: map α β ⋙ fst L' R' ≅ fst L R ⋙ F₁

Full source

/-- The isomorphism between `map α β ⋙ fst L' R'` and `fst L R ⋙ F₁`,
where `α : F₁ ⋙ L' ⟶ L ⋙ F`. -/
@[simps!]
def mapFst : mapmap α β ⋙ fst L' R'map α β ⋙ fst L' R' ≅ fst L R ⋙ F₁ :=
  NatIso.ofComponents (fun _ => Iso.refl _) (by simp)

Natural isomorphism between composed projection functors in comma categories

Informal description

The natural isomorphism between the functors $\text{map}(\alpha, \beta) \circ \text{fst}(L', R')$ and $\text{fst}(L, R) \circ F_1$, where $\text{map}(\alpha, \beta)$ is the functor between comma categories induced by natural transformations $\alpha$ and $\beta$, and $\text{fst}$ is the first projection functor from the comma category. At each object, this isomorphism is given by the identity morphism.

CategoryTheory.Comma.map_snd theorem

: map α β ⋙ snd L' R' = snd L R ⋙ F₂

Full source

/-- The equality between `map α β ⋙ snd L' R'` and `snd L R ⋙ F₂`,
where `β : R ⋙ F ⟶ F₂ ⋙ R'`. -/
@[simp]
theorem map_snd : mapmap α β ⋙ snd L' R' = sndsnd L R ⋙ F₂ :=
  rfl

Equality of Functor Compositions: $\text{map}_{\alpha,\beta} \circ \text{snd}_{L', R'} = \text{snd}_{L, R} \circ F_2$

Informal description

Given functors $L \colon A \to T$, $R \colon B \to T$, $L' \colon A' \to T'$, $R' \colon B' \to T'$, $F_1 \colon A \to A'$, $F_2 \colon B \to B'$, $F \colon T \to T'$, and natural transformations $\alpha \colon F_1 \circ L' \Rightarrow L \circ F$ and $\beta \colon R \circ F \Rightarrow F_2 \circ R'$, the composition of the induced functor $\text{map}_{\alpha,\beta} \colon \text{Comma}(L, R) \to \text{Comma}(L', R')$ with the second projection functor $\text{snd}_{L', R'}$ is equal to the composition of the second projection functor $\text{snd}_{L, R}$ with the functor $F_2$. In other words, the following diagram of functors commutes: \[ \text{Comma}(L, R) \xrightarrow{\text{map}_{\alpha,\beta}} \text{Comma}(L', R') \xrightarrow{\text{snd}_{L', R'}} B' = \text{Comma}(L, R) \xrightarrow{\text{snd}_{L, R}} B \xrightarrow{F_2} B' \]

CategoryTheory.Comma.mapSnd definition

: map α β ⋙ snd L' R' ≅ snd L R ⋙ F₂

Full source

/-- The isomorphism between `map α β ⋙ snd L' R'` and `snd L R ⋙ F₂`,
where `β : R ⋙ F ⟶ F₂ ⋙ R'`. -/
@[simps!]
def mapSnd : mapmap α β ⋙ snd L' R'map α β ⋙ snd L' R' ≅ snd L R ⋙ F₂ :=
  NatIso.ofComponents (fun _ => Iso.refl _) (by simp)

Natural isomorphism between second projections in comma categories

Informal description

The natural isomorphism between the functors $\text{map} \alpha \beta \circ \text{snd}_{L', R'}$ and $\text{snd}_{L, R} \circ F_2$, where $\beta \colon R \circ F \Rightarrow F_2 \circ R'$ is a natural transformation. This isomorphism is constructed componentwise using the identity isomorphism on each object.

CategoryTheory.Comma.mapLeft definition

(l : L₁ ⟶ L₂) : Comma L₂ R ⥤ Comma L₁ R

Full source

/-- A natural transformation `L₁ ⟶ L₂` induces a functor `Comma L₂ R ⥤ Comma L₁ R`. -/
@[simps]
def mapLeft (l : L₁ ⟶ L₂) : CommaComma L₂ R ⥤ Comma L₁ R where
  obj X :=
    { left := X.left
      right := X.right
      hom := l.app X.left ≫ X.hom }
  map f :=
    { left := f.left
      right := f.right }

Functor induced by a natural transformation on comma categories

Informal description

Given a natural transformation $l \colon L_1 \to L_2$ between functors $L_1, L_2 \colon A \to T$, the functor $\text{mapLeft} \, R \, l \colon \text{Comma}(L_2, R) \to \text{Comma}(L_1, R)$ is defined as follows: - On objects: For an object $(a, b, f)$ in $\text{Comma}(L_2, R)$, where $a \in A$, $b \in B$, and $f \colon L_2(a) \to R(b)$, the functor maps it to $(a, b, l_a \circ f)$. - On morphisms: For a morphism $(g, h)$ between $(a, b, f)$ and $(a', b', f')$, the functor maps it to $(g, h)$. This functor transforms objects by precomposing the morphism $f$ with the component $l_a$ of the natural transformation $l$ at $a$.

CategoryTheory.Comma.mapLeftId definition

: mapLeft R (𝟙 L) ≅ 𝟭 _

Full source

/-- The functor `Comma L R ⥤ Comma L R` induced by the identity natural transformation on `L` is
    naturally isomorphic to the identity functor. -/
@[simps!]
def mapLeftId : mapLeftmapLeft R (𝟙 L) ≅ 𝟭 _ :=
  NatIso.ofComponents (fun X => isoMk (Iso.refl _) (Iso.refl _))

Natural isomorphism induced by identity transformation on comma categories

Informal description

The identity natural transformation on a functor $L \colon A \to T$ induces a natural isomorphism between the functor $\text{mapLeft} \, R \, (𝟙 L) \colon \text{Comma}(L, R) \to \text{Comma}(L, R)$ and the identity functor on $\text{Comma}(L, R)$. Concretely, for any object $(a, b, f)$ in $\text{Comma}(L, R)$, the isomorphism is given by the pair of identity isomorphisms $(\text{id}_a, \text{id}_b)$ in $A$ and $B$ respectively.

CategoryTheory.Comma.mapLeftComp definition

(l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃) : mapLeft R (l ≫ l') ≅ mapLeft R l' ⋙ mapLeft R l

Full source

/-- 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. -/
@[simps!]
def mapLeftComp (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃) :
    mapLeftmapLeft R (l ≫ l') ≅ mapLeft R l' ⋙ mapLeft R l :=
  NatIso.ofComponents (fun X => isoMk (Iso.refl _) (Iso.refl _))

Natural isomorphism between composition of left-induced functors in comma categories

Informal description

Given natural transformations $l \colon L_1 \to L_2$ and $l' \colon L_2 \to L_3$ between functors $L_1, L_2, L_3 \colon A \to T$, the functor $\text{mapLeft} \, R \, (l \circ l')$ induced by the composition of $l$ and $l'$ is naturally isomorphic to the composition of the functors $\text{mapLeft} \, R \, l'$ and $\text{mapLeft} \, R \, l$.

CategoryTheory.Comma.mapLeftEq definition

(l l' : L₁ ⟶ L₂) (h : l = l') : mapLeft R l ≅ mapLeft R l'

Full source

/-- Two equal natural transformations `L₁ ⟶ L₂` yield naturally isomorphic functors
    `Comma L₁ R ⥤ Comma L₂ R`. -/
@[simps!]
def mapLeftEq (l l' : L₁ ⟶ L₂) (h : l = l') : mapLeftmapLeft R l ≅ mapLeft R l' :=
  NatIso.ofComponents (fun X => isoMk (Iso.refl _) (Iso.refl _))

Natural isomorphism between functors induced by equal natural transformations on comma categories

Informal description

Given two equal natural transformations $ l, l' \colon L_1 \to L_2 $ between functors $ L_1, L_2 \colon A \to T $, the functors $\text{mapLeft} \, R \, l$ and $\text{mapLeft} \, R \, l'$ from $\text{Comma}(L_2, R)$ to $\text{Comma}(L_1, R)$ are naturally isomorphic. This isomorphism is constructed componentwise using identity isomorphisms on the objects of the comma category.

CategoryTheory.Comma.mapLeftIso definition

(i : L₁ ≅ L₂) : Comma L₁ R ≌ Comma L₂ R

Full source

/-- A natural isomorphism `L₁ ≅ L₂` induces an equivalence of categories
    `Comma L₁ R ≌ Comma L₂ R`. -/
@[simps!]
def mapLeftIso (i : L₁ ≅ L₂) : CommaComma L₁ R ≌ Comma L₂ R where
  functor := mapLeft _ i.inv
  inverse := mapLeft _ i.hom
  unitIso := (mapLeftId _ _).symm ≪≫ mapLeftEq _ _ _ i.hom_inv_id.symm ≪≫ mapLeftComp _ _ _
  counitIso := (mapLeftComp _ _ _).symm ≪≫ mapLeftEq _ _ _ i.inv_hom_id ≪≫ mapLeftId _ _

Equivalence of comma categories induced by natural isomorphism of functors

Informal description

Given a natural isomorphism $i \colon L_1 \cong L_2$ between functors $L_1, L_2 \colon A \to T$, there is an equivalence of categories between the comma categories $\text{Comma}(L_1, R)$ and $\text{Comma}(L_2, R)$. The equivalence is constructed as follows: - The forward functor is $\text{mapLeft} \, R \, i^{-1}$ (using the inverse of $i$) - The inverse functor is $\text{mapLeft} \, R \, i$ - The unit and counit natural isomorphisms are built from: - The identity isomorphism $\text{mapLeft} \, R \, \text{id}_{L_1} \cong \text{id}$ - The composition isomorphism $\text{mapLeft} \, R \, (i \circ i^{-1}) \cong \text{mapLeft} \, R \, i \circ \text{mapLeft} \, R \, i^{-1}$ - The equality isomorphism $\text{mapLeft} \, R \, i \cong \text{mapLeft} \, R \, i$ when $i = i$

CategoryTheory.Comma.mapRight definition

(r : R₁ ⟶ R₂) : Comma L R₁ ⥤ Comma L R₂

Full source

/-- A natural transformation `R₁ ⟶ R₂` induces a functor `Comma L R₁ ⥤ Comma L R₂`. -/
@[simps]
def mapRight (r : R₁ ⟶ R₂) : CommaComma L R₁ ⥤ Comma L R₂ where
  obj X :=
    { left := X.left
      right := X.right
      hom := X.hom ≫ r.app X.right }
  map f :=
    { left := f.left
      right := f.right }

Functor induced by natural transformation on comma categories

Informal description

Given a natural transformation $r \colon R_1 \to R_2$ between functors $R_1, R_2 \colon B \to T$, the functor $\text{mapRight}(L, r) \colon \text{Comma}(L, R_1) \to \text{Comma}(L, R_2)$ is defined as follows: - On objects $(a, b, f)$ in $\text{Comma}(L, R_1)$, it maps to $(a, b, f \circ r_b)$, where $r_b \colon R_1(b) \to R_2(b)$ is the component of $r$ at $b$. - On morphisms $(g, h) \colon (a, b, f) \to (a', b', f')$, it maps to $(g, h)$. This functor preserves the structure of the comma category by post-composing the homomorphism with the natural transformation $r$.

CategoryTheory.Comma.mapRightId definition

: mapRight L (𝟙 R) ≅ 𝟭 _

Full source

/-- The functor `Comma L R ⥤ Comma L R` induced by the identity natural transformation on `R` is
    naturally isomorphic to the identity functor. -/
@[simps!]
def mapRightId : mapRightmapRight L (𝟙 R) ≅ 𝟭 _ :=
  NatIso.ofComponents (fun X => isoMk (Iso.refl _) (Iso.refl _))

Natural isomorphism between $\text{mapRight}(L, \text{id}_R)$ and the identity functor

Informal description

The functor $\text{mapRight}(L, \text{id}_R)$ induced by the identity natural transformation on $R$ is naturally isomorphic to the identity functor on the comma category $\text{Comma}(L, R)$. More precisely, for each object $(a, b, f)$ in $\text{Comma}(L, R)$, the isomorphism is given by the pair of identity isomorphisms $(\text{id}_a, \text{id}_b)$ on $a$ and $b$.

CategoryTheory.Comma.mapRightComp definition

(r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃) : mapRight L (r ≫ r') ≅ mapRight L r ⋙ mapRight L r'

Full source

/-- 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. -/
@[simps!]
def mapRightComp (r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃) :
    mapRightmapRight L (r ≫ r') ≅ mapRight L r ⋙ mapRight L r' :=
  NatIso.ofComponents (fun X => isoMk (Iso.refl _) (Iso.refl _))

Natural isomorphism between composed mapRight functors

Informal description

Given functors $L \colon A \to T$, $R_1, R_2, R_3 \colon B \to T$ and natural transformations $r \colon R_1 \to R_2$, $r' \colon R_2 \to R_3$, the functor $\text{mapRight}(L, r \circ r')$ from $\text{Comma}(L, R_1)$ to $\text{Comma}(L, R_3)$ is naturally isomorphic to the composition of the functors $\text{mapRight}(L, r)$ and $\text{mapRight}(L, r')$.

CategoryTheory.Comma.mapRightEq definition

(r r' : R₁ ⟶ R₂) (h : r = r') : mapRight L r ≅ mapRight L r'

Full source

/-- Two equal natural transformations `R₁ ⟶ R₂` yield naturally isomorphic functors
    `Comma L R₁ ⥤ Comma L R₂`. -/
@[simps!]
def mapRightEq (r r' : R₁ ⟶ R₂) (h : r = r') : mapRightmapRight L r ≅ mapRight L r' :=
  NatIso.ofComponents (fun X => isoMk (Iso.refl _) (Iso.refl _))

Natural isomorphism between functors induced by equal natural transformations

Informal description

Given two equal natural transformations $r, r' \colon R_1 \to R_2$ between functors $R_1, R_2 \colon B \to T$, the induced functors $\text{mapRight}(L, r)$ and $\text{mapRight}(L, r')$ from the comma category $\text{Comma}(L, R_1)$ to $\text{Comma}(L, R_2)$ are naturally isomorphic. Specifically, for each object $(a, b, f)$ in $\text{Comma}(L, R_1)$, the isomorphism is given by the identity morphisms on $a$ and $b$, ensuring the naturality condition holds.

CategoryTheory.Comma.mapRightIso definition

(i : R₁ ≅ R₂) : Comma L R₁ ≌ Comma L R₂

Full source

/-- A natural isomorphism `R₁ ≅ R₂` induces an equivalence of categories
    `Comma L R₁ ≌ Comma L R₂`. -/
@[simps!]
def mapRightIso (i : R₁ ≅ R₂) : CommaComma L R₁ ≌ Comma L R₂ where
  functor := mapRight _ i.hom
  inverse := mapRight _ i.inv
  unitIso := (mapRightId _ _).symm ≪≫ mapRightEq _ _ _ i.hom_inv_id.symm ≪≫ mapRightComp _ _ _
  counitIso := (mapRightComp _ _ _).symm ≪≫ mapRightEq _ _ _ i.inv_hom_id ≪≫ mapRightId _ _

Equivalence of comma categories induced by a natural isomorphism

Informal description

Given a natural isomorphism $i \colon R_1 \cong R_2$ between functors $R_1, R_2 \colon B \to T$, there is an equivalence of categories $\text{Comma}(L, R_1) \simeq \text{Comma}(L, R_2)$. The equivalence is constructed as follows: - The forward functor is $\text{mapRight}(L, i_{\text{hom}})$, which applies the natural transformation $i_{\text{hom}} \colon R_1 \to R_2$ to the right component of each object in $\text{Comma}(L, R_1)$. - The inverse functor is $\text{mapRight}(L, i_{\text{inv}})$, which applies the inverse natural transformation $i_{\text{inv}} \colon R_2 \to R_1$. - The unit and counit isomorphisms are built from the identities $\text{mapRight}(L, \text{id}_{R_1}) \cong \text{id}_{\text{Comma}(L, R_1)}$ and $\text{mapRight}(L, \text{id}_{R_2}) \cong \text{id}_{\text{Comma}(L, R_2)}$, and the compositions $\text{mapRight}(L, i_{\text{hom}} \circ i_{\text{inv}}) \cong \text{id}$ and $\text{mapRight}(L, i_{\text{inv}} \circ i_{\text{hom}}) \cong \text{id}$.

CategoryTheory.Comma.preLeft definition

(F : C ⥤ A) (L : A ⥤ T) (R : B ⥤ T) : Comma (F ⋙ L) R ⥤ Comma L R

Full source

/-- The functor `(F ⋙ L, R) ⥤ (L, R)` -/
@[simps]
def preLeft (F : C ⥤ A) (L : A ⥤ T) (R : B ⥤ T) : CommaComma (F ⋙ L) R ⥤ Comma L R where
  obj X :=
    { left := F.obj X.left
      right := X.right
      hom := X.hom }
  map f :=
    { left := F.map f.left
      right := f.right
      w := by simpa using f.w }

Precomposition functor for comma categories

Informal description

The functor $\text{preLeft}(F, L, R)$ maps objects and morphisms from the comma category $\text{Comma}(F \circ L, R)$ to $\text{Comma}(L, R)$ as follows: - For an object $(c, b, f)$ in $\text{Comma}(F \circ L, R)$, where $c$ is an object in $C$, $b$ is an object in $B$, and $f \colon (F \circ L)(c) \to R(b)$ is a morphism in $T$, the functor sends it to $(F(c), b, f)$ in $\text{Comma}(L, R)$. - For a morphism $(g, h)$ between $(c, b, f)$ and $(c', b', f')$ in $\text{Comma}(F \circ L, R)$, where $g \colon c \to c'$ in $C$ and $h \colon b \to b'$ in $B$, the functor sends it to $(F(g), h)$ in $\text{Comma}(L, R)$, ensuring the resulting square commutes.

CategoryTheory.Comma.preLeftIso definition

 (F : C ⥤ A) (L : A ⥤ T) (R : B ⥤ T) :
  preLeft F L R ≅ map (F ⋙ L).rightUnitor.inv (R.rightUnitor.hom ≫ R.leftUnitor.inv)

Full source

/-- `Comma.preLeft` is a particular case of `Comma.map`,
but with better definitional properties. -/
def preLeftIso (F : C ⥤ A) (L : A ⥤ T) (R : B ⥤ T) :
    preLeftpreLeft F L R ≅ map (F ⋙ L).rightUnitor.inv (R.rightUnitor.hom ≫ R.leftUnitor.inv) :=
  NatIso.ofComponents (fun X => isoMk (Iso.refl _) (Iso.refl _))

Natural isomorphism between precomposition and mapping functors for comma categories

Informal description

For functors $F \colon C \to A$, $L \colon A \to T$, and $R \colon B \to T$, there is a natural isomorphism between the functor $\text{preLeft}(F, L, R) \colon \text{Comma}(F \circ L, R) \to \text{Comma}(L, R)$ and the functor $\text{map}((F \circ L).\text{rightUnitor}^{-1}, R.\text{rightUnitor} \circ R.\text{leftUnitor}^{-1})$. This isomorphism is constructed componentwise using identity isomorphisms, meaning that for any object $X$ in $\text{Comma}(F \circ L, R)$, the isomorphism at $X$ is given by identity isomorphisms on the components of $X$.

CategoryTheory.Comma.instFaithfulCompPreLeft instance

(F : C ⥤ A) (L : A ⥤ T) (R : B ⥤ T) [F.Faithful] : (preLeft F L R).Faithful

Full source

instance (F : C ⥤ A) (L : A ⥤ T) (R : B ⥤ T) [F.Faithful] : (preLeft F L R).Faithful :=
  Functor.Faithful.of_iso (preLeftIso F L R).symm

Faithfulness of Precomposition Functor for Comma Categories

Informal description

For any faithful functor $F \colon C \to A$ and functors $L \colon A \to T$, $R \colon B \to T$, the precomposition functor $\text{preLeft}(F, L, R) \colon \text{Comma}(F \circ L, R) \to \text{Comma}(L, R)$ is faithful.

CategoryTheory.Comma.instFullCompPreLeft instance

(F : C ⥤ A) (L : A ⥤ T) (R : B ⥤ T) [F.Full] : (preLeft F L R).Full

Full source

instance (F : C ⥤ A) (L : A ⥤ T) (R : B ⥤ T) [F.Full] : (preLeft F L R).Full :=
  Functor.Full.of_iso (preLeftIso F L R).symm

Fullness of Precomposition Functor for Comma Categories

Informal description

For any functors $F \colon C \to A$, $L \colon A \to T$, and $R \colon B \to T$, if $F$ is a full functor, then the precomposition functor $\text{preLeft}(F, L, R) \colon \text{Comma}(F \circ L, R) \to \text{Comma}(L, R)$ is also full.

CategoryTheory.Comma.instEssSurjCompPreLeft instance

(F : C ⥤ A) (L : A ⥤ T) (R : B ⥤ T) [F.EssSurj] : (preLeft F L R).EssSurj

Full source

instance (F : C ⥤ A) (L : A ⥤ T) (R : B ⥤ T) [F.EssSurj] : (preLeft F L R).EssSurj :=
  Functor.essSurj_of_iso (preLeftIso F L R).symm

Essential Surjectivity of the Precomposition Functor for Comma Categories

Informal description

For any functors $F \colon C \to A$, $L \colon A \to T$, and $R \colon B \to T$, if $F$ is essentially surjective, then the precomposition functor $\text{preLeft}(F, L, R) \colon \text{Comma}(F \circ L, R) \to \text{Comma}(L, R)$ is also essentially surjective.

CategoryTheory.Comma.isEquivalence_preLeft instance

(F : C ⥤ A) (L : A ⥤ T) (R : B ⥤ T) [F.IsEquivalence] : (preLeft F L R).IsEquivalence

Full source

/-- If `F` is an equivalence, then so is `preLeft F L R`. -/
instance isEquivalence_preLeft (F : C ⥤ A) (L : A ⥤ T) (R : B ⥤ T) [F.IsEquivalence] :
    (preLeft F L R).IsEquivalence where

Precomposition Functor Preserves Equivalence for Comma Categories

Informal description

For any equivalence of categories $F \colon C \to A$ and functors $L \colon A \to T$ and $R \colon B \to T$, the precomposition functor $\text{preLeft}(F, L, R) \colon \text{Comma}(F \circ L, R) \to \text{Comma}(L, R)$ is also an equivalence of categories.

CategoryTheory.Comma.preRight definition

(L : A ⥤ T) (F : C ⥤ B) (R : B ⥤ T) : Comma L (F ⋙ R) ⥤ Comma L R

Full source

/-- The functor `(L, F ⋙ R) ⥤ (L, R)` -/
@[simps]
def preRight (L : A ⥤ T) (F : C ⥤ B) (R : B ⥤ T) : CommaComma L (F ⋙ R) ⥤ Comma L R where
  obj X :=
    { left := X.left
      right := F.obj X.right
      hom := X.hom }
  map f :=
    { left := f.left
      right := F.map f.right }

Precomposition Functor for Comma Categories (Right)

Informal description

The functor $\text{preRight}(L, F, R)$ maps objects and morphisms from the comma category $\text{Comma}(L, F \circ R)$ to $\text{Comma}(L, R)$. Specifically: - For an object $(a, c, f)$ in $\text{Comma}(L, F \circ R)$, where $a \in A$, $c \in C$, and $f \colon L(a) \to (F \circ R)(c)$ is a morphism in $T$, the functor sends it to $(a, F(c), f)$ in $\text{Comma}(L, R)$. - For a morphism $(g, h)$ between $(a, c, f)$ and $(a', c', f')$ in $\text{Comma}(L, F \circ R)$, where $g \colon a \to a'$ in $A$ and $h \colon c \to c'$ in $C$, the functor sends it to $(g, F(h))$ in $\text{Comma}(L, R)$.

CategoryTheory.Comma.preRightIso definition

 (L : A ⥤ T) (F : C ⥤ B) (R : B ⥤ T) :
  preRight L F R ≅ map (L.leftUnitor.hom ≫ L.rightUnitor.inv) (F ⋙ R).rightUnitor.hom

Full source

/-- `Comma.preRight` is a particular case of `Comma.map`,
but with better definitional properties. -/
def preRightIso (L : A ⥤ T) (F : C ⥤ B) (R : B ⥤ T) :
    preRightpreRight L F R ≅ map (L.leftUnitor.hom ≫ L.rightUnitor.inv) (F ⋙ R).rightUnitor.hom :=
  NatIso.ofComponents (fun X => isoMk (Iso.refl _) (Iso.refl _))

Natural isomorphism between preRight and map functors for comma categories

Informal description

The natural isomorphism between the functor $\text{preRight}(L, F, R)$ and the composition of $\text{map}$ with certain unitor transformations. Specifically, for functors $L \colon A \to T$, $F \colon C \to B$, and $R \colon B \to T$, the isomorphism is constructed componentwise using identity isomorphisms on the objects of the comma categories.

CategoryTheory.Comma.instFaithfulCompPreRight instance

(L : A ⥤ T) (F : C ⥤ B) (R : B ⥤ T) [F.Faithful] : (preRight L F R).Faithful

Full source

instance (L : A ⥤ T) (F : C ⥤ B) (R : B ⥤ T) [F.Faithful] : (preRight L F R).Faithful :=
  Functor.Faithful.of_iso (preRightIso L F R).symm

Faithfulness of the Precomposition Functor for Comma Categories

Informal description

For any functors $L \colon A \to T$, $F \colon C \to B$, and $R \colon B \to T$, if $F$ is faithful, then the precomposition functor $\text{preRight}(L, F, R) \colon \text{Comma}(L, F \circ R) \to \text{Comma}(L, R)$ is also faithful.

CategoryTheory.Comma.instFullCompPreRight instance

(L : A ⥤ T) (F : C ⥤ B) (R : B ⥤ T) [F.Full] : (preRight L F R).Full

Full source

instance (L : A ⥤ T) (F : C ⥤ B) (R : B ⥤ T) [F.Full] : (preRight L F R).Full :=
  Functor.Full.of_iso (preRightIso L F R).symm

Fullness of the Precomposition Functor for Comma Categories

Informal description

For any functors $L \colon A \to T$, $F \colon C \to B$, and $R \colon B \to T$, if $F$ is full, then the precomposition functor $\text{preRight}(L, F, R) \colon \text{Comma}(L, F \circ R) \to \text{Comma}(L, R)$ is also full.

CategoryTheory.Comma.instEssSurjCompPreRight instance

(L : A ⥤ T) (F : C ⥤ B) (R : B ⥤ T) [F.EssSurj] : (preRight L F R).EssSurj

Full source

instance (L : A ⥤ T) (F : C ⥤ B) (R : B ⥤ T) [F.EssSurj] : (preRight L F R).EssSurj :=
  Functor.essSurj_of_iso (preRightIso L F R).symm

Essential Surjectivity of the Precomposition Functor for Comma Categories

Informal description

For any functors $L \colon A \to T$, $F \colon C \to B$, and $R \colon B \to T$, if $F$ is essentially surjective, then the precomposition functor $\text{preRight}(L, F, R) \colon \text{Comma}(L, F \circ R) \to \text{Comma}(L, R)$ is also essentially surjective.

CategoryTheory.Comma.isEquivalence_preRight instance

(L : A ⥤ T) (F : C ⥤ B) (R : B ⥤ T) [F.IsEquivalence] : (preRight L F R).IsEquivalence

Full source

/-- If `F` is an equivalence, then so is `preRight L F R`. -/
instance isEquivalence_preRight (L : A ⥤ T) (F : C ⥤ B) (R : B ⥤ T) [F.IsEquivalence] :
    (preRight L F R).IsEquivalence where

Precomposition Functor Preserves Equivalence for Comma Categories

Informal description

For any functors $L \colon A \to T$, $F \colon C \to B$, and $R \colon B \to T$, if $F$ is an equivalence of categories, then the precomposition functor $\text{preRight}(L, F, R) \colon \text{Comma}(L, F \circ R) \to \text{Comma}(L, R)$ is also an equivalence of categories.

CategoryTheory.Comma.post definition

(L : A ⥤ T) (R : B ⥤ T) (F : T ⥤ C) : Comma L R ⥤ Comma (L ⋙ F) (R ⋙ F)

Full source

/-- The functor `(L, R) ⥤ (L ⋙ F, R ⋙ F)` -/
@[simps]
def post (L : A ⥤ T) (R : B ⥤ T) (F : T ⥤ C) : CommaComma L R ⥤ Comma (L ⋙ F) (R ⋙ F) where
  obj X :=
    { left := X.left
      right := X.right
      hom := F.map X.hom }
  map f :=
    { left := f.left
      right := f.right
      w := by simp only [Functor.comp_map, ← F.map_comp, f.w] }

Post-composition functor for comma categories

Informal description

Given functors $L \colon A \to T$, $R \colon B \to T$, and $F \colon T \to C$, the functor $\text{post}(L, R, F) \colon \text{Comma}(L, R) \to \text{Comma}(L \circ F, R \circ F)$ maps: - An object $(a, b, f)$ in $\text{Comma}(L, R)$ to $(a, b, F(f))$ in $\text{Comma}(L \circ F, R \circ F)$. - A morphism $(g, h)$ between $(a, b, f)$ and $(a', b', f')$ to $(g, h)$, where the commutativity of the resulting square follows from the functoriality of $F$.

CategoryTheory.Comma.postIso definition

 (L : A ⥤ T) (R : B ⥤ T) (F : T ⥤ C) :
  post L R F ≅ map (F₁ := 𝟭 _) (F₂ := 𝟭 _) (L ⋙ F).leftUnitor.hom (R ⋙ F).leftUnitor.inv

Full source

/-- `Comma.post` is a particular case of `Comma.map`, but with better definitional properties. -/
def postIso (L : A ⥤ T) (R : B ⥤ T) (F : T ⥤ C) :
    postpost L R F ≅ map (F₁ := 𝟭 _) (F₂ := 𝟭 _) (L ⋙ F).leftUnitor.hom (R ⋙ F).leftUnitor.inv :=
  NatIso.ofComponents (fun X => isoMk (Iso.refl _) (Iso.refl _))

Natural isomorphism between post-composition and mapping functors for comma categories

Informal description

For functors $L \colon A \to T$, $R \colon B \to T$, and $F \colon T \to C$, the natural isomorphism $\text{post}(L, R, F) \cong \text{map}(id_A, id_B, (L \circ F).\text{leftUnitor}.\text{hom}, (R \circ F).\text{leftUnitor}.\text{inv})$ is defined componentwise by identity isomorphisms on the objects of the comma category $\text{Comma}(L, R)$. Here, $\text{post}(L, R, F)$ is the post-composition functor that applies $F$ to the morphisms in the comma category, while $\text{map}(id_A, id_B, \cdots)$ constructs a functor using the left unitor natural transformations of the composed functors $L \circ F$ and $R \circ F$.

CategoryTheory.Comma.instFaithfulCompPost instance

(L : A ⥤ T) (R : B ⥤ T) (F : T ⥤ C) : (post L R F).Faithful

Full source

instance (L : A ⥤ T) (R : B ⥤ T) (F : T ⥤ C) : (post L R F).Faithful :=
  Functor.Faithful.of_iso (postIso L R F).symm

Faithfulness of the Post-Composition Functor on Comma Categories

Informal description

For any functors $L \colon A \to T$, $R \colon B \to T$, and $F \colon T \to C$, the post-composition functor $\text{post}(L, R, F) \colon \text{Comma}(L, R) \to \text{Comma}(L \circ F, R \circ F)$ is faithful. This means that it reflects the equality of morphisms in the comma category $\text{Comma}(L, R)$.

CategoryTheory.Comma.instFullCompPostOfFaithful instance

(L : A ⥤ T) (R : B ⥤ T) (F : T ⥤ C) [F.Faithful] : (post L R F).Full

Full source

instance (L : A ⥤ T) (R : B ⥤ T) (F : T ⥤ C) [F.Faithful] : (post L R F).Full :=
  Functor.Full.of_iso (postIso L R F).symm

Fullness of Post-Composition Functor for Comma Categories with Faithful Functor

Informal description

For any faithful functor $F \colon T \to C$ and functors $L \colon A \to T$, $R \colon B \to T$, the post-composition functor $\text{post}(L, R, F) \colon \text{Comma}(L, R) \to \text{Comma}(L \circ F, R \circ F)$ is full. Here, $\text{post}(L, R, F)$ maps an object $(a, b, f \colon L(a) \to R(b))$ to $(a, b, F(f) \colon (L \circ F)(a) \to (R \circ F)(b))$, and a morphism $(g, h)$ to $(g, h)$, where the commutativity of the resulting square follows from the functoriality of $F$.

CategoryTheory.Comma.instEssSurjCompPostOfFull instance

(L : A ⥤ T) (R : B ⥤ T) (F : T ⥤ C) [F.Full] : (post L R F).EssSurj

Full source

instance (L : A ⥤ T) (R : B ⥤ T) (F : T ⥤ C) [F.Full] : (post L R F).EssSurj :=
  Functor.essSurj_of_iso (postIso L R F).symm

Essential Surjectivity of Post-Composition Functor for Comma Categories with Full Functor

Informal description

For any full functor $F \colon T \to C$ and functors $L \colon A \to T$, $R \colon B \to T$, the post-composition functor $\text{post}(L, R, F) \colon \text{Comma}(L, R) \to \text{Comma}(L \circ F, R \circ F)$ is essentially surjective. This means that for every object $(a, b, f')$ in $\text{Comma}(L \circ F, R \circ F)$, there exists an object $(a, b, f)$ in $\text{Comma}(L, R)$ such that $\text{post}(L, R, F)(a, b, f)$ is isomorphic to $(a, b, f')$.

CategoryTheory.Comma.isEquivalence_post instance

(L : A ⥤ T) (R : B ⥤ T) (F : T ⥤ C) [F.IsEquivalence] : (post L R F).IsEquivalence

Full source

/-- If `F` is an equivalence, then so is `post L R F`. -/
instance isEquivalence_post (L : A ⥤ T) (R : B ⥤ T) (F : T ⥤ C) [F.IsEquivalence] :
    (post L R F).IsEquivalence where

Post-Composition Functor Preserves Equivalence for Comma Categories

Informal description

For any functors $L \colon A \to T$ and $R \colon B \to T$, and an equivalence of categories $F \colon T \to C$, the post-composition functor $\text{post}(L, R, F) \colon \text{Comma}(L, R) \to \text{Comma}(L \circ F, R \circ F)$ is also an equivalence of categories.

CategoryTheory.Comma.fromProd definition

(L : A ⥤ Discrete PUnit) (R : B ⥤ Discrete PUnit) : A × B ⥤ Comma L R

Full source

/-- The canonical functor from the product of two categories to the comma category of their
respective functors into `Discrete PUnit`. -/
@[simps]
def fromProd (L : A ⥤ Discrete PUnit) (R : B ⥤ Discrete PUnit) :
    A × BA × B ⥤ Comma L R where
  obj X :=
    { left := X.1
      right := X.2
      hom := Discrete.eqToHom rfl }
  map {X} {Y} f :=
    { left := f.1
      right := f.2 }

Functor from product category to comma category over discrete PUnit

Informal description

Given functors $L \colon A \to \mathrm{Discrete}\, \mathrm{PUnit}$ and $R \colon B \to \mathrm{Discrete}\, \mathrm{PUnit}$, the functor $\mathrm{fromProd}\, L\, R \colon A \times B \to \mathrm{Comma}(L, R)$ maps each object $(X, Y)$ in the product category $A \times B$ to the comma category object $(X, Y, \mathrm{eqToHom}\, \mathrm{rfl})$, where $\mathrm{eqToHom}\, \mathrm{rfl}$ is the identity morphism in the discrete category over $\mathrm{PUnit}$. On morphisms, it maps a pair $(f, g)$ to the morphism $(f, g)$ in the comma category.

CategoryTheory.Comma.equivProd definition

(L : A ⥤ Discrete PUnit) (R : B ⥤ Discrete PUnit) : Comma L R ≌ A × B

Full source

/-- Taking the comma category of two functors into `Discrete PUnit` results in something
is equivalent to their product. -/
@[simps!]
def equivProd (L : A ⥤ Discrete PUnit) (R : B ⥤ Discrete PUnit) :
    CommaComma L R ≌ A × B where
  functor := (fst L R).prod' (snd L R)
  inverse := fromProd L R
  unitIso := Iso.refl _
  counitIso := Iso.refl _

Equivalence between comma category and product category for functors to discrete PUnit

Informal description

Given functors $L \colon A \to \mathrm{Discrete}\, \mathrm{PUnit}$ and $R \colon B \to \mathrm{Discrete}\, \mathrm{PUnit}$, there is an equivalence of categories between the comma category $\mathrm{Comma}(L, R)$ and the product category $A \times B$. The equivalence is given by: - A functor from $\mathrm{Comma}(L, R)$ to $A \times B$ which is the product of the first and second projection functors. - A functor from $A \times B$ to $\mathrm{Comma}(L, R)$ which maps each object $(X, Y)$ to $(X, Y, \mathrm{eqToHom}\, \mathrm{rfl})$, where $\mathrm{eqToHom}\, \mathrm{rfl}$ is the identity morphism in the discrete category over $\mathrm{PUnit}$. - The unit and counit of the equivalence are both identity isomorphisms.

CategoryTheory.Comma.toPUnitIdEquiv definition

(L : A ⥤ Discrete PUnit) (R : Discrete PUnit ⥤ Discrete PUnit) : Comma L R ≌ A

Full source

/-- 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`. -/
@[simps!]
def toPUnitIdEquiv (L : A ⥤ Discrete PUnit) (R : DiscreteDiscrete PUnit ⥤ Discrete PUnit) :
    CommaComma L R ≌ A :=
  (equivProd L _).trans (prod.rightUnitorEquivalence A)

Equivalence between comma category and base category for functors to discrete PUnit

Informal description

Given a functor $L \colon A \to \mathrm{Discrete}\, \mathrm{PUnit}$ and the identity functor $R \colon \mathrm{Discrete}\, \mathrm{PUnit} \to \mathrm{Discrete}\, \mathrm{PUnit}$, there is an equivalence of categories between the comma category $\mathrm{Comma}(L, R)$ and the category $A$. This equivalence is constructed by first establishing an equivalence between $\mathrm{Comma}(L, R)$ and $A \times \mathrm{Discrete}\, \mathrm{PUnit}$ (via `equivProd`), and then composing with the right unitor equivalence that identifies $A \times \mathrm{Discrete}\, \mathrm{PUnit}$ with $A$.

CategoryTheory.Comma.toPUnitIdEquiv_functor_iso theorem

{L : A ⥤ Discrete PUnit} {R : Discrete PUnit ⥤ Discrete PUnit} : (toPUnitIdEquiv L R).functor = fst L R

Full source

@[simp]
theorem toPUnitIdEquiv_functor_iso {L : A ⥤ Discrete PUnit}
    {R : DiscreteDiscrete PUnit ⥤ Discrete PUnit} :
    (toPUnitIdEquiv L R).functor = fst L R :=
  rfl

Equivalence Functor Isomorphism for Comma Category to PUnit

Informal description

For any functor $L \colon A \to \mathrm{Discrete}\, \mathrm{PUnit}$ and the identity functor $R \colon \mathrm{Discrete}\, \mathrm{PUnit} \to \mathrm{Discrete}\, \mathrm{PUnit}$, the functor component of the equivalence $\mathrm{Comma}(L, R) \simeq A$ is equal to the first projection functor $\mathrm{fst} \colon \mathrm{Comma}(L, R) \to A$.

CategoryTheory.Comma.toIdPUnitEquiv definition

(L : Discrete PUnit ⥤ Discrete PUnit) (R : B ⥤ Discrete PUnit) : Comma L R ≌ B

Full source

/-- Taking the comma category of the identity `Discrete PUnit ⥤ Discrete PUnit`
and a functor `B ⥤ Discrete PUnit` results in a category equivalent to `B`. -/
@[simps!]
def toIdPUnitEquiv (L : DiscreteDiscrete PUnit ⥤ Discrete PUnit) (R : B ⥤ Discrete PUnit) :
    CommaComma L R ≌ B :=
  (equivProd _ R).trans (prod.leftUnitorEquivalence B)

Equivalence between comma category and base category for functors from discrete PUnit

Informal description

Given functors $L \colon \mathrm{Discrete}\, \mathrm{PUnit} \to \mathrm{Discrete}\, \mathrm{PUnit}$ and $R \colon B \to \mathrm{Discrete}\, \mathrm{PUnit}$, there is an equivalence of categories between the comma category $\mathrm{Comma}(L, R)$ and $B$. This equivalence is constructed by first establishing an equivalence with the product category $\mathrm{Discrete}\, \mathrm{PUnit} \times B$ (via `equivProd`), and then applying the left unitor equivalence for product categories (which shows $\mathrm{Discrete}\, \mathrm{PUnit} \times B \simeq B$).

CategoryTheory.Comma.toIdPUnitEquiv_functor_iso theorem

{L : Discrete PUnit ⥤ Discrete PUnit} {R : B ⥤ Discrete PUnit} : (toIdPUnitEquiv L R).functor = snd L R

Full source

@[simp]
theorem toIdPUnitEquiv_functor_iso {L : DiscreteDiscrete PUnit ⥤ Discrete PUnit}
    {R : B ⥤ Discrete PUnit} :
    (toIdPUnitEquiv L R).functor = snd L R :=
  rfl

Equivalence Functor as Second Projection in Comma Category with Discrete PUnit

Informal description

For functors $L \colon \mathrm{Discrete}\, \mathrm{PUnit} \to \mathrm{Discrete}\, \mathrm{PUnit}$ and $R \colon B \to \mathrm{Discrete}\, \mathrm{PUnit}$, the functor component of the equivalence $\mathrm{Comma}(L, R) \simeq B$ is equal to the second projection functor $\mathrm{snd} \colon \mathrm{Comma}(L, R) \to B$.

CategoryTheory.Comma.opFunctor definition

: Comma L R ⥤ (Comma R.op L.op)ᵒᵖ

Full source

/-- The canonical functor from `Comma L R` to `(Comma R.op L.op)ᵒᵖ`. -/
@[simps]
def opFunctor : CommaComma L R ⥤ (Comma R.op L.op)ᵒᵖ where
  obj X := ⟨op X.right, op X.left, op X.hom⟩
  map f := ⟨op f.right, op f.left, Quiver.Hom.unop_inj (by simp)⟩

Opposite functor for comma categories

Informal description

The functor from the comma category $\text{Comma}(L, R)$ to the opposite of the comma category $\text{Comma}(R^{\mathrm{op}}, L^{\mathrm{op}})$, which: - On objects: Maps an object $(a, b, f)$ in $\text{Comma}(L, R)$ to the object $(b^{\mathrm{op}}, a^{\mathrm{op}}, f^{\mathrm{op}})$ in $(\text{Comma}(R^{\mathrm{op}}, L^{\mathrm{op}}))^{\mathrm{op}}$. - On morphisms: Maps a morphism $(g, h)$ in $\text{Comma}(L, R)$ to the morphism $(h^{\mathrm{op}}, g^{\mathrm{op}})$ in $(\text{Comma}(R^{\mathrm{op}}, L^{\mathrm{op}}))^{\mathrm{op}}$.

CategoryTheory.Comma.opFunctorCompFst definition

: (opFunctor L R).leftOp ⋙ fst _ _ ≅ (snd _ _).op

Full source

/-- Composing the `leftOp` of `opFunctor L R` with `fst L.op R.op` is naturally isomorphic
to `snd L R`. -/
@[simps!]
def opFunctorCompFst : (opFunctor L R).leftOp ⋙ fst _ _(opFunctor L R).leftOp ⋙ fst _ _ ≅ (snd _ _).op :=
  Iso.refl _

Natural isomorphism between left opposite of comma opposite functor composed with first projection and opposite of second projection

Informal description

The composition of the left opposite of the opposite functor for comma categories with the first projection functor is naturally isomorphic to the opposite of the second projection functor. In other words, for functors $L \colon A \to T$ and $R \colon B \to T$, the diagram \[ \text{leftOp}(\text{opFunctor}(L, R)) \circ \text{fst} \cong (\text{snd})^{\mathrm{op}} \] commutes up to natural isomorphism.

CategoryTheory.Comma.opFunctorCompSnd definition

: (opFunctor L R).leftOp ⋙ snd _ _ ≅ (fst _ _).op

Full source

/-- Composing the `leftOp` of `opFunctor L R` with `snd L.op R.op` is naturally isomorphic
to `fst L R`. -/
@[simps!]
def opFunctorCompSnd : (opFunctor L R).leftOp ⋙ snd _ _(opFunctor L R).leftOp ⋙ snd _ _ ≅ (fst _ _).op :=
  Iso.refl _

Natural isomorphism between composed functors in comma categories

Informal description

The composition of the left opposite of the opposite functor for comma categories with the second projection functor is naturally isomorphic to the opposite of the first projection functor. In other words, for functors $L \colon A \to T$ and $R \colon B \to T$, the functor $\mathrm{leftOp}(\mathrm{opFunctor}(L, R)) \circ \mathrm{snd}$ is naturally isomorphic to $(\mathrm{fst})^{\mathrm{op}}$.

CategoryTheory.Comma.unopFunctor definition

: Comma L.op R.op ⥤ (Comma R L)ᵒᵖ

Full source

/-- The canonical functor from `Comma L.op R.op` to `(Comma R L)ᵒᵖ`. -/
@[simps]
def unopFunctor : CommaComma L.op R.op ⥤ (Comma R L)ᵒᵖ where
  obj X := ⟨X.right.unop, X.left.unop, X.hom.unop⟩
  map f := ⟨f.right.unop, f.left.unop, Quiver.Hom.op_inj (by simpa using f.w.symm)⟩

Unop functor between comma categories

Informal description

The functor from the comma category $\text{Comma}(L^{\mathrm{op}}, R^{\mathrm{op}})$ to the opposite of the comma category $\text{Comma}(R, L)^{\mathrm{op}}$, defined by: - On objects: Maps an object $(a, b, f)$ in $\text{Comma}(L^{\mathrm{op}}, R^{\mathrm{op}})$ to the object $(b^{\mathrm{unop}}, a^{\mathrm{unop}}, f^{\mathrm{unop}})$ in $\text{Comma}(R, L)^{\mathrm{op}}$. - On morphisms: Maps a morphism $(g, h)$ in $\text{Comma}(L^{\mathrm{op}}, R^{\mathrm{op}})$ to the morphism $(h^{\mathrm{unop}}, g^{\mathrm{unop}})$ in $\text{Comma}(R, L)^{\mathrm{op}}$.

CategoryTheory.Comma.unopFunctorCompFst definition

: unopFunctor L R ⋙ (fst _ _).op ≅ snd _ _

Full source

/-- Composing `unopFunctor L R` with `(fst L R).op` is isomorphic to `snd L.op R.op`. -/
@[simps!]
def unopFunctorCompFst : unopFunctorunopFunctor L R ⋙ (fst _ _).opunopFunctor L R ⋙ (fst _ _).op ≅ snd _ _ :=
  Iso.refl _

Isomorphism between unop functor composed with opposite fst and snd

Informal description

The composition of the unop functor $\text{unopFunctor} \colon \text{Comma}(L^{\mathrm{op}}, R^{\mathrm{op}}) \to \text{Comma}(R, L)^{\mathrm{op}}$ with the opposite of the first projection functor $(\text{fst} \colon \text{Comma}(R, L) \to B)^{\mathrm{op}}$ is naturally isomorphic to the second projection functor $\text{snd} \colon \text{Comma}(L^{\mathrm{op}}, R^{\mathrm{op}}) \to A$.

CategoryTheory.Comma.unopFunctorCompSnd definition

: unopFunctor L R ⋙ (snd _ _).op ≅ fst _ _

Full source

/-- Composing `unopFunctor L R` with `(snd L R).op` is isomorphic to `fst L.op R.op`. -/
@[simps!]
def unopFunctorCompSnd : unopFunctorunopFunctor L R ⋙ (snd _ _).opunopFunctor L R ⋙ (snd _ _).op ≅ fst _ _ :=
  Iso.refl _

Isomorphism between unopFunctor composed with snd.op and fst

Informal description

The composition of the functor `unopFunctor L R` with the opposite of the second projection functor `(snd L R).op` is naturally isomorphic to the first projection functor `fst L R`.

CategoryTheory.Comma.opEquiv definition

: Comma L R ≌ (Comma R.op L.op)ᵒᵖ

Full source

/-- The canonical equivalence between `Comma L R` and `(Comma R.op L.op)ᵒᵖ`. -/
@[simps]
def opEquiv : CommaComma L R ≌ (Comma R.op L.op)ᵒᵖ where
  functor := opFunctor L R
  inverse := (unopFunctor R L).leftOp
  unitIso := NatIso.ofComponents (fun X => Iso.refl _)
  counitIso := NatIso.ofComponents (fun X => Iso.refl _)

Equivalence between comma category and opposite comma category

Informal description

The canonical equivalence between the comma category $\text{Comma}(L, R)$ and the opposite of the comma category $\text{Comma}(R^{\mathrm{op}}, L^{\mathrm{op}})$. This equivalence consists of: - A functor $\text{opFunctor} \colon \text{Comma}(L, R) \to (\text{Comma}(R^{\mathrm{op}}, L^{\mathrm{op}}))^{\mathrm{op}}$ - An inverse functor $\text{unopFunctor} \colon \text{Comma}(R^{\mathrm{op}}, L^{\mathrm{op}}) \to (\text{Comma}(L, R))^{\mathrm{op}}$ - Natural isomorphisms showing these functors form an equivalence of categories.

Mathlib.CategoryTheory.Comma.Basic

Main definitions

References

Tags