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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F F' : Functor C D} {G : 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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F F' : Functor C D} {G : 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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F F' : Functor C D} {G : Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :

CategoryStruct.comp adj1.unit (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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F F' : Functor C D} {G : Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) {Z : Functor C C} (h : F'.comp G ⟶ Z) :

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

source

@[simp]

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

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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F F' : Functor C D} {G : Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : C) {Z : C} (h : G.obj (F'.obj x) ⟶ Z) :

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

source

@[simp]

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

CategoryStruct.comp (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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F F' : Functor C D} {G : Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) {Z : Functor D D} (h : Functor.id D ⟶ Z) :

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

source

@[simp]

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

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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F F' : Functor C D} {G : Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (x : D) {Z : D} (h : x ⟶ Z) :

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

source

theorem CategoryTheory.Adjunction.leftAdjointUniq_inv_app {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F F' : Functor C D} {G : 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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F F' F'' : Functor C D} {G : Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (adj3 : F'' ⊣ G) :

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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F F' F'' : Functor C D} {G : Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (adj3 : F'' ⊣ G) {Z : Functor C D} (h : F'' ⟶ Z) :

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

source

@[simp]

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

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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F F' F'' : Functor C D} {G : Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) (adj3 : F'' ⊣ G) (x : C) {Z : D} (h : F''.obj x ⟶ Z) :

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

source

@[simp]

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

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

source

def CategoryTheory.Adjunction.rightAdjointUniq {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G G' : 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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G G' : 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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G G' : Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : C) :

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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G G' : Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : C) {Z : C} (h : G'.obj (F.obj x) ⟶ Z) :

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

source

@[simp]

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

CategoryStruct.comp adj1.unit (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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G G' : Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') {Z : Functor C C} (h : F.comp G' ⟶ Z) :

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

source

@[simp]

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

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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G G' : Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : D) {Z : D} (h : x ⟶ Z) :

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

source

@[simp]

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

CategoryStruct.comp (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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G G' : Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') {Z : Functor D D} (h : Functor.id D ⟶ Z) :

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

source

theorem CategoryTheory.Adjunction.rightAdjointUniq_inv_app {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G G' : 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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G G' G'' : Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (adj3 : F ⊣ G'') :

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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G G' G'' : Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (adj3 : F ⊣ G'') {Z : Functor D C} (h : G'' ⟶ Z) :

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

source

@[simp]

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

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} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {F : Functor C D} {G G' G'' : Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (adj3 : F ⊣ G'') (x : D) {Z : C} (h : G''.obj x ⟶ Z) :

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

source

@[simp]

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

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

Documentation

Mathlib.CategoryTheory.Adjunction.Unique

Uniqueness of adjoints #

Main results #