Imaginary quadratic fields: class numbers, finiteness and class number one
The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.
TheoremThe radicand classification of imaginary quadratic fields#
Every totally complex number
field of degree 2 over ℚ is isomorphic to QuadraticAlgebra ℚ d 0 for exactly one negative
squarefree integer d.
NumberField.existsUnique_neg_squarefree_algEquiv.{u_1} {K : Type u_1} [Field K] [NumberField K]
[NumberField.IsTotallyComplex K] (hK : Module.finrank ℚ K = 2) :
∃! d, d < 0 ∧ Squarefree d ∧ Nonempty (K ≃ₐ[ℚ] QuadraticAlgebra ℚ (↑d) 0)
Lean
Formalized in Tau Ceti as NumberField.existsUnique_neg_squarefree_algEquiv.
Sources
TheoremThe squarefree radicand is an isomorphism invariant#
Two quadratic fields presented by
square roots of squarefree integers d and e are ℚ-isomorphic exactly when d = e. Taking
L = K and the identity shows that the squarefree radicand of a quadratic field does not depend on
the presentation.
NumberField.nonempty_algEquiv_iff_of_squarefree.{u_1, u_2} {K : Type u_1} {L : Type u_2} [Field K]
[NumberField K] [Field L] [NumberField L] {d e : ℤ} (hK : Module.finrank ℚ K = 2)
(hL : Module.finrank ℚ L = 2) {θ : NumberField.RingOfIntegers K}
{η : NumberField.RingOfIntegers L} (hθ : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d)
(hη : minpoly ℤ η = Polynomial.X ^ 2 - Polynomial.C e) (hd : Squarefree d) (he : Squarefree e) :
Nonempty (K ≃ₐ[ℚ] L) ↔ d = e
Lean
Formalized in Tau Ceti as NumberField.nonempty_algEquiv_iff_of_squarefree.
Sources
TheoremThe two complex embeddings of an imaginary quadratic field#
For a nonsquare a ≤ 0, every
complex embedding of the field QuadraticAlgebra ℚ a 0 is the distinguished embedding or its
complex conjugate.
QuadraticAlgebra.ringHom_eq_or_eq_conjugate {a : ℚ} [Fact ¬IsSquare a] (ha : a ≤ 0)
(φ : QuadraticAlgebra ℚ a 0 →+* ℂ) :
φ = ↑(QuadraticAlgebra.complexEmbedding ha) ∨
φ = NumberField.ComplexEmbedding.conjugate ↑(QuadraticAlgebra.complexEmbedding ha)
Uses 1
ℚ(√a) for a ≤ 0TheoremQuadraticAlgebra.nrComplexPlaces_eq_one#
An imaginary quadratic field has exactly one complex place, so its signature is (0, 1).
QuadraticAlgebra.nrComplexPlaces_eq_one {a : ℚ} [Fact ¬IsSquare a] (ha : a < 0) :
NumberField.InfinitePlace.nrComplexPlaces (QuadraticAlgebra ℚ a 0) = 1
TheoremDirichletCharacter.LFunction_apply_one_pos#
The value at s = 1 of the L-function of a nontrivial quadratic Dirichlet character is a
positive real number.
DirichletCharacter.LFunction_apply_one_pos {N : ℕ} {χ : DirichletCharacter ℂ N} [NeZero N]
(hχ : MulChar.IsQuadratic χ) (hχ₁ : χ ≠ 1) : 0 < DirichletCharacter.LFunction χ 1
TheoremDistinct proper classes of primitive positive definite forms have distinct Picard classes#
This is the injective half of the correspondence between proper classes of primitive positive
definite forms of discriminant -n and the Picard group of the order of discriminant -n.
TauCeti.BinaryQuadraticForm.posDefProperClassToPic_injective (n : ℕ) [NeZero n]
(hn : -↑n % 4 = 0 ∨ -↑n % 4 = 1) :
Function.Injective (TauCeti.BinaryQuadraticForm.posDefProperClassToPic n hn)
Lean
Formalized in Tau Ceti as TauCeti.BinaryQuadraticForm.posDefProperClassToPic_injective.
Sources
- Tau Ceti documentation:
TauCeti.BinaryQuadraticForm.posDefProperClassToPic_injective - Source of
TauCeti.BinaryQuadraticForm.posDefProperClassToPic_injectivein TauCeti/NumberTheory/BinaryQuadraticForm/Ideal/Class.lean - Tau Ceti roadmap status: Imaginary quadratic fields: class numbers, finiteness and class number one
Uses 1
DefinitionThe distinguished complex embedding of ℚ(√a) for a ≤ 0#
the ℚ-algebra map
QuadraticAlgebra ℚ a 0 →ₐ[ℚ] ℂ sending ω to √(-a) · i, the square root of a with
nonnegative imaginary part.
QuadraticAlgebra.complexEmbedding {a : ℚ} (ha : a ≤ 0) : QuadraticAlgebra ℚ a 0 →ₐ[ℚ] ℂ
Used by 1
DefinitionThe Siegel function g_r(τ) attached to r = (r₁, r₂) ∈ ℝ²#
g_r(τ) = -e^{π i B₂(r₁) τ} e^{π i r₂ (r₁ - 1)} (1 - w) ∏_{n ≥ 1} (1 - qⁿ w) (1 - qⁿ w⁻¹)
with q = e^{2π i τ}, w = e^{2π i (r₁ τ + r₂)} and B₂ = bernoulliFun 2 the second Bernoulli
polynomial x² - x + 1/6. The product converges for τ in the upper half-plane, where g_r is
holomorphic; elsewhere the value is a junk value.
TauCeti.ModularForm.siegelFunction (r : Fin 2 → ℝ) (τ : ℂ) : ℂ
Used by 1
DefinitionTauCeti.qTheta#
The theta product θ_q(w) = (w; q)_∞ (q w⁻¹; q)_∞, written as
(1 - w) ∏_{n ≥ 1} (1 - qⁿ w) (1 - qⁿ w⁻¹). The product converges for ‖q‖ < 1; otherwise the
value is a junk value. With q = e^{2π i τ} and w = e^{2π i (r₁ τ + r₂)} it is the product in
the Siegel function g_r(τ).
TauCeti.qTheta.{u_1} {𝕜 : Type u_1} [NormedField 𝕜] (q w : 𝕜) : 𝕜
Used by 1
DefinitionThe Picard class of a proper class of primitive positive definite forms#
The Picard class of a proper class of primitive positive definite forms, the class of
aℤ + ((-b + √(-n))/2)ℤ in the Picard group of the quadratic order of discriminant -n.
TauCeti.BinaryQuadraticForm.posDefProperClassToPic (n : ℕ) [NeZero n]
(hn : -↑n % 4 = 0 ∨ -↑n % 4 = 1) :
TauCeti.BinaryQuadraticForm.PosDefProperClass n →
TauCeti.GlobalNumberFields.Pic (TauCeti.QuadraticOrder.numberFieldOrder (-↑n) hn)
Lean
Formalized in Tau Ceti as TauCeti.BinaryQuadraticForm.posDefProperClassToPic.
Sources
TheoremEuler's identity (TauCeti.tprod_one_add_pow_mul_tprod_one_sub_pow_odd)#
Euler's identity ∏_{n ≥ 1} (1 + qⁿ) ∏_{n ≥ 0} (1 - q^{2n+1}) = 1 for ‖q‖ < 1. Comparing
coefficients, partitions into distinct parts and partitions into odd parts are equinumerous.
TauCeti.tprod_one_add_pow_mul_tprod_one_sub_pow_odd.{u_1} {𝕜 : Type u_1} [NormedField 𝕜]
[CompleteSpace 𝕜] {q : 𝕜} (hq : ‖q‖ < 1) :
(∏' (n : ℕ), (1 + q ^ (n + 1))) * ∏' (n : ℕ), (1 - q ^ (2 * n + 1)) = 1
Lean
Formalized in Tau Ceti as TauCeti.tprod_one_add_pow_mul_tprod_one_sub_pow_odd.
Sources
Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.