Documentation

TauCeti.NumberTheory.NumberField.WorkedExamples.GaussianRationals.Invariants

Invariants of ℚ(i) #

For K generated over ℚ by an algebraic integer θ with minpoly ℤ θ = X² + 1: the radicand −1 is 3 modulo 4, so the quadratic-field theory of the radicand presentation applies directly: 𝓞 K = ℤ[θ], the field is monogenic with index 1, and discr K = 4 · (−1) = −4. The negative radicand rules out real places, so the signature is (0, 1) and the intrinsic label prefix is 2.0.4. The discriminant is below the quadratic Minkowski threshold, so 𝓞 K is a principal ideal domain and the class number is 1.

Main results #

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

The ring of integers of ℚ(i) is ℤ[θ]: the radicand −1 is not 1 modulo 4.

source
@[simp]
theorem TauCeti.NumberField.GaussianRationals.index_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 + 1) (hgen : ℚ[↑θ] = ⊤) :
IntegralPrimitiveElement.index ⟨θ, hgen⟩ = 1

The generator θ has index 1 in the full ring of integers.

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

ℚ(i) is monogenic, generated integrally by θ.

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

The discriminant of ℚ(i) is −4.

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

ℚ(i) has exactly one complex place: its discriminant −4 is negative.

source
theorem TauCeti.NumberField.GaussianRationals.isTotallyComplex {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 + 1) :
NumberField.IsTotallyComplex K

A number field containing a square root of −1 is totally complex.

source
theorem TauCeti.NumberField.GaussianRationals.nrRealPlaces_eq_zero {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 + 1) :
NumberField.InfinitePlace.nrRealPlaces K = 0

A number field containing a square root of −1 has no real place.

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

The intrinsic label prefix of ℚ(i) is 2.0.4.

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

ℤ[i] is a principal ideal domain: the discriminant −4 is below the quadratic Minkowski threshold 9 of isPrincipalIdealRing_of_finrank_eq_two_of_natAbs_discr_le_nine.

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

The class number of ℚ(i) is 1.