Documentation

Mathlib.CategoryTheory.Adjunction.Mates

Mate of natural transformations #

This file establishes the bijection between the 2-cells

         L₁                  R₁
      C --→ D             C ←-- D
    G ↓  ↗  ↓ H         G ↓  ↘  ↓ H
      E --→ F             E ←-- F
         L₂                  R₂

where L₁ ⊣ R₁ and L₂ ⊣ R₂. The corresponding natural transformations are called mates.

This bijection includes a number of interesting cases as specializations. For instance, in the special case where G,H are identity functors then the bijection preserves and reflects isomorphisms (i.e. we have bijections(L₂ ⟶ L₁) ≃ (R₁ ⟶ R₂), and if either side is an iso then the other side is as well). This demonstrates that adjoints to a given functor are unique up to isomorphism (since if L₁ ≅ L₂ then we deduce R₁ ≅ R₂).

Another example arises from considering the square representing that a functor H preserves products, in particular the morphism HA ⨯ H- ⟶ H(A ⨯ -). Then provided (A ⨯ -) and HA ⨯ - have left adjoints (for instance if the relevant categories are cartesian closed), the transferred natural transformation is the exponential comparison morphism: H(A ^ -) ⟶ HA ^ H-. Furthermore if H has a left adjoint L, this morphism is an isomorphism iff its mate L(HA ⨯ -) ⟶ A ⨯ L- is an isomorphism, see https://ncatlab.org/nlab/show/Frobenius+reciprocity#InCategoryTheory. This also relates to Grothendieck's yoga of six operations, though this is not spelled out in mathlib: https://ncatlab.org/nlab/show/six+operations.

def CategoryTheory.mateEquiv {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} E] [Category.{v₄, u₄} F] {G : Functor C E} {H : Functor D F} {L₁ : Functor C D} {R₁ : Functor D C} {L₂ : Functor E F} {R₂ : Functor F E} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) :
TwoSquare G L₁ L₂ H TwoSquare R₁ H G R₂

Suppose we have a square of functors (where the top and bottom are adjunctions L₁ ⊣ R₁ and L₂ ⊣ R₂ respectively).

  C ↔ D
G ↓   ↓ H
  E ↔ F

Then we have a bijection between natural transformations G ⋙ L₂ ⟶ L₁ ⋙ H and R₁ ⋙ G ⟶ H ⋙ R₂. This can be seen as a bijection of the 2-cells:

     L₁                  R₁
  C --→ D             C ←-- D
G ↓  ↗  ↓ H         G ↓  ↘  ↓ H
  E --→ F             E ←-- F
     L₂                  R₂

Note that if one of the transformations is an iso, it does not imply the other is an iso.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.mateEquiv_apply {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} E] [Category.{v₄, u₄} F] {G : Functor C E} {H : Functor D F} {L₁ : Functor C D} {R₁ : Functor D C} {L₂ : Functor E F} {R₂ : Functor F E} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (α : TwoSquare G L₁ L₂ H) :
    (mateEquiv adj₁ adj₂) α = TwoSquare.mk R₁ H G R₂ (CategoryStruct.comp (whiskerLeft (R₁.comp G) adj₂.unit) (CategoryStruct.comp (whiskerRight (whiskerLeft R₁ α.natTrans) R₂) (whiskerRight adj₁.counit (H.comp R₂))))
    @[simp]
    theorem CategoryTheory.mateEquiv_symm_apply {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} E] [Category.{v₄, u₄} F] {G : Functor C E} {H : Functor D F} {L₁ : Functor C D} {R₁ : Functor D C} {L₂ : Functor E F} {R₂ : Functor F E} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (β : TwoSquare R₁ H G R₂) :
    (mateEquiv adj₁ adj₂).symm β = TwoSquare.mk G L₁ L₂ H (CategoryStruct.comp (whiskerRight adj₁.unit (G.comp L₂)) (CategoryStruct.comp (whiskerRight (whiskerLeft L₁ β.natTrans) L₂) (whiskerLeft (L₁.comp H) adj₂.counit)))
    theorem CategoryTheory.mateEquiv_counit {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} E] [Category.{v₄, u₄} F] {G : Functor C E} {H : Functor D F} {L₁ : Functor C D} {R₁ : Functor D C} {L₂ : Functor E F} {R₂ : Functor F E} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (α : TwoSquare G L₁ L₂ H) (d : D) :
    CategoryStruct.comp (L₂.map (((mateEquiv adj₁ adj₂) α).app d)) (adj₂.counit.app (H.obj d)) = CategoryStruct.comp (α.app (R₁.obj d)) (H.map (adj₁.counit.app d))

    A component of a transposed version of the mates correspondence.

    theorem CategoryTheory.mateEquiv_counit_symm {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} E] [Category.{v₄, u₄} F] {G : Functor C E} {H : Functor D F} {L₁ : Functor C D} {R₁ : Functor D C} {L₂ : Functor E F} {R₂ : Functor F E} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (α : TwoSquare R₁ H G R₂) (d : D) :
    CategoryStruct.comp (L₂.map (α.app d)) (adj₂.counit.app (H.obj d)) = CategoryStruct.comp (((mateEquiv adj₁ adj₂).symm α).app (R₁.obj d)) (H.map (adj₁.counit.app d))

    A component of a transposed version of the inverse mates correspondence.

    theorem CategoryTheory.unit_mateEquiv {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} E] [Category.{v₄, u₄} F] {G : Functor C E} {H : Functor D F} {L₁ : Functor C D} {R₁ : Functor D C} {L₂ : Functor E F} {R₂ : Functor F E} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (α : TwoSquare G L₁ L₂ H) (c : C) :
    CategoryStruct.comp (G.map (adj₁.unit.app c)) (((mateEquiv adj₁ adj₂) α).app (L₁.obj c)) = CategoryStruct.comp (adj₂.unit.app (G.obj ((Functor.id C).obj c))) (R₂.map (α.app ((Functor.id C).obj c)))
    theorem CategoryTheory.unit_mateEquiv_symm {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} E] [Category.{v₄, u₄} F] {G : Functor C E} {H : Functor D F} {L₁ : Functor C D} {R₁ : Functor D C} {L₂ : Functor E F} {R₂ : Functor F E} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (α : TwoSquare R₁ H G R₂) (c : C) :
    CategoryStruct.comp (G.map (adj₁.unit.app c)) (α.app (L₁.obj c)) = CategoryStruct.comp (adj₂.unit.app (G.obj ((Functor.id C).obj c))) (R₂.map (((mateEquiv adj₁ adj₂).symm α).app ((Functor.id C).obj c)))

    A component of a transposed version of the inverse mates correspondence.

    theorem CategoryTheory.mateEquiv_vcomp {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} {E : Type u₅} {F : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] [Category.{v₄, u₄} D] [Category.{v₅, u₅} E] [Category.{v₆, u₆} F] {G₁ : Functor A C} {G₂ : Functor C E} {H₁ : Functor B D} {H₂ : Functor D F} {L₁ : Functor A B} {R₁ : Functor B A} {L₂ : Functor C D} {R₂ : Functor D C} {L₃ : Functor E F} {R₃ : Functor F E} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : L₃ R₃) (α : TwoSquare G₁ L₁ L₂ H₁) (β : TwoSquare G₂ L₂ L₃ H₂) :
    (mateEquiv adj₁ adj₃) (α.hComp β) = ((mateEquiv adj₁ adj₂) α).vComp ((mateEquiv adj₂ adj₃) β)

    The mates equivalence commutes with vertical composition.

    theorem CategoryTheory.mateEquiv_hcomp {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} {E : Type u₅} {F : Type u₆} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] [Category.{v₄, u₄} D] [Category.{v₅, u₅} E] [Category.{v₆, u₆} F] {G : Functor A D} {H : Functor B E} {K : Functor C F} {L₁ : Functor A B} {R₁ : Functor B A} {L₂ : Functor D E} {R₂ : Functor E D} {L₃ : Functor B C} {R₃ : Functor C B} {L₄ : Functor E F} {R₄ : Functor F E} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : L₃ R₃) (adj₄ : L₄ R₄) (α : TwoSquare G L₁ L₂ H) (β : TwoSquare H L₃ L₄ K) :
    (mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄)) (α.vComp β) = ((mateEquiv adj₃ adj₄) β).hComp ((mateEquiv adj₁ adj₂) α)

    The mates equivalence commutes with horizontal composition of squares.

    theorem CategoryTheory.mateEquiv_square {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} {E : Type u₅} {F : Type u₆} {X : Type u₇} {Y : Type u₈} {Z : Type u₉} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] [Category.{v₄, u₄} D] [Category.{v₅, u₅} E] [Category.{v₆, u₆} F] [Category.{v₇, u₇} X] [Category.{v₈, u₈} Y] [Category.{v₉, u₉} Z] {G₁ : Functor A D} {H₁ : Functor B E} {K₁ : Functor C F} {G₂ : Functor D X} {H₂ : Functor E Y} {K₂ : Functor F Z} {L₁ : Functor A B} {R₁ : Functor B A} {L₂ : Functor B C} {R₂ : Functor C B} {L₃ : Functor D E} {R₃ : Functor E D} {L₄ : Functor E F} {R₄ : Functor F E} {L₅ : Functor X Y} {R₅ : Functor Y X} {L₆ : Functor Y Z} {R₆ : Functor Z Y} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : L₃ R₃) (adj₄ : L₄ R₄) (adj₅ : L₅ R₅) (adj₆ : L₆ R₆) (α : TwoSquare G₁ L₁ L₃ H₁) (β : TwoSquare H₁ L₂ L₄ K₁) (γ : TwoSquare G₂ L₃ L₅ H₂) (δ : TwoSquare H₂ L₄ L₆ K₂) :
    (mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) ((α.vComp β).hComp (γ.vComp δ)) = (((mateEquiv adj₂ adj₄) β).hComp ((mateEquiv adj₁ adj₃) α)).vComp (((mateEquiv adj₄ adj₆) δ).hComp ((mateEquiv adj₃ adj₅) γ))

    The mates equivalence commutes with composition of squares of squares. These results form the basis for an isomorphism of double categories to be proven later.

    def CategoryTheory.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₁) (R₁ R₂)

    Given two adjunctions L₁ ⊣ R₁ and L₂ ⊣ R₂ both between categories C, D, there is a bijection between natural transformations L₂ ⟶ L₁ and natural transformations R₁ ⟶ R₂. This is defined as a special case of mateEquiv, where the two "vertical" functors are identity, modulo composition with the unitors. Corresponding natural transformations are called conjugateEquiv. TODO: Generalise to when the two vertical functors are equivalences rather than being exactly 𝟭.

    Furthermore, this bijection preserves (and reflects) isomorphisms, i.e. a transformation is an iso iff its image under the bijection is an iso, see eg CategoryTheory.conjugateIsoEquiv. This is in contrast to the general case mateEquiv which does not in general have this property.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem CategoryTheory.conjugateEquiv_symm_apply_app {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₂) (a✝ : R₁ R₂) (X : C) :
      ((conjugateEquiv adj₁ adj₂).symm a✝).app X = CategoryStruct.comp (L₂.map (adj₁.unit.app X)) (CategoryStruct.comp (L₂.map (a✝.app (L₁.obj X))) (adj₂.counit.app (L₁.obj X)))
      @[simp]
      theorem CategoryTheory.conjugateEquiv_apply_app {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₂) (a✝ : L₂ L₁) (X : D) :
      ((conjugateEquiv adj₁ adj₂) a✝).app X = CategoryStruct.comp (adj₂.unit.app (R₁.obj X)) (CategoryStruct.comp (R₂.map (a✝.app (R₁.obj X))) (R₂.map (adj₁.counit.app X)))
      theorem CategoryTheory.conjugateEquiv_counit {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₁) (d : D) :
      CategoryStruct.comp (L₂.map (((conjugateEquiv adj₁ adj₂) α).app d)) (adj₂.counit.app d) = CategoryStruct.comp (α.app (R₁.obj d)) (adj₁.counit.app d)

      A component of a transposed form of the conjugation definition.

      theorem CategoryTheory.conjugateEquiv_counit_symm {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₂) (α : R₁ R₂) (d : D) :
      CategoryStruct.comp (L₂.map (α.app d)) (adj₂.counit.app d) = CategoryStruct.comp (((conjugateEquiv adj₁ adj₂).symm α).app (R₁.obj d)) (adj₁.counit.app d)

      A component of a transposed form of the inverse conjugation definition.

      theorem CategoryTheory.unit_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) :
      CategoryStruct.comp (adj₁.unit.app c) (((conjugateEquiv adj₁ adj₂) α).app (L₁.obj c)) = CategoryStruct.comp (adj₂.unit.app c) (R₂.map (α.app c))

      A component of a transposed form of the conjugation definition.

      theorem CategoryTheory.unit_conjugateEquiv_symm {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₂) (α : R₁ R₂) (c : C) :
      CategoryStruct.comp (adj₁.unit.app c) (α.app (L₁.obj c)) = CategoryStruct.comp (adj₂.unit.app c) (R₂.map (((conjugateEquiv adj₁ adj₂).symm α).app c))

      A component of a transposed form of the inverse conjugation definition.

      @[simp]
      theorem CategoryTheory.conjugateEquiv_id {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L₁ : Functor C D} {R₁ : Functor D C} (adj₁ : L₁ R₁) :
      @[simp]
      theorem CategoryTheory.conjugateEquiv_symm_id {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L₁ : Functor C D} {R₁ : Functor D C} (adj₁ : L₁ R₁) :
      theorem CategoryTheory.conjugateEquiv_adjunction_id {C : Type u₁} [Category.{v₁, u₁} C] {L R : Functor C C} (adj : L R) (α : Functor.id C L) (c : C) :
      theorem CategoryTheory.conjugateEquiv_adjunction_id_symm {C : Type u₁} [Category.{v₁, u₁} C] {L R : Functor C C} (adj : L R) (α : R Functor.id C) (c : C) :
      @[simp]
      theorem CategoryTheory.conjugateEquiv_comp {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L₁ L₂ L₃ : Functor C D} {R₁ R₂ R₃ : Functor D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : L₃ R₃) (α : L₂ L₁) (β : L₃ L₂) :
      CategoryStruct.comp ((conjugateEquiv adj₁ adj₂) α) ((conjugateEquiv adj₂ adj₃) β) = (conjugateEquiv adj₁ adj₃) (CategoryStruct.comp β α)
      @[simp]
      theorem CategoryTheory.conjugateEquiv_symm_comp {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] {L₁ L₂ L₃ : Functor C D} {R₁ R₂ R₃ : Functor D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : L₃ R₃) (α : R₁ R₂) (β : R₂ R₃) :
      CategoryStruct.comp ((conjugateEquiv adj₂ adj₃).symm β) ((conjugateEquiv adj₁ adj₂).symm α) = (conjugateEquiv adj₁ adj₃).symm (CategoryStruct.comp α β)
      theorem CategoryTheory.conjugateEquiv_comm {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₁} {β : L₁ L₂} (βα : CategoryStruct.comp β α = CategoryStruct.id L₁) :
      CategoryStruct.comp ((conjugateEquiv adj₁ adj₂) α) ((conjugateEquiv adj₂ adj₁) β) = CategoryStruct.id R₁
      theorem CategoryTheory.conjugateEquiv_symm_comm {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₂) {α : R₁ R₂} {β : R₂ R₁} (αβ : CategoryStruct.comp α β = CategoryStruct.id R₁) :
      CategoryStruct.comp ((conjugateEquiv adj₂ adj₁).symm β) ((conjugateEquiv adj₁ adj₂).symm α) = CategoryStruct.id L₁
      instance CategoryTheory.conjugateEquiv_iso {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₁) [IsIso α] :
      IsIso ((conjugateEquiv adj₁ adj₂) α)

      If α is an isomorphism between left adjoints, then its conjugate transformation is an isomorphism. The converse is given in conjugateEquiv_of_iso.

      instance CategoryTheory.conjugateEquiv_symm_iso {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₂) (α : R₁ R₂) [IsIso α] :
      IsIso ((conjugateEquiv adj₁ adj₂).symm α)

      If α is an isomorphism between right adjoints, then its conjugate transformation is an isomorphism. The converse is given in conjugateEquiv_symm_of_iso.

      theorem CategoryTheory.conjugateEquiv_of_iso {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₁) [IsIso ((conjugateEquiv adj₁ adj₂) α)] :

      If α is a natural transformation between left adjoints whose conjugate natural transformation is an isomorphism, then α is an isomorphism. The converse is given in Conjugate_iso.

      theorem CategoryTheory.conjugateEquiv_symm_of_iso {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₂) (α : R₁ R₂) [IsIso ((conjugateEquiv adj₁ adj₂).symm α)] :

      If α is a natural transformation between right adjoints whose conjugate natural transformation is an isomorphism, then α is an isomorphism. The converse is given in conjugateEquiv_symm_iso.

      def CategoryTheory.conjugateIsoEquiv {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₁) (R₁ R₂)

      Thus conjugation defines an equivalence between natural isomorphisms.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem CategoryTheory.conjugateIsoEquiv_symm_apply_inv {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₂) (β : R₁ R₂) :
        ((conjugateIsoEquiv adj₁ adj₂).symm β).inv = (conjugateEquiv adj₂ adj₁).symm β.inv
        @[simp]
        theorem CategoryTheory.conjugateIsoEquiv_symm_apply_hom {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₂) (β : R₁ R₂) :
        ((conjugateIsoEquiv adj₁ adj₂).symm β).hom = (conjugateEquiv adj₁ adj₂).symm β.hom
        @[simp]
        theorem CategoryTheory.conjugateIsoEquiv_apply_hom {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₁) :
        ((conjugateIsoEquiv adj₁ adj₂) α).hom = (conjugateEquiv adj₁ adj₂) α.hom
        @[simp]
        theorem CategoryTheory.conjugateIsoEquiv_apply_inv {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₁) :
        ((conjugateIsoEquiv adj₁ adj₂) α).inv = (conjugateEquiv adj₂ adj₁) α.inv
        theorem CategoryTheory.iterated_mateEquiv_conjugateEquiv {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] [Category.{v₄, u₄} D] {F₁ : Functor A C} {U₁ : Functor C A} {F₂ : Functor B D} {U₂ : Functor D B} {L₁ : Functor A B} {R₁ : Functor B A} {L₂ : Functor C D} {R₂ : Functor D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : F₁ U₁) (adj₄ : F₂ U₂) (α : TwoSquare F₁ L₁ L₂ F₂) :
        ((mateEquiv adj₄ adj₃) ((mateEquiv adj₁ adj₂) α)).natTrans = (conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)) α

        When all four functors in a sequare are left adjoints, the mates operation can be iterated:

             L₁                  R₁                  R₁
          C --→ D             C ←-- D             C ←-- D
        

        F₁ ↓ ↗ ↓ F₂ F₁ ↓ ↘ ↓ F₂ U₁ ↑ ↙ ↑ U₂ E --→ F E ←-- F E ←-- F L₂ R₂ R₂

        In this case the iterated mate equals the conjugate of the original transformation and is thus an isomorphism if and only if the original transformation is. This explains why some Beck-Chevalley natural transformations are natural isomorphisms.

        theorem CategoryTheory.iterated_mateEquiv_conjugateEquiv_symm {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] [Category.{v₄, u₄} D] {F₁ : Functor A C} {U₁ : Functor C A} {F₂ : Functor B D} {U₂ : Functor D B} {L₁ : Functor A B} {R₁ : Functor B A} {L₂ : Functor C D} {R₂ : Functor D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : F₁ U₁) (adj₄ : F₂ U₂) (α : TwoSquare U₂ R₂ R₁ U₁) :
        (mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α) = ((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm.trans (TwoSquare.equivNatTrans F₁ L₁ L₂ F₂).symm) α
        theorem CategoryTheory.mateEquiv_conjugateEquiv_vcomp {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] [Category.{v₄, u₄} D] {G : Functor A C} {H : Functor B D} {L₁ : Functor A B} {R₁ : Functor B A} {L₂ : Functor C D} {R₂ : Functor D C} {L₃ : Functor C D} {R₃ : Functor D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : L₃ R₃) (α : TwoSquare G L₁ L₂ H) (β : L₃ L₂) :
        (mateEquiv adj₁ adj₃) (α.whiskerRight β) = ((mateEquiv adj₁ adj₂) α).whiskerBottom ((conjugateEquiv adj₂ adj₃) β)

        The mates equivalence commutes with this composition, essentially by mateEquiv_vcomp.

        theorem CategoryTheory.conjugateEquiv_mateEquiv_vcomp {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] [Category.{v₄, u₄} D] {G : Functor A C} {H : Functor B D} {L₁ : Functor A B} {R₁ : Functor B A} {L₂ : Functor A B} {R₂ : Functor B A} {L₃ : Functor C D} {R₃ : Functor D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : L₃ R₃) (α : L₂ L₁) (β : TwoSquare G L₂ L₃ H) :
        (mateEquiv adj₁ adj₃) (β.whiskerLeft α) = ((mateEquiv adj₂ adj₃) β).whiskerTop ((conjugateEquiv adj₁ adj₂) α)

        The mates equivalence commutes with this composition, essentially by mateEquiv_vcomp.