English
If α is iso between left adjoints, then the induced Iso via conjugation is an iso; conversely, an iso in conjugate corresponds to an iso of left adjoints.
Русский
Если α — изоморфизм между левыми сопряжённостями, то получившийся изоморфизм через сопряжение тоже изоморфизм; наоборот.
LaTeX
$$$$ \\text{IsIso}(\\text{conjugateEquiv adj1 adj2 } α) \\;\\Rightarrow\\; IsIso(α). $$$$
Lean4
/-- When all four morphisms 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₂
a --→ b a ←-- b a ←-- b
l₂ r₂ r₂
```
In this case the iterated mate equals the conjugate of the original 2-morphism and is thus an
isomorphism if and only if the original 2-morphism is. This explains why some Beck-Chevalley
2-morphisms are isomorphisms.
-/
theorem iterated_mateEquiv_conjugateEquiv (α : f₁ ≫ l₂ ⟶ l₁ ≫ f₂) :
mateEquiv adj₄ adj₃ (mateEquiv adj₁ adj₂ α) = conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂) α :=
by
simp only [conjugateEquiv_apply, mateEquiv_apply']
dsimp [Adjunction.comp]
bicategory
