Documentation

Mathlib.CategoryTheory.Adjunction.Opposites

Opposite adjunctions #

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

Tags #

adjunction, opposite, uniqueness

source
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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Adjunction.unop_unit_app {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) (X : C) :
    h.unop.unit.app X = (h.counit.app (Opposite.op X)).unop
    source
    @[simp]
    theorem CategoryTheory.Adjunction.unop_counit_app {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) (X : D) :
    h.unop.counit.app X = (h.unit.app (Opposite.op X)).unop
    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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Adjunction.op_unit_app {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) (X : Cᵒᵖ) :
      h.op.unit.app X = (h.counit.app (Opposite.unop X)).op
      source
      @[simp]
      theorem CategoryTheory.Adjunction.op_counit_app {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) (X : Dᵒᵖ) :
      h.op.counit.app X = (h.unit.app (Opposite.unop X)).op
      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
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Adjunction.leftOp_counit_app {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) (X : Cᵒᵖ) :
        a.leftOp.counit.app X = (a.unit.app (Opposite.unop X)).op
        source
        @[simp]
        theorem CategoryTheory.Adjunction.leftOp_unit_app {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) (X : D) :
        a.leftOp.unit.app X = (a.counit.app (Opposite.op X)).unop
        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
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Adjunction.rightOp_unit_app {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) (X : D) :
          a.rightOp.unit.app X = (a.counit.app (Opposite.op X)).unop
          source
          @[simp]
          theorem CategoryTheory.Adjunction.rightOp_counit_app {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) (X : Cᵒᵖ) :
          a.rightOp.counit.app X = (a.unit.app (Opposite.unop X)).op
          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
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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