Opposite adjunctions #

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

Tags #

adjunction, opposite, uniqueness

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

h.unop = { unit := CategoryTheory.NatTrans.unop h.counit, counit := CategoryTheory.NatTrans.unop h.unit, left_triangle_components := ⋯, right_triangle_components := ⋯ }

Instances For

source

@[simp]

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

h.unop.counit = NatTrans.unop h.unit

source

@[simp]

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

h.unop.unit = NatTrans.unop h.counit

source

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

h.op = { unit := CategoryTheory.NatTrans.op h.counit, counit := CategoryTheory.NatTrans.op h.unit, left_triangle_components := ⋯, right_triangle_components := ⋯ }

Instances For

source

@[simp]

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

h.op.unit = NatTrans.op h.counit

source

@[simp]

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

h.op.counit = NatTrans.op h.unit

source

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

G ⊣ F.leftOp

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

Equations

a.leftOp = { unit := CategoryTheory.NatTrans.unop a.counit, counit := CategoryTheory.NatTrans.op a.unit, left_triangle_components := ⋯, right_triangle_components := ⋯ }

Instances For

source

@[simp]

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

a.leftOp.counit = NatTrans.op a.unit

source

@[simp]

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

a.leftOp.unit = NatTrans.unop a.counit

source

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

G.rightOp ⊣ F

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

Equations

a.rightOp = { unit := CategoryTheory.NatTrans.unop a.counit, counit := CategoryTheory.NatTrans.op a.unit, left_triangle_components := ⋯, right_triangle_components := ⋯ }

Instances For

source

@[simp]

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

a.rightOp.counit = NatTrans.op a.unit

source

@[simp]

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

a.rightOp.unit = NatTrans.unop a.counit

source

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

a.leftOp = (opOpEquivalence D).symm.toAdjunction.comp a.op

source

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

a.rightOp = (opOpEquivalence D).symm.toAdjunction.comp a.op

source

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

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

Instances For

source

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