Documentation

Mathlib.CategoryTheory.Adjunction.Unique

Uniqueness of adjoints #

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

Main results #

@[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))
@[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)))

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
    @[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)
    @[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)
    @[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
    @[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
    @[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
    @[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

    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

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

      Equations
      Instances For
        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
        @[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
        @[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
        @[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
        @[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
        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
        @[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
        @[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
        @[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
        @[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

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

        Equations
        Instances For
          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
          @[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
          @[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
          @[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
          @[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
          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
          @[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
          @[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
          @[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
          @[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