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.

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

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

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.

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

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

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.

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

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

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.

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

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

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

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

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.

@[deprecated "Use `(Adjunction.conjugateIsoEquiv adj1 adj2).symm` (requires `import Mathlib.CategoryTheory.Adjunction.Mates`)." (since := "2026-01-31")]

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'

Deprecated: prefer (Adjunction.conjugateIsoEquiv adj1 adj2).symm.

@[deprecated "Use `Adjunction.conjugateIsoEquiv adj1 adj2` (requires `import Mathlib.CategoryTheory.Adjunction.Mates`)." (since := "2026-01-31")]

def CategoryTheory.Adjunction.natIsoOfLeftAdjointNatIso {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') (l : F ≅ F') : G ≅ G'

Deprecated: prefer Adjunction.conjugateIsoEquiv adj1 adj2.

instance CategoryTheory.Functor.IsLeftAdjoint.op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} [F.IsLeftAdjoint] : F.op.IsRightAdjoint

instance CategoryTheory.Functor.IsRightAdjoint.op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} [F.IsRightAdjoint] : F.op.IsLeftAdjoint

instance CategoryTheory.Functor.IsLeftAdjoint.leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C Dᵒᵖ} [F.IsLeftAdjoint] : F.leftOp.IsRightAdjoint

instance CategoryTheory.Functor.IsRightAdjoint.leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C Dᵒᵖ} [F.IsRightAdjoint] : F.leftOp.IsLeftAdjoint

instance CategoryTheory.Functor.IsLeftAdjoint.rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor Cᵒᵖ D} [F.IsLeftAdjoint] : F.rightOp.IsRightAdjoint

instance CategoryTheory.Functor.IsRightAdjoint.rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor Cᵒᵖ D} [F.IsRightAdjoint] : F.rightOp.IsLeftAdjoint