English
An algebra isomorphism induces a group isomorphism between automorphism groups by conjugation.
Русский
Алгебраизоморфизм индуцирует групповую изоморфность автоморфизмов через конъюгацию.
LaTeX
$$$\\text{autCongr} (\\varphi) : (A_1 \\simeq_{R} A_1) \\to (A_2 \\simeq_{R} A_2)$$$
Lean4
/-- An algebra isomorphism induces a group isomorphism between automorphism groups.
This is a more bundled version of `AlgEquiv.equivCongr`. -/
@[simps apply]
def autCongr (ϕ : A₁ ≃ₐ[R] A₂) : (A₁ ≃ₐ[R] A₁) ≃* A₂ ≃ₐ[R] A₂
where
__ := equivCongr ϕ ϕ
toFun ψ := ϕ.symm.trans (ψ.trans ϕ)
invFun ψ := ϕ.trans (ψ.trans ϕ.symm)
map_mul' ψ
χ := by
ext
simp only [mul_apply, trans_apply, symm_apply_apply]
