Mates and conjugates

CategoryTheory.mateEquiv_adjunction_id is the case of the mate bijection CategoryTheory.mateEquiv in which both adjunctions are identity adjunctions: a two-square between the identity functors of the source and target category is its own mate. Use it to normalize a mate that has been routed through the identity functors, so a computation about such a square can be read back on the square itself. It is the two-square counterpart of Mathlib's CategoryTheory.conjugateEquiv_id.

The internal-Hom comparison of a monoidal functor is one such computation: at the tensor unit the left unitor identifies the unit with left tensoring by the unit, and the mate that remains is taken between the two tensor--Hom adjunctions.

CategoryTheory.Adjunction.homEquiv_conjugateEquiv transposes a morphism across two adjunctions whose left adjoints are compared by a natural transformation α: transposing along the first adjunction and then applying the conjugate of α is transposing α followed by the morphism along the second. It computes transposes along an adjunction whose left adjoint is only known up to a comparison with another left adjoint, such as a composite of pullback functors.

Main declarations

• CategoryTheory.mateEquiv_adjunction_id;
• CategoryTheory.Adjunction.homEquiv_conjugateEquiv.

@[simp]

theorem CategoryTheory.mateEquiv_adjunction_id {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {G H : Functor C D} (α : TwoSquare G (Functor.id C) (Functor.id D) H) : (mateEquiv Adjunction.id Adjunction.id) α = α

The mate of a two-square between the identity functors of the source and target category is the two-square itself.

theorem CategoryTheory.Adjunction.homEquiv_conjugateEquiv {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L₁ L₂ : Functor C D} {R₁ R₂ : Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (α : L₂ ⟶ L₁) {c : C} {d : D} (a : L₁.obj c ⟶ d) : CategoryStruct.comp ((adj₁.homEquiv c d) a) (((conjugateEquiv adj₁ adj₂) α).app d) = (adj₂.homEquiv c d) (CategoryStruct.comp (α.app c) a)

Transposing a : L₁ c ⟶ d along adj₁ and then applying the conjugate of α : L₂ ⟶ L₁ is the transpose of α.app c ≫ a along adj₂.