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 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.toPrefunctor.obj (G.toPrefunctor.obj Y)))) ((h.homEquiv (Opposite.op Y) (Opposite.op (G.toPrefunctor.obj Y))) ((CategoryTheory.opEquiv (Opposite.op (G.toPrefunctor.obj Y)) (Opposite.op (G.toPrefunctor.obj Y))).symm (CategoryTheory.CategoryStruct.id (G.toPrefunctor.obj Y))))

@[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.toPrefunctor.obj (F.toPrefunctor.obj X))) (Opposite.op X)) ((h.homEquiv (Opposite.op (F.toPrefunctor.obj X)) (Opposite.op X)).symm ((CategoryTheory.opEquiv (Opposite.op (F.toPrefunctor.obj X)) (Opposite.op (F.toPrefunctor.obj X))).symm (CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X))))

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

@[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.toPrefunctor.obj X.unop)))).symm (CategoryTheory.CategoryStruct.comp (G.toPrefunctor.map ((CategoryTheory.opEquiv (Opposite.op (F.toPrefunctor.obj X.unop)) (Opposite.op (F.toPrefunctor.obj X.unop))) (CategoryTheory.CategoryStruct.id (Opposite.op (F.toPrefunctor.obj X.unop))))) (h.counit.app X.unop))

@[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.toPrefunctor.obj (G.toPrefunctor.obj Y.unop))) Y).symm (CategoryTheory.CategoryStruct.comp (h.unit.app Y.unop) (F.toPrefunctor.map ((CategoryTheory.opEquiv (Opposite.op (G.toPrefunctor.obj Y.unop)) (Opposite.op (G.toPrefunctor.1 Y.unop))) (CategoryTheory.CategoryStruct.id (Opposite.op (G.toPrefunctor.obj Y.unop))))))

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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) : (adj1.homEquiv x (F'.toPrefunctor.obj x)) ((CategoryTheory.Adjunction.leftAdjointUniq adj1 adj2).hom.app x) = adj2.unit.app x

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

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

@[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.toPrefunctor.obj (F'.toPrefunctor.obj x) ⟶ Z) : CategoryTheory.CategoryStruct.comp (adj1.unit.app x) (CategoryTheory.CategoryStruct.comp (G.toPrefunctor.map ((CategoryTheory.Adjunction.leftAdjointUniq adj1 adj2).hom.app x)) h) = CategoryTheory.CategoryStruct.comp (adj2.unit.app x) h

@[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.toPrefunctor.map ((CategoryTheory.Adjunction.leftAdjointUniq adj1 adj2).hom.app x)) = adj2.unit.app x

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

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

@[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 : x ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.leftAdjointUniq adj1 adj2).hom.app (G.toPrefunctor.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₁} [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.toPrefunctor.obj x)) (adj2.counit.app x) = adj1.counit.app x

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

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

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

@[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''.toPrefunctor.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

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

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

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.

Equations

• One or more equations did not get rendered due to their size.

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) : (adj2.homEquiv (G.toPrefunctor.obj x) x).symm ((CategoryTheory.Adjunction.rightAdjointUniq adj1 adj2).hom.app x) = adj1.counit.app x

@[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'.toPrefunctor.obj (F.toPrefunctor.obj x) ⟶ Z) : CategoryTheory.CategoryStruct.comp (adj1.unit.app x) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.rightAdjointUniq adj1 adj2).hom.app (F.toPrefunctor.obj x)) h) = CategoryTheory.CategoryStruct.comp (adj2.unit.app x) h

@[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.toPrefunctor.obj x)) = adj2.unit.app x

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

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

@[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 : x ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.toPrefunctor.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

@[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.toPrefunctor.map ((CategoryTheory.Adjunction.rightAdjointUniq adj1 adj2).hom.app x)) (adj2.counit.app x) = adj1.counit.app x

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

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

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

@[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''.toPrefunctor.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

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

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

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

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

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.

Equations

• CategoryTheory.Adjunction.natIsoOfLeftAdjointNatIso adj1 adj2 l = CategoryTheory.Adjunction.rightAdjointUniq adj1 (CategoryTheory.Adjunction.ofNatIsoLeft adj2 l.symm)

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.

Equations

• CategoryTheory.Adjunction.natIsoOfRightAdjointNatIso adj1 adj2 r = CategoryTheory.Adjunction.leftAdjointUniq adj1 (CategoryTheory.Adjunction.ofNatIsoRight adj2 r.symm)