Theorems · Theorem · number theory

IsDecompositionField.ramificationIdx_eq

∀ (A : Type u_1) (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 A] [inst_4 : CommRing B] [inst_5 : Algebra A B] {p : Ideal A} (P : Ideal B) [P.LiesOver p]
  [inst_7 : Algebra A K] [IsFractionRing A K] [inst_9 : Algebra A L] [IsScalarTower A K L] [inst_11 : Algebra B L]
  [IsScalarTower A B L] [IsFractionRing B L] [inst_14 : MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L]
  (D : Type u_5) (𝓞D : Type u_6) [inst_16 : Field D] [inst_17 : Algebra D L] [IsDecompositionField K L P D]
  [inst_19 : CommRing 𝓞D] [inst_20 : Algebra 𝓞D D] [IsFractionRing 𝓞D D] [inst_22 : Algebra 𝓞D B]
  [inst_23 : Algebra 𝓞D L] [IsScalarTower 𝓞D D L] [IsScalarTower 𝓞D B L] (𝓟D : Ideal 𝓞D) [hD : P.LiesOver 𝓟D]
  [IsGalois K L] [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B]
  [inst_31 : Algebra A 𝓞D] [Module.Finite A 𝓞D] [IsScalarTower A 𝓞D B] [IsDedekindDomain 𝓞D] [𝓟D.LiesOver p]
  [FiniteDimensional K L] [Ring.HasFiniteQuotients A] [𝓟D.IsMaximal] [P.IsMaximal], p ≠ ⊥ → 𝓟D.ramificationIdx A = 1

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

Defined in

Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraCommRingCommRingAlgebraIdeal.LiesOverAlgebraIsFractionRingAlgebraIsScalarTowerAlgebraIsScalarTowerIsFractionRingMulSemiringActionSMulDistribClassFieldAlgebraIsDecompositionFieldCommRingAlgebraIsFractionRingAlgebraAlgebraIsScalarTowerIsScalarTowerIdeal.LiesOverIsGaloisIsDedekindDomainIsDedekindDomainModule.FiniteModule.IsTorsionFreeAlgebraModule.FiniteIsScalarTowerIsDedekindDomainIdeal.LiesOverFiniteDimensionalRing.HasFiniteQuotientsIdeal.IsMaximalIdeal.IsMaximal