Theorems · Theorem · commutative algebra

Ideal.map_algebraMap_eq_finsetProd_pow

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : Algebra S R] [inst_4 : Algebra.IsIntegral S R] [inst_5 : IsDomain S] [inst_6 : Module.IsTorsionFree S R]
  {p : Ideal S} [inst_7 : p.IsMaximal],
  p ≠ 0 → Ideal.map (algebraMap S R) p = ∏ P ∈ (p.primesOver R).toFinset, P ^ P.ramificationIdx S

If p is a maximal ideal, then the lift of p in an extension is the product of the primes over p to the power the ramification index.

Defined in

Mathlib.RingTheory.DedekindDomain.Factorization

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomainCommRingAlgebraAlgebra.IsIntegralIsDomainModule.IsTorsionFreeIdeal.IsMaximal