THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The R-alg_equiv between the localization of R away from r and
R with an inverse of r adjoined.
noncomputable
def
localization.away_equiv_adjoin
{R : Type u_1}
[comm_ring R]
(r : R) :
localization.away r ≃ₐ[R] adjoin_root (⇑polynomial.C r * polynomial.X - 1)
The R-alg_equiv between the localization of R away from r and
R with an inverse of r adjoined.
Equations
- localization.away_equiv_adjoin r = alg_equiv.of_alg_hom {to_fun := (localization.away_lift (algebra_map R (adjoin_root (⇑polynomial.C r * polynomial.X - 1))) r _).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _} (adjoin_root.lift_hom (⇑polynomial.C r * polynomial.X - 1) (is_localization.away.inv_self r) _) _ _
theorem
is_localization.adjoin_inv
{R : Type u_1}
[comm_ring R]
(r : R) :
is_localization.away r (adjoin_root (⇑polynomial.C r * polynomial.X - 1))
theorem
is_localization.away.finite_presentation
{R : Type u_1}
[comm_ring R]
(r : R)
{S : Type u_2}
[comm_ring S]
[algebra R S]
[is_localization.away r S] :