English
If algebra maps f: A1 →ₐ[R] A2 and g: A2 →ₐ[R] A1 have two-sided inverses (f ∘ g = id and g ∘ f = id), then there exists an algebra equivalence A1 ≃ₐ[R] A2 with f as its forward map and g as its inverse.
Русский
Если между алгебраическими морфизмами f и g существуют взаимно обратные, то образуется алгебраическая эквивалентность между A1 и A2.
LaTeX
$$$\\exists (\\phi : A_1 \\simeq_{R}^{\\mathrm{alg}} A_2),\\;\\phi = \\mathrm{ofAlgHom}(f,g,h_1,h_2)$$$
Lean4
/-- If an algebra morphism has an inverse, it is an algebra isomorphism. -/
@[simps]
def ofAlgHom (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = AlgHom.id R A₂) (h₂ : g.comp f = AlgHom.id R A₁) :
A₁ ≃ₐ[R] A₂ :=
{ f with
toFun := f
invFun := g
left_inv := AlgHom.ext_iff.1 h₂
right_inv := AlgHom.ext_iff.1 h₁ }
