Theorems · Theorem · number theory

IsDecompositionField.primesOver_eq_singleton

∀ (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] (P : Ideal B) [inst_4 : Algebra B L] [IsFractionRing B L]
  [inst_6 : MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L] (D : Type u_5) (𝓞D : Type u_6)
  [inst_8 : Field D] [inst_9 : Algebra D L] [IsDecompositionField K L P D] [inst_11 : CommRing 𝓞D]
  [inst_12 : Algebra 𝓞D D] [IsFractionRing 𝓞D D] [inst_14 : Algebra 𝓞D B] [inst_15 : Algebra 𝓞D L]
  [IsScalarTower 𝓞D D L] [IsScalarTower 𝓞D B L] (𝓟D : Ideal 𝓞D) [hD : P.LiesOver 𝓟D] [hP : P.IsPrime]
  [Finite ↥(MulAction.stabilizer Gal(L/K) P)] [IsIntegrallyClosed 𝓞D] [Algebra.IsIntegral 𝓞D B], 𝓟D.primesOver B = {P}

Let D be the decomposition field of P in L/K. Let 𝓟D be a prime ideal of D below P, then P is the only prime of L above 𝓟D.

Defined in

Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraCommRingAlgebraIsFractionRingMulSemiringActionSMulDistribClassFieldAlgebraIsDecompositionFieldCommRingAlgebraIsFractionRingAlgebraAlgebraIsScalarTowerIsScalarTowerIdeal.LiesOverIdeal.IsPrimeFiniteIsIntegrallyClosedAlgebra.IsIntegral