The dyadic different of ℚ(√2)

For K generated over ℚ by an algebraic integer θ with minpoly ℤ θ = X² − 2, the radicand 2 is squarefree and not 1 modulo 4, so 𝓞 K = ℤ[θ] and discr K = 8. The prime 2 ramifies: 𝔭 = (θ) is the only prime of 𝓞 K above it, and 2 𝓞 K = 𝔭² since θ² = 2.

The different of ℤ[θ] is generated by f'(θ) = 2θ = θ³, so 𝔡 = 𝔭³. With e = 2 and v_𝔭(e) = v_𝔭(2) = 2, the different exponent v_𝔭(𝔡) = 3 equals e − 1 + v_𝔭(e): at this wildly ramified prime the upper bound of Dedekind's different theorem is attained, and the exponent strictly exceeds the lower bound e. In ℚ(i) the opposite happens, v_𝔭(𝔡) = e = 2 < 3 (GaussianRationals.multiplicity_differentIdeal_lt_ramificationIdx_sub_one_add), so neither bound determines the wild different exponent.

Main results

• TauCeti.NumberField.Sqrt2.adjoin_eq_top: 𝓞 K = ℤ[θ], and discr_eq_eight: discr K = 8.
• TauCeti.NumberField.Sqrt2.eq_span_gen: the prime above 2 is (θ), with ramificationIdx_eq_two: e = 2, and map_span_two_eq_sq: 2 𝓞 K = 𝔭².
• TauCeti.NumberField.Sqrt2.differentIdeal_eq_pow_three and multiplicity_differentIdeal_eq_three: 𝔡 = 𝔭³, that is v_𝔭(𝔡) = 3.
• TauCeti.NumberField.Sqrt2.multiplicity_span_two_eq_two: v_𝔭(2) = 2.
• TauCeti.NumberField.Sqrt2.multiplicity_differentIdeal_eq_ramificationIdx_sub_one_add: v_𝔭(𝔡) = e − 1 + v_𝔭(e), and ramificationIdx_lt_multiplicity_differentIdeal: e < v_𝔭(𝔡).

References

• J. Neukirch, Algebraic Number Theory, Chapter III, Theorem 2.6.
• J.-P. Serre, Local Fields, Chapter III, §6, Proposition 13.

@[simp]

theorem TauCeti.NumberField.Sqrt2.sq_eq_two {K : Type u_1} [Field K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - 2) : θ ^ 2 = 2

The defining identity θ² = 2.

theorem TauCeti.NumberField.Sqrt2.finrank_eq_two {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - 2) (hgen : ℚ[↑θ] = ⊤) : Module.finrank ℚ K = 2

ℚ(√2) has degree 2.

@[simp]

theorem TauCeti.NumberField.Sqrt2.adjoin_eq_top {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - 2) (hgen : ℚ[↑θ] = ⊤) : ℤ[θ] = ⊤

The ring of integers of ℚ(√2) is ℤ[θ]: the radicand 2 is squarefree and not 1 modulo 4.

theorem TauCeti.NumberField.Sqrt2.discr_eq_eight {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - 2) (hgen : ℚ[↑θ] = ⊤) : NumberField.discr K = 8

The discriminant of ℚ(√2) is 8.

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

2 ramifies in ℚ(√2): it divides the discriminant 8.

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

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

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

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

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

The prime above 2 in ℚ(√2) is (θ).

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

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

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

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

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

The different of ℚ(√2) is 𝔭³.

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

The different exponent of ℚ(√2) at the dyadic prime is 3: v_𝔭(𝔡) = 3.

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

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

theorem TauCeti.NumberField.Sqrt2.multiplicity_differentIdeal_eq_ramificationIdx_sub_one_add {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - 2) (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 attained in ℚ(√2): at the dyadic prime, v_𝔭(𝔡) = e − 1 + v_𝔭(e), with e = 2 and both sides equal to 3.

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

The wild lower bound is strict in ℚ(√2): at the dyadic prime, e = 2 < 3 = v_𝔭(𝔡).