The dyadic ramification of ℚ(i)

For K generated over ℚ by an algebraic integer θ with minpoly ℤ θ = X² + 1, the prime 2 divides the discriminant −4, so it ramifies: the prime 𝔭 = (1 + θ) is the only prime of 𝓞 K above 2, with e = 2, f = 1 and 2 𝓞 K = 𝔭². The different of the monogenic ring 𝓞 K = ℤ[θ] is generated by f'(θ) = 2θ, and θ is a unit, so 𝔡 = (2) = 𝔭²: the different exponent v_𝔭(𝔡) = 2 equals the ramification index. This is the wild dyadic case, where the lower bound e of the different exponent is attained and the tame formula e − 1 fails. Since v_𝔭(e) = v_𝔭(2) = 2, the upper bound e − 1 + v_𝔭(e) = 3 of Dedekind's different theorem is strict here; it is attained in ℚ(√2) (TauCeti.NumberField.Sqrt2.multiplicity_differentIdeal_eq_ramificationIdx_sub_one_add).

Main results

• TauCeti.NumberField.GaussianRationals.two_mem_ramifiedPrimes: 2 ramifies, and ncard_primesOver_two_eq_one: there is one prime above it.
• TauCeti.NumberField.GaussianRationals.eq_span_one_add: the prime above 2 is (1 + θ).
• TauCeti.NumberField.GaussianRationals.ramificationIdx_eq_two, ramificationIdxIn_two_eq_two, inertiaDeg_eq_one, map_span_two_eq_sq: e = 2, f = 1, and 2 𝓞 K = 𝔭².
• TauCeti.NumberField.GaussianRationals.differentIdeal_eq_span_two: 𝔡 = (2).
• TauCeti.NumberField.GaussianRationals.differentIdeal_eq_sq and multiplicity_differentIdeal_eq_two: 𝔡 = 𝔭², that is v_𝔭(𝔡) = 2.
• TauCeti.NumberField.GaussianRationals.multiplicity_span_two_eq_two: v_𝔭(2) = 2, and multiplicity_differentIdeal_lt_ramificationIdx_sub_one_add: v_𝔭(𝔡) < e − 1 + v_𝔭(e).

theorem TauCeti.NumberField.GaussianRationals.two_mem_ramifiedPrimes {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) : 2 ∈ NumberField.ramifiedPrimes K

2 ramifies in ℚ(i): it divides the discriminant −4.

theorem TauCeti.NumberField.GaussianRationals.absNorm_span_one_add {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) : Ideal.absNorm (Ideal.span {1 + θ}) = 2

The ideal (1 + θ) has absolute norm 2: N(1 + θ) = 1² − (−1) · 1².

theorem TauCeti.NumberField.GaussianRationals.ncard_primesOver_two_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) : ((Ideal.span {2}).primesOver (NumberField.RingOfIntegers K)).ncard = 1

There is a single prime of 𝓞 K above 2.

theorem TauCeti.NumberField.GaussianRationals.ramificationIdxIn_two_eq_two {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) : (Ideal.span {2}).ramificationIdxIn (NumberField.RingOfIntegers K) = 2

The ramification index of 2 in ℚ(i) is 2, in the form that does not name a prime above 2.

theorem TauCeti.NumberField.GaussianRationals.differentIdeal_eq_span_two {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) : differentIdeal ℤ (NumberField.RingOfIntegers K) = Ideal.span {2}

The different of ℚ(i) is (2): the different of ℤ[θ] is generated by f'(θ) = 2θ, and θ is a unit.

theorem TauCeti.NumberField.GaussianRationals.eq_span_one_add {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) (𝔭 : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {2})] : 𝔭 = Ideal.span {1 + θ}

The prime above 2 in ℚ(i) is (1 + θ).

theorem TauCeti.NumberField.GaussianRationals.ramificationIdx_eq_two {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) (𝔭 : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {2})] : 𝔭.ramificationIdx ℤ = 2

2 is totally ramified in ℚ(i): e(𝔭 ∣ 2) = 2.

theorem TauCeti.NumberField.GaussianRationals.inertiaDeg_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) (𝔭 : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {2})] : 𝔭.inertiaDeg ℤ = 1

The prime above 2 in ℚ(i) has residue degree 1.

theorem TauCeti.NumberField.GaussianRationals.map_span_two_eq_sq {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) (𝔭 : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {2})] : Ideal.map (algebraMap ℤ (NumberField.RingOfIntegers K)) (Ideal.span {2}) = 𝔭 ^ 2

2 𝓞 K = 𝔭² in ℚ(i).

theorem TauCeti.NumberField.GaussianRationals.differentIdeal_eq_sq {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) (𝔭 : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {2})] : differentIdeal ℤ (NumberField.RingOfIntegers K) = 𝔭 ^ 2

The different of ℚ(i) is 𝔭²: 𝔡 = (2) = 𝔭².

theorem TauCeti.NumberField.GaussianRationals.multiplicity_differentIdeal_eq_two {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) (𝔭 : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {2})] : multiplicity 𝔭 (differentIdeal ℤ (NumberField.RingOfIntegers K)) = 2

The different exponent at the dyadic prime is 2 = e: v_𝔭(𝔡) = 2, the wild lower bound attained.

theorem TauCeti.NumberField.GaussianRationals.multiplicity_span_two_eq_two {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) (𝔭 : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {2})] : multiplicity 𝔭 (Ideal.span {2}) = 2

The dyadic valuation of 2 in ℚ(i) is 2: v_𝔭(2) = 2.

theorem TauCeti.NumberField.GaussianRationals.multiplicity_differentIdeal_lt_ramificationIdx_sub_one_add {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) (𝔭 : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {2})] : multiplicity 𝔭 (differentIdeal ℤ (NumberField.RingOfIntegers K)) < 𝔭.ramificationIdx ℤ - 1 + multiplicity 𝔭 (Ideal.span {↑(𝔭.ramificationIdx ℤ)})

The wild upper bound is strict in ℚ(i): at the dyadic prime, v_𝔭(𝔡) = 2 < 3 = e − 1 + v_𝔭(e).