Theorems · Theorem · commutative algebra

IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime

∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] (S : Type u_2) [inst_2 : CommRing S] [inst_3 : Algebra R S]
  [Module.IsTorsionFree R S] [Module.Finite R S] (p : Ideal R),
  p ≠ ⊥ →
    ∀ [inst_6 : p.IsPrime] {Sₚ : Type u_3} [inst_7 : CommRing Sₚ] [inst_8 : Algebra S Sₚ]
      [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [inst_10 : Algebra R Sₚ] [IsScalarTower R S Sₚ]
      [inst_12 : IsDedekindDomain Sₚ] [IsDomain S] {P : Ideal Sₚ},
      P.IsPrime → P ≠ ⊥ → P ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R Sₚ) p)

If p is a prime in the Dedekind domain R, S an extension of R and Sₚ the localization of S at p, then all primes in Sₚ are factors of the image of p in Sₚ.

Defined in

Mathlib.RingTheory.DedekindDomain.PID

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomainCommRingAlgebraModule.IsTorsionFreeModule.FiniteIdeal.IsPrimeCommRingAlgebraIsLocalizationAlgebraIsScalarTowerIsDedekindDomainIsDomain