doc-next-gen

Mathlib.CategoryTheory.Adjunction.Unique

Module docstring

{"# Uniqueness of adjoints

This file shows that adjoints are unique up to natural isomorphism.

Main results

  • Adjunction.leftAdjointUniq : If F and F' are both left adjoint to G, then they are naturally isomorphic.

  • Adjunction.rightAdjointUniq : If G and G' are both right adjoint to F, then they are naturally isomorphic.

"}

CategoryTheory.Adjunction.leftAdjointUniq definition
{F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) : F ≅ F'
Full source 
/-- If `F` and `F'` are both left adjoint to `G`, then they are naturally isomorphic. -/
def leftAdjointUniq {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) : F ≅ F' :=
  ((conjugateIsoEquiv adj1 adj2).symm (Iso.refl G)).symm
Natural isomorphism between left adjoints
Informal description
Given two functors $F$ and $F'$ from category $\mathcal{C}$ to $\mathcal{D}$ that are both left adjoint to a functor $G$ from $\mathcal{D}$ to $\mathcal{C}$, there exists a natural isomorphism between $F$ and $F'$. This isomorphism is constructed using the equivalence of adjunctions and the identity isomorphism on $G$.
CategoryTheory.Adjunction.homEquiv_leftAdjointUniq_hom_app theorem
{F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) : adj1.homEquiv _ _ ((leftAdjointUniq adj1 adj2).hom.app x) = adj2.unit.app x
Full source 
theorem homEquiv_leftAdjointUniq_hom_app {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G)
    (x : C) : adj1.homEquiv _ _ ((leftAdjointUniq adj1 adj2).hom.app x) = adj2.unit.app x := by
  simp [leftAdjointUniq]
Hom-equivalence of left adjoint uniqueness isomorphism equals unit
Informal description
Let $\mathcal{C}$ and $\mathcal{D}$ be categories, with functors $F, F' \colon \mathcal{C} \to \mathcal{D}$ and $G \colon \mathcal{D} \to \mathcal{C}$. Suppose $F$ and $F'$ are both left adjoint to $G$ via adjunctions $\text{adj}_1 \colon F \dashv G$ and $\text{adj}_2 \colon F' \dashv G$, respectively. Let $\eta_2$ denote the unit of $\text{adj}_2$. Then for any object $x \in \mathcal{C}$, the hom-equivalence of $\text{adj}_1$ evaluated at the component of the natural isomorphism $\text{leftAdjointUniq}(\text{adj}_1, \text{adj}_2)_x$ equals the unit $\eta_2$ evaluated at $x$. In symbols: \[ \text{adj}_1.\text{homEquiv}_{x, Gx}\left((\text{leftAdjointUniq}(\text{adj}_1, \text{adj}_2).\text{hom})_x\right) = (\eta_2)_x. \]
CategoryTheory.Adjunction.unit_leftAdjointUniq_hom theorem
{F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) : adj1.unit ≫ whiskerRight (leftAdjointUniq adj1 adj2).hom G = adj2.unit
Full source 
@[reassoc (attr := simp)]
theorem unit_leftAdjointUniq_hom {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
    adj1.unit ≫ whiskerRight (leftAdjointUniq adj1 adj2).hom G = adj2.unit := by
  ext x
  rw [NatTrans.comp_app, ← homEquiv_leftAdjointUniq_hom_app adj1 adj2]
  simp [← G.map_comp]
Unit Condition for Natural Isomorphism Between Left Adjoints
Informal description
Let $\mathcal{C}$ and $\mathcal{D}$ be categories, with functors $F, F' \colon \mathcal{C} \to \mathcal{D}$ and $G \colon \mathcal{D} \to \mathcal{C}$. Suppose $F$ and $F'$ are both left adjoint to $G$ via adjunctions $\text{adj}_1 \colon F \dashv G$ and $\text{adj}_2 \colon F' \dashv G$, respectively. Let $\eta_1$ and $\eta_2$ be the units of $\text{adj}_1$ and $\text{adj}_2$, respectively. Then the composition of $\eta_1$ with the right whiskering of the natural isomorphism $\text{leftAdjointUniq}(\text{adj}_1, \text{adj}_2).\text{hom}$ by $G$ equals $\eta_2$. In symbols: \[ \eta_1 \circ (\text{leftAdjointUniq}(\text{adj}_1, \text{adj}_2).\text{hom} \circ G) = \eta_2. \]
CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_app theorem
{F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) : adj1.unit.app x ≫ G.map ((leftAdjointUniq adj1 adj2).hom.app x) = adj2.unit.app x
Full source 
@[reassoc (attr := simp)]
theorem unit_leftAdjointUniq_hom_app
    {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) :
    adj1.unit.app x ≫ G.map ((leftAdjointUniq adj1 adj2).hom.app x) = adj2.unit.app x := by
  rw [← unit_leftAdjointUniq_hom adj1 adj2]; rfl
Componentwise Unit Condition for Natural Isomorphism Between Left Adjoints
Informal description
Let $\mathcal{C}$ and $\mathcal{D}$ be categories, with functors $F, F' \colon \mathcal{C} \to \mathcal{D}$ and $G \colon \mathcal{D} \to \mathcal{C}$. Suppose $F$ and $F'$ are both left adjoint to $G$ via adjunctions $\text{adj}_1 \colon F \dashv G$ and $\text{adj}_2 \colon F' \dashv G$, respectively. Let $\eta_1$ and $\eta_2$ denote the units of $\text{adj}_1$ and $\text{adj}_2$, and let $\eta \colon F \Rightarrow F'$ be the natural isomorphism between $F$ and $F'$. Then for any object $x \in \mathcal{C}$, the following diagram commutes: \[ \eta_{1,x} \circ G(\eta_x) = \eta_{2,x}. \]
CategoryTheory.Adjunction.leftAdjointUniq_hom_counit theorem
{F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) : whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit = adj1.counit
Full source 
@[reassoc (attr := simp)]
theorem leftAdjointUniq_hom_counit {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
    whiskerLeftwhiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit = adj1.counit := by
  ext x
  simp only [Functor.comp_obj, Functor.id_obj, leftAdjointUniq, Iso.symm_hom,
    conjugateIsoEquiv_symm_apply_inv, Iso.refl_inv, NatTrans.comp_app, whiskerLeft_app,
    conjugateEquiv_symm_apply_app, NatTrans.id_app, Functor.map_id, Category.id_comp,
    Category.assoc]
  rw [← adj1.counit_naturality, ← Category.assoc, ← F.map_comp]
  simp
Counit condition for the natural isomorphism between left adjoints
Informal description
Given two adjunctions $F \dashv G$ and $F' \dashv G$ between categories $\mathcal{C}$ and $\mathcal{D}$, the natural isomorphism $\eta \colon F \cong F'$ induced by the uniqueness of left adjoints satisfies the counit condition: the composition of the left whiskering of $\eta$ with $G$ followed by the counit of $F' \dashv G$ equals the counit of $F \dashv G$. In symbols, if $\eta \colon F \Rightarrow F'$ is the natural isomorphism and $\epsilon_1$, $\epsilon_2$ are the counits of the adjunctions $F \dashv G$ and $F' \dashv G$ respectively, then: \[ G \circ \eta \circ \epsilon_2 = \epsilon_1. \]
CategoryTheory.Adjunction.leftAdjointUniq_hom_app_counit theorem
{F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : D) : (leftAdjointUniq adj1 adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x
Full source 
@[reassoc (attr := simp)]
theorem leftAdjointUniq_hom_app_counit {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G)
    (x : D) :
    (leftAdjointUniq adj1 adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x := by
  rw [← leftAdjointUniq_hom_counit adj1 adj2]
  rfl
Componentwise counit condition for natural isomorphism between left adjoints
Informal description
Given two adjunctions $F \dashv G$ and $F' \dashv G$ between categories $\mathcal{C}$ and $\mathcal{D}$, for any object $x \in \mathcal{D}$, the component of the natural isomorphism $\eta \colon F \cong F'$ at $G(x)$, composed with the counit $\epsilon_2$ of $F' \dashv G$ at $x$, equals the counit $\epsilon_1$ of $F \dashv G$ at $x$. In symbols: \[ \eta_{G(x)} \circ \epsilon_{2,x} = \epsilon_{1,x}. \]
CategoryTheory.Adjunction.leftAdjointUniq_inv_app theorem
{F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) : (leftAdjointUniq adj1 adj2).inv.app x = (leftAdjointUniq adj2 adj1).hom.app x
Full source 
theorem leftAdjointUniq_inv_app {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) :
    (leftAdjointUniq adj1 adj2).inv.app x = (leftAdjointUniq adj2 adj1).hom.app x :=
  rfl
Inverse of Natural Isomorphism Between Left Adjoints
Informal description
For any functors $F, F' \colon \mathcal{C} \to \mathcal{D}$ that are both left adjoint to a functor $G \colon \mathcal{D} \to \mathcal{C}$, and for any object $x \in \mathcal{C}$, the component of the inverse natural isomorphism at $x$ satisfies $$ (\text{leftAdjointUniq}\ adj1\ adj2)^{-1}_x = (\text{leftAdjointUniq}\ adj2\ adj1)_x. $$
CategoryTheory.Adjunction.leftAdjointUniq_trans theorem
{F F' F'' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (adj3 : F'' ⊣ G) : (leftAdjointUniq adj1 adj2).hom ≫ (leftAdjointUniq adj2 adj3).hom = (leftAdjointUniq adj1 adj3).hom
Full source 
@[reassoc (attr := simp)]
theorem leftAdjointUniq_trans {F F' F'' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G)
    (adj3 : F'' ⊣ G) :
    (leftAdjointUniq adj1 adj2).hom ≫ (leftAdjointUniq adj2 adj3).hom =
      (leftAdjointUniq adj1 adj3).hom := by
  simp [leftAdjointUniq]
Transitivity of Natural Isomorphism Between Left Adjoints
Informal description
Given three functors $F$, $F'$, and $F''$ from category $\mathcal{C}$ to $\mathcal{D}$, each left adjoint to a functor $G$ from $\mathcal{D}$ to $\mathcal{C}$, the composition of the natural isomorphisms $F \cong F'$ and $F' \cong F''$ is equal to the natural isomorphism $F \cong F''$. In other words, the following diagram commutes: \[ (F \cong F') \circ (F' \cong F'') = (F \cong F'') \] where $\circ$ denotes the composition of natural transformations.
CategoryTheory.Adjunction.leftAdjointUniq_trans_app theorem
{F F' F'' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (adj3 : F'' ⊣ G) (x : C) : (leftAdjointUniq adj1 adj2).hom.app x ≫ (leftAdjointUniq adj2 adj3).hom.app x = (leftAdjointUniq adj1 adj3).hom.app x
Full source 
@[reassoc (attr := simp)]
theorem leftAdjointUniq_trans_app {F F' F'' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G)
    (adj3 : F'' ⊣ G) (x : C) :
    (leftAdjointUniq adj1 adj2).hom.app x ≫ (leftAdjointUniq adj2 adj3).hom.app x =
      (leftAdjointUniq adj1 adj3).hom.app x := by
  rw [← leftAdjointUniq_trans adj1 adj2 adj3]
  rfl
Component-wise Transitivity of Natural Isomorphism Between Left Adjoints
Informal description
For any functors $F, F', F'' \colon \mathcal{C} \to \mathcal{D}$ that are each left adjoint to a functor $G \colon \mathcal{D} \to \mathcal{C}$ via adjunctions $adj1$, $adj2$, and $adj3$ respectively, and for any object $x \in \mathcal{C}$, the composition of the components of the natural isomorphisms $F \cong F'$ and $F' \cong F''$ at $x$ equals the component of the natural isomorphism $F \cong F''$ at $x$. In symbols: $$ (\text{leftAdjointUniq}\ adj1\ adj2)_x \circ (\text{leftAdjointUniq}\ adj2\ adj3)_x = (\text{leftAdjointUniq}\ adj1\ adj3)_x. $$
CategoryTheory.Adjunction.leftAdjointUniq_refl theorem
{F : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) : (leftAdjointUniq adj1 adj1).hom = 𝟙 _
Full source 
@[simp]
theorem leftAdjointUniq_refl {F : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) :
    (leftAdjointUniq adj1 adj1).hom = 𝟙 _ := by
  simp [leftAdjointUniq]
Identity Natural Isomorphism for Self-Adjoint Functor
Informal description
For any functor $F \colon \mathcal{C} \to \mathcal{D}$ that is left adjoint to a functor $G \colon \mathcal{D} \to \mathcal{C}$ via an adjunction $adj1$, the natural isomorphism $\text{leftAdjointUniq}(adj1, adj1)$ between $F$ and itself is the identity natural transformation.
CategoryTheory.Adjunction.rightAdjointUniq definition
{F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') : G ≅ G'
Full source 
/-- If `G` and `G'` are both right adjoint to `F`, then they are naturally isomorphic. -/
def rightAdjointUniq {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') : G ≅ G' :=
  conjugateIsoEquiv adj1 adj2 (Iso.refl _)
Uniqueness of right adjoints up to natural isomorphism
Informal description
Given two adjunctions $F \dashv G$ and $F \dashv G'$ in a category, there exists a natural isomorphism between the right adjoints $G$ and $G'$.
CategoryTheory.Adjunction.homEquiv_symm_rightAdjointUniq_hom_app theorem
{F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : D) : (adj2.homEquiv _ _).symm ((rightAdjointUniq adj1 adj2).hom.app x) = adj1.counit.app x
Full source 
theorem homEquiv_symm_rightAdjointUniq_hom_app {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G)
    (adj2 : F ⊣ G') (x : D) :
    (adj2.homEquiv _ _).symm ((rightAdjointUniq adj1 adj2).hom.app x) = adj1.counit.app x := by
  simp [rightAdjointUniq]
Naturality of Right Adjoint Uniqueness Isomorphism with Respect to Counit
Informal description
Let $F \colon C \to D$ and $G, G' \colon D \to C$ be functors with adjunctions $F \dashv G$ and $F \dashv G'$. For any object $x \in D$, the inverse of the hom-set bijection $\text{adj2.homEquiv}$ evaluated at the component of the natural isomorphism $\text{rightAdjointUniq}(adj1, adj2).\text{hom}$ at $x$ equals the counit of $adj1$ at $x$. In symbols: \[ \text{adj2.homEquiv}^{-1}\left(\text{rightAdjointUniq}(adj1, adj2).\text{hom}_x\right) = \text{adj1.counit}_x. \]
CategoryTheory.Adjunction.unit_rightAdjointUniq_hom_app theorem
{F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : C) : adj1.unit.app x ≫ (rightAdjointUniq adj1 adj2).hom.app (F.obj x) = adj2.unit.app x
Full source 
@[reassoc (attr := simp)]
theorem unit_rightAdjointUniq_hom_app {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
    (x : C) : adj1.unit.app x ≫ (rightAdjointUniq adj1 adj2).hom.app (F.obj x) =
      adj2.unit.app x := by
  simp only [Functor.id_obj, Functor.comp_obj, rightAdjointUniq, conjugateIsoEquiv_apply_hom,
    Iso.refl_hom, conjugateEquiv_apply_app, NatTrans.id_app, Functor.map_id, Category.id_comp]
  rw [← adj2.unit_naturality_assoc, ← G'.map_comp]
  simp
Naturality of Right Adjoint Uniqueness Isomorphism with Respect to Unit
Informal description
For any functors $F \colon C \to D$ and $G, G' \colon D \to C$ with adjunctions $F \dashv G$ and $F \dashv G'$, and for any object $x \in C$, the composition of the unit of $adj1$ at $x$ with the component at $F(x)$ of the natural isomorphism $\text{rightAdjointUniq}(adj1, adj2).\text{hom}$ equals the unit of $adj2$ at $x$. In symbols: \[ \text{adj1.unit}_x \circ \text{rightAdjointUniq}(adj1, adj2).\text{hom}_{F(x)} = \text{adj2.unit}_x. \]
CategoryTheory.Adjunction.unit_rightAdjointUniq_hom theorem
{F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') : adj1.unit ≫ whiskerLeft F (rightAdjointUniq adj1 adj2).hom = adj2.unit
Full source 
@[reassoc (attr := simp)]
theorem unit_rightAdjointUniq_hom {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :
    adj1.unit ≫ whiskerLeft F (rightAdjointUniq adj1 adj2).hom = adj2.unit := by
  ext x
  simp
Naturality of Units with Respect to Right Adjoint Uniqueness Isomorphism
Informal description
Given two adjunctions $F \dashv G$ and $F \dashv G'$ between categories $C$ and $D$, the composition of the unit natural transformation of the first adjunction with the left whiskering of $F$ applied to the natural isomorphism between $G$ and $G'$ equals the unit natural transformation of the second adjunction. In symbols: \[ \eta_1 \circ (F \circ \varphi) = \eta_2 \] where $\eta_1$ and $\eta_2$ are the unit transformations of the two adjunctions respectively, and $\varphi \colon G \to G'$ is the natural isomorphism between the right adjoints.
CategoryTheory.Adjunction.rightAdjointUniq_hom_app_counit theorem
{F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : D) : F.map ((rightAdjointUniq adj1 adj2).hom.app x) ≫ adj2.counit.app x = adj1.counit.app x
Full source 
@[reassoc (attr := simp)]
theorem rightAdjointUniq_hom_app_counit {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
    (x : D) :
    F.map ((rightAdjointUniq adj1 adj2).hom.app x) ≫ adj2.counit.app x = adj1.counit.app x := by
  simp [rightAdjointUniq]
Naturality of Right Adjoint Uniqueness Isomorphism with Respect to Counit
Informal description
For any functors $F \colon C \to D$ and $G, G' \colon D \to C$ with adjunctions $F \dashv G$ and $F \dashv G'$, and for any object $x \in D$, the composition of $F$ applied to the component at $x$ of the natural isomorphism $\text{rightAdjointUniq}(adj1, adj2).\text{hom}$ with the counit of $adj2$ at $x$ equals the counit of $adj1$ at $x$. In symbols: \[ F(\text{rightAdjointUniq}(adj1, adj2).\text{hom}_x) \circ \text{adj2.counit}_x = \text{adj1.counit}_x. \]
CategoryTheory.Adjunction.rightAdjointUniq_hom_counit theorem
{F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') : whiskerRight (rightAdjointUniq adj1 adj2).hom F ≫ adj2.counit = adj1.counit
Full source 
@[reassoc (attr := simp)]
theorem rightAdjointUniq_hom_counit {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :
    whiskerRightwhiskerRight (rightAdjointUniq adj1 adj2).hom F ≫ adj2.counit = adj1.counit := by
  ext
  simp
Naturality of Right Adjoint Uniqueness Isomorphism with Respect to Counit via Whiskering
Informal description
Given functors $F \colon C \to D$ and $G, G' \colon D \to C$ with adjunctions $F \dashv G$ and $F \dashv G'$, the composition of the right whiskering of the natural isomorphism $\text{rightAdjointUniq}(adj1, adj2).\text{hom}$ with $F$ and the counit of $adj2$ equals the counit of $adj1$. In symbols: \[ (\text{rightAdjointUniq}(adj1, adj2).\text{hom} \circ F) \circ \text{adj2.counit} = \text{adj1.counit}. \]
CategoryTheory.Adjunction.rightAdjointUniq_inv_app theorem
{F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : D) : (rightAdjointUniq adj1 adj2).inv.app x = (rightAdjointUniq adj2 adj1).hom.app x
Full source 
theorem rightAdjointUniq_inv_app {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
    (x : D) : (rightAdjointUniq adj1 adj2).inv.app x = (rightAdjointUniq adj2 adj1).hom.app x :=
  rfl
Inverse of Right Adjoint Uniqueness Isomorphism Equals Forward Isomorphism with Swapped Adjunctions
Informal description
For any functors $F \colon C \to D$ and $G, G' \colon D \to C$ with adjunctions $F \dashv G$ and $F \dashv G'$, and for any object $x \in D$, the component at $x$ of the inverse of the natural isomorphism $\text{rightAdjointUniq}(adj1, adj2)$ equals the component at $x$ of the natural isomorphism $\text{rightAdjointUniq}(adj2, adj1)$. In symbols: \[ (\text{rightAdjointUniq}(adj1, adj2))^{-1}_x = \text{rightAdjointUniq}(adj2, adj1)_x. \]
CategoryTheory.Adjunction.rightAdjointUniq_trans theorem
{F : C ⥤ D} {G G' G'' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (adj3 : F ⊣ G'') : (rightAdjointUniq adj1 adj2).hom ≫ (rightAdjointUniq adj2 adj3).hom = (rightAdjointUniq adj1 adj3).hom
Full source 
@[reassoc (attr := simp)]
theorem rightAdjointUniq_trans {F : C ⥤ D} {G G' G'' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
    (adj3 : F ⊣ G'') :
    (rightAdjointUniq adj1 adj2).hom ≫ (rightAdjointUniq adj2 adj3).hom =
      (rightAdjointUniq adj1 adj3).hom := by
  simp [rightAdjointUniq]
Transitivity of Right Adjoint Uniqueness Isomorphisms
Informal description
Given functors $F \colon C \to D$ and $G, G', G'' \colon D \to C$ with adjunctions $F \dashv G$, $F \dashv G'$, and $F \dashv G''$, the composition of the natural isomorphisms $G \cong G'$ and $G' \cong G''$ equals the natural isomorphism $G \cong G''$. In symbols, if $\eta_{12} \colon G \to G'$ and $\eta_{23} \colon G' \to G''$ are the isomorphisms provided by $\text{rightAdjointUniq}$ for the respective adjunctions, then $\eta_{12} \circ \eta_{23} = \eta_{13}$, where $\eta_{13} \colon G \to G''$ is the isomorphism for $F \dashv G$ and $F \dashv G''$.
CategoryTheory.Adjunction.rightAdjointUniq_trans_app theorem
{F : C ⥤ D} {G G' G'' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (adj3 : F ⊣ G'') (x : D) : (rightAdjointUniq adj1 adj2).hom.app x ≫ (rightAdjointUniq adj2 adj3).hom.app x = (rightAdjointUniq adj1 adj3).hom.app x
Full source 
@[reassoc (attr := simp)]
theorem rightAdjointUniq_trans_app {F : C ⥤ D} {G G' G'' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
    (adj3 : F ⊣ G'') (x : D) :
    (rightAdjointUniq adj1 adj2).hom.app x ≫ (rightAdjointUniq adj2 adj3).hom.app x =
      (rightAdjointUniq adj1 adj3).hom.app x := by
  rw [← rightAdjointUniq_trans adj1 adj2 adj3]
  rfl
Component-wise Transitivity of Right Adjoint Uniqueness Isomorphisms
Informal description
Given functors $F \colon C \to D$ and $G, G', G'' \colon D \to C$ with adjunctions $F \dashv G$, $F \dashv G'$, and $F \dashv G''$, and given any object $x \in D$, the composition of the components at $x$ of the natural isomorphisms $G \cong G'$ and $G' \cong G''$ equals the component at $x$ of the natural isomorphism $G \cong G''$. In symbols, for the natural isomorphisms $\eta_{12} \colon G \to G'$, $\eta_{23} \colon G' \to G''$, and $\eta_{13} \colon G \to G''$ provided by $\text{rightAdjointUniq}$, we have: \[ \eta_{12}(x) \circ \eta_{23}(x) = \eta_{13}(x). \]
CategoryTheory.Adjunction.rightAdjointUniq_refl theorem
{F : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) : (rightAdjointUniq adj1 adj1).hom = 𝟙 _
Full source 
@[simp]
theorem rightAdjointUniq_refl {F : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) :
    (rightAdjointUniq adj1 adj1).hom = 𝟙 _ := by
  delta rightAdjointUniq
  simp
Identity Natural Isomorphism for Self-Adjoint Right Adjoint
Informal description
Given a functor $F \colon C \to D$ and a functor $G \colon D \to C$ with an adjunction $F \dashv G$, the natural isomorphism between $G$ and itself provided by $\text{rightAdjointUniq}$ is the identity natural transformation, i.e., $(\text{rightAdjointUniq}\, adj1\, adj1).\text{hom} = \mathrm{id}_G$.