English
The localization away from r is canonically isomorphic to the root-adjoin construction AdjoinRoot(C_r X − 1).
Русский
Локализация вдали от r канонически изоморфна конструктору AdjoinRoot(C_r X − 1).
LaTeX
$$IsLocalization.Away r S ≃ AdjoinRoot (C r * X - 1)$$
Lean4
/-- The `R`-`AlgEquiv` between the localization of `R` away from `r` and
`R` with an inverse of `r` adjoined. -/
noncomputable def awayEquivAdjoin (r : R) : Away r ≃ₐ[R] AdjoinRoot (C r * X - 1) :=
AlgEquiv.ofAlgHom
{ awayLift _ r _ with commutes' := IsLocalization.Away.lift_eq r (isUnit_of_mul_eq_one _ _ <| root_isInv r) }
(liftHom _ (IsLocalization.Away.invSelf r) <| by
simp only [map_sub, map_mul, aeval_C, aeval_X, IsLocalization.Away.mul_invSelf, aeval_one, sub_self])
(Subsingleton.elim _ _) (Subsingleton.elim (h := IsLocalization.algHom_subsingleton (Submonoid.powers r)) _ _)
