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

source

@[simp]

theorem CategoryTheory.Adjunction.adjointOfOpAdjointOp_counit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) (h : G.op ⊣ F.op) (Y : D) :

(CategoryTheory.Adjunction.adjointOfOpAdjointOp F G h).counit.app Y = ↑(CategoryTheory.opEquiv (Opposite.op Y) (Opposite.op (F.obj (G.obj Y)))) (↑(CategoryTheory.Adjunction.homEquiv h (Opposite.op Y) (Opposite.op (G.obj Y))) (↑(CategoryTheory.opEquiv (Opposite.op (G.obj Y)) (Opposite.op (G.obj Y))).symm (CategoryTheory.CategoryStruct.id (G.obj Y))))

source

@[simp]

theorem CategoryTheory.Adjunction.adjointOfOpAdjointOp_unit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) (h : G.op ⊣ F.op) (X : C) :

(CategoryTheory.Adjunction.adjointOfOpAdjointOp F G h).unit.app X = ↑(CategoryTheory.opEquiv (Opposite.op (G.obj (F.obj X))) (Opposite.op X)) (↑(CategoryTheory.Adjunction.homEquiv h (Opposite.op (F.obj X)) (Opposite.op X)).symm (↑(CategoryTheory.opEquiv (Opposite.op (F.obj X)) (Opposite.op (F.obj X))).symm (CategoryTheory.CategoryStruct.id (F.obj X))))

source

def CategoryTheory.Adjunction.adjointOfOpAdjointOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) (h : G.op ⊣ F.op) :

F ⊣ G

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

Instances For

source

def CategoryTheory.Adjunction.adjointUnopOfAdjointOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor Dᵒᵖ Cᵒᵖ) (h : G ⊣ F.op) :

F ⊣ CategoryTheory.Functor.unop G

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

Instances For

source

def CategoryTheory.Adjunction.unopAdjointOfOpAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (G : CategoryTheory.Functor D C) (h : G.op ⊣ F) :

CategoryTheory.Functor.unop F ⊣ G

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

Instances For

source

def CategoryTheory.Adjunction.unopAdjointUnopOfAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (G : CategoryTheory.Functor Dᵒᵖ Cᵒᵖ) (h : G ⊣ F) :

CategoryTheory.Functor.unop F ⊣ CategoryTheory.Functor.unop G

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

Instances For

source

@[simp]

theorem CategoryTheory.Adjunction.opAdjointOpOfAdjoint_unit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) (h : G ⊣ F) (X : Cᵒᵖ) :

(CategoryTheory.Adjunction.opAdjointOpOfAdjoint F G h).unit.app X = ↑(CategoryTheory.opEquiv X (Opposite.op (G.toPrefunctor.1 (F.obj X.unop)))).symm (CategoryTheory.CategoryStruct.comp (G.map (↑(CategoryTheory.opEquiv (Opposite.op (F.obj X.unop)) (Opposite.op (F.obj X.unop))) (CategoryTheory.CategoryStruct.id (Opposite.op (F.obj X.unop))))) (h.counit.app X.unop))

source

@[simp]

theorem CategoryTheory.Adjunction.opAdjointOpOfAdjoint_counit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) (h : G ⊣ F) (Y : Dᵒᵖ) :

(CategoryTheory.Adjunction.opAdjointOpOfAdjoint F G h).counit.app Y = ↑(CategoryTheory.opEquiv (Opposite.op (F.obj (G.obj Y.unop))) Y).symm (CategoryTheory.CategoryStruct.comp (h.unit.app Y.unop) (F.map (↑(CategoryTheory.opEquiv (Opposite.op (G.obj Y.unop)) (Opposite.op (G.toPrefunctor.1 Y.unop))) (CategoryTheory.CategoryStruct.id (Opposite.op (G.obj Y.unop))))))

source

def CategoryTheory.Adjunction.opAdjointOpOfAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D C) (h : G ⊣ F) :

F.op ⊣ G.op

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

Instances For

source

def CategoryTheory.Adjunction.adjointOpOfAdjointUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (G : CategoryTheory.Functor D C) (h : G ⊣ CategoryTheory.Functor.unop F) :

F ⊣ G.op

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

Instances For

source

def CategoryTheory.Adjunction.opAdjointOfUnopAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor Dᵒᵖ Cᵒᵖ) (h : CategoryTheory.Functor.unop G ⊣ F) :

F.op ⊣ G

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

Instances For

source

def CategoryTheory.Adjunction.adjointOfUnopAdjointUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (G : CategoryTheory.Functor Dᵒᵖ Cᵒᵖ) (h : CategoryTheory.Functor.unop G ⊣ CategoryTheory.Functor.unop F) :

F ⊣ G

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

Instances For

source

def CategoryTheory.Adjunction.leftAdjointsCoyonedaEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :

CategoryTheory.Functor.comp F.op CategoryTheory.coyoneda ≅ CategoryTheory.Functor.comp F'.op CategoryTheory.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 fullyFaithfulCancelRight to show left adjoints are unique.

Instances For

source

def CategoryTheory.Adjunction.leftAdjointUniq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {F' : CategoryTheory.Functor C D} {G : CategoryTheory.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.

Instances For

source

theorem CategoryTheory.Adjunction.homEquiv_leftAdjointUniq_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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.Adjunction.homEquiv adj1 x (F'.obj x)) ((CategoryTheory.Adjunction.leftAdjointUniq adj1 adj2).hom.app x) = adj2.unit.app x

source

@[simp]

theorem CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) {Z : CategoryTheory.Functor C C} (h : CategoryTheory.Functor.comp F' G ⟶ Z) :

CategoryTheory.CategoryStruct.comp adj1.unit (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.Adjunction.leftAdjointUniq adj1 adj2).hom G) h) = CategoryTheory.CategoryStruct.comp adj2.unit h

source

@[simp]

theorem CategoryTheory.Adjunction.unit_leftAdjointUniq_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :

CategoryTheory.CategoryStruct.comp adj1.unit (CategoryTheory.whiskerRight (CategoryTheory.Adjunction.leftAdjointUniq adj1 adj2).hom G) = adj2.unit

source

@[simp]

theorem CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_app_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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 ((CategoryTheory.Adjunction.leftAdjointUniq adj1 adj2).hom.app x)) h) = CategoryTheory.CategoryStruct.comp (adj2.unit.app x) h

source

@[simp]

theorem CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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 ((CategoryTheory.Adjunction.leftAdjointUniq adj1 adj2).hom.app x)) = adj2.unit.app x

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_hom_counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) {Z : CategoryTheory.Functor D D} (h : CategoryTheory.Functor.id D ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft G (CategoryTheory.Adjunction.leftAdjointUniq adj1 adj2).hom) (CategoryTheory.CategoryStruct.comp adj2.counit h) = CategoryTheory.CategoryStruct.comp adj1.counit h

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_hom_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft G (CategoryTheory.Adjunction.leftAdjointUniq adj1 adj2).hom) adj2.counit = adj1.counit

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_hom_app_counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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 : (CategoryTheory.Functor.id D).obj x ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.leftAdjointUniq adj1 adj2).hom.app (G.obj x)) (CategoryTheory.CategoryStruct.comp (adj2.counit.app x) h) = CategoryTheory.CategoryStruct.comp (adj1.counit.app x) h

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_hom_app_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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 ((CategoryTheory.Adjunction.leftAdjointUniq adj1 adj2).hom.app (G.obj x)) (adj2.counit.app x) = adj1.counit.app x

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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.Adjunction.leftAdjointUniq adj1 adj2).inv.app x = (CategoryTheory.Adjunction.leftAdjointUniq adj2 adj1).hom.app x

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_trans_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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 (CategoryTheory.Adjunction.leftAdjointUniq adj1 adj2).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Adjunction.leftAdjointUniq adj2 adj3).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Adjunction.leftAdjointUniq adj1 adj3).hom h

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_trans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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 (CategoryTheory.Adjunction.leftAdjointUniq adj1 adj2).hom (CategoryTheory.Adjunction.leftAdjointUniq adj2 adj3).hom = (CategoryTheory.Adjunction.leftAdjointUniq adj1 adj3).hom

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_trans_app_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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 ((CategoryTheory.Adjunction.leftAdjointUniq adj1 adj2).hom.app x) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.leftAdjointUniq adj2 adj3).hom.app x) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.leftAdjointUniq adj1 adj3).hom.app x) h

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_trans_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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 ((CategoryTheory.Adjunction.leftAdjointUniq adj1 adj2).hom.app x) ((CategoryTheory.Adjunction.leftAdjointUniq adj2 adj3).hom.app x) = (CategoryTheory.Adjunction.leftAdjointUniq adj1 adj3).hom.app x

source

@[simp]

theorem CategoryTheory.Adjunction.leftAdjointUniq_refl {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) :

(CategoryTheory.Adjunction.leftAdjointUniq adj1 adj1).hom = CategoryTheory.CategoryStruct.id F

source

def CategoryTheory.Adjunction.rightAdjointUniq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {G' : CategoryTheory.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.

Instances For

source

theorem CategoryTheory.Adjunction.homEquiv_symm_rightAdjointUniq_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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.Adjunction.homEquiv adj2 (G.obj x) x).symm ((CategoryTheory.Adjunction.rightAdjointUniq adj1 adj2).hom.app x) = adj1.counit.app x

source

@[simp]

theorem CategoryTheory.Adjunction.unit_rightAdjointUniq_hom_app_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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 ((CategoryTheory.Adjunction.rightAdjointUniq adj1 adj2).hom.app (F.obj x)) h) = CategoryTheory.CategoryStruct.comp (adj2.unit.app x) h

source

@[simp]

theorem CategoryTheory.Adjunction.unit_rightAdjointUniq_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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) ((CategoryTheory.Adjunction.rightAdjointUniq adj1 adj2).hom.app (F.obj x)) = adj2.unit.app x

source

@[simp]

theorem CategoryTheory.Adjunction.unit_rightAdjointUniq_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') {Z : CategoryTheory.Functor C C} (h : CategoryTheory.Functor.comp F G' ⟶ Z) :

CategoryTheory.CategoryStruct.comp adj1.unit (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft F (CategoryTheory.Adjunction.rightAdjointUniq adj1 adj2).hom) h) = CategoryTheory.CategoryStruct.comp adj2.unit h

source

@[simp]

theorem CategoryTheory.Adjunction.unit_rightAdjointUniq_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :

CategoryTheory.CategoryStruct.comp adj1.unit (CategoryTheory.whiskerLeft F (CategoryTheory.Adjunction.rightAdjointUniq adj1 adj2).hom) = adj2.unit

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_hom_app_counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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 : (CategoryTheory.Functor.id D).obj x ⟶ Z) :

CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Adjunction.rightAdjointUniq adj1 adj2).hom.app x)) (CategoryTheory.CategoryStruct.comp (adj2.counit.app x) h) = CategoryTheory.CategoryStruct.comp (adj1.counit.app x) h

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_hom_app_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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 ((CategoryTheory.Adjunction.rightAdjointUniq adj1 adj2).hom.app x)) (adj2.counit.app x) = adj1.counit.app x

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_hom_counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') {Z : CategoryTheory.Functor D D} (h : CategoryTheory.Functor.id D ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.Adjunction.rightAdjointUniq adj1 adj2).hom F) (CategoryTheory.CategoryStruct.comp adj2.counit h) = CategoryTheory.CategoryStruct.comp adj1.counit h

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_hom_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {G' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') :

CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.Adjunction.rightAdjointUniq adj1 adj2).hom F) adj2.counit = adj1.counit

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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.Adjunction.rightAdjointUniq adj1 adj2).inv.app x = (CategoryTheory.Adjunction.rightAdjointUniq adj2 adj1).hom.app x

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_trans_app_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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 ((CategoryTheory.Adjunction.rightAdjointUniq adj1 adj2).hom.app x) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.rightAdjointUniq adj2 adj3).hom.app x) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.rightAdjointUniq adj1 adj3).hom.app x) h

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_trans_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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 ((CategoryTheory.Adjunction.rightAdjointUniq adj1 adj2).hom.app x) ((CategoryTheory.Adjunction.rightAdjointUniq adj2 adj3).hom.app x) = (CategoryTheory.Adjunction.rightAdjointUniq adj1 adj3).hom.app x

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_trans_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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 (CategoryTheory.Adjunction.rightAdjointUniq adj1 adj2).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Adjunction.rightAdjointUniq adj2 adj3).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Adjunction.rightAdjointUniq adj1 adj3).hom h

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_trans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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 (CategoryTheory.Adjunction.rightAdjointUniq adj1 adj2).hom (CategoryTheory.Adjunction.rightAdjointUniq adj2 adj3).hom = (CategoryTheory.Adjunction.rightAdjointUniq adj1 adj3).hom

source

@[simp]

theorem CategoryTheory.Adjunction.rightAdjointUniq_refl {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj1 : F ⊣ G) :

(CategoryTheory.Adjunction.rightAdjointUniq adj1 adj1).hom = CategoryTheory.CategoryStruct.id G

source

def CategoryTheory.Adjunction.natIsoOfLeftAdjointNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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') (l : F ≅ F') :

G ≅ G'

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

Instances For

source

def CategoryTheory.Adjunction.natIsoOfRightAdjointNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} 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') (r : G ≅ G') :

F ≅ F'

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

Instances For