English
Explicates how conjugateEquiv sends α: l₂ ⟶ l₁ to a morphism in the opposite direction using adjunction data.
Русский
Поясняет, как conjugateEquiv переводит α: l₂ ⟶ l₁ в морфизм в противоположном направлении с использованием данных adjunction.
LaTeX
$$$\\mathrm{conjugateEquiv}\\ adj_1\\ adj_2 \\alpha = (\\rho_{r_1})^{-1} \\!\\;\\circ\\!\\; (r_1 \\curvearrowleft adj_2.unit) \\!\\circ\\!\\; (r_1 \\curvearrowleft \\alpha) \\!\\circ\\!\\; (\\lambda_{r_2}).hom$$$
Lean4
/-- Given two adjunctions `l₁ ⊣ r₁` and `l₂ ⊣ r₂` both between objects `c`, `d`, there is a
bijection between 2-morphisms `l₂ ⟶ l₁` and 2-morphisms `r₁ ⟶ r₂`. This is
defined as a special case of `mateEquiv`, where the two "vertical" 1-morphisms are identities.
Corresponding 2-morphisms are called `conjugateEquiv`.
Furthermore, this bijection preserves (and reflects) isomorphisms, i.e. a 2-morphism is an iso
iff its image under the bijection is an iso.
-/
def conjugateEquiv : (l₂ ⟶ l₁) ≃ (r₁ ⟶ r₂) :=
calc
(l₂ ⟶ l₁) ≃ _ := (Iso.homCongr (λ_ l₂) (ρ_ l₁)).symm
_ ≃ _ := (mateEquiv adj₁ adj₂)
_ ≃ (r₁ ⟶ r₂) := Iso.homCongr (ρ_ r₁) (λ_ r₂)
