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.

def CategoryTheory.Adjunction.leftAdjointUniq {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :

F ≅ F'

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

Equations

adj1.leftAdjointUniq adj2 = ((CategoryTheory.conjugateIsoEquiv adj1 adj2).symm (CategoryTheory.Iso.refl G)).symm

Instances For

source

theorem CategoryTheory.Adjunction.homEquiv_leftAdjointUniq_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) :

(adj1.homEquiv x (F'.obj x)) ((adj1.leftAdjointUniq adj2).hom.app x) = adj2.unit.app x

source

@[simp]

theorem CategoryTheory.Adjunction.unit_leftAdjointUniq_hom {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :

CategoryTheory.CategoryStruct.comp adj1.unit (CategoryTheory.whiskerRight (adj1.leftAdjointUniq adj2).hom G) = adj2.unit

source

@[simp]

theorem CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) {Z : CategoryTheory.Functor C C} (h : F'.comp G ⟶ Z) :

CategoryTheory.CategoryStruct.comp adj1.unit (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (adj1.leftAdjointUniq adj2).hom G) h) = CategoryTheory.CategoryStruct.comp adj2.unit h

source

@[simp]

theorem CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) :

CategoryTheory.CategoryStruct.comp (adj1.unit.app x) (G.map ((adj1.leftAdjointUniq adj2).hom.app x)) = adj2.unit.app x

source

@[simp]

theorem CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_app_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) {Z : C} (h : G.obj (F'.obj x) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (adj1.unit.app x) (CategoryTheory.CategoryStruct.comp (G.map ((adj1.leftAdjointUniq adj2).hom.app x)) h) = CategoryTheory.CategoryStruct.comp (adj2.unit.app x) h

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_hom_counit {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft G (adj1.leftAdjointUniq adj2).hom) adj2.counit = adj1.counit

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_hom_counit_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) {Z : CategoryTheory.Functor D D} (h : CategoryTheory.Functor.id D ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft G (adj1.leftAdjointUniq adj2).hom) (CategoryTheory.CategoryStruct.comp adj2.counit h) = CategoryTheory.CategoryStruct.comp adj1.counit h

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_hom_app_counit {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : D) :

CategoryTheory.CategoryStruct.comp ((adj1.leftAdjointUniq adj2).hom.app (G.obj x)) (adj2.counit.app x) = adj1.counit.app x

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_hom_app_counit_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : D) {Z : D} (h : x ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((adj1.leftAdjointUniq adj2).hom.app (G.obj x)) (CategoryTheory.CategoryStruct.comp (adj2.counit.app x) h) = CategoryTheory.CategoryStruct.comp (adj1.counit.app x) h

source

theorem CategoryTheory.Adjunction.leftAdjointUniq_inv_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) :

(adj1.leftAdjointUniq adj2).inv.app x = (adj2.leftAdjointUniq adj1).hom.app x

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_trans {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F F' F'' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (adj3 : F'' ⊣ G) :

CategoryTheory.CategoryStruct.comp (adj1.leftAdjointUniq adj2).hom (adj2.leftAdjointUniq adj3).hom = (adj1.leftAdjointUniq adj3).hom

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_trans_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F F' F'' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (adj3 : F'' ⊣ G) {Z : CategoryTheory.Functor C D} (h : F'' ⟶ Z) :

CategoryTheory.CategoryStruct.comp (adj1.leftAdjointUniq adj2).hom (CategoryTheory.CategoryStruct.comp (adj2.leftAdjointUniq adj3).hom h) = CategoryTheory.CategoryStruct.comp (adj1.leftAdjointUniq adj3).hom h

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_trans_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F F' F'' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (adj3 : F'' ⊣ G) (x : C) :

CategoryTheory.CategoryStruct.comp ((adj1.leftAdjointUniq adj2).hom.app x) ((adj2.leftAdjointUniq adj3).hom.app x) = (adj1.leftAdjointUniq adj3).hom.app x

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_trans_app_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F F' F'' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (adj3 : F'' ⊣ G) (x : C) {Z : D} (h : F''.obj x ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((adj1.leftAdjointUniq adj2).hom.app x) (CategoryTheory.CategoryStruct.comp ((adj2.leftAdjointUniq adj3).hom.app x) h) = CategoryTheory.CategoryStruct.comp ((adj1.leftAdjointUniq adj3).hom.app x) h

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_refl {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) :

(adj1.leftAdjointUniq adj1).hom = CategoryTheory.CategoryStruct.id F

source

def CategoryTheory.Adjunction.rightAdjointUniq {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :

G ≅ G'

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

Equations

adj1.rightAdjointUniq adj2 = (CategoryTheory.conjugateIsoEquiv adj1 adj2) (CategoryTheory.Iso.refl F)

Instances For

source

theorem CategoryTheory.Adjunction.homEquiv_symm_rightAdjointUniq_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : D) :

(adj2.homEquiv (G.obj x) x).symm ((adj1.rightAdjointUniq adj2).hom.app x) = adj1.counit.app x

source

@[simp]

theorem CategoryTheory.Adjunction.unit_rightAdjointUniq_hom_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : C) :

CategoryTheory.CategoryStruct.comp (adj1.unit.app x) ((adj1.rightAdjointUniq adj2).hom.app (F.obj x)) = adj2.unit.app x

source

@[simp]

theorem CategoryTheory.Adjunction.unit_rightAdjointUniq_hom_app_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : C) {Z : C} (h : G'.obj (F.obj x) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (adj1.unit.app x) (CategoryTheory.CategoryStruct.comp ((adj1.rightAdjointUniq adj2).hom.app (F.obj x)) h) = CategoryTheory.CategoryStruct.comp (adj2.unit.app x) h

source

@[simp]

theorem CategoryTheory.Adjunction.unit_rightAdjointUniq_hom {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :

CategoryTheory.CategoryStruct.comp adj1.unit (CategoryTheory.whiskerLeft F (adj1.rightAdjointUniq adj2).hom) = adj2.unit

source

@[simp]

theorem CategoryTheory.Adjunction.unit_rightAdjointUniq_hom_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') {Z : CategoryTheory.Functor C C} (h : F.comp G' ⟶ Z) :

CategoryTheory.CategoryStruct.comp adj1.unit (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft F (adj1.rightAdjointUniq adj2).hom) h) = CategoryTheory.CategoryStruct.comp adj2.unit h

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_hom_app_counit {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : D) :

CategoryTheory.CategoryStruct.comp (F.map ((adj1.rightAdjointUniq adj2).hom.app x)) (adj2.counit.app x) = adj1.counit.app x

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_hom_app_counit_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : D) {Z : D} (h : x ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.map ((adj1.rightAdjointUniq adj2).hom.app x)) (CategoryTheory.CategoryStruct.comp (adj2.counit.app x) h) = CategoryTheory.CategoryStruct.comp (adj1.counit.app x) h

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_hom_counit {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :

CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (adj1.rightAdjointUniq adj2).hom F) adj2.counit = adj1.counit

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_hom_counit_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') {Z : CategoryTheory.Functor D D} (h : CategoryTheory.Functor.id D ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (adj1.rightAdjointUniq adj2).hom F) (CategoryTheory.CategoryStruct.comp adj2.counit h) = CategoryTheory.CategoryStruct.comp adj1.counit h

source

theorem CategoryTheory.Adjunction.rightAdjointUniq_inv_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : D) :

(adj1.rightAdjointUniq adj2).inv.app x = (adj2.rightAdjointUniq adj1).hom.app x

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_trans {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {G G' G'' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (adj3 : F ⊣ G'') :

CategoryTheory.CategoryStruct.comp (adj1.rightAdjointUniq adj2).hom (adj2.rightAdjointUniq adj3).hom = (adj1.rightAdjointUniq adj3).hom

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_trans_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {G G' G'' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (adj3 : F ⊣ G'') {Z : CategoryTheory.Functor D C} (h : G'' ⟶ Z) :

CategoryTheory.CategoryStruct.comp (adj1.rightAdjointUniq adj2).hom (CategoryTheory.CategoryStruct.comp (adj2.rightAdjointUniq adj3).hom h) = CategoryTheory.CategoryStruct.comp (adj1.rightAdjointUniq adj3).hom h

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_trans_app {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {G G' G'' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (adj3 : F ⊣ G'') (x : D) :

CategoryTheory.CategoryStruct.comp ((adj1.rightAdjointUniq adj2).hom.app x) ((adj2.rightAdjointUniq adj3).hom.app x) = (adj1.rightAdjointUniq adj3).hom.app x

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_trans_app_assoc {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {G G' G'' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (adj3 : F ⊣ G'') (x : D) {Z : C} (h : G''.obj x ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((adj1.rightAdjointUniq adj2).hom.app x) (CategoryTheory.CategoryStruct.comp ((adj2.rightAdjointUniq adj3).hom.app x) h) = CategoryTheory.CategoryStruct.comp ((adj1.rightAdjointUniq adj3).hom.app x) h

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_refl {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) :

(adj1.rightAdjointUniq adj1).hom = CategoryTheory.CategoryStruct.id G

source

@[deprecated CategoryTheory.conjugateEquiv (since := "2024-10-07")]

def CategoryTheory.Adjunction.natTransEquiv {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) :

(L₂ ⟶ L₁) ≃ (R₁ ⟶ R₂)

Alias of CategoryTheory.conjugateEquiv.

Given two adjunctions L₁ ⊣ R₁ and L₂ ⊣ R₂ both between categories C, D, there is a bijection between natural transformations L₂ ⟶ L₁ and natural transformations R₁ ⟶ R₂. This is defined as a special case of mateEquiv, where the two "vertical" functors are identity, modulo composition with the unitors. Corresponding natural transformations are called conjugateEquiv. TODO: Generalise to when the two vertical functors are equivalences rather than being exactly 𝟭.

Furthermore, this bijection preserves (and reflects) isomorphisms, i.e. a transformation is an iso iff its image under the bijection is an iso, see eg CategoryTheory.conjugateIsoEquiv. This is in contrast to the general case mateEquiv which does not in general have this property.

Equations

@CategoryTheory.Adjunction.natTransEquiv = @CategoryTheory.conjugateEquiv

Instances For

source

@[deprecated CategoryTheory.conjugateIsoEquiv (since := "2024-10-07")]

def CategoryTheory.Adjunction.natIsoEquiv {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) :

(L₂ ≅ L₁) ≃ (R₁ ≅ R₂)

Alias of CategoryTheory.conjugateIsoEquiv.

Thus conjugation defines an equivalence between natural isomorphisms.

Equations

@CategoryTheory.Adjunction.natIsoEquiv = @CategoryTheory.conjugateIsoEquiv

Instances For

Documentation

Mathlib.CategoryTheory.Adjunction.Unique

Uniqueness of adjoints #

Main results #