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 := ⋯ }

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

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

@[deprecated CategoryTheory.Adjunction.unop (since := "2025-01-01")]

def CategoryTheory.Adjunction.adjointOfOpAdjointOp {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

Alias of CategoryTheory.Adjunction.unop.

---

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

Equations

• @CategoryTheory.Adjunction.adjointOfOpAdjointOp = @CategoryTheory.Adjunction.unop

@[deprecated CategoryTheory.Adjunction.unop (since := "2025-01-01")]

def CategoryTheory.Adjunction.adjointUnopOfAdjointOp {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

Alias of CategoryTheory.Adjunction.unop.

---

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

Equations

• @CategoryTheory.Adjunction.adjointUnopOfAdjointOp = @CategoryTheory.Adjunction.unop

@[deprecated CategoryTheory.Adjunction.unop (since := "2025-01-01")]

def CategoryTheory.Adjunction.unopAdjointOfOpAdjoint {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

Alias of CategoryTheory.Adjunction.unop.

---

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

Equations

• @CategoryTheory.Adjunction.unopAdjointOfOpAdjoint = @CategoryTheory.Adjunction.unop

@[deprecated CategoryTheory.Adjunction.unop (since := "2025-01-01")]

def CategoryTheory.Adjunction.unopAdjointUnopOfAdjoint {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

Alias of CategoryTheory.Adjunction.unop.

---

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

Equations

• @CategoryTheory.Adjunction.unopAdjointUnopOfAdjoint = @CategoryTheory.Adjunction.unop

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 := ⋯ }

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

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

@[deprecated CategoryTheory.Adjunction.op (since := "2025-01-01")]

def CategoryTheory.Adjunction.opAdjointOpOfAdjoint {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

Alias of CategoryTheory.Adjunction.op.

---

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

Equations

• @CategoryTheory.Adjunction.opAdjointOpOfAdjoint = @CategoryTheory.Adjunction.op

@[deprecated CategoryTheory.Adjunction.op (since := "2025-01-01")]

def CategoryTheory.Adjunction.adjointOpOfAdjointUnop {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

Alias of CategoryTheory.Adjunction.op.

---

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

Equations

• @CategoryTheory.Adjunction.adjointOpOfAdjointUnop = @CategoryTheory.Adjunction.op

@[deprecated CategoryTheory.Adjunction.op (since := "2025-01-01")]

def CategoryTheory.Adjunction.opAdjointOfUnopAdjoint {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

Alias of CategoryTheory.Adjunction.op.

---

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

Equations

• @CategoryTheory.Adjunction.opAdjointOfUnopAdjoint = @CategoryTheory.Adjunction.op

@[deprecated CategoryTheory.Adjunction.op (since := "2025-01-01")]

def CategoryTheory.Adjunction.adjointOfUnopAdjointUnop {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

Alias of CategoryTheory.Adjunction.op.

---

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

Equations

• @CategoryTheory.Adjunction.adjointOfUnopAdjointUnop = @CategoryTheory.Adjunction.op

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 := ⋯ }

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

Equations

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

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

Equations

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

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

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

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'

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

• adj1.natIsoOfLeftAdjointNatIso adj2 l = CategoryTheory.NatIso.removeOp (adj2.op.natIsoOfRightAdjointNatIso adj1.op (CategoryTheory.NatIso.op l))