category_theory.adjunction.opposites

@[simp]

theorem adjunction.adjoint_of_op_adjoint_op_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.op ⊣ F.op) (X : C) (Y : D) (ᾰ : opposite.unop (F.op.obj (opposite.op X)) ⟶ opposite.unop (opposite.op Y)) :

⇑((adjunction.adjoint_of_op_adjoint_op F G h).hom_equiv X Y) ᾰ = (h.counit.app (opposite.op X)).unop ≫ G.map ᾰ

source

@[simp]

theorem 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) :

⇑(((adjunction.adjoint_of_op_adjoint_op F G h).hom_equiv X Y).symm) ᾰ = F.map ᾰ ≫ (h.unit.app (opposite.op Y)).unop

source

@[simp]

theorem 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) :

(adjunction.adjoint_of_op_adjoint_op F G h).counit.app Y = F.map (𝟙 (G.obj Y)) ≫ (h.unit.app (opposite.op Y)).unop

source

@[simp]

theorem 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) :

(adjunction.adjoint_of_op_adjoint_op F G h).unit.app X = (h.counit.app (opposite.op X)).unop ≫ G.map (𝟙 (F.obj X))

source

def 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

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' := _}

source

def 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) :

F ⊣ G.unop

If G is adjoint to F.op then F is adjoint to G.unop.

Equations

adjunction.adjoint_unop_of_adjoint_op F G h = adjunction.adjoint_of_op_adjoint_op F G.unop (h.of_nat_iso_left G.op_unop_iso.symm)

source

def 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) :

F.unop ⊣ G

If G.op is adjoint to F then F.unop is adjoint to G.

Equations

adjunction.unop_adjoint_of_op_adjoint F G h = adjunction.adjoint_of_op_adjoint_op F.unop G (h.of_nat_iso_right F.op_unop_iso.symm)

source

def 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) :

F.unop ⊣ G.unop

If G is adjoint to F then F.unop is adjoint to G.unop.

Equations

adjunction.unop_adjoint_unop_of_adjoint F G h = adjunction.adjoint_unop_of_adjoint_op F.unop G (h.of_nat_iso_right F.op_unop_iso.symm)

source

@[simp]

theorem 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ᵒᵖ) :

(adjunction.op_adjoint_op_of_adjoint F G h).counit.app Y = (h.unit.app (opposite.unop Y)).op

source

@[simp]

theorem 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ᵒᵖ) :

(adjunction.op_adjoint_op_of_adjoint F G h).unit.app X = (h.counit.app (opposite.unop X)).op

source

@[simp]

theorem 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) :

⇑((adjunction.op_adjoint_op_of_adjoint F G h).hom_equiv X Y) ᾰ = (h.counit.app (opposite.unop X)).op ≫ (G.map ᾰ.unop).op

source

@[simp]

theorem 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) :

⇑(((adjunction.op_adjoint_op_of_adjoint F G h).hom_equiv X Y).symm) ᾰ = (F.map ᾰ.unop).op ≫ (h.unit.app (opposite.unop Y)).op

source

def 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) :

F.op ⊣ G.op

If G is adjoint to F then F.op is adjoint to G.op.

Equations

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' := _}

source

def 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) :

F ⊣ G.op

If G is adjoint to F.unop then F is adjoint to G.op.

Equations

adjunction.adjoint_op_of_adjoint_unop F G h = (adjunction.op_adjoint_op_of_adjoint F.unop G h).of_nat_iso_left F.op_unop_iso

source

def 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) :

F.op ⊣ G

If G.unop is adjoint to F then F.op is adjoint to G.

Equations

adjunction.op_adjoint_of_unop_adjoint F G h = (adjunction.op_adjoint_op_of_adjoint F G.unop h).of_nat_iso_right G.op_unop_iso

source

def 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.

Equations

adjunction.adjoint_of_unop_adjoint_unop F G h = (adjunction.adjoint_op_of_adjoint_unop F G.unop h).of_nat_iso_right G.op_unop_iso

source

def 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) :

F.op ⋙ category_theory.coyoneda ≅ F'.op ⋙ category_theory.coyoneda

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

adjunction.left_adjoints_coyoneda_equiv adj1 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) _) _

source

def 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

adjunction.left_adjoint_uniq adj1 adj2 = category_theory.nat_iso.remove_op (category_theory.fully_faithful_cancel_right category_theory.coyoneda (adjunction.left_adjoints_coyoneda_equiv adj2 adj1))

source

@[simp]

theorem 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)) ((adjunction.left_adjoint_uniq adj1 adj2).hom.app x) = adj2.unit.app x

source

@[simp]

theorem 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 (adjunction.left_adjoint_uniq adj1 adj2).hom G ≫ f' = adj2.unit ≫ f'

source

@[simp]

theorem 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 (adjunction.left_adjoint_uniq adj1 adj2).hom G = adj2.unit

source

@[simp]

theorem 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 ((adjunction.left_adjoint_uniq adj1 adj2).hom.app x) = adj2.unit.app x

source

@[simp]

theorem 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 ((adjunction.left_adjoint_uniq adj1 adj2).hom.app x) ≫ f' = adj2.unit.app x ≫ f'

source

@[simp]

theorem 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 (adjunction.left_adjoint_uniq adj1 adj2).hom ≫ adj2.counit ≫ f' = adj1.counit ≫ f'

source

@[simp]

theorem 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 (adjunction.left_adjoint_uniq adj1 adj2).hom ≫ adj2.counit = adj1.counit

source

@[simp]

theorem 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') :

(adjunction.left_adjoint_uniq adj1 adj2).hom.app (G.obj x) ≫ adj2.counit.app x ≫ f' = adj1.counit.app x ≫ f'

source

@[simp]

theorem 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) :

(adjunction.left_adjoint_uniq adj1 adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x

source

@[simp]

theorem 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) :

(adjunction.left_adjoint_uniq adj1 adj2).inv.app x = (adjunction.left_adjoint_uniq adj2 adj1).hom.app x

source

@[simp]

theorem 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) :

(adjunction.left_adjoint_uniq adj1 adj2).hom ≫ (adjunction.left_adjoint_uniq adj2 adj3).hom = (adjunction.left_adjoint_uniq adj1 adj3).hom

source

@[simp]

theorem 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') :

(adjunction.left_adjoint_uniq adj1 adj2).hom ≫ (adjunction.left_adjoint_uniq adj2 adj3).hom ≫ f' = (adjunction.left_adjoint_uniq adj1 adj3).hom ≫ f'

source

@[simp]

theorem 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') :

(adjunction.left_adjoint_uniq adj1 adj2).hom.app x ≫ (adjunction.left_adjoint_uniq adj2 adj3).hom.app x ≫ f' = (adjunction.left_adjoint_uniq adj1 adj3).hom.app x ≫ f'

source

@[simp]

theorem 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) :

(adjunction.left_adjoint_uniq adj1 adj2).hom.app x ≫ (adjunction.left_adjoint_uniq adj2 adj3).hom.app x = (adjunction.left_adjoint_uniq adj1 adj3).hom.app x

source

@[simp]

theorem 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) :

(adjunction.left_adjoint_uniq adj1 adj1).hom = 𝟙 F

source

def 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

adjunction.right_adjoint_uniq adj1 adj2 = category_theory.nat_iso.remove_op (adjunction.left_adjoint_uniq (adjunction.op_adjoint_op_of_adjoint G' F adj2) (adjunction.op_adjoint_op_of_adjoint G F adj1))

source

@[simp]

theorem 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) ((adjunction.right_adjoint_uniq adj1 adj2).hom.app x) = adj1.counit.app x

source

@[simp]

theorem 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 ≫ (adjunction.right_adjoint_uniq adj1 adj2).hom.app (F.obj x) ≫ f' = adj2.unit.app x ≫ f'

source

@[simp]

theorem 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 ≫ (adjunction.right_adjoint_uniq adj1 adj2).hom.app (F.obj x) = adj2.unit.app x

source

@[simp]

theorem 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 (adjunction.right_adjoint_uniq adj1 adj2).hom = adj2.unit

source

@[simp]

theorem 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 (adjunction.right_adjoint_uniq adj1 adj2).hom ≫ f' = adj2.unit ≫ f'

source

@[simp]

theorem 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 ((adjunction.right_adjoint_uniq adj1 adj2).hom.app x) ≫ adj2.counit.app x = adj1.counit.app x

source

@[simp]

theorem 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 ((adjunction.right_adjoint_uniq adj1 adj2).hom.app x) ≫ adj2.counit.app x ≫ f' = adj1.counit.app x ≫ f'

source

@[simp]

theorem 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 (adjunction.right_adjoint_uniq adj1 adj2).hom F ≫ adj2.counit ≫ f' = adj1.counit ≫ f'

source

@[simp]

theorem 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 (adjunction.right_adjoint_uniq adj1 adj2).hom F ≫ adj2.counit = adj1.counit

source

@[simp]

theorem 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) :

(adjunction.right_adjoint_uniq adj1 adj2).inv.app x = (adjunction.right_adjoint_uniq adj2 adj1).hom.app x

source

@[simp]

theorem 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) :

(adjunction.right_adjoint_uniq adj1 adj2).hom.app x ≫ (adjunction.right_adjoint_uniq adj2 adj3).hom.app x = (adjunction.right_adjoint_uniq adj1 adj3).hom.app x

source

@[simp]

theorem 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') :

(adjunction.right_adjoint_uniq adj1 adj2).hom.app x ≫ (adjunction.right_adjoint_uniq adj2 adj3).hom.app x ≫ f' = (adjunction.right_adjoint_uniq adj1 adj3).hom.app x ≫ f'

source

@[simp]

theorem 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'') :

(adjunction.right_adjoint_uniq adj1 adj2).hom ≫ (adjunction.right_adjoint_uniq adj2 adj3).hom = (adjunction.right_adjoint_uniq adj1 adj3).hom

source

@[simp]

theorem 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') :

(adjunction.right_adjoint_uniq adj1 adj2).hom ≫ (adjunction.right_adjoint_uniq adj2 adj3).hom ≫ f' = (adjunction.right_adjoint_uniq adj1 adj3).hom ≫ f'

source

@[simp]

theorem 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) :

(adjunction.right_adjoint_uniq adj1 adj1).hom = 𝟙 G

source

def 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

adjunction.nat_iso_of_left_adjoint_nat_iso adj1 adj2 l = adjunction.right_adjoint_uniq adj1 (adj2.of_nat_iso_left l.symm)

source

def 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

adjunction.nat_iso_of_right_adjoint_nat_iso adj1 adj2 r = adjunction.left_adjoint_uniq adj1 (adj2.of_nat_iso_right r.symm)

mathlib documentation

Opposite adjunctions #

Tags #