Uniqueness of adjoints #

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

Main results #

Adjunction.natTransEquiv and Adjunction.natIsoEquiv If F ⊣ G and F' ⊣ G' are adjunctions, then there are equivalences (G ⟶ G') ≃ (F' ⟶ F) and (G ≅ G') ≃ (F' ≅ F). Everything else is deduced from this:
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.

@[simp]

theorem CategoryTheory.Adjunction.natTransEquiv_apply_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} {F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G') (f : G ⟶ G') (X : C) :

((adj1.natTransEquiv adj2) f).app X = CategoryTheory.CategoryStruct.comp (F'.map ((CategoryTheory.CategoryStruct.comp adj1.unit (CategoryTheory.whiskerLeft F f)).app X)) (adj2.counit.app (F.obj X))

source

@[simp]

theorem CategoryTheory.Adjunction.natTransEquiv_symm_apply_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} {F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G') (f : F' ⟶ F) (X : D) :

((adj1.natTransEquiv adj2).symm f).app X = CategoryTheory.CategoryStruct.comp (adj2.unit.app (G.obj X)) (G'.map (CategoryTheory.CategoryStruct.comp (f.app (G.obj X)) (adj1.counit.app X)))

source

def CategoryTheory.Adjunction.natTransEquiv {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} {F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G') :

(G ⟶ G') ≃ (F' ⟶ F)

If F ⊣ G and F' ⊣ G' are adjunctions, then giving a natural transformation G ⟶ G' is the same as giving a natural transformation F' ⟶ F.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.Adjunction.natTransEquiv_id {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} (adj : F ⊣ G) :

(adj.natTransEquiv adj) (CategoryTheory.CategoryStruct.id G) = CategoryTheory.CategoryStruct.id F

source

@[simp]

theorem CategoryTheory.Adjunction.natTransEquiv_id_symm {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} (adj : F ⊣ G) :

(adj.natTransEquiv adj).symm (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id G

source

@[simp]

theorem CategoryTheory.Adjunction.natTransEquiv_comp {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} {F' : CategoryTheory.Functor C D} {F'' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} {G'' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G') (adj3 : F'' ⊣ G'') (f : G ⟶ G') (g : G' ⟶ G'') :

CategoryTheory.CategoryStruct.comp ((adj2.natTransEquiv adj3) g) ((adj1.natTransEquiv adj2) f) = (adj1.natTransEquiv adj3) (CategoryTheory.CategoryStruct.comp f g)

source

@[simp]

theorem CategoryTheory.Adjunction.natTransEquiv_comp_symm {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} {F' : CategoryTheory.Functor C D} {F'' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} {G'' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G') (adj3 : F'' ⊣ G'') (f : F' ⟶ F) (g : F'' ⟶ F') :

CategoryTheory.CategoryStruct.comp ((adj1.natTransEquiv adj2).symm f) ((adj2.natTransEquiv adj3).symm g) = (adj1.natTransEquiv adj3).symm (CategoryTheory.CategoryStruct.comp g f)

source

@[simp]

theorem CategoryTheory.Adjunction.natIsoEquiv_symm_apply_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} {F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G') (i : F' ≅ F) :

((adj1.natIsoEquiv adj2).symm i).hom = (adj1.natTransEquiv adj2).symm i.hom

source

@[simp]

theorem CategoryTheory.Adjunction.natIsoEquiv_symm_apply_inv {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} {F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G') (i : F' ≅ F) :

((adj1.natIsoEquiv adj2).symm i).inv = (adj2.natTransEquiv adj1).symm i.inv

source

@[simp]

theorem CategoryTheory.Adjunction.natIsoEquiv_apply_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} {F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G') (i : G ≅ G') :

((adj1.natIsoEquiv adj2) i).hom = (adj1.natTransEquiv adj2) i.hom

source

@[simp]

theorem CategoryTheory.Adjunction.natIsoEquiv_apply_inv {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} {F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G') (i : G ≅ G') :

((adj1.natIsoEquiv adj2) i).inv = (adj2.natTransEquiv adj1) i.inv

source

def CategoryTheory.Adjunction.natIsoEquiv {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} {F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G') :

(G ≅ G') ≃ (F' ≅ F)

If F ⊣ G and F' ⊣ G' are adjunctions, then giving a natural isomorphism G ≅ G' is the same as giving a natural transformation F' ≅ F.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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 : CategoryTheory.Functor C D} {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 = ((adj1.natIsoEquiv adj2) (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 : CategoryTheory.Functor C D} {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_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} {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 {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} {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_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} {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.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 : CategoryTheory.Functor C D} {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.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 : CategoryTheory.Functor C D} {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_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} {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_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} {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

@[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 : CategoryTheory.Functor C D} {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

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 : CategoryTheory.Functor C D} {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_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} {F' : CategoryTheory.Functor C D} {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 {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} {F' : CategoryTheory.Functor C D} {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_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} {F' : CategoryTheory.Functor C D} {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_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} {F' : CategoryTheory.Functor C D} {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_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 : CategoryTheory.Functor D C} {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 = (adj1.natIsoEquiv adj2).symm (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 : CategoryTheory.Functor D C} {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_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 : CategoryTheory.Functor D C} {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_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 : CategoryTheory.Functor D C} {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_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 : CategoryTheory.Functor D C} {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.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 : CategoryTheory.Functor D C} {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.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 : CategoryTheory.Functor D C} {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_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 : CategoryTheory.Functor D C} {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_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 : CategoryTheory.Functor D C} {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

@[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 : CategoryTheory.Functor D C} {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

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 : CategoryTheory.Functor D C} {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_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 : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} {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 {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} {G' : CategoryTheory.Functor D C} {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_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 : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} {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_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 : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} {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_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

Documentation

Mathlib.CategoryTheory.Adjunction.Unique

Uniqueness of adjoints #

Main results #