Mathlib.CategoryTheory.Adjunction.Mates

Module docstring

{"# 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. "}

CategoryTheory.mateEquiv definition

: TwoSquare G L₁ L₂ H ≃ TwoSquare R₁ H G R₂

Full source

/-- 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.
-/
@[simps]
def mateEquiv : TwoSquareTwoSquare G L₁ L₂ H ≃ TwoSquare R₁ H G R₂ where
  toFun α := .mk _ _ _ _ <|
    whiskerLeftwhiskerLeft (R₁ ⋙ G) adj₂.unit ≫
    whiskerRight (whiskerLeft R₁ α.natTrans) R₂ ≫
    whiskerRight adj₁.counit (H ⋙ R₂)
  invFun β := .mk _ _ _ _ <|
    whiskerRightwhiskerRight adj₁.unit (G ⋙ L₂) ≫
    whiskerRight (whiskerLeft L₁ β.natTrans) L₂ ≫
    whiskerLeft (L₁ ⋙ H) adj₂.counit
  left_inv α := by
    ext
    unfold whiskerRight whiskerLeft
    simp only [comp_obj, id_obj, Functor.comp_map, comp_app, map_comp, assoc, counit_naturality,
      counit_naturality_assoc, left_triangle_components_assoc]
    rw [← assoc, ← Functor.comp_map, α.natTrans.naturality, Functor.comp_map, assoc, ← H.map_comp,
      left_triangle_components, map_id]
    simp only [comp_obj, comp_id]
  right_inv β := by
    ext
    unfold whiskerLeft whiskerRight
    simp only [comp_obj, id_obj, Functor.comp_map, comp_app, map_comp, assoc,
      unit_naturality_assoc, right_triangle_components_assoc]
    rw [← assoc, ← Functor.comp_map, assoc, ← β.natTrans.naturality, ← assoc, Functor.comp_map,
      ← G.map_comp, right_triangle_components, map_id, id_comp]

Mate correspondence for adjunctions

Informal description

Given a square of functors where the top and bottom are adjunctions $L_1 \dashv R_1$ and $L_2 \dashv R_2$ respectively: \[ \begin{array}{ccc} C & \xleftrightarrow[L_1]{R_1} & D \\ G \downarrow & & \downarrow H \\ E & \xleftrightarrow[L_2]{R_2} & F \end{array} \] there is a bijection between natural transformations $G \circ L_2 \Rightarrow L_1 \circ H$ and $R_1 \circ G \Rightarrow H \circ R_2$. This bijection is given explicitly by: \[ \alpha \mapsto \text{whiskerLeft}\, (R_1 \circ G)\, \eta_2 \circ \text{whiskerRight}\, (\text{whiskerLeft}\, R_1\, \alpha)\, R_2 \circ \text{whiskerRight}\, \epsilon_1\, (H \circ R_2) \] with inverse: \[ \beta \mapsto \text{whiskerRight}\, \eta_1\, (G \circ L_2) \circ \text{whiskerRight}\, (\text{whiskerLeft}\, L_1\, \beta)\, L_2 \circ \text{whiskerLeft}\, (L_1 \circ H)\, \epsilon_2 \] where $\eta_1, \epsilon_1$ are the unit and counit of $L_1 \dashv R_1$, and $\eta_2, \epsilon_2$ are the unit and counit of $L_2 \dashv R_2$.

CategoryTheory.mateEquiv_counit theorem

 (α : TwoSquare G L₁ L₂ H) (d : D) :
  L₂.map ((mateEquiv adj₁ adj₂ α).app _) ≫ adj₂.counit.app _ = α.app _ ≫ H.map (adj₁.counit.app d)

Full source

/-- A component of a transposed version of the mates correspondence. -/
theorem mateEquiv_counit (α : TwoSquare G L₁ L₂ H) (d : D) :
    L₂.map ((mateEquiv adj₁ adj₂ α).app _) ≫ adj₂.counit.app _ =
      α.app _ ≫ H.map (adj₁.counit.app d) := by simp

Counit Compatibility in Mate Correspondence for Adjunctions

Informal description

Given a natural transformation $\alpha \colon G \circ L_2 \Rightarrow L_1 \circ H$ between functors in the square of adjunctions: \[ \begin{array}{ccc} C & \xleftrightarrow[L_1]{R_1} & D \\ G \downarrow & & \downarrow H \\ E & \xleftrightarrow[L_2]{R_2} & F \end{array} \] where $L_1 \dashv R_1$ and $L_2 \dashv R_2$ with counits $\epsilon_1$ and $\epsilon_2$ respectively, for any object $d \in D$, the following diagram commutes: \[ L_2(\text{mate}(\alpha)(d)) \circ \epsilon_2(d) = \alpha(d) \circ H(\epsilon_1(d)) \] Here $\text{mate}(\alpha)$ denotes the mate of $\alpha$ under the bijection $\text{mateEquiv}$.

CategoryTheory.mateEquiv_counit_symm theorem

 (α : TwoSquare R₁ H G R₂) (d : D) :
  L₂.map (α.app _) ≫ adj₂.counit.app _ = ((mateEquiv adj₁ adj₂).symm α).app _ ≫ H.map (adj₁.counit.app d)

Full source

/-- A component of a transposed version of the inverse mates correspondence. -/
theorem mateEquiv_counit_symm (α : TwoSquare R₁ H G R₂) (d : D) :
    L₂.map (α.app _) ≫ adj₂.counit.app _ =
      ((mateEquiv adj₁ adj₂).symm α).app _ ≫ H.map (adj₁.counit.app d) := by
  conv_lhs => rw [← (mateEquiv adj₁ adj₂).right_inv α]
  exact (mateEquiv_counit adj₁ adj₂ ((mateEquiv adj₁ adj₂).symm α) d)

Inverse Mate Compatibility with Counits in Adjunction Square

Informal description

Given a natural transformation $\alpha \colon R_1 \circ H \Rightarrow G \circ R_2$ between functors in the square of adjunctions: \[ \begin{array}{ccc} C & \xleftrightarrow[L_1]{R_1} & D \\ G \downarrow & & \downarrow H \\ E & \xleftrightarrow[L_2]{R_2} & F \end{array} \] where $L_1 \dashv R_1$ and $L_2 \dashv R_2$ with counits $\epsilon_1$ and $\epsilon_2$ respectively, for any object $d \in D$, the following diagram commutes: \[ L_2(\alpha(d)) \circ \epsilon_2(d) = \text{mate}^{-1}(\alpha)(d) \circ H(\epsilon_1(d)) \] Here $\text{mate}^{-1}(\alpha)$ denotes the inverse mate of $\alpha$ under the bijection $\text{mateEquiv}$.

CategoryTheory.unit_mateEquiv theorem

 (α : TwoSquare G L₁ L₂ H) (c : C) :
  G.map (adj₁.unit.app c) ≫ (mateEquiv adj₁ adj₂ α).app _ = adj₂.unit.app _ ≫ R₂.map (α.app _)

Full source

theorem unit_mateEquiv (α : TwoSquare G L₁ L₂ H) (c : C) :
    G.map (adj₁.unit.app c) ≫ (mateEquiv adj₁ adj₂ α).app _ =
      adj₂.unit.app _ ≫ R₂.map (α.app _) := by
  dsimp [mateEquiv]
  rw [← adj₂.unit_naturality_assoc]
  slice_lhs 2 3 =>
    rw [← R₂.map_comp, ← Functor.comp_map G L₂, α.naturality]
  rw [R₂.map_comp]
  slice_lhs 3 4 =>
    rw [← R₂.map_comp, Functor.comp_map L₁ H, ← H.map_comp, left_triangle_components]
  simp only [comp_obj, map_id, comp_id]

Unit Compatibility in Mate Correspondence for Adjunctions

Informal description

Given a natural transformation $\alpha \colon G \circ L_2 \Rightarrow L_1 \circ H$ between functors in the square of adjunctions: \[ \begin{array}{ccc} C & \xleftrightarrow[L_1]{R_1} & D \\ G \downarrow & & \downarrow H \\ E & \xleftrightarrow[L_2]{R_2} & F \end{array} \] where $L_1 \dashv R_1$ and $L_2 \dashv R_2$ with units $\eta_1$ and $\eta_2$ respectively, for any object $c \in C$, the following diagram commutes: \[ G(\eta_1(c)) \circ \text{mate}(\alpha)(c) = \eta_2(G(c)) \circ R_2(\alpha(c)) \] Here $\text{mate}(\alpha)$ denotes the mate of $\alpha$ under the bijection $\text{mateEquiv}$.

CategoryTheory.unit_mateEquiv_symm theorem

 (α : TwoSquare R₁ H G R₂) (c : C) :
  G.map (adj₁.unit.app c) ≫ α.app _ = adj₂.unit.app _ ≫ R₂.map (((mateEquiv adj₁ adj₂).symm α).app _)

Full source

/-- A component of a transposed version of the inverse mates correspondence. -/
theorem unit_mateEquiv_symm (α : TwoSquare R₁ H G R₂) (c : C) :
    G.map (adj₁.unit.app c) ≫ α.app _ =
      adj₂.unit.app _ ≫ R₂.map (((mateEquiv adj₁ adj₂).symm α).app _) := by
  conv_lhs => rw [← (mateEquiv adj₁ adj₂).right_inv α]
  exact (unit_mateEquiv adj₁ adj₂ ((mateEquiv adj₁ adj₂).symm α) c)

Unit Compatibility for Inverse Mate Correspondence in Adjunctions

Informal description

Given a natural transformation $\alpha \colon R_1 \circ H \Rightarrow G \circ R_2$ between functors in the square of adjunctions: \[ \begin{array}{ccc} C & \xleftrightarrow[L_1]{R_1} & D \\ G \downarrow & & \downarrow H \\ E & \xleftrightarrow[L_2]{R_2} & F \end{array} \] where $L_1 \dashv R_1$ and $L_2 \dashv R_2$ with units $\eta_1$ and $\eta_2$ respectively, for any object $c \in C$, the following diagram commutes: \[ G(\eta_1(c)) \circ \alpha(c) = \eta_2(G(c)) \circ R_2(\text{mate}^{-1}(\alpha)(c)) \] Here $\text{mate}^{-1}(\alpha)$ denotes the inverse mate of $\alpha$ under the bijection $\text{mateEquiv}$.

CategoryTheory.mateEquiv_vcomp theorem

 (α : TwoSquare G₁ L₁ L₂ H₁) (β : TwoSquare G₂ L₂ L₃ H₂) :
  (mateEquiv adj₁ adj₃) (α ≫ₕ β) = (mateEquiv adj₁ adj₂ α) ≫ᵥ (mateEquiv adj₂ adj₃ β)

Full source

/-- The mates equivalence commutes with vertical composition. -/
theorem mateEquiv_vcomp (α : TwoSquare G₁ L₁ L₂ H₁) (β : TwoSquare G₂ L₂ L₃ H₂) :
    (mateEquiv adj₁ adj₃) (α ≫ₕ β) = (mateEquiv adj₁ adj₂ α) ≫ᵥ (mateEquiv adj₂ adj₃ β) := by
  unfold hComp vComp mateEquiv
  ext b
  simp only [comp_obj, Equiv.coe_fn_mk, whiskerLeft_comp, whiskerLeft_twice, whiskerRight_comp,
    assoc, comp_app, whiskerLeft_app, whiskerRight_app, associator_hom_app, map_id,
    associator_inv_app, id_obj, Functor.comp_map, id_comp, whiskerRight_twice, comp_id]
  slice_rhs 1 4 => rw [← assoc, ← assoc, ← unit_naturality (adj₃)]
  rw [L₃.map_comp, R₃.map_comp]
  slice_rhs 2 4 =>
    rw [← R₃.map_comp, ← R₃.map_comp, ← assoc, ← L₃.map_comp, ← G₂.map_comp, ← G₂.map_comp]
    rw [← Functor.comp_map G₂ L₃, β.naturality]
  rw [(L₂ ⋙ H₂).map_comp, R₃.map_comp, R₃.map_comp]
  slice_rhs 4 5 =>
    rw [← R₃.map_comp, Functor.comp_map L₂ _, ← Functor.comp_map _ L₂, ← H₂.map_comp]
    rw [adj₂.counit.naturality]
  simp only [comp_obj, Functor.comp_map, map_comp, id_obj, Functor.id_map, assoc]
  slice_rhs 4 5 =>
    rw [← R₃.map_comp, ← H₂.map_comp, ← Functor.comp_map _ L₂, adj₂.counit.naturality]
  simp only [comp_obj, id_obj, Functor.id_map, map_comp, assoc]
  slice_rhs 3 4 =>
    rw [← R₃.map_comp, ← H₂.map_comp, left_triangle_components]
  simp only [map_id, id_comp]

Compatibility of Mate Correspondence with Vertical Composition of Natural Transformations

Informal description

Given two natural transformations $\alpha \colon G_1 \circ L_2 \Rightarrow L_1 \circ H_1$ and $\beta \colon G_2 \circ L_3 \Rightarrow L_2 \circ H_2$ in the squares of adjunctions: \[ \begin{array}{ccc} C & \xleftrightarrow[L_1]{R_1} & D \\ G_1 \downarrow & & \downarrow H_1 \\ E & \xleftrightarrow[L_2]{R_2} & F \end{array} \quad \text{and} \quad \begin{array}{ccc} E & \xleftrightarrow[L_2]{R_2} & F \\ G_2 \downarrow & & \downarrow H_2 \\ G & \xleftrightarrow[L_3]{R_3} & H \end{array} \] where $L_1 \dashv R_1$, $L_2 \dashv R_2$, and $L_3 \dashv R_3$, the mate of the horizontal composition $\alpha \circ_h \beta$ is equal to the vertical composition of the mates of $\alpha$ and $\beta$. That is, \[ \text{mate}(\alpha \circ_h \beta) = \text{mate}(\alpha) \circ_v \text{mate}(\beta). \]

CategoryTheory.mateEquiv_hcomp theorem

 (α : TwoSquare G L₁ L₂ H) (β : TwoSquare H L₃ L₄ K) :
  (mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄)) (α ≫ᵥ β) = (mateEquiv adj₃ adj₄ β) ≫ₕ (mateEquiv adj₁ adj₂ α)

Full source

/-- The mates equivalence commutes with horizontal composition of squares. -/
theorem mateEquiv_hcomp (α : TwoSquare G L₁ L₂ H) (β : TwoSquare H L₃ L₄ K) :
    (mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄)) (α ≫ᵥ β) =
      (mateEquiv adj₃ adj₄ β) ≫ₕ (mateEquiv adj₁ adj₂ α) := by
  unfold vComp hComp mateEquiv Adjunction.comp
  ext c
  dsimp
  simp only [comp_id, map_comp, id_comp, assoc]
  slice_rhs 2 4 =>
    rw [← R₂.map_comp, ← R₂.map_comp, ← assoc, ← unit_naturality (adj₄)]
  rw [R₂.map_comp, L₄.map_comp, R₄.map_comp, R₂.map_comp]
  slice_rhs 4 5 =>
    rw [← R₂.map_comp, ← R₄.map_comp, ← Functor.comp_map _ L₄ , β.naturality]
  simp only [comp_obj, Functor.comp_map, map_comp, assoc]

Compatibility of Mate Correspondence with Horizontal and Vertical Composition

Informal description

Given two natural transformations $\alpha \colon G \circ L_2 \Rightarrow L_1 \circ H$ and $\beta \colon H \circ L_4 \Rightarrow L_3 \circ K$ in the squares of adjunctions: \[ \begin{array}{ccc} C & \xleftrightarrow[L_1]{R_1} & D \\ G \downarrow & & \downarrow H \\ E & \xleftrightarrow[L_2]{R_2} & F \end{array} \quad \text{and} \quad \begin{array}{ccc} E & \xleftrightarrow[L_3]{R_3} & F \\ H \downarrow & & \downarrow K \\ G & \xleftrightarrow[L_4]{R_4} & H \end{array} \] where $L_1 \dashv R_1$, $L_2 \dashv R_2$, $L_3 \dashv R_3$, and $L_4 \dashv R_4$, the mate of the vertical composition $\alpha \circ_v \beta$ under the composed adjunctions $L_1 \circ L_3 \dashv R_3 \circ R_1$ and $L_2 \circ L_4 \dashv R_4 \circ R_2$ is equal to the horizontal composition of the mates of $\beta$ and $\alpha$. That is, \[ \text{mate}(\alpha \circ_v \beta) = \text{mate}(\beta) \circ_h \text{mate}(\alpha). \]

CategoryTheory.mateEquiv_square theorem

 (α : 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₆)) ((α ≫ᵥ β) ≫ₕ (γ ≫ᵥ δ)) =
    ((mateEquiv adj₂ adj₄ β) ≫ₕ (mateEquiv adj₁ adj₃ α)) ≫ᵥ ((mateEquiv adj₄ adj₆ δ) ≫ₕ (mateEquiv adj₃ adj₅ γ))

Full source

/-- 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.
-/
theorem mateEquiv_square (α : 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₆)) ((α ≫ᵥ β) ≫ₕ (γ ≫ᵥ δ)) =
      ((mateEquiv adj₂ adj₄ β) ≫ₕ (mateEquiv adj₁ adj₃ α))
         ≫ᵥ ((mateEquiv adj₄ adj₆ δ) ≫ₕ (mateEquiv adj₃ adj₅ γ)) := by
  have vcomp :=
    mateEquiv_vcomp (adj₁.comp adj₂) (adj₃.comp adj₄) (adj₅.comp adj₆) (α ≫ᵥ β) (γ ≫ᵥ δ)
  simp only [mateEquiv_hcomp] at vcomp
  assumption

Compatibility of Mate Correspondence with Composition of Squares of Natural Transformations

Informal description

Given four natural transformations $\alpha \colon G_1 \circ L_3 \Rightarrow L_1 \circ H_1$, $\beta \colon H_1 \circ L_4 \Rightarrow L_2 \circ K_1$, $\gamma \colon G_2 \circ L_5 \Rightarrow L_3 \circ H_2$, and $\delta \colon H_2 \circ L_6 \Rightarrow L_4 \circ K_2$ in squares of adjunctions: \[ \begin{array}{ccc} C & \xleftrightarrow[L_1]{R_1} & D \\ G_1 \downarrow & & \downarrow H_1 \\ E & \xleftrightarrow[L_3]{R_3} & F \end{array} \quad \begin{array}{ccc} E & \xleftrightarrow[L_2]{R_2} & F \\ H_1 \downarrow & & \downarrow K_1 \\ G & \xleftrightarrow[L_4]{R_4} & H \end{array} \] \[ \begin{array}{ccc} C & \xleftrightarrow[L_3]{R_3} & D \\ G_2 \downarrow & & \downarrow H_2 \\ E & \xleftrightarrow[L_5]{R_5} & F \end{array} \quad \begin{array}{ccc} E & \xleftrightarrow[L_4]{R_4} & F \\ H_2 \downarrow & & \downarrow K_2 \\ G & \xleftrightarrow[L_6]{R_6} & H \end{array} \] where $L_i \dashv R_i$ for $i=1,\ldots,6$, the mate of the composite transformation $(\alpha \circ_v \beta) \circ_h (\gamma \circ_v \delta)$ under the composed adjunctions $L_1 \circ L_2 \dashv R_2 \circ R_1$ and $L_5 \circ L_6 \dashv R_6 \circ R_5$ equals the vertical composition of the horizontal compositions of mates: \[ \text{mate}((\alpha \circ_v \beta) \circ_h (\gamma \circ_v \delta)) = (\text{mate}(\beta) \circ_h \text{mate}(\alpha)) \circ_v (\text{mate}(\delta) \circ_h \text{mate}(\gamma)). \]

CategoryTheory.conjugateEquiv definition

: (L₂ ⟶ L₁) ≃ (R₁ ⟶ R₂)

Full source

/-- 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.
-/
@[simps!]
def conjugateEquiv : (L₂ ⟶ L₁) ≃ (R₁ ⟶ R₂) :=
  calc
    (L₂ ⟶ L₁) ≃ (𝟭 C ⋙ L₂ ⟶ L₁ ⋙ 𝟭 D) := (Iso.homCongr L₂.leftUnitor L₁.rightUnitor).symm
    _ ≃ TwoSquare _ _ _ _calc
    (L₂ ⟶ L₁) ≃ (𝟭 C ⋙ L₂ ⟶ L₁ ⋙ 𝟭 D) := (Iso.homCongr L₂.leftUnitor L₁.rightUnitor).symm
    _ ≃ TwoSquare _ _ _ _ := (TwoSquare.equivNatTrans _ _ _ _).symm
    _ ≃ _calc
    (L₂ ⟶ L₁) ≃ (𝟭 C ⋙ L₂ ⟶ L₁ ⋙ 𝟭 D) := (Iso.homCongr L₂.leftUnitor L₁.rightUnitor).symm
    _ ≃ TwoSquare _ _ _ _ := (TwoSquare.equivNatTrans _ _ _ _).symm
    _ ≃ _ := mateEquiv adj₁ adj₂
    _ ≃ (R₁ ⋙ 𝟭 C ⟶ 𝟭 D ⋙ R₂)calc
    (L₂ ⟶ L₁) ≃ (𝟭 C ⋙ L₂ ⟶ L₁ ⋙ 𝟭 D) := (Iso.homCongr L₂.leftUnitor L₁.rightUnitor).symm
    _ ≃ TwoSquare _ _ _ _ := (TwoSquare.equivNatTrans _ _ _ _).symm
    _ ≃ _ := mateEquiv adj₁ adj₂
    _ ≃ (R₁ ⋙ 𝟭 C ⟶ 𝟭 D ⋙ R₂) := TwoSquare.equivNatTrans _ _ _ _
    _ ≃ (R₁ ⟶ R₂) := R₁.rightUnitor.homCongr R₂.leftUnitor

Bijection between conjugate natural transformations for adjoint pairs

Informal description

Given two adjunctions $L_1 \dashv R_1$ and $L_2 \dashv R_2$ between categories $C$ and $D$, there is a natural bijection between the sets of natural transformations $\text{Nat}(L_2, L_1)$ and $\text{Nat}(R_1, R_2)$. This bijection is constructed by first identifying natural transformations $L_2 \Rightarrow L_1$ with certain squares involving identity functors, then applying the mate correspondence `mateEquiv`, and finally translating back to natural transformations $R_1 \Rightarrow R_2$ via unit and counit isomorphisms. Furthermore, this bijection preserves and reflects isomorphisms: a natural transformation is an isomorphism if and only if its image under the bijection is an isomorphism.

CategoryTheory.conjugateEquiv_counit theorem

 (α : L₂ ⟶ L₁) (d : D) : L₂.map ((conjugateEquiv adj₁ adj₂ α).app _) ≫ adj₂.counit.app d = α.app _ ≫ adj₁.counit.app d

Full source

/-- A component of a transposed form of the conjugation definition. -/
theorem conjugateEquiv_counit (α : L₂ ⟶ L₁) (d : D) :
    L₂.map ((conjugateEquiv adj₁ adj₂ α).app _) ≫ adj₂.counit.app d =
      α.app _ ≫ adj₁.counit.app d := by
  dsimp [conjugateEquiv]
  rw [id_comp, comp_id]
  have := mateEquiv_counit adj₁ adj₂ (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) d
  dsimp at this
  rw [this]
  simp only [comp_id, id_comp]

Counit Compatibility in Conjugate Natural Transformation for Adjoint Pairs

Informal description

Given two adjunctions $L_1 \dashv R_1$ and $L_2 \dashv R_2$ between categories $C$ and $D$, and a natural transformation $\alpha \colon L_2 \Rightarrow L_1$, for any object $d \in D$, the following diagram commutes: \[ L_2(\text{conj}(\alpha)(d)) \circ \epsilon_2(d) = \alpha(d) \circ \epsilon_1(d) \] where $\text{conj}(\alpha)$ is the conjugate of $\alpha$ under the bijection $\text{conjugateEquiv}$, and $\epsilon_1$, $\epsilon_2$ are the counits of the adjunctions $L_1 \dashv R_1$ and $L_2 \dashv R_2$ respectively.

CategoryTheory.conjugateEquiv_counit_symm theorem

 (α : R₁ ⟶ R₂) (d : D) :
  L₂.map (α.app _) ≫ adj₂.counit.app d = ((conjugateEquiv adj₁ adj₂).symm α).app _ ≫ adj₁.counit.app d

Full source

/-- A component of a transposed form of the inverse conjugation definition. -/
theorem conjugateEquiv_counit_symm (α : R₁ ⟶ R₂) (d : D) :
    L₂.map (α.app _) ≫ adj₂.counit.app d =
      ((conjugateEquiv adj₁ adj₂).symm α).app _ ≫ adj₁.counit.app d := by
    conv_lhs => rw [← (conjugateEquiv adj₁ adj₂).right_inv α]
    exact (conjugateEquiv_counit adj₁ adj₂ ((conjugateEquiv adj₁ adj₂).symm α) d)

Counit Compatibility for Inverse Conjugate Natural Transformation in Adjoint Pairs

Informal description

Given two adjunctions $L_1 \dashv R_1$ and $L_2 \dashv R_2$ between categories $C$ and $D$, and a natural transformation $\alpha \colon R_1 \Rightarrow R_2$, for any object $d \in D$, the following diagram commutes: \[ L_2(\alpha(d)) \circ \epsilon_2(d) = \text{conj}^{-1}(\alpha)(d) \circ \epsilon_1(d) \] where $\text{conj}^{-1}(\alpha)$ is the inverse conjugate of $\alpha$ under the bijection $\text{conjugateEquiv}$, and $\epsilon_1$, $\epsilon_2$ are the counits of the adjunctions $L_1 \dashv R_1$ and $L_2 \dashv R_2$ respectively.

CategoryTheory.unit_conjugateEquiv theorem

 (α : L₂ ⟶ L₁) (c : C) : adj₁.unit.app _ ≫ (conjugateEquiv adj₁ adj₂ α).app _ = adj₂.unit.app c ≫ R₂.map (α.app _)

Full source

/-- A component of a transposed form of the conjugation definition. -/
theorem unit_conjugateEquiv (α : L₂ ⟶ L₁) (c : C) :
    adj₁.unit.app _ ≫ (conjugateEquiv adj₁ adj₂ α).app _ =
      adj₂.unit.app c ≫ R₂.map (α.app _) := by
  dsimp [conjugateEquiv]
  rw [id_comp, comp_id]
  have := unit_mateEquiv adj₁ adj₂ (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) c
  dsimp at this
  rw [this]
  simp

Unit Compatibility in Conjugate Natural Transformation for Adjunctions

Informal description

Given two adjunctions $L_1 \dashv R_1$ and $L_2 \dashv R_2$ between categories $C$ and $D$, for any natural transformation $\alpha \colon L_2 \Rightarrow L_1$ and any object $c \in C$, the following diagram commutes: \[ \eta_1(c) \circ \text{conj}(\alpha)(c) = \eta_2(c) \circ R_2(\alpha(c)) \] where $\eta_1$ and $\eta_2$ are the unit transformations of the adjunctions, and $\text{conj}(\alpha)$ is the conjugate transformation of $\alpha$ under the bijection $\text{conjugateEquiv}$.

CategoryTheory.unit_conjugateEquiv_symm theorem

 (α : R₁ ⟶ R₂) (c : C) :
  adj₁.unit.app _ ≫ α.app _ = adj₂.unit.app c ≫ R₂.map (((conjugateEquiv adj₁ adj₂).symm α).app _)

Full source

/-- A component of a transposed form of the inverse conjugation definition. -/
theorem unit_conjugateEquiv_symm (α : R₁ ⟶ R₂) (c : C) :
    adj₁.unit.app _ ≫ α.app _ =
      adj₂.unit.app c ≫ R₂.map (((conjugateEquiv adj₁ adj₂).symm α).app _) := by
    conv_lhs => rw [← (conjugateEquiv adj₁ adj₂).right_inv α]
    exact (unit_conjugateEquiv adj₁ adj₂ ((conjugateEquiv adj₁ adj₂).symm α) c)

Unit Compatibility for Inverse Conjugate Natural Transformation in Adjunctions

Informal description

Given two adjunctions $L_1 \dashv R_1$ and $L_2 \dashv R_2$ between categories $C$ and $D$, for any natural transformation $\alpha \colon R_1 \Rightarrow R_2$ and any object $c \in C$, the following diagram commutes: \[ \eta_1(c) \circ \alpha(c) = \eta_2(c) \circ R_2(\text{conj}^{-1}(\alpha)(c)) \] where $\eta_1$ and $\eta_2$ are the unit transformations of the adjunctions, and $\text{conj}^{-1}(\alpha)$ is the inverse conjugate transformation of $\alpha$ under the bijection $\text{conjugateEquiv}$.

CategoryTheory.conjugateEquiv_id theorem

: conjugateEquiv adj₁ adj₁ (𝟙 _) = 𝟙 _

Full source

@[simp]
theorem conjugateEquiv_id : conjugateEquiv adj₁ adj₁ (𝟙 _) = 𝟙 _ := by
  ext
  simp

Identity Preservation under Conjugate Bijection for Adjoint Functors

Informal description

Given an adjunction $L_1 \dashv R_1$ between categories $C$ and $D$, the conjugate bijection $\text{conjugateEquiv}$ maps the identity natural transformation $\text{id}_{L_1} \colon L_1 \Rightarrow L_1$ to the identity natural transformation $\text{id}_{R_1} \colon R_1 \Rightarrow R_1$.

CategoryTheory.conjugateEquiv_symm_id theorem

: (conjugateEquiv adj₁ adj₁).symm (𝟙 _) = 𝟙 _

Full source

@[simp]
theorem conjugateEquiv_symm_id : (conjugateEquiv adj₁ adj₁).symm (𝟙 _) = 𝟙 _ := by
  rw [Equiv.symm_apply_eq]
  simp only [conjugateEquiv_id]

Inverse Conjugate Bijection Preserves Identity for Adjoint Functors

Informal description

Given an adjunction $L_1 \dashv R_1$ between categories $C$ and $D$, the inverse of the conjugate bijection $\text{conjugateEquiv}$ maps the identity natural transformation $\text{id}_{R_1} \colon R_1 \Rightarrow R_1$ to the identity natural transformation $\text{id}_{L_1} \colon L_1 \Rightarrow L_1$. In other words, $(\text{conjugateEquiv}(L_1, R_1)^{-1})(\text{id}_{R_1}) = \text{id}_{L_1}$.

CategoryTheory.conjugateEquiv_adjunction_id theorem

 {L R : C ⥤ C} (adj : L ⊣ R) (α : 𝟭 C ⟶ L) (c : C) :
  (conjugateEquiv adj Adjunction.id α).app c = α.app (R.obj c) ≫ adj.counit.app c

Full source

theorem conjugateEquiv_adjunction_id {L R : C ⥤ C} (adj : L ⊣ R) (α : 𝟭𝟭 C ⟶ L) (c : C) :
    (conjugateEquiv adj Adjunction.id α).app c = α.app (R.obj c) ≫ adj.counit.app c := by
  simp [conjugateEquiv, mateEquiv, Adjunction.id]

Component Formula for Conjugate Natural Transformation under Identity Adjunction

Informal description

Given an adjunction $L \dashv R$ between endofunctors on a category $C$ and a natural transformation $\alpha \colon \text{id}_C \Rightarrow L$, the component at an object $c$ of the conjugate natural transformation $\text{conjugateEquiv}\, \text{adj}\, \text{Adjunction.id}\, \alpha$ is given by the composition $\alpha_{R(c)} \circ \epsilon_c$, where $\epsilon$ is the counit of the adjunction.

CategoryTheory.conjugateEquiv_adjunction_id_symm theorem

 {L R : C ⥤ C} (adj : L ⊣ R) (α : R ⟶ 𝟭 C) (c : C) :
  ((conjugateEquiv adj Adjunction.id).symm α).app c = adj.unit.app c ≫ α.app (L.obj c)

Full source

theorem conjugateEquiv_adjunction_id_symm {L R : C ⥤ C} (adj : L ⊣ R) (α : R ⟶ 𝟭 C) (c : C) :
    ((conjugateEquiv adj Adjunction.id).symm α).app c = adj.unit.app c ≫ α.app (L.obj c) := by
  simp [conjugateEquiv, mateEquiv, Adjunction.id]

Component Formula for Inverse Mate of Natural Transformation under Identity Adjunction

Informal description

Given an adjunction $L \dashv R$ between endofunctors on a category $\mathcal{C}$ and a natural transformation $\alpha \colon R \Rightarrow \text{id}_{\mathcal{C}}$, the component at $c \in \mathcal{C}$ of the inverse mate transformation under the conjugate equivalence is given by the composition: \[ (\text{conjugateEquiv}(adj, \text{id})^{-1}(\alpha))_c = \eta_c \circ \alpha_{L(c)}, \] where $\eta$ is the unit of the adjunction $L \dashv R$.

CategoryTheory.conjugateEquiv_comp theorem

 (α : L₂ ⟶ L₁) (β : L₃ ⟶ L₂) :
  conjugateEquiv adj₁ adj₂ α ≫ conjugateEquiv adj₂ adj₃ β = conjugateEquiv adj₁ adj₃ (β ≫ α)

Full source

@[simp]
theorem conjugateEquiv_comp (α : L₂ ⟶ L₁) (β : L₃ ⟶ L₂) :
    conjugateEquivconjugateEquiv adj₁ adj₂ α ≫ conjugateEquiv adj₂ adj₃ β =
      conjugateEquiv adj₁ adj₃ (β ≫ α) := by
  ext d
  dsimp [conjugateEquiv, mateEquiv]
  have vcomp := mateEquiv_vcomp adj₁ adj₂ adj₃
    (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)
    (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)
  have vcompd := congr_app vcomp d
  dsimp [mateEquiv, vComp, vComp] at vcompd
  simp only [hComp_app, id_obj, comp_app, comp_obj, leftUnitor_hom_app, rightUnitor_inv_app,
    comp_id, id_comp, Functor.id_map, map_comp, assoc] at vcompd ⊢
  rw [vcompd]

Compatibility of Conjugate Bijection with Composition of Natural Transformations

Informal description

Given two adjunctions $L_1 \dashv R_1$ and $L_2 \dashv R_2$ between categories $C$ and $D$, and natural transformations $\alpha \colon L_2 \Rightarrow L_1$ and $\beta \colon L_3 \Rightarrow L_2$, the composition of their conjugate transformations under the bijection $\text{conjugateEquiv}$ is equal to the conjugate transformation of the composition $\beta \circ \alpha$. That is, \[ \text{conjugateEquiv}(\alpha) \circ \text{conjugateEquiv}(\beta) = \text{conjugateEquiv}(\beta \circ \alpha). \]

CategoryTheory.conjugateEquiv_symm_comp theorem

 (α : R₁ ⟶ R₂) (β : R₂ ⟶ R₃) :
  (conjugateEquiv adj₂ adj₃).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = (conjugateEquiv adj₁ adj₃).symm (α ≫ β)

Full source

@[simp]
theorem conjugateEquiv_symm_comp (α : R₁ ⟶ R₂) (β : R₂ ⟶ R₃) :
    (conjugateEquiv adj₂ adj₃).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α =
      (conjugateEquiv adj₁ adj₃).symm (α ≫ β) := by
  rw [Equiv.eq_symm_apply, ← conjugateEquiv_comp _ adj₂]
  simp only [Equiv.apply_symm_apply]

Compatibility of Inverse Conjugate Bijection with Composition of Natural Transformations

Informal description

Given two adjunctions $L_1 \dashv R_1$ and $L_2 \dashv R_2$ between categories $C$ and $D$, and natural transformations $\alpha \colon R_1 \Rightarrow R_2$ and $\beta \colon R_2 \Rightarrow R_3$, the composition of their inverse conjugate transformations under the bijection $\text{conjugateEquiv}^{-1}$ is equal to the inverse conjugate transformation of the composition $\alpha \circ \beta$. That is, \[ \text{conjugateEquiv}^{-1}(\beta) \circ \text{conjugateEquiv}^{-1}(\alpha) = \text{conjugateEquiv}^{-1}(\alpha \circ \beta). \]

CategoryTheory.conjugateEquiv_comm theorem

 {α : L₂ ⟶ L₁} {β : L₁ ⟶ L₂} (βα : β ≫ α = 𝟙 _) : conjugateEquiv adj₁ adj₂ α ≫ conjugateEquiv adj₂ adj₁ β = 𝟙 _

Full source

theorem conjugateEquiv_comm {α : L₂ ⟶ L₁} {β : L₁ ⟶ L₂} (βα : β ≫ α = 𝟙 _) :
    conjugateEquivconjugateEquiv adj₁ adj₂ α ≫ conjugateEquiv adj₂ adj₁ β = 𝟙 _ := by
  rw [conjugateEquiv_comp, βα, conjugateEquiv_id]

Identity Preservation under Composition of Conjugate Transformations for Adjoint Pairs

Informal description

Given two adjoint pairs $L_1 \dashv R_1$ and $L_2 \dashv R_2$ between categories $C$ and $D$, and natural transformations $\alpha \colon L_2 \Rightarrow L_1$ and $\beta \colon L_1 \Rightarrow L_2$ such that $\beta \circ \alpha = \text{id}_{L_2}$, the composition of their conjugate transformations under the bijection $\text{conjugateEquiv}$ is the identity transformation. That is, \[ \text{conjugateEquiv}(\alpha) \circ \text{conjugateEquiv}(\beta) = \text{id}_{R_2}. \]

CategoryTheory.conjugateEquiv_symm_comm theorem

 {α : R₁ ⟶ R₂} {β : R₂ ⟶ R₁} (αβ : α ≫ β = 𝟙 _) :
  (conjugateEquiv adj₂ adj₁).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = 𝟙 _

Full source

theorem conjugateEquiv_symm_comm {α : R₁ ⟶ R₂} {β : R₂ ⟶ R₁} (αβ : α ≫ β = 𝟙 _) :
    (conjugateEquiv adj₂ adj₁).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = 𝟙 _ := by
  rw [conjugateEquiv_symm_comp, αβ, conjugateEquiv_symm_id]

Identity Preservation under Composition of Inverse Conjugate Transformations for Adjoint Pairs

Informal description

Given two adjoint pairs $L_1 \dashv R_1$ and $L_2 \dashv R_2$ between categories $C$ and $D$, and natural transformations $\alpha \colon R_1 \Rightarrow R_2$ and $\beta \colon R_2 \Rightarrow R_1$ such that $\alpha \circ \beta = \text{id}_{R_2}$, the composition of their inverse conjugate transformations under the bijection $\text{conjugateEquiv}^{-1}$ is the identity transformation. That is, \[ \text{conjugateEquiv}^{-1}(\beta) \circ \text{conjugateEquiv}^{-1}(\alpha) = \text{id}_{L_1}. \]

CategoryTheory.conjugateEquiv_iso instance

(α : L₂ ⟶ L₁) [IsIso α] : IsIso (conjugateEquiv adj₁ adj₂ α)

Full source

/-- If `α` is an isomorphism between left adjoints, then its conjugate transformation is an
isomorphism. The converse is given in `conjugateEquiv_of_iso`.
-/
instance conjugateEquiv_iso (α : L₂ ⟶ L₁) [IsIso α] :
    IsIso (conjugateEquiv adj₁ adj₂ α) :=
  ⟨⟨conjugateEquiv adj₂ adj₁ (inv α),
      ⟨conjugateEquiv_comm _ _ (by simp), conjugateEquiv_comm _ _ (by simp)⟩⟩⟩

Isomorphism Preservation under Conjugate Transformation for Adjoint Pairs

Informal description

Given two adjunctions $L_1 \dashv R_1$ and $L_2 \dashv R_2$ between categories $C$ and $D$, if a natural transformation $\alpha \colon L_2 \Rightarrow L_1$ is an isomorphism, then its conjugate transformation under the bijection $\text{conjugateEquiv}$ is also an isomorphism.

CategoryTheory.conjugateEquiv_symm_iso instance

(α : R₁ ⟶ R₂) [IsIso α] : IsIso ((conjugateEquiv adj₁ adj₂).symm α)

Full source

/-- If `α` is an isomorphism between right adjoints, then its conjugate transformation is an
isomorphism. The converse is given in `conjugateEquiv_symm_of_iso`.
-/
instance conjugateEquiv_symm_iso (α : R₁ ⟶ R₂) [IsIso α] :
    IsIso ((conjugateEquiv adj₁ adj₂).symm α) :=
  ⟨⟨(conjugateEquiv adj₂ adj₁).symm (inv α),
      ⟨conjugateEquiv_symm_comm _ _ (by simp), conjugateEquiv_symm_comm _ _ (by simp)⟩⟩⟩

Isomorphism Preservation under Inverse Conjugate Transformation for Adjoint Pairs

Informal description

Given two adjunctions $L_1 \dashv R_1$ and $L_2 \dashv R_2$ between categories $C$ and $D$, if a natural transformation $\alpha \colon R_1 \Rightarrow R_2$ is an isomorphism, then its conjugate transformation under the inverse of the bijection $\text{conjugateEquiv}$ is also an isomorphism.

CategoryTheory.conjugateEquiv_of_iso theorem

(α : L₂ ⟶ L₁) [IsIso (conjugateEquiv adj₁ adj₂ α)] : IsIso α

Full source

/-- 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 conjugateEquiv_of_iso (α : L₂ ⟶ L₁) [IsIso (conjugateEquiv adj₁ adj₂ α)] :
    IsIso α := by
  suffices IsIso ((conjugateEquiv adj₁ adj₂).symm (conjugateEquiv adj₁ adj₂ α))
    by simpa using this
  infer_instance

Isomorphism Reflection for Conjugate Natural Transformations of Left Adjoints

Informal description

Given two adjunctions $L_1 \dashv R_1$ and $L_2 \dashv R_2$ between categories $C$ and $D$, if the conjugate natural transformation of $\alpha \colon L_2 \Rightarrow L_1$ under the bijection $\text{conjugateEquiv}$ is an isomorphism, then $\alpha$ itself is an isomorphism.

CategoryTheory.conjugateEquiv_symm_of_iso theorem

(α : R₁ ⟶ R₂) [IsIso ((conjugateEquiv adj₁ adj₂).symm α)] : IsIso α

Full source

/--
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`.
-/
theorem conjugateEquiv_symm_of_iso (α : R₁ ⟶ R₂)
    [IsIso ((conjugateEquiv adj₁ adj₂).symm α)] : IsIso α := by
  suffices IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
    by simpa using this
  infer_instance

Isomorphism Reflection for Conjugate Natural Transformations of Right Adjoints

Informal description

Given two adjunctions $L_1 \dashv R_1$ and $L_2 \dashv R_2$ between categories $C$ and $D$, if the inverse image of a natural transformation $\alpha \colon R_1 \Rightarrow R_2$ under the conjugate bijection is an isomorphism, then $\alpha$ itself is an isomorphism.

CategoryTheory.conjugateIsoEquiv definition

: (L₂ ≅ L₁) ≃ (R₁ ≅ R₂)

Full source

/-- Thus conjugation defines an equivalence between natural isomorphisms. -/
@[simps]
def conjugateIsoEquiv : (L₂ ≅ L₁) ≃ (R₁ ≅ R₂) where
  toFun α := {
    hom := conjugateEquiv adj₁ adj₂ α.hom
    inv := conjugateEquiv adj₂ adj₁ α.inv
  }
  invFun β := {
    hom := (conjugateEquiv adj₁ adj₂).symm β.hom
    inv := (conjugateEquiv adj₂ adj₁).symm β.inv
  }
  left_inv := by aesop_cat
  right_inv := by aesop_cat

Bijection between conjugate natural isomorphisms for adjoint pairs

Informal description

Given two adjunctions $ L_1 \dashv R_1 $ and $ L_2 \dashv R_2 $ between categories $ C $ and $ D $, there is a natural bijection between the sets of natural isomorphisms $ L_2 \cong L_1 $ and $ R_1 \cong R_2 $. This bijection is constructed by applying the mate correspondence to both the hom and inverse components of the isomorphisms. Furthermore, this bijection preserves and reflects isomorphisms: a natural transformation is an isomorphism if and only if its image under the bijection is an isomorphism.

CategoryTheory.iterated_mateEquiv_conjugateEquiv theorem

 (α : TwoSquare F₁ L₁ L₂ F₂) :
  (mateEquiv adj₄ adj₃ (mateEquiv adj₁ adj₂ α)).natTrans = conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂) α

Full source

/-- 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 iterated_mateEquiv_conjugateEquiv (α : TwoSquare F₁ L₁ L₂ F₂) :
    (mateEquiv adj₄ adj₃ (mateEquiv adj₁ adj₂ α)).natTrans =
      conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂) α := by
  ext d
  unfold conjugateEquiv mateEquiv Adjunction.comp
  simp

Iterated Mate Transformation Equals Conjugate Transformation under Composed Adjoints

Informal description

Given adjunctions $L_1 \dashv R_1$ and $L_2 \dashv R_2$ between categories $C$ and $D$, and adjunctions $L_3 \dashv R_3$ and $L_4 \dashv R_4$ between categories $E$ and $F$, consider a natural transformation $\alpha$ fitting into the square: \[ \begin{array}{ccc} C & \xrightarrow{L_1} & D \\ F_1 \downarrow & \alpha & \downarrow F_2 \\ E & \xrightarrow{L_2} & F \end{array} \] Then the iterated mate transformation of $\alpha$ (first under $L_1 \dashv R_1$ and $L_2 \dashv R_2$, then under $L_3 \dashv R_3$ and $L_4 \dashv R_4$) equals the conjugate transformation of $\alpha$ under the composed adjunctions $(L_1 \circ L_4) \dashv (R_4 \circ R_1)$ and $(L_3 \circ L_2) \dashv (R_2 \circ R_3)$. In symbols: \[ \text{mate}_{L_3 \dashv R_3, L_4 \dashv R_4}(\text{mate}_{L_1 \dashv R_1, L_2 \dashv R_2}(\alpha)) = \text{conjugate}_{(L_1 \circ L_4) \dashv (R_4 \circ R_1), (L_3 \circ L_2) \dashv (R_2 \circ R_3)}(\alpha) \]

CategoryTheory.iterated_mateEquiv_conjugateEquiv_symm theorem

 (α : TwoSquare U₂ R₂ R₁ U₁) :
  (mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α) =
    (conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm.trans (equivNatTrans _ _ _ _).symm α

Full source

theorem iterated_mateEquiv_conjugateEquiv_symm (α : TwoSquare U₂ R₂ R₁ U₁) :
    (mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α) =
      (conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm.trans
        (equivNatTrans _ _ _ _).symm α := by
  ext
  simp

Inverse Iterated Mate Transformation Equals Composed Inverse Conjugate Transformation

Informal description

Given adjunctions $L_1 \dashv R_1$ and $L_2 \dashv R_2$ between categories $C$ and $D$, and adjunctions $L_3 \dashv R_3$ and $L_4 \dashv R_4$ between categories $E$ and $F$, consider a natural transformation $\alpha$ fitting into the square: \[ \begin{array}{ccc} D & \xleftrightarrow[R_2]{L_2} & C \\ U_2 \downarrow & \alpha \Downarrow & \downarrow U_1 \\ F & \xleftrightarrow[R_1]{L_1} & E \end{array} \] Then the inverse of the iterated mate transformation of $\alpha$ (first under $L_3 \dashv R_3$ and $L_4 \dashv R_4$, then under $L_1 \dashv R_1$ and $L_2 \dashv R_2$) equals the composition of the inverse conjugate transformation of $\alpha$ under the composed adjunctions $(L_1 \circ L_4) \dashv (R_4 \circ R_1)$ and $(L_3 \circ L_2) \dashv (R_2 \circ R_3)$ with the inverse of the natural transformation equivalence. In symbols: \[ \text{mate}^{-1}_{L_1 \dashv R_1, L_2 \dashv R_2}(\text{mate}^{-1}_{L_3 \dashv R_3, L_4 \dashv R_4}(\alpha)) = \text{conj}^{-1}_{(L_1 \circ L_4) \dashv (R_4 \circ R_1), (L_3 \circ L_2) \dashv (R_2 \circ R_3)}(\alpha) \circ \text{equivNatTrans}^{-1} \]

CategoryTheory.mateEquiv_conjugateEquiv_vcomp theorem

 {L₁ : A ⥤ B} {R₁ : B ⥤ A} {L₂ : C ⥤ D} {R₂ : D ⥤ C} {L₃ : C ⥤ D} {R₃ : 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₃ β)

Full source

/-- The mates equivalence commutes with this composition, essentially by `mateEquiv_vcomp`. -/
theorem mateEquiv_conjugateEquiv_vcomp {L₁ : A ⥤ B} {R₁ : B ⥤ A} {L₂ : C ⥤ D} {R₂ : D ⥤ C}
    {L₃ : C ⥤ D} {R₃ : 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₃ β) := by
  ext b
  have vcomp := mateEquiv_vcomp adj₁ adj₂ adj₃ α (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)
  unfold vComp hComp at vcomp
  unfold TwoSquare.whiskerRight TwoSquare.whiskerBottom conjugateEquiv
  have vcompb := congr_app vcomp b
  simp only [comp_obj, id_obj, whiskerLeft_comp, assoc, mateEquiv_apply, whiskerLeft_twice,
    whiskerRight_comp, comp_app, whiskerLeft_app, whiskerRight_app, associator_hom_app, map_id,
    leftUnitor_hom_app, rightUnitor_inv_app, associator_inv_app, Functor.id_map, Functor.comp_map,
    id_comp, whiskerRight_twice, comp_id] at vcompb
  simpa [mateEquiv]

Compatibility of Mate Correspondence with Right Whiskering and Conjugation

Informal description

Given adjunctions $L_1 \dashv R_1$ between categories $A$ and $B$, $L_2 \dashv R_2$ between $C$ and $D$, and $L_3 \dashv R_3$ between $C$ and $D$, a natural transformation $\alpha \colon G \circ L_2 \Rightarrow L_1 \circ H$ (where $G \colon C \to A$ and $H \colon D \to B$), and a natural transformation $\beta \colon L_3 \Rightarrow L_2$, the mate of the right whiskering $\alpha \circ \beta$ is equal to the vertical composition of the mate of $\alpha$ with the conjugate of $\beta$. In symbols: \[ \text{mate}(\alpha \circ \beta) = \text{mate}(\alpha) \circ_v \text{conj}(\beta), \] where $\text{conj}(\beta) \colon R_1 \circ G \Rightarrow H \circ R_3$ is the conjugate of $\beta$ under the adjunctions $L_2 \dashv R_2$ and $L_3 \dashv R_3$.

CategoryTheory.conjugateEquiv_mateEquiv_vcomp theorem

 {L₁ : A ⥤ B} {R₁ : B ⥤ A} {L₂ : A ⥤ B} {R₂ : B ⥤ A} {L₃ : C ⥤ D} {R₃ : 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₂ α)

Full source

/-- The mates equivalence commutes with this composition, essentially by `mateEquiv_vcomp`. -/
theorem conjugateEquiv_mateEquiv_vcomp {L₁ : A ⥤ B} {R₁ : B ⥤ A} {L₂ : A ⥤ B} {R₂ : B ⥤ A}
    {L₃ : C ⥤ D} {R₃ : 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₂ α) := by
  ext b
  have vcomp := mateEquiv_vcomp adj₁ adj₂ adj₃ (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) β
  unfold vComp hComp at vcomp
  unfold TwoSquare.whiskerLeft TwoSquare.whiskerTop conjugateEquiv
  have vcompb := congr_app vcomp b
  simp only [comp_obj, id_obj, whiskerRight_comp, assoc, mateEquiv_apply, whiskerLeft_comp,
    whiskerLeft_twice, comp_app, whiskerLeft_app, whiskerRight_app, associator_hom_app, map_id,
    associator_inv_app, leftUnitor_hom_app, rightUnitor_inv_app, Functor.comp_map, Functor.id_map,
    id_comp, whiskerRight_twice, comp_id] at vcompb
  simpa [mateEquiv]

Compatibility of Mate Correspondence with Left Whiskering and Conjugation

Informal description

Given three adjunctions $L_1 \dashv R_1$, $L_2 \dashv R_2$, and $L_3 \dashv R_3$ between categories $A \leftrightarrows B$ and $C \leftrightarrows D$, a natural transformation $\alpha \colon L_2 \Rightarrow L_1$, and a natural transformation $\beta \colon G \circ L_3 \Rightarrow L_2 \circ H$ forming a square: \[ \begin{array}{ccc} A & \xleftrightarrow[L_2]{R_2} & B \\ G \downarrow & \beta \Downarrow & \downarrow H \\ C & \xleftrightarrow[L_3]{R_3} & D \end{array} \] the mate of the left whiskering $\beta \circ_L \alpha$ is equal to the top whiskering of the mate of $\beta$ with the conjugate of $\alpha$. That is, \[ \text{mate}(\beta \circ_L \alpha) = \text{mate}(\beta) \circ_T \text{conj}(\alpha). \]