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

@[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 { unop := G.obj (F.obj X) } { unop := X }) ((h.homEquiv { unop := F.obj X } { unop := X }).symm ((CategoryTheory.opEquiv { unop := F.obj X } { unop := F.obj X }).symm (CategoryTheory.CategoryStruct.id (F.obj X))))
@[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 { unop := Y } { unop := F.obj (G.obj Y) }) ((h.homEquiv { unop := Y } { unop := G.obj Y }) ((CategoryTheory.opEquiv { unop := G.obj Y } { unop := G.obj Y }).symm (CategoryTheory.CategoryStruct.id (G.obj Y))))

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.
Instances For

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

    Equations
    Instances For

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

      Equations
      Instances For

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

        Equations
        Instances For
          @[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 { unop := G.toPrefunctor.1 (F.obj X.unop) }).symm (CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.opEquiv { unop := F.obj X.unop } { unop := F.obj X.unop }) (CategoryTheory.CategoryStruct.id { unop := F.obj X.unop }))) (h.counit.app X.unop))
          @[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 { unop := F.obj (G.obj Y.unop) } Y).symm (CategoryTheory.CategoryStruct.comp (h.unit.app Y.unop) (F.map ((CategoryTheory.opEquiv { unop := G.obj Y.unop } { unop := G.toPrefunctor.1 Y.unop }) (CategoryTheory.CategoryStruct.id { unop := G.obj Y.unop }))))

          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

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

            Equations
            Instances For

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

              Equations
              Instances For

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

                Equations
                Instances For
                  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.
                  Instances For

                    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.
                    Instances For

                      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.
                      Instances For