# 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.

@[simp]
theorem CategoryTheory.mateEquiv_apply {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [] [] [] [] {G : } {H : } {L₁ : } {R₁ : } {L₂ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (α : G.comp L₂ L₁.comp H) :
@[simp]
theorem CategoryTheory.mateEquiv_symm_apply {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [] [] [] [] {G : } {H : } {L₁ : } {R₁ : } {L₂ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (β : R₁.comp G H.comp R₂) :
def CategoryTheory.mateEquiv {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [] [] [] [] {G : } {H : } {L₁ : } {R₁ : } {L₂ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) :
(G.comp L₂ L₁.comp H) (R₁.comp G H.comp 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
@[deprecated CategoryTheory.mateEquiv]
def CategoryTheory.transferNatTrans {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [] [] [] [] {G : } {H : } {L₁ : } {R₁ : } {L₂ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) :
(G.comp L₂ L₁.comp H) (R₁.comp G H.comp R₂)

Alias of CategoryTheory.mateEquiv.

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
Instances For
theorem CategoryTheory.mateEquiv_counit {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [] [] [] [] {G : } {H : } {L₁ : } {R₁ : } {L₂ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (α : G.comp L₂ L₁.comp H) (d : 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₄} [] [] [] [] {G : } {H : } {L₁ : } {R₁ : } {L₂ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (α : R₁.comp G H.comp R₂) (d : 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₄} [] [] [] [] {G : } {H : } {L₁ : } {R₁ : } {L₂ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (α : G.comp L₂ L₁.comp H) (c : C) :
theorem CategoryTheory.unit_mateEquiv_symm {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [] [] [] [] {G : } {H : } {L₁ : } {R₁ : } {L₂ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (α : R₁.comp G H.comp R₂) (c : C) :

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

def CategoryTheory.leftAdjointSquare.vcomp {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} {E : Type u₅} {F : Type u₆} [] [] [] [] [] [] {G₁ : } {G₂ : } {H₁ : } {H₂ : } {L₁ : } {L₂ : } {L₃ : } :
(G₁.comp L₂ L₁.comp H₁)(G₂.comp L₃ L₂.comp H₂)((G₁.comp G₂).comp L₃ L₁.comp (H₁.comp H₂))

Squares between left adjoints can be composed "vertically" by pasting.

Equations
Instances For
def CategoryTheory.rightAdjointSquare.vcomp {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} {E : Type u₅} {F : Type u₆} [] [] [] [] [] [] {G₁ : } {G₂ : } {H₁ : } {H₂ : } {R₁ : } {R₂ : } {R₃ : } :
(R₁.comp G₁ H₁.comp R₂)(R₂.comp G₂ H₂.comp R₃)(R₁.comp (G₁.comp G₂) (H₁.comp H₂).comp R₃)

Squares between right adjoints can be composed "vertically" by pasting.

Equations
Instances For
theorem CategoryTheory.mateEquiv_vcomp {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} {E : Type u₅} {F : Type u₆} [] [] [] [] [] [] {G₁ : } {G₂ : } {H₁ : } {H₂ : } {L₁ : } {R₁ : } {L₂ : } {R₂ : } {L₃ : } {R₃ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : L₃ R₃) (α : G₁.comp L₂ L₁.comp H₁) (β : G₂.comp L₃ L₂.comp H₂) :

The mates equivalence commutes with vertical composition.

def CategoryTheory.leftAdjointSquare.hcomp {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} {E : Type u₅} {F : Type u₆} [] [] [] [] [] [] {G : } {H : } {K : } {L₁ : } {L₂ : } {L₃ : } {L₄ : } :
(G.comp L₂ L₁.comp H)(H.comp L₄ L₃.comp K)(G.comp (L₂.comp L₄) (L₁.comp L₃).comp K)

Squares between left adjoints can be composed "horizontally" by pasting.

Equations
Instances For
def CategoryTheory.rightAdjointSquare.hcomp {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} {E : Type u₅} {F : Type u₆} [] [] [] [] [] [] {G : } {H : } {K : } {R₁ : } {R₂ : } {R₃ : } {R₄ : } :
(R₁.comp G H.comp R₂)(R₃.comp H K.comp R₄)((R₃.comp R₁).comp G K.comp (R₄.comp R₂))

Squares between right adjoints can be composed "horizontally" by pasting.

Equations
Instances For
theorem CategoryTheory.mateEquiv_hcomp {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} {E : Type u₅} {F : Type u₆} [] [] [] [] [] [] {G : } {H : } {K : } {L₁ : } {R₁ : } {L₂ : } {R₂ : } {L₃ : } {R₃ : } {L₄ : } {R₄ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : L₃ R₃) (adj₄ : L₄ R₄) (α : G.comp L₂ L₁.comp H) (β : H.comp L₄ L₃.comp K) :

The mates equivalence commutes with horizontal composition of squares.

def CategoryTheory.leftAdjointSquare.comp {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₉} [] [] [] [] [] [] [] [] [] {G₁ : } {H₁ : } {K₁ : } {G₂ : } {H₂ : } {K₂ : } {L₁ : } {L₂ : } {L₃ : } {L₄ : } {L₅ : } {L₆ : } (α : G₁.comp L₃ L₁.comp H₁) (β : H₁.comp L₄ L₂.comp K₁) (γ : G₂.comp L₅ L₃.comp H₂) (δ : H₂.comp L₆ L₄.comp K₂) :
(G₁.comp G₂).comp (L₅.comp L₆) (L₁.comp L₂).comp (K₁.comp K₂)

Squares of squares between left adjoints can be composed by iterating vertical and horizontal composition.

Equations
Instances For
theorem CategoryTheory.leftAdjointSquare.comp_vhcomp {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₉} [] [] [] [] [] [] [] [] [] {G₁ : } {H₁ : } {K₁ : } {G₂ : } {H₂ : } {K₂ : } {L₁ : } {L₂ : } {L₃ : } {L₄ : } {L₅ : } {L₆ : } (α : G₁.comp L₃ L₁.comp H₁) (β : H₁.comp L₄ L₂.comp K₁) (γ : G₂.comp L₅ L₃.comp H₂) (δ : H₂.comp L₆ L₄.comp K₂) :
theorem CategoryTheory.leftAdjointSquare.comp_hvcomp {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₉} [] [] [] [] [] [] [] [] [] {G₁ : } {H₁ : } {K₁ : } {G₂ : } {H₂ : } {K₂ : } {L₁ : } {L₂ : } {L₃ : } {L₄ : } {L₅ : } {L₆ : } (α : G₁.comp L₃ L₁.comp H₁) (β : H₁.comp L₄ L₂.comp K₁) (γ : G₂.comp L₅ L₃.comp H₂) (δ : H₂.comp L₆ L₄.comp K₂) :

Horizontal and vertical composition of squares commutes.

def CategoryTheory.rightAdjointSquare.comp {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₉} [] [] [] [] [] [] [] [] [] {G₁ : } {H₁ : } {K₁ : } {G₂ : } {H₂ : } {K₂ : } {R₁ : } {R₂ : } {R₃ : } {R₄ : } {R₅ : } {R₆ : } (α : R₁.comp G₁ H₁.comp R₃) (β : R₂.comp H₁ K₁.comp R₄) (γ : R₃.comp G₂ H₂.comp R₅) (δ : R₄.comp H₂ K₂.comp R₆) :
(R₂.comp R₁).comp (G₁.comp G₂) (K₁.comp K₂).comp (R₆.comp R₅)

Squares of squares between right adjoints can be composed by iterating vertical and horizontal composition.

Equations
Instances For
theorem CategoryTheory.rightAdjointSquare.comp_vhcomp {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₉} [] [] [] [] [] [] [] [] [] {G₁ : } {H₁ : } {K₁ : } {G₂ : } {H₂ : } {K₂ : } {R₁ : } {R₂ : } {R₃ : } {R₄ : } {R₅ : } {R₆ : } (α : R₁.comp G₁ H₁.comp R₃) (β : R₂.comp H₁ K₁.comp R₄) (γ : R₃.comp G₂ H₂.comp R₅) (δ : R₄.comp H₂ K₂.comp R₆) :
theorem CategoryTheory.rightAdjointSquare.comp_hvcomp {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₉} [] [] [] [] [] [] [] [] [] {G₁ : } {H₁ : } {K₁ : } {G₂ : } {H₂ : } {K₂ : } {R₁ : } {R₂ : } {R₃ : } {R₄ : } {R₅ : } {R₆ : } (α : R₁.comp G₁ H₁.comp R₃) (β : R₂.comp H₁ K₁.comp R₄) (γ : R₃.comp G₂ H₂.comp R₅) (δ : R₄.comp H₂ K₂.comp R₆) :

Horizontal and vertical composition of squares commutes.

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₉} [] [] [] [] [] [] [] [] [] {G₁ : } {H₁ : } {K₁ : } {G₂ : } {H₂ : } {K₂ : } {L₁ : } {R₁ : } {L₂ : } {R₂ : } {L₃ : } {R₃ : } {L₄ : } {R₄ : } {L₅ : } {R₅ : } {L₆ : } {R₆ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : L₃ R₃) (adj₄ : L₄ R₄) (adj₅ : L₅ R₅) (adj₆ : L₆ R₆) (α : G₁.comp L₃ L₁.comp H₁) (β : H₁.comp L₄ L₂.comp K₁) (γ : G₂.comp L₅ L₃.comp H₂) (δ : H₂.comp L₆ L₄.comp K₂) :

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₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (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
Instances For
@[deprecated CategoryTheory.conjugateEquiv]
def CategoryTheory.transferNatTransSelf {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) :
(L₂ L₁) (R₁ R₂)

Alias of CategoryTheory.conjugateEquiv.

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
Instances For
theorem CategoryTheory.conjugateEquiv_counit {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (α : L₂ L₁) (d : D) :

A component of a transposed form of the conjugation definition.

theorem CategoryTheory.conjugateEquiv_counit_symm {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (α : R₁ R₂) (d : D) :

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

theorem CategoryTheory.unit_conjugateEquiv {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (α : L₂ L₁) (c : C) :

A component of a transposed form of the conjugation definition.

theorem CategoryTheory.unit_conjugateEquiv_symm {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (α : R₁ R₂) (c : C) :

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

@[simp]
theorem CategoryTheory.conjugateEquiv_id {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {R₁ : } (adj₁ : L₁ R₁) :
@[simp]
theorem CategoryTheory.conjugateEquiv_symm_id {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {R₁ : } (adj₁ : L₁ R₁) :
theorem CategoryTheory.conjugateEquiv_adjunction_id {C : Type u₁} [] {L : } {R : } (adj : L R) (α : ) (c : C) :
theorem CategoryTheory.conjugateEquiv_adjunction_id_symm {C : Type u₁} [] {L : } {R : } (adj : L R) (α : ) (c : C) :
theorem CategoryTheory.conjugateEquiv_comp {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {L₃ : } {R₁ : } {R₂ : } {R₃ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : L₃ R₃) (α : L₂ L₁) (β : L₃ L₂) :
theorem CategoryTheory.conjugateEquiv_symm_comp {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {L₃ : } {R₁ : } {R₂ : } {R₃ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : L₃ R₃) (α : R₁ R₂) (β : R₂ R₃) :
theorem CategoryTheory.conjugateEquiv_comm {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) {α : L₂ L₁} {β : L₁ L₂} :
theorem CategoryTheory.conjugateEquiv_symm_comm {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) {α : R₁ R₂} {β : R₂ R₁} :
instance CategoryTheory.conjugateEquiv_iso {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (α : L₂ L₁) :

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

Equations
• =
instance CategoryTheory.conjugateEquiv_symm_iso {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (α : R₁ R₂) :

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

Equations
• =
theorem CategoryTheory.conjugateEquiv_of_iso {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (α : L₂ L₁) [CategoryTheory.IsIso ((CategoryTheory.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₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (α : R₁ R₂) [CategoryTheory.IsIso ((CategoryTheory.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.

noncomputable def CategoryTheory.conjugateIsoEquiv {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (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
theorem CategoryTheory.iterated_mateEquiv_conjugateEquiv {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} [] [] [] [] {F₁ : } {U₁ : } {F₂ : } {U₂ : } {L₁ : } {R₁ : } {L₂ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : F₁ U₁) (adj₄ : F₂ U₂) (α : F₁.comp L₂ L₁.comp F₂) :

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₄} [] [] [] [] {F₁ : } {U₁ : } {F₂ : } {U₂ : } {L₁ : } {R₁ : } {L₂ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : F₁ U₁) (adj₄ : F₂ U₂) (α : U₂.comp R₁ R₂.comp U₁) :
def CategoryTheory.leftAdjointSquareConjugate.vcomp {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} [] [] [] [] {G : } {H : } {L₁ : } {L₂ : } {L₃ : } :
(G.comp L₂ L₁.comp H)(L₃ L₂)(G.comp L₃ L₁.comp H)

Composition of a squares between left adjoints with a conjugate square.

Equations
Instances For
def CategoryTheory.rightAdjointSquareConjugate.vcomp {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} [] [] [] [] {G : } {H : } {R₁ : } {R₂ : } {R₃ : } :
(R₁.comp G H.comp R₂)(R₂ R₃)(R₁.comp G H.comp R₃)

Composition of a squares between right adjoints with a conjugate square.

Equations
Instances For
theorem CategoryTheory.mateEquiv_conjugateEquiv_vcomp {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} [] [] [] [] {G : } {H : } {L₁ : } {R₁ : } {L₂ : } {R₂ : } {L₃ : } {R₃ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : L₃ R₃) (α : G.comp L₂ L₁.comp H) (β : L₃ L₂) :

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

def CategoryTheory.leftAdjointConjugateSquare.vcomp {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} [] [] [] [] {G : } {H : } {L₁ : } {L₂ : } {L₃ : } :
(L₂ L₁)(G.comp L₃ L₂.comp H)(G.comp L₃ L₁.comp H)

Composition of a conjugate square with a squares between left adjoints.

Equations
Instances For
def CategoryTheory.rightAdjointConjugateSquare.vcomp {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} [] [] [] [] {G : } {H : } {R₁ : } {R₂ : } {R₃ : } :
(R₁ R₂)(R₂.comp G H.comp R₃)(R₁.comp G H.comp R₃)

Composition of a conjugate square with a squares between right adjoints.

Equations
Instances For
theorem CategoryTheory.conjugateEquiv_mateEquiv_vcomp {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} [] [] [] [] {G : } {H : } {L₁ : } {R₁ : } {L₂ : } {R₂ : } {L₃ : } {R₃ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : L₃ R₃) (α : L₂ L₁) (β : G.comp L₃ L₂.comp H) :

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