Opposite adjunctions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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_counit_app
{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)
(Y : D) :
def
category_theory.adjunction.adjoint_of_op_adjoint_op
{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) :
F ⊣ G
If G.op is adjoint to F.op then F is adjoint to G.
Equations
- category_theory.adjunction.adjoint_of_op_adjoint_op F G h = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : C) (Y : D), ((h.hom_equiv (opposite.op Y) (opposite.op X)).trans (category_theory.op_equiv (opposite.op Y) (F.op.obj (opposite.op X)))).symm.trans (category_theory.op_equiv (G.op.obj (opposite.op Y)) (opposite.op X)), hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}
@[simp]
theorem
category_theory.adjunction.adjoint_of_op_adjoint_op_unit_app
{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) :
def
category_theory.adjunction.adjoint_unop_of_adjoint_op
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(G : Dᵒᵖ ⥤ Cᵒᵖ)
(h : G ⊣ F.op) :
If G is adjoint to F.op then F is adjoint to G.unop.
def
category_theory.adjunction.unop_adjoint_of_op_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : Cᵒᵖ ⥤ Dᵒᵖ)
(G : D ⥤ C)
(h : G.op ⊣ F) :
If G.op is adjoint to F then F.unop is adjoint to G.
def
category_theory.adjunction.unop_adjoint_unop_of_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : Cᵒᵖ ⥤ Dᵒᵖ)
(G : Dᵒᵖ ⥤ Cᵒᵖ)
(h : G ⊣ F) :
If G is adjoint to F then F.unop is adjoint to G.unop.
@[simp]
theorem
category_theory.adjunction.op_adjoint_op_of_adjoint_counit_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(G : D ⥤ C)
(h : G ⊣ F)
(Y : Dᵒᵖ) :
(category_theory.adjunction.op_adjoint_op_of_adjoint F G h).counit.app Y = (h.unit.app (opposite.unop Y)).op
def
category_theory.adjunction.op_adjoint_op_of_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(G : D ⥤ C)
(h : G ⊣ F) :
If G is adjoint to F then F.op is adjoint to G.op.
Equations
- category_theory.adjunction.op_adjoint_op_of_adjoint F G h = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : Cᵒᵖ) (Y : Dᵒᵖ), (category_theory.op_equiv (F.op.obj X) Y).trans ((h.hom_equiv (opposite.unop Y) (opposite.unop X)).symm.trans (category_theory.op_equiv X (opposite.op (G.obj (opposite.unop Y)))).symm), hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}
@[simp]
theorem
category_theory.adjunction.op_adjoint_op_of_adjoint_unit_app
{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ᵒᵖ) :
(category_theory.adjunction.op_adjoint_op_of_adjoint F G h).unit.app X = (h.counit.app (opposite.unop X)).op
def
category_theory.adjunction.adjoint_op_of_adjoint_unop
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : Cᵒᵖ ⥤ Dᵒᵖ)
(G : D ⥤ C)
(h : G ⊣ F.unop) :
If G is adjoint to F.unop then F is adjoint to G.op.
def
category_theory.adjunction.op_adjoint_of_unop_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(G : Dᵒᵖ ⥤ Cᵒᵖ)
(h : G.unop ⊣ F) :
If G.unop is adjoint to F then F.op is adjoint to G.
def
category_theory.adjunction.adjoint_of_unop_adjoint_unop
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : Cᵒᵖ ⥤ Dᵒᵖ)
(G : Dᵒᵖ ⥤ Cᵒᵖ)
(h : G.unop ⊣ F.unop) :
F ⊣ G
If G.unop is adjoint to F.unop then F is adjoint to G.
def
category_theory.adjunction.left_adjoints_coyoneda_equiv
{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) :
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
- adj1.left_adjoints_coyoneda_equiv adj2 = category_theory.nat_iso.of_components (λ (X : Cᵒᵖ), category_theory.nat_iso.of_components (λ (Y : D), ((adj1.hom_equiv (opposite.unop X) Y).trans (adj2.hom_equiv (opposite.unop X) Y).symm).to_iso) _) _
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) :
@[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') :
adj1.unit ≫ category_theory.whisker_right (adj1.left_adjoint_uniq adj2).hom G ≫ f' = adj2.unit ≫ f'
@[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) :
adj1.unit ≫ category_theory.whisker_right (adj1.left_adjoint_uniq adj2).hom G = adj2.unit
@[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') :
@[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) :
@[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') :
category_theory.whisker_left G (adj1.left_adjoint_uniq adj2).hom ≫ adj2.counit ≫ f' = adj1.counit ≫ f'
@[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) :
category_theory.whisker_left G (adj1.left_adjoint_uniq adj2).hom ≫ adj2.counit = adj1.counit
@[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) :
@[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') :
@[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) :
@[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) :
@[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') :
@[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') :
adj1.unit ≫ category_theory.whisker_left F (adj1.right_adjoint_uniq adj2).hom = adj2.unit
@[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') :
adj1.unit ≫ category_theory.whisker_left F (adj1.right_adjoint_uniq adj2).hom ≫ f' = adj2.unit ≫ f'
@[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') :
@[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) :
@[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') :
category_theory.whisker_right (adj1.right_adjoint_uniq adj2).hom F ≫ adj2.counit = adj1.counit
@[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') :
category_theory.whisker_right (adj1.right_adjoint_uniq adj2).hom F ≫ adj2.counit ≫ f' = adj1.counit ≫ f'
@[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'') :
(adj1.right_adjoint_uniq adj2).hom ≫ (adj2.right_adjoint_uniq adj3).hom = (adj1.right_adjoint_uniq adj3).hom
@[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) :
(adj1.right_adjoint_uniq adj1).hom = 𝟙 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
- adj1.nat_iso_of_left_adjoint_nat_iso adj2 l = adj1.right_adjoint_uniq (adj2.of_nat_iso_left l.symm)
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
- adj1.nat_iso_of_right_adjoint_nat_iso adj2 r = adj1.left_adjoint_uniq (adj2.of_nat_iso_right r.symm)