Documentation

Mathlib.CategoryTheory.Adjunction.Unique

Uniqueness of adjoints #

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

Main results #

source
def CategoryTheory.Adjunction.leftAdjointUniq {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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
Instances For
    source
    theorem CategoryTheory.Adjunction.homEquiv_leftAdjointUniq_hom_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, u_2} D] {F F' : Functor C D} {G : Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
    CategoryStruct.comp adj1.unit (Functor.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.{v_1, u_1} C] [Category.{v_2, 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 (Functor.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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, u_2} D] {F F' : Functor C D} {G : Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
    CategoryStruct.comp (G.whiskerLeft (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.{v_1, u_1} C] [Category.{v_2, 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 (G.whiskerLeft (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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, 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
    Instances For
      source
      theorem CategoryTheory.Adjunction.homEquiv_symm_rightAdjointUniq_hom_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor C D} {G G' : Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :
      CategoryStruct.comp adj1.unit (F.whiskerLeft (adj1.rightAdjointUniq adj2).hom) = adj2.unit
      source
      @[simp]
      theorem CategoryTheory.Adjunction.unit_rightAdjointUniq_hom_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, 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 (F.whiskerLeft (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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor C D} {G G' : Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :
      CategoryStruct.comp (Functor.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.{v_1, u_1} C] [Category.{v_2, 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 (Functor.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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, 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.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor C D} {G : Functor D C} (adj1 : F ⊣ G) :
      (adj1.rightAdjointUniq adj1).hom = CategoryStruct.id G