English
Thus conjugation defines an equivalence between natural isomorphisms: there is an equivalence between left-isomorphisms and right-isomorphisms given by conjugation.
Русский
Сопряжение задаёт эквивалентность между естественными изоморфизмами слева и справа.
LaTeX
$$$$ \\text{conjugateIsoEquiv } : (l_2 \\cong l_1) \\simeq (r_1 \\cong r_2). $$$$
Lean4
/-- 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
hom_inv_id := by rw [conjugateEquiv_comp, Iso.inv_hom_id, conjugateEquiv_id]
inv_hom_id := by rw [conjugateEquiv_comp, Iso.hom_inv_id, conjugateEquiv_id] }
invFun
β :=
{ hom := (conjugateEquiv adj₁ adj₂).symm β.hom
inv := (conjugateEquiv adj₂ adj₁).symm β.inv
hom_inv_id := by rw [conjugateEquiv_symm_comp, Iso.inv_hom_id, conjugateEquiv_symm_id]
inv_hom_id := by rw [conjugateEquiv_symm_comp, Iso.hom_inv_id, conjugateEquiv_symm_id] }
left_inv := by
intro α
simp only [Equiv.symm_apply_apply]
right_inv := by
intro α
simp only [Equiv.apply_symm_apply]
