English
There is an equivalence between natural transformations L₂ ⟶ L₁ and R₁ ⟶ R₂ given adjunctions L₁ ⊣ R₁ and L₂ ⊣ R₂.
Русский
Существуют биекции между естественными преобразованиями L₂ ⟶ L₁ и R₁ ⟶ R₂, задаваемые сопряжениями.
LaTeX
$$$$\\text{conjugateEquiv} : (L_2 \\Rightarrow L_1) \\simeq (R_1 \\Rightarrow R_2).$$$$
Lean4
/-- 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 e.g. `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 _ _ _ _ := (TwoSquare.equivNatTrans _ _ _ _).symm
_ ≃ _ := (mateEquiv adj₁ adj₂)
_ ≃ (R₁ ⋙ 𝟭 C ⟶ 𝟭 D ⋙ R₂) := (TwoSquare.equivNatTrans _ _ _ _)
_ ≃ (R₁ ⟶ R₂) := R₁.rightUnitor.homCongr R₂.leftUnitor
