theorem
DedekindKummer.inertiaDeg_eq_natDegree_lift
{K : Type u_1}
[Field K]
[NumberField K]
{θ : NumberField.RingOfIntegers K}
{p : ℕ}
[Fact (Nat.Prime p)]
(hp : ¬p ∣ RingOfIntegers.exponent θ)
{Q : Polynomial ℤ}
(hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ RingOfIntegers.monicFactorsMod θ p)
:
(Ideal.span {↑p}).inertiaDeg
↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp).symm
⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩) = (Polynomial.map (Int.castRingHom (ZMod p)) Q).natDegree
theorem
DedekindKummer.ramificationIdx_eq_multiplicity_lift
{K : Type u_1}
[Field K]
[NumberField K]
{θ : NumberField.RingOfIntegers K}
{p : ℕ}
[Fact (Nat.Prime p)]
(hp : ¬p ∣ RingOfIntegers.exponent θ)
{Q : Polynomial ℤ}
(hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ RingOfIntegers.monicFactorsMod θ p)
:
(Ideal.span {↑p}).ramificationIdx
↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp).symm
⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩) = multiplicity (Polynomial.map (Int.castRingHom (ZMod p)) Q) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))
theorem
DedekindKummer.prime_eq_span_pair
{K : Type u_1}
[Field K]
[NumberField K]
{θ : NumberField.RingOfIntegers K}
{p : ℕ}
[Fact (Nat.Prime p)]
(hp : ¬p ∣ RingOfIntegers.exponent θ)
{Q : Polynomial ℤ}
(hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ RingOfIntegers.monicFactorsMod θ p)
:
↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩) = Ideal.span {↑p, (Polynomial.aeval θ) Q}
theorem
DedekindKummer.kummer_inertiaDeg_ramificationIdx_prime
{K : Type u_1}
[Field K]
[NumberField K]
{θ : NumberField.RingOfIntegers K}
{p : ℕ}
[Fact (Nat.Prime p)]
(hp : ¬p ∣ RingOfIntegers.exponent θ)
{Q : Polynomial ℤ}
(hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ RingOfIntegers.monicFactorsMod θ p)
:
(Ideal.span {↑p}).inertiaDeg
↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp).symm
⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩) = (Polynomial.map (Int.castRingHom (ZMod p)) Q).natDegree ∧ (Ideal.span {↑p}).ramificationIdx
↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp).symm
⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩) = multiplicity (Polynomial.map (Int.castRingHom (ZMod p)) Q)
(Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)) ∧ ↑((NumberField.Ideal.primesOverSpanEquivMonicFactorsMod hp).symm
⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩) = Ideal.span {↑p, (Polynomial.aeval θ) Q}