Number Field
Results named in Tau Ceti's TauCeti.NumberTheory.NumberField modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremBrill's theorem, parity form#
The number of complex places is even exactly when the discriminant is positive.
NumberField.InfinitePlace.even_nrComplexPlaces_iff_zero_lt_discr.{u_1} (K : Type u_1) [Field K]
[NumberField K] : Even (NumberField.InfinitePlace.nrComplexPlaces K) ↔ 0 < NumberField.discr K
Lean
Formalized in Tau Ceti as NumberField.InfinitePlace.even_nrComplexPlaces_iff_zero_lt_discr.
Sources
Used by 1
TheoremDedekind's criterion#
Let θ be an integral primitive element of K with minimal
polynomial f = minpoly ℤ θ, let p be a prime, and factor f mod p = ∏ i, φ i ^ e i into
distinct monic irreducible polynomials φ i over ZMod p, each with multiplicity e i > 0.
Choose lifts Φ i : ℤ[X] of the φ i and let H : ℤ[X] satisfy p H = f - ∏ i, Φ i ^ e i
(which records the factorisation, by map_minpoly_eq_prod_of_C_mul_eq). Then p does not
divide the index [𝓞 K : ℤ[θ]] if and only if, for every i, either e i = 1 or φ i does
not divide H mod p.
TauCeti.NumberField.IntegralPrimitiveElement.not_dvd_index_iff.{u_1, u_2} {K : Type u_1} [Field K]
[NumberField K] {p : ℕ} (θ : TauCeti.NumberField.IntegralPrimitiveElement K) [Fact (Nat.Prime p)]
{ι : Type u_2} [Fintype ι] {φ : ι → Polynomial (ZMod p)} {e : ι → ℕ} {Φ : ι → Polynomial ℤ}
{H : Polynomial ℤ} (hφ : ∀ (i : ι), Irreducible (φ i)) (hφm : ∀ (i : ι), (φ i).Monic)
(hinj : Function.Injective φ) (he : ∀ (i : ι), 0 < e i)
(hΦ : ∀ (i : ι), Polynomial.map (Int.castRingHom (ZMod p)) (Φ i) = φ i)
(hH : Polynomial.C ↑p * H = minpoly ℤ ↑θ - ∏ i, Φ i ^ e i) :
¬p ∣ θ.index ↔ ∀ (i : ι), e i = 1 ∨ ¬φ i ∣ Polynomial.map (Int.castRingHom (ZMod p)) H
Lean
Formalized in Tau Ceti as TauCeti.NumberField.IntegralPrimitiveElement.not_dvd_index_iff.
Other forms
Dedekind's criterion, the necessary direction. Formalized in Tau Ceti as TauCeti.NumberField.IntegralPrimitiveElement.dvd_index_of_ne_one_of_dvd_map.
TauCeti.NumberField.IntegralPrimitiveElement.dvd_index_of_ne_one_of_dvd_map.{u_1, u_2}
{K : Type u_1} [Field K] [NumberField K] {p : ℕ}
(θ : TauCeti.NumberField.IntegralPrimitiveElement K) [Fact (Nat.Prime p)] {ι : Type u_2}
[Fintype ι] {φ : ι → Polynomial (ZMod p)} {e : ι → ℕ} {Φ : ι → Polynomial ℤ} {H : Polynomial ℤ}
(i : ι) (hφi : Irreducible (φ i))
(hΦ : ∀ (i : ι), Polynomial.map (Int.castRingHom (ZMod p)) (Φ i) = φ i)
(hH : Polynomial.C ↑p * H = minpoly ℤ ↑θ - ∏ i, Φ i ^ e i) (h1 : e i ≠ 1) (he : 0 < e i)
(hdvd : φ i ∣ Polynomial.map (Int.castRingHom (ZMod p)) H) : p ∣ θ.index
Dedekind's criterion, the sufficient direction. Formalized in Tau Ceti as TauCeti.NumberField.IntegralPrimitiveElement.not_dvd_index_of_forall_eq_one_or_not_dvd_map.
TauCeti.NumberField.IntegralPrimitiveElement.not_dvd_index_of_forall_eq_one_or_not_dvd_map.{u_1,
u_2}
{K : Type u_1} [Field K] [NumberField K] {p : ℕ}
(θ : TauCeti.NumberField.IntegralPrimitiveElement K) [Fact (Nat.Prime p)] {ι : Type u_2}
[Fintype ι] {φ : ι → Polynomial (ZMod p)} {e : ι → ℕ} {Φ : ι → Polynomial ℤ} {H : Polynomial ℤ}
(hφ : ∀ (i : ι), Irreducible (φ i)) (hφm : ∀ (i : ι), (φ i).Monic) (hinj : Function.Injective φ)
(he : ∀ (i : ι), 0 < e i) (hΦ : ∀ (i : ι), Polynomial.map (Int.castRingHom (ZMod p)) (Φ i) = φ i)
(hH : Polynomial.C ↑p * H = minpoly ℤ ↑θ - ∏ i, Φ i ^ e i)
(hcrit : ∀ (i : ι), e i = 1 ∨ ¬φ i ∣ Polynomial.map (Int.castRingHom (ZMod p)) H) : ¬p ∣ θ.index
Sources
TheoremDirichlet's unit lattice theorem, with all places retained#
The logarithmic image of the units is a full integral lattice in the sum-zero hyperplane.
TauCeti.isZLattice_fullUnitLattice.{u_1} (K : Type u_1) [Field K] [NumberField K] :
IsZLattice ℝ (TauCeti.fullUnitLattice K)
TheoremDirichlet's unit theorem (NumberField.fg_units_integralClosure)#
Dirichlet's unit theorem (finite generation) for the integral closure of 𝓞 K in a
finite extension L of the number field K: its unit group is finitely generated.
NumberField.fg_units_integralClosure.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [Field L]
[Algebra K L] [NumberField K] [FiniteDimensional K L] :
Group.FG (↥(integralClosure (NumberField.RingOfIntegers K) L))ˣ
Lean
Formalized in Tau Ceti as NumberField.fg_units_integralClosure.
Other forms
Dirichlet's unit theorem, structural form. Formalized in Tau Ceti as NumberField.unitsMulEquivTorsionProdMultiplicative.
NumberField.unitsMulEquivTorsionProdMultiplicative.{u_1} (F : Type u_1) [Field F] [NumberField F] :
(NumberField.RingOfIntegers F)ˣ ≃*
↥(NumberField.Units.torsion F) × Multiplicative (Fin (NumberField.Units.rank F) → ℤ)
Sources
TheoremEvertse's lemma (Evertse; Bombieri–Gubler, Lemma 7.5.29)#
There is a constant C,
depending only on K and m, with the following property. Let S₀ be a finite set of finite
places, x a basis of a K-vector space V indexed by Fin m, and at every infinite place and
every place of S₀ let the forms L v k be linearly independent, the weights ν v k positive
and μ v nondecreasing, with |L v k (x j)|_v ≤ ν v k * μ v j. Then there are ξ j l ∈ K,
integral outside S₀, and permutations π v, such that y j = x j + ∑ l < j, ξ j l • x l
satisfies |L v (π v i) (y j)|_v ≤ C * (ν v (π v i) * min (μ v i) (μ v j)) at every infinite
place and |L v (π v i) (y j)|_v ≤ ν v (π v i) * min (μ v i) (μ v j) at every place of S₀.
NumberField.exists_evertse.{u_1, u_2} {K : Type u_1} [Field K] [NumberField K] (m : ℕ) :
∃ C,
∀ (V : Type u_2) [inst : AddCommGroup V] [inst_1 : _root_.Module K V]
(Sfin : Finset (NumberField.FinitePlace K)) (L : AbsoluteValue K ℝ → Fin m → Module.Dual K V)
(x : Module.Basis (Fin m) K V) (ν μ : AbsoluteValue K ℝ → Fin m → ℝ),
(∀ (v : NumberField.InfinitePlace K), LinearIndependent K (L ↑v)) →
(∀ v ∈ Sfin, LinearIndependent K (L ↑v)) →
(∀ (v : NumberField.InfinitePlace K) (k : Fin m), 0 < ν (↑v) k) →
(∀ v ∈ Sfin, ∀ (k : Fin m), 0 < ν (↑v) k) →
(∀ (v : NumberField.InfinitePlace K), Monotone (μ ↑v)) →
(∀ v ∈ Sfin, Monotone (μ ↑v)) →
(∀ (v : NumberField.InfinitePlace K) (k j : Fin m),
v ((L (↑v) k) (x j)) ≤ ν (↑v) k * μ (↑v) j) →
(∀ v ∈ Sfin, ∀ (k j : Fin m), v ((L (↑v) k) (x j)) ≤ ν (↑v) k * μ (↑v) j) →
∃ ξ π,
(∀ (j l : Fin m), ∀ u ∉ Sfin, u (ξ j l) ≤ 1) ∧
(∀ (v : NumberField.InfinitePlace K) (i j : Fin m),
v ((L (↑v) ((π ↑v) i)) (x j + ∑ l with l < j, ξ j l • x l)) ≤
C * (ν (↑v) ((π ↑v) i) * min (μ (↑v) i) (μ (↑v) j))) ∧
∀ v ∈ Sfin,
∀ (i j : Fin m),
v ((L (↑v) ((π ↑v) i)) (x j + ∑ l with l < j, ξ j l • x l)) ≤
ν (↑v) ((π ↑v) i) * min (μ (↑v) i) (μ (↑v) j)
Lean
Formalized in Tau Ceti as NumberField.exists_evertse.
Other forms
Evertse's lemma without weights (Evertse; Bombieri–Gubler, Lemma 7.5.29). Formalized in Tau Ceti as NumberField.exists_evertse_unweighted.
NumberField.exists_evertse_unweighted.{u_1, u_2} {K : Type u_1} [Field K] [NumberField K] (m : ℕ) :
∃ C,
∀ (V : Type u_2) [inst : AddCommGroup V] [inst_1 : _root_.Module K V]
(Sfin : Finset (NumberField.FinitePlace K)) (L : AbsoluteValue K ℝ → Fin m → Module.Dual K V)
(x : Module.Basis (Fin m) K V) (μ : AbsoluteValue K ℝ → Fin m → ℝ),
(∀ (v : NumberField.InfinitePlace K), LinearIndependent K (L ↑v)) →
(∀ v ∈ Sfin, LinearIndependent K (L ↑v)) →
(∀ (v : NumberField.InfinitePlace K), Monotone (μ ↑v)) →
(∀ v ∈ Sfin, Monotone (μ ↑v)) →
(∀ (v : NumberField.InfinitePlace K) (k j : Fin m), v ((L (↑v) k) (x j)) ≤ μ (↑v) j) →
(∀ v ∈ Sfin, ∀ (k j : Fin m), v ((L (↑v) k) (x j)) ≤ μ (↑v) j) →
∃ ξ π,
(∀ (j l : Fin m), ∀ u ∉ Sfin, u (ξ j l) ≤ 1) ∧
(∀ (v : NumberField.InfinitePlace K) (i j : Fin m),
v ((L (↑v) ((π ↑v) i)) (x j + ∑ l with l < j, ξ j l • x l)) ≤
C * min (μ (↑v) i) (μ (↑v) j)) ∧
∀ v ∈ Sfin,
∀ (i j : Fin m),
v ((L (↑v) ((π ↑v) i)) (x j + ∑ l with l < j, ξ j l • x l)) ≤
min (μ (↑v) i) (μ (↑v) j)
Sources
Uses 1
TheoremThe Galois action on the semi-local decomposition#
Under infiniteAdeleSemilocalEquiv,
the Galois action of σ ∈ Aut(L/K) on infinite adeles applies the base change id ⊗ σ to each
semi-local factor K_v ⊗[K] L.
TauCeti.GlobalNumberFields.infiniteAdeleSemilocalEquiv_infiniteAdeleGaloisAction.{u_1, u_2}
{K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L]
(σ : Gal(L/K)) (a : NumberField.InfiniteAdeleRing L) (v : NumberField.InfinitePlace K) :
(TauCeti.GlobalNumberFields.infiniteAdeleSemilocalEquiv K L)
(((TauCeti.GlobalNumberFields.infiniteAdeleGaloisAction K L) σ) a) v =
((TauCeti.Algebra.TensorProduct.baseChangeAutHom v.Completion L) σ)
((TauCeti.GlobalNumberFields.infiniteAdeleSemilocalEquiv K L) a v)
Lean
Formalized in Tau Ceti as TauCeti.GlobalNumberFields.infiniteAdeleSemilocalEquiv_infiniteAdeleGaloisAction.
Sources
Used by 9
H¹ · The Kronecker–Weber theorem · The Kummer case of the second fundamental inequality
TheoremHadamard's bound at ℚ(√2)#
The regulator is at most (2d) ^ r = 4 times the absolute
logarithmic height of the fundamental unit; here log (1 + √2) ≤ 4 · log (1 + √2) / 2.
TauCeti.NumberField.Sqrt2.regulator_le_four_mul_absLogHeight₁_one_add.{u_1} {K : Type u_1} [Field K]
[NumberField K] {θ : NumberField.RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - 2)
(hgen : ℚ[↑θ] = ⊤) : NumberField.Units.regulator K ≤ 4 * NumberField.absLogHeight₁ ↑(1 + θ)
Informally uses
Lean
Formalized in Tau Ceti as TauCeti.NumberField.Sqrt2.regulator_le_four_mul_absLogHeight₁_one_add.
Other forms
Hadamard's bound for the regulator. Formalized in Tau Ceti as TauCeti.NumberField.Units.regulator_le_prod_sum_abs_logEmbedding.
TauCeti.NumberField.Units.regulator_le_prod_sum_abs_logEmbedding.{u_1} {K : Type u_1} [Field K]
[NumberField K] {ε : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ}
(hε : Subgroup.closure (Set.range ε) ⊔ NumberField.Units.torsion K = ⊤) :
NumberField.Units.regulator K ≤
∏ i, ∑ w, |(NumberField.Units.logEmbedding K) (Additive.ofMul (ε i)) w|
Hadamard's bound for the regulator of a family. Formalized in Tau Ceti as TauCeti.NumberField.Units.regOfFamily_le_prod_sum_abs_logEmbedding.
TauCeti.NumberField.Units.regOfFamily_le_prod_sum_abs_logEmbedding.{u_1} {K : Type u_1} [Field K]
[NumberField K] (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ) :
NumberField.Units.regOfFamily u ≤
∏ i, ∑ w, |(NumberField.Units.logEmbedding K) (Additive.ofMul (u i)) w|
Hadamard's bound for the regulator of a family, over all places. Formalized in Tau Ceti as TauCeti.NumberField.Units.regOfFamily_le_prod_sum_mult_mul_abs_log.
TauCeti.NumberField.Units.regOfFamily_le_prod_sum_mult_mul_abs_log.{u_1} {K : Type u_1} [Field K]
[NumberField K] (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ) :
NumberField.Units.regOfFamily u ≤
∏ i, ∑ w, ↑w.mult * |Real.log (w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(u i)))|
Hadamard's bound for the regulator, over all places. Formalized in Tau Ceti as TauCeti.NumberField.Units.regulator_le_prod_sum_mult_mul_abs_log.
TauCeti.NumberField.Units.regulator_le_prod_sum_mult_mul_abs_log.{u_1} {K : Type u_1} [Field K]
[NumberField K] {ε : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ}
(hε : Subgroup.closure (Set.range ε) ⊔ NumberField.Units.torsion K = ⊤) :
NumberField.Units.regulator K ≤
∏ i, ∑ w, ↑w.mult * |Real.log (w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(ε i)))|
Sources
Uses 2 · Used by 1
TheoremHermite's theorem: finitely many extensions of bounded degree are unramified outside a finite set#
Inside a field A containing the number field K, only finitely many finite extensions
L / K have degree at most d and are ramified only at places in the finite set S.
TauCeti.NumberField.finite_of_finrank_le_of_ramifiedSupport_subset.{u_1, u_3} {K : Type u_1}
[Field K] [NumberField K] (A : Type u_3) [Field A] [Algebra K A] (d : ℕ)
(S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) :
{L | Module.finrank K ↥↑L ≤ d ∧ TauCeti.NumberField.ramifiedSupport K ↥↑L ⊆ S}.Finite
Lean
Formalized in Tau Ceti as TauCeti.NumberField.finite_of_finrank_le_of_ramifiedSupport_subset.
Sources
TheoremHilbert's different formula, checked in ℚ(i)#
the sum Σ_{i ≥ 0} (#G_i − 1) over the
ramification groups of the prime above 2 is the different exponent v_𝔭(𝔡) = 2, as the
general multiplicity_differentIdeal_eq_finsum_card_ramificationGroup_sub_one predicts.
TauCeti.NumberField.GaussianRationals.finsum_card_ramificationGroup_sub_one_eq_two.{u_1}
{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})] :
∑ᶠ (i : ℕ), (Nat.card ↥(Ideal.ramificationGroup Gal(K/ℚ) 𝔭 i) - 1) = 2
Lean
Formalized in Tau Ceti as TauCeti.NumberField.GaussianRationals.finsum_card_ramificationGroup_sub_one_eq_two.
Sources
Uses 1
TheoremHilbert's Theorem 90 for quadratic conjugation#
Let σ be the quadratic conjugation of a
quadratic number field and let x y : 𝓞 K with x ≠ 0 have equal norms, x σx = y σy. Then there
is a nonzero ε : 𝓞 K with x ε = y σε; equivalently y / x = ε / σε is a "coboundary". The
construction is explicit: ε = σx (x + y) works unless x + y = 0, and then ε = σx θ x does.
NumberField.exists_ne_zero_mul_eq_mul_ringOfIntegersQuadraticConj.{u_1} {K : Type u_1} [Field K]
[NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ}
(hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤)
{x y : NumberField.RingOfIntegers K} (hx : x ≠ 0)
(hnorm :
x * (NumberField.ringOfIntegersQuadraticConj hmin hgen) x =
y * (NumberField.ringOfIntegersQuadraticConj hmin hgen) y) :
∃ ε, ε ≠ 0 ∧ x * ε = y * (NumberField.ringOfIntegersQuadraticConj hmin hgen) ε
Lean
Formalized in Tau Ceti as NumberField.exists_ne_zero_mul_eq_mul_ringOfIntegersQuadraticConj.
Sources
Used by 1
TheoremThe Kummer–Dedekind counting bound#
For a θ whose conductor exponent is prime to p,
the primes of 𝓞 K above p with residue degree d are no more numerous than the degree-d
monic irreducible factors of minpoly ℤ θ modulo p.
TauCeti.NumberField.ncard_primesOverOfInertiaDeg_le.{u_1} {K : Type u_1} [Field K] [NumberField K]
(p : ℕ) [Fact (Nat.Prime p)] {θ : NumberField.RingOfIntegers K}
(hp : ¬p ∣ RingOfIntegers.exponent θ) (d : ℕ) :
(TauCeti.NumberField.primesOverOfInertiaDeg K p d).ncard ≤
{Q ∈ RingOfIntegers.monicFactorsMod θ p | Q.natDegree = d}.card
Lean
Formalized in Tau Ceti as TauCeti.NumberField.ncard_primesOverOfInertiaDeg_le.
Sources
TheoremLiouville's inequality at a finite place#
The absolute value of the order
-WithZero.log (v.valuation K x) of an element x of a number field at a finite place v,
weighted by the logarithm of the norm of v, is at most the logarithmic height of x. Both sides
vanish at x = 0.
IsDedekindDomain.HeightOneSpectrum.abs_log_valuation_mul_log_absNorm_le_logHeight₁.{u_1}
{K : Type u_1} [Field K] [NumberField K]
(v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : K) :
↑|((IsDedekindDomain.HeightOneSpectrum.valuation K v) x).log| *
Real.log ↑(Ideal.absNorm v.asIdeal) ≤
Height.logHeight₁ x
Lean
Formalized in Tau Ceti as IsDedekindDomain.HeightOneSpectrum.abs_log_valuation_mul_log_absNorm_le_logHeight₁.
Sources
Used by 1
TheoremSiegel's lemma over a number field, with rational integer unknowns (Evertse, Theorem 3.20)#
Let K be a number field of degree d and a a matrix over 𝓞 K with M rows
and N columns, whose entries have house at most A ≥ 1. If d * M < N, there is a nonzero
x ∈ ℤ^N with a x = 0 and |xⱼ| ≤ (3 N A) ^ (d M / (N - d M)) for every j.
NumberField.exists_ne_zero_int_vec_abs_le_of_house_le.{u_1, u_2, u_3} {K : Type u_1} [Field K]
[NumberField K] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β]
(a : Matrix α β (NumberField.RingOfIntegers K)) {A : ℝ} (hA : 1 ≤ A)
(hcard : Module.finrank ℚ K * Fintype.card α < Fintype.card β)
(ha : ∀ (i : α) (j : β), NumberField.house ↑(a i j) ≤ A) :
∃ x,
x ≠ 0 ∧
(a.mulVec fun j => ↑(x j)) = 0 ∧
∀ (j : β),
|↑(x j)| ≤
(3 * ↑(Fintype.card β) * A) ^
(↑(Module.finrank ℚ K) * ↑(Fintype.card α) /
(↑(Fintype.card β) - ↑(Module.finrank ℚ K) * ↑(Fintype.card α)))
Lean
Formalized in Tau Ceti as NumberField.exists_ne_zero_int_vec_abs_le_of_house_le.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.