Opposite adjunctions

This file contains constructions to relate adjunctions of functors to adjunctions of their opposites.

Tags

adjunction, opposite, uniqueness

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.

@[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)))) ((h.homEquiv (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))))

@[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)) ((h.homEquiv (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))))

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 ⊣ G.unop

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

Equations

• CategoryTheory.Adjunction.adjointUnopOfAdjointOp F G h = CategoryTheory.Adjunction.adjointOfOpAdjointOp F G.unop (h.ofNatIsoLeft G.opUnopIso.symm)

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) : F.unop ⊣ G

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

Equations

• CategoryTheory.Adjunction.unopAdjointOfOpAdjoint F G h = CategoryTheory.Adjunction.adjointOfOpAdjointOp F.unop G (h.ofNatIsoRight F.opUnopIso.symm)

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) : F.unop ⊣ G.unop

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

Equations

• CategoryTheory.Adjunction.unopAdjointUnopOfAdjoint F G h = CategoryTheory.Adjunction.adjointUnopOfAdjointOp F.unop G (h.ofNatIsoRight F.opUnopIso.symm)

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.

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

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

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 ⊣ F.unop) : F ⊣ G.op

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

Equations

• CategoryTheory.Adjunction.adjointOpOfAdjointUnop F G h = (CategoryTheory.Adjunction.opAdjointOpOfAdjoint F.unop G h).ofNatIsoLeft F.opUnopIso

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 : G.unop ⊣ F) : F.op ⊣ G

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

Equations

• CategoryTheory.Adjunction.opAdjointOfUnopAdjoint F G h = (CategoryTheory.Adjunction.opAdjointOpOfAdjoint F G.unop h).ofNatIsoRight G.opUnopIso

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 : G.unop ⊣ F.unop) : F ⊣ G

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

Equations

• CategoryTheory.Adjunction.adjointOfUnopAdjointUnop F G h = (CategoryTheory.Adjunction.adjointOpOfAdjointUnop F G.unop h).ofNatIsoRight G.opUnopIso

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) : F.op.comp CategoryTheory.coyoneda ≅ F'.op.comp 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.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.

Note: it is generally better to use Adjunction.natIsoEquiv, see the file Adjunction.Unique. The reason this definition still exists is that apparently CategoryTheory.extendAlongYonedaYoneda uses its definitional properties (TODO: figure out a way to avoid this).

Equations

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

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.

Note: it is generally better to use Adjunction.natIsoEquiv, see the file Adjunction.Unique.

Equations

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