The R-AlgEquiv between the localization of R away from r and R with an inverse of r adjoined.

noncomputable def Localization.awayEquivAdjoin {R : Type u_1} [CommRing R] (r : R) : Away r ≃ₐ[R] AdjoinRoot (Polynomial.C r * Polynomial.X - 1)

The R-AlgEquiv between the localization of R away from r and R with an inverse of r adjoined.

Equations

• One or more equations did not get rendered due to their size.

theorem IsLocalization.adjoin_inv {R : Type u_1} [CommRing R] (r : R) : Away r (AdjoinRoot (Polynomial.C r * Polynomial.X - 1))

theorem IsLocalization.Away.finitePresentation {R : Type u_1} [CommRing R] (r : R) {S : Type u_2} [CommRing S] [Algebra R S] [Away r S] : Algebra.FinitePresentation R S

theorem Algebra.FinitePresentation.of_isLocalizationAway {R : Type u_2} {S : Type u_3} {S' : Type u_4} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S] [Algebra R S'] [Algebra S S'] [IsScalarTower R S S'] (f : S) [IsLocalization.Away f S'] [FinitePresentation R S] : FinitePresentation R S'

instance instFinitePresentationAway {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Algebra.FinitePresentation R S] (f : S) : Algebra.FinitePresentation R (Localization.Away f)

instance instFiniteTypeAway {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Algebra.FiniteType R S] (f : S) : Algebra.FiniteType R (Localization.Away f)