Factorization of invariant integral ideals in a quadratic extension. The only prime factors left after extending a base ideal are ramified primes; repeated ramified factors can be absorbed in pairs.
def
CCDN.IsQuadraticRamifiedPrime
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[Algebra F K]
(Q : Ideal (NumberField.RingOfIntegers K))
:
The predicate that Q is a nonzero prime ideal of 𝓞 K with ramification index 2 over
𝓞 F.
Equations
- CCDN.IsQuadraticRamifiedPrime F K Q = (Q.IsPrime ∧ Q ≠ ⊥ ∧ Q.ramificationIdx (NumberField.RingOfIntegers F) = 2)
Instances For
theorem
CCDN.invariant_integral_ideal_ramified_factorization
(F : Type u_1)
(K : Type u_2)
[Field F]
[Field K]
[NumberField F]
[NumberField K]
[Algebra F K]
[FiniteDimensional F K]
(hd : Module.finrank F K = 2)
(σ : Gal(K/F))
(hσ : σ ≠ 1)
(I : Ideal (NumberField.RingOfIntegers K))
(hI : I ≠ 0)
(hinv : σ • I = I)
:
∃ (J : Ideal (NumberField.RingOfIntegers F)) (t : Finset (Ideal (NumberField.RingOfIntegers K))),
J ≠ 0 ∧ (∀ Q ∈ t, IsQuadraticRamifiedPrime F K Q) ∧ I = Ideal.map (algebraMap (NumberField.RingOfIntegers F) (NumberField.RingOfIntegers K)) J * ∏ Q ∈ t, Q
Every invariant integral ideal is an extended base ideal times a product of distinct ramified prime ideals.