Theorems · Theorem · commutative algebra

IsLocalization.isLocalization_isLocalization_atPrime_isLocalization

∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (T : Type u_3) [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [IsScalarTower R S T] [IsLocalization M S] (p : Ideal S) [Hp : p.IsPrime] [IsLocalization.AtPrime T p],
  IsLocalization.AtPrime T (Ideal.comap (algebraMap R S) p)

Given a submodule M ⊆ R and a prime ideal p of S = M⁻¹R, with f : R →+* S the localization map, then T = Sₚ is the localization of R at f⁻¹(p).

Defined in

Mathlib.RingTheory.Localization.LocalizationLocalization

Cited by

3 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraCommSemiringAlgebraAlgebraIsScalarTowerIsLocalizationIdeal.IsPrimeIsLocalization.AtPrime