mathlib documentation

category_theory.adjunction.opposites

Opposite adjunctions #

This file contains constructions to relate adjunctions of functors to adjunctions of their opposites. These constructions are used to show uniqueness of adjoints (up to natural isomorphism).

Tags #

adjunction, opposite, uniqueness

@[simp]
theorem category_theory.adjunction.adjoint_of_op_adjoint_op_hom_equiv_symm_apply {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) (G : D C) (h : G.op F.op) (X : C) (Y : D) (ᾰ : X G.obj Y) :
@[simp]
theorem category_theory.adjunction.op_adjoint_op_of_adjoint_hom_equiv_symm_apply {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) (G : D C) (h : G F) (X : Cᵒᵖ) (Y : Dᵒᵖ) (ᾰ : X G.op.obj Y) :
@[simp]
theorem category_theory.adjunction.op_adjoint_op_of_adjoint_hom_equiv_apply {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) (G : D C) (h : G F) (X : Cᵒᵖ) (Y : Dᵒᵖ) (ᾰ : F.op.obj X Y) :

If F and F' are both adjoint to G, there is a natural isomorphism F.op ⋙ coyoneda ≅ F'.op ⋙ coyoneda. We use this in combination with fully_faithful_cancel_right to show left adjoints are unique.

Equations
def category_theory.adjunction.left_adjoint_uniq {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C D} {G : 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
@[simp]
theorem category_theory.adjunction.hom_equiv_left_adjoint_uniq_hom_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C D} {G : D C} (adj1 : F G) (adj2 : F' G) (x : C) :
(adj1.hom_equiv x (F'.obj x)) ((adj1.left_adjoint_uniq adj2).hom.app x) = adj2.unit.app x
@[simp]
theorem category_theory.adjunction.unit_left_adjoint_uniq_hom_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C D} {G : D C} (adj1 : F G) (adj2 : F' G) {X' : C C} (f' : F' G X') :
@[simp]
theorem category_theory.adjunction.unit_left_adjoint_uniq_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C D} {G : D C} (adj1 : F G) (adj2 : F' G) :
@[simp]
theorem category_theory.adjunction.unit_left_adjoint_uniq_hom_app_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C D} {G : D C} (adj1 : F G) (adj2 : F' G) (x : C) {X' : C} (f' : G.obj (F'.obj x) X') :
adj1.unit.app x G.map ((adj1.left_adjoint_uniq adj2).hom.app x) f' = adj2.unit.app x f'
@[simp]
theorem category_theory.adjunction.unit_left_adjoint_uniq_hom_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C D} {G : D C} (adj1 : F G) (adj2 : F' G) (x : C) :
adj1.unit.app x G.map ((adj1.left_adjoint_uniq adj2).hom.app x) = adj2.unit.app x
@[simp]
theorem category_theory.adjunction.left_adjoint_uniq_hom_counit_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C D} {G : D C} (adj1 : F G) (adj2 : F' G) {X' : D D} (f' : 𝟭 D X') :
@[simp]
theorem category_theory.adjunction.left_adjoint_uniq_hom_counit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C D} {G : D C} (adj1 : F G) (adj2 : F' G) :
@[simp]
theorem category_theory.adjunction.left_adjoint_uniq_hom_app_counit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C D} {G : D C} (adj1 : F G) (adj2 : F' G) (x : D) :
(adj1.left_adjoint_uniq adj2).hom.app (G.obj x) adj2.counit.app x = adj1.counit.app x
@[simp]
theorem category_theory.adjunction.left_adjoint_uniq_hom_app_counit_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C D} {G : D C} (adj1 : F G) (adj2 : F' G) (x : D) {X' : D} (f' : (𝟭 D).obj x X') :
(adj1.left_adjoint_uniq adj2).hom.app (G.obj x) adj2.counit.app x f' = adj1.counit.app x f'
@[simp]
theorem category_theory.adjunction.left_adjoint_uniq_inv_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C D} {G : D C} (adj1 : F G) (adj2 : F' G) (x : C) :
(adj1.left_adjoint_uniq adj2).inv.app x = (adj2.left_adjoint_uniq adj1).hom.app x
@[simp]
theorem category_theory.adjunction.left_adjoint_uniq_trans_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' F'' : C D} {G : D C} (adj1 : F G) (adj2 : F' G) (adj3 : F'' G) {X' : C D} (f' : F'' X') :
(adj1.left_adjoint_uniq adj2).hom (adj2.left_adjoint_uniq adj3).hom f' = (adj1.left_adjoint_uniq adj3).hom f'
@[simp]
theorem category_theory.adjunction.left_adjoint_uniq_trans {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' F'' : C D} {G : D C} (adj1 : F G) (adj2 : F' G) (adj3 : F'' G) :
(adj1.left_adjoint_uniq adj2).hom (adj2.left_adjoint_uniq adj3).hom = (adj1.left_adjoint_uniq adj3).hom
@[simp]
theorem category_theory.adjunction.left_adjoint_uniq_trans_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' F'' : C D} {G : D C} (adj1 : F G) (adj2 : F' G) (adj3 : F'' G) (x : C) :
(adj1.left_adjoint_uniq adj2).hom.app x (adj2.left_adjoint_uniq adj3).hom.app x = (adj1.left_adjoint_uniq adj3).hom.app x
@[simp]
theorem category_theory.adjunction.left_adjoint_uniq_trans_app_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' F'' : C D} {G : D C} (adj1 : F G) (adj2 : F' G) (adj3 : F'' G) (x : C) {X' : D} (f' : F''.obj x X') :
(adj1.left_adjoint_uniq adj2).hom.app x (adj2.left_adjoint_uniq adj3).hom.app x f' = (adj1.left_adjoint_uniq adj3).hom.app x f'
@[simp]
theorem category_theory.adjunction.left_adjoint_uniq_refl {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj1 : F G) :
(adj1.left_adjoint_uniq adj1).hom = 𝟙 F
def category_theory.adjunction.right_adjoint_uniq {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G G' : 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
@[simp]
theorem category_theory.adjunction.hom_equiv_symm_right_adjoint_uniq_hom_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G G' : D C} (adj1 : F G) (adj2 : F G') (x : D) :
((adj2.hom_equiv (G.obj x) x).symm) ((adj1.right_adjoint_uniq adj2).hom.app x) = adj1.counit.app x
@[simp]
theorem category_theory.adjunction.unit_right_adjoint_uniq_hom_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G G' : D C} (adj1 : F G) (adj2 : F G') (x : C) :
adj1.unit.app x (adj1.right_adjoint_uniq adj2).hom.app (F.obj x) = adj2.unit.app x
@[simp]
theorem category_theory.adjunction.unit_right_adjoint_uniq_hom_app_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G G' : D C} (adj1 : F G) (adj2 : F G') (x : C) {X' : C} (f' : G'.obj (F.obj x) X') :
adj1.unit.app x (adj1.right_adjoint_uniq adj2).hom.app (F.obj x) f' = adj2.unit.app x f'
@[simp]
theorem category_theory.adjunction.unit_right_adjoint_uniq_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G G' : D C} (adj1 : F G) (adj2 : F G') :
@[simp]
theorem category_theory.adjunction.unit_right_adjoint_uniq_hom_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G G' : D C} (adj1 : F G) (adj2 : F G') {X' : C C} (f' : F G' X') :
@[simp]
theorem category_theory.adjunction.right_adjoint_uniq_hom_app_counit_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G G' : D C} (adj1 : F G) (adj2 : F G') (x : D) {X' : D} (f' : (𝟭 D).obj x X') :
F.map ((adj1.right_adjoint_uniq adj2).hom.app x) adj2.counit.app x f' = adj1.counit.app x f'
@[simp]
theorem category_theory.adjunction.right_adjoint_uniq_hom_app_counit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G G' : D C} (adj1 : F G) (adj2 : F G') (x : D) :
F.map ((adj1.right_adjoint_uniq adj2).hom.app x) adj2.counit.app x = adj1.counit.app x
@[simp]
theorem category_theory.adjunction.right_adjoint_uniq_hom_counit {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G G' : D C} (adj1 : F G) (adj2 : F G') :
@[simp]
theorem category_theory.adjunction.right_adjoint_uniq_hom_counit_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G G' : D C} (adj1 : F G) (adj2 : F G') {X' : D D} (f' : 𝟭 D X') :
@[simp]
theorem category_theory.adjunction.right_adjoint_uniq_inv_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G G' : D C} (adj1 : F G) (adj2 : F G') (x : D) :
(adj1.right_adjoint_uniq adj2).inv.app x = (adj2.right_adjoint_uniq adj1).hom.app x
@[simp]
theorem category_theory.adjunction.right_adjoint_uniq_trans_app_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G G' G'' : D C} (adj1 : F G) (adj2 : F G') (adj3 : F G'') (x : D) {X' : C} (f' : G''.obj x X') :
(adj1.right_adjoint_uniq adj2).hom.app x (adj2.right_adjoint_uniq adj3).hom.app x f' = (adj1.right_adjoint_uniq adj3).hom.app x f'
@[simp]
theorem category_theory.adjunction.right_adjoint_uniq_trans_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G G' G'' : D C} (adj1 : F G) (adj2 : F G') (adj3 : F G'') (x : D) :
(adj1.right_adjoint_uniq adj2).hom.app x (adj2.right_adjoint_uniq adj3).hom.app x = (adj1.right_adjoint_uniq adj3).hom.app x
@[simp]
theorem category_theory.adjunction.right_adjoint_uniq_trans {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G G' G'' : D C} (adj1 : F G) (adj2 : F G') (adj3 : F G'') :
@[simp]
theorem category_theory.adjunction.right_adjoint_uniq_trans_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G G' G'' : D C} (adj1 : F G) (adj2 : F G') (adj3 : F G'') {X' : D C} (f' : G'' X') :
(adj1.right_adjoint_uniq adj2).hom (adj2.right_adjoint_uniq adj3).hom f' = (adj1.right_adjoint_uniq adj3).hom f'
@[simp]
theorem category_theory.adjunction.right_adjoint_uniq_refl {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj1 : F G) :
def category_theory.adjunction.nat_iso_of_left_adjoint_nat_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C D} {G G' : D C} (adj1 : F G) (adj2 : F' G') (l : F F') :
G G'

Given two adjunctions, if the left adjoints are naturally isomorphic, then so are the right adjoints.

Equations
def category_theory.adjunction.nat_iso_of_right_adjoint_nat_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C D} {G G' : D C} (adj1 : F G) (adj2 : F' G') (r : G G') :
F F'

Given two adjunctions, if the right adjoints are naturally isomorphic, then so are the left adjoints.

Equations