English
The mates operation commutes with composition when transferring along a three-corner corner of a diagram.
Русский
Матэш-операция сохраняет композицию при переносе вдоль угла диаграммы.
LaTeX
$$$(\\text{mateEquiv } adj_1 adj_3)(α \\;\\mathrm{whiskerRight}\\; β) = (\\text{mateEquiv } adj_1 adj_2 α) \\;\\mathrm{whiskerBottom}\\; (\\text{conjugateEquiv } adj_2 adj_3 β)$$$
Lean4
/-- When all four functors in a square 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
