@[reducible, inline]

noncomputable abbrev FieldNormTrace.fieldNorm (k : Type u_1) {K : Type u_2} [CommRing k] [Ring K] [Algebra k K] : K →* k

The field norm K → k of a k-algebra K, packaged as a monoid homomorphism.

@[reducible, inline]

noncomputable abbrev FieldNormTrace.fieldTrace (k : Type u_1) (K : Type u_2) [CommRing k] [CommRing K] [Algebra k K] : K →ₗ[k] k

The field trace K → k of a k-algebra K, packaged as a k-linear map.

theorem FieldNormTrace.norm_eq_sq {D : ℤ} (α : ℤ√D) : α.norm = α.re ^ 2 - D * α.im ^ 2

The norm form on ℤ√D: N(α) = α.re² - D · α.im².

theorem FieldNormTrace.norm_eq_mul_conj {D : ℤ} (α : ℤ√D) : ↑α.norm = α * star α

The norm of α ∈ ℤ√D, embedded back into ℤ√D, equals α · star α.

theorem FieldNormTrace.trace_eq {D : ℤ} (α : ℤ√D) : α + star α = ↑(2 * α.re)

The trace form on ℤ√D: α + star α = 2 · α.re (as an element of ℤ√D).

theorem FieldNormTrace.trace_re {D : ℤ} (α : ℤ√D) : (α + star α).re = 2 * α.re

The real part of α + star α equals 2 · α.re.

theorem FieldNormTrace.trace_im {D : ℤ} (α : ℤ√D) : (α + star α).im = 0

The imaginary part of α + star α vanishes.

theorem FieldNormTrace.conj_eq_trace_sub {D : ℤ} (α : ℤ√D) : star α = ↑(2 * α.re) - α

The conjugate star α equals 2 · α.re - α.

theorem FieldNormTrace.mul_star_re {D : ℤ} (α : ℤ√D) : (α * star α).re = α.re ^ 2 - D * α.im ^ 2

The real part of α · star α equals the norm α.re² - D · α.im².

theorem FieldNormTrace.mul_star_im {D : ℤ} (α : ℤ√D) : (α * star α).im = 0

The imaginary part of α · star α vanishes.

theorem FieldNormTrace.norm_mul {D : ℤ} (α β : ℤ√D) : (α * β).norm = α.norm * β.norm

Multiplicativity of the norm on ℤ√D: N(αβ) = N(α) · N(β).

theorem FieldNormTrace.norm_conj {D : ℤ} (α : ℤ√D) : (star α).norm = α.norm

The norm is invariant under conjugation: N(star α) = N(α).

theorem FieldNormTrace.norm_nonneg {D : ℤ} (hD : D ≤ 0) (α : ℤ√D) : 0 ≤ α.norm

For D ≤ 0 (imaginary quadratic case), the norm on ℤ√D is nonnegative.

def QuadraticOrder.disc (t n : ℤ) : ℤ

The discriminant t² - 4n of a monic quadratic x² - t x + n.

@[simp]

theorem QuadraticOrder.disc_def (t n : ℤ) : disc t n = t ^ 2 - 4 * n

Defining equation for disc: disc t n = t² - 4n.

def QuadraticOrder.traceZ {d : ℤ} (τ : ℤ√d) : ℤ

The integer trace of τ ∈ ℤ√d, defined as 2 · τ.re.

@[simp]

theorem QuadraticOrder.traceZ_eq {d : ℤ} (τ : ℤ√d) : traceZ τ = 2 * τ.re

Defining equation for traceZ.

def QuadraticOrder.discZsqrtd {d : ℤ} (τ : ℤ√d) : ℤ

The discriminant of τ ∈ ℤ√d, given by disc (traceZ τ) (N τ).

@[simp]

theorem QuadraticOrder.discZsqrtd_eq {d : ℤ} (τ : ℤ√d) : discZsqrtd τ = 4 * d * τ.im ^ 2

Computation: the discriminant of τ ∈ ℤ√d equals 4 d · τ.im².

theorem QuadraticOrder.discZsqrtd_eq_sq_sub_conj_re {d : ℤ} (τ : ℤ√d) : discZsqrtd τ = ((τ - star τ) * (τ - star τ)).re

The discriminant of τ can also be expressed as Re((τ - star τ)²).

theorem QuadraticOrder.sq_sub_conj_im_eq_zero {d : ℤ} (τ : ℤ√d) : ((τ - star τ) * (τ - star τ)).im = 0

The imaginary part of (τ - star τ)² vanishes.

theorem QuadraticOrder.discZsqrtd_eq_trace_sq_sub_four_norm {d : ℤ} (τ : ℤ√d) : discZsqrtd τ = traceZ τ ^ 2 - 4 * τ.norm

The discriminant of τ equals (traceZ τ)² - 4 · N(τ), exhibiting it as the discriminant of the minimal polynomial.

theorem QuadraticOrder.discZsqrtd_sqrtd {d : ℤ} : discZsqrtd { re := 0, im := 1 } = 4 * d

The element √d ∈ ℤ√d has discriminant 4d.

def ImaginaryQuadraticDiscriminant.IsImaginaryQuadraticDiscriminant (D : ℤ) : Prop

D is an imaginary quadratic discriminant if D < 0 and D ≡ 0 or 1 (mod 4).

def ImaginaryQuadraticDiscriminant.IsFundamentalImaginaryQuadraticDiscriminant (D : ℤ) : Prop

D is a fundamental imaginary quadratic discriminant if it is an imaginary quadratic discriminant and is not of the form u² · D' for u > 1 and another imaginary quadratic discriminant D'.

structure ImaginaryQuadraticDiscriminant.ImaginaryQuadraticDiscriminantDecomposition (D : ℤ) : Type

A decomposition D = u² · D_K of an imaginary quadratic discriminant D into the conductor u ≥ 1 and the fundamental discriminant D_K of the maximal order.

• u : ℤ
• D_K : ℤ
• hu : self.u ≥ 1
• hD_K : IsFundamentalImaginaryQuadraticDiscriminant self.D_K
• hD : D = self.u ^ 2 * self.D_K

theorem ImaginaryQuadraticDiscriminant.discriminant_decomposition_exists (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : ∃ (D_K : ℤ), ∃ u ≥ 1, IsFundamentalImaginaryQuadraticDiscriminant D_K ∧ D = u ^ 2 * D_K

Every imaginary quadratic discriminant D admits a decomposition D = u² · D_K where D_K is fundamental and u ≥ 1.

theorem ImaginaryQuadraticDiscriminant.discriminant_decomposition_unique (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) {D_K₁ D_K₂ u₁ u₂ : ℤ} (hu₁ : u₁ ≥ 1) (hu₂ : u₂ ≥ 1) (hfund₁ : IsFundamentalImaginaryQuadraticDiscriminant D_K₁) (hfund₂ : IsFundamentalImaginaryQuadraticDiscriminant D_K₂) (h₁ : D = u₁ ^ 2 * D_K₁) (h₂ : D = u₂ ^ 2 * D_K₂) : u₁ = u₂ ∧ D_K₁ = D_K₂

Uniqueness of the decomposition D = u² · D_K: the conductor u and fundamental discriminant D_K are uniquely determined by D.

@[reducible, inline]

abbrev FractionalOIdeal (R : Type u_1) [CommRing R] [IsDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : Type u_2

Convenient abbreviation FractionalOIdeal R K for the type of fractional R-ideals in the fraction field K.

theorem FractionalOIdeal.mul_eq {R : Type u_1} [CommRing R] [IsDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (l l' : K) (a a' : Ideal R) : FractionalIdeal.spanSingleton (nonZeroDivisors R) l * ↑a * (FractionalIdeal.spanSingleton (nonZeroDivisors R) l' * ↑a') = FractionalIdeal.spanSingleton (nonZeroDivisors R) (l * l') * ↑(a * a')

Multiplicativity formula for fractional ideals written in the form (l) · a where l is a scalar and a an integral ideal: ((l)·a) · ((l')·a') = (l·l') · (a·a').

noncomputable def NormTrace.idealNorm {𝒪 : Type u_1} [CommRing 𝒪] (𝔞 : Ideal 𝒪) : ℕ

The ideal norm N(𝔞) := |𝒪/𝔞|, defined as the cardinality of the quotient ring.

theorem NormTrace.idealNorm_eq_card_quotient {𝒪 : Type u_1} [CommRing 𝒪] (𝔞 : Ideal 𝒪) : idealNorm 𝔞 = Nat.card (𝒪 ⧸ 𝔞)

Defining property of idealNorm: it equals the cardinality of 𝒪 / 𝔞.

theorem NormTrace.idealNorm_top {𝒪 : Type u_1} [CommRing 𝒪] : idealNorm ⊤ = 1

The norm of the unit ideal is 1.

theorem NormTrace.idealNorm_bot {𝒪 : Type u_1} [CommRing 𝒪] [Infinite 𝒪] : idealNorm ⊥ = 0

The norm of the zero ideal in an infinite ring is 0.

theorem NormTrace.idealNorm_pos {𝒪 : Type u_2} [CommRing 𝒪] [IsDomain 𝒪] [Module.Free ℤ 𝒪] [Module.Finite ℤ 𝒪] (𝔞 : Ideal 𝒪) (h : 𝔞 ≠ ⊥) : 0 < idealNorm 𝔞

For a free, finite ℤ-module domain 𝒪, every nonzero ideal has positive (and hence finite, nonzero) norm.

theorem NormTrace.idealNorm_eq_absNorm {𝒪 : Type u_2} [CommRing 𝒪] [Nontrivial 𝒪] [IsDedekindDomain 𝒪] [Module.Free ℤ 𝒪] (𝔞 : Ideal 𝒪) : Ideal.absNorm 𝔞 = idealNorm 𝔞

For a Dedekind domain 𝒪 that is free as a ℤ-module, the Ideal.absNorm agrees with the cardinality-based idealNorm defined here.

theorem PrincipalIdealNorm.idealNorm_span_singleton_eq_natAbs_norm {𝒪 : Type u_1} [CommRing 𝒪] [IsDedekindDomain 𝒪] [Module.Free ℤ 𝒪] [Module.Finite ℤ 𝒪] (α : 𝒪) : NormTrace.idealNorm (Ideal.span {α}) = ((Algebra.norm ℤ) α).natAbs

For a principal ideal (α) in a Dedekind domain, the ideal norm equals |N(α)|, as natural numbers.

theorem PrincipalIdealNorm.idealNorm_span_singleton_eq_abs_norm {𝒪 : Type u_1} [CommRing 𝒪] [IsDedekindDomain 𝒪] [Module.Free ℤ 𝒪] [Module.Finite ℤ 𝒪] (α : 𝒪) : ↑(NormTrace.idealNorm (Ideal.span {α})) = |(Algebra.norm ℤ) α|

Integer version: (N (α)) = |N_{𝒪/ℤ}(α)| for principal ideals.

theorem PrincipalIdealNorm.idealNorm_principal_ringOfIntegers (K : Type u_1) [Field K] [NumberField K] (α : NumberField.RingOfIntegers K) : Ideal.absNorm (Ideal.span {α}) = ((Algebra.norm ℤ) α).natAbs

Specialised version for the ring of integers of a number field K: N((α)) = |N_{K/ℚ}(α)|.

theorem IdealNormMultiplicativity.mem_span_singleton_mul {𝒪 : Type u_1} [CommRing 𝒪] [IsDomain 𝒪] [Module.Free ℤ 𝒪] [Module.Finite ℤ 𝒪] {α : 𝒪} {𝔞 : Ideal 𝒪} {z : 𝒪} (hz : z ∈ Ideal.span {α} * 𝔞) : ∃ w ∈ 𝔞, z = α * w

Membership lemma: any element of (α) · 𝔞 is of the form α · w for some w ∈ 𝔞.

theorem IdealNormMultiplicativity.idealNorm_mul_principal {𝒪 : Type u_1} [CommRing 𝒪] [IsDomain 𝒪] [Module.Free ℤ 𝒪] [Module.Finite ℤ 𝒪] (α : 𝒪) (𝔞 : Ideal 𝒪) : NormTrace.idealNorm (Ideal.span {α} * 𝔞) = NormTrace.idealNorm (Ideal.span {α}) * NormTrace.idealNorm 𝔞

Multiplicativity of the ideal norm against a principal ideal: N((α) · 𝔞) = N((α)) · N(𝔞).

theorem IdealNormMultiplicativity.idealNorm_smul_eq_natAbs_mul {𝒪 : Type u_1} [CommRing 𝒪] [IsDomain 𝒪] [Module.Free ℤ 𝒪] [Module.Finite ℤ 𝒪] [IsDedekindDomain 𝒪] (α : 𝒪) (𝔞 : Ideal 𝒪) : NormTrace.idealNorm (Ideal.span {α} * 𝔞) = ((Algebra.norm ℤ) α).natAbs * NormTrace.idealNorm 𝔞

Refined version in the Dedekind case: N((α) · 𝔞) = |N(α)| · N(𝔞).

noncomputable def FractionalIdealNorm.fractionalIdealNorm {𝒪 : Type u_1} [CommRing 𝒪] [IsDedekindDomain 𝒪] [Module.Free ℤ 𝒪] {K : Type u_2} [CommRing K] [Algebra 𝒪 K] (𝔟 : FractionalIdeal (nonZeroDivisors 𝒪) K) : ℚ

The norm of a fractional ideal 𝔟 = (1/d) · 𝔟.num: N(𝔟) = N(𝔟.num) / |N(𝔟.den)|, as a rational number.

theorem FractionalIdealNorm.fractionalIdealNorm_eq_absNorm {𝒪 : Type u_1} [CommRing 𝒪] [IsDedekindDomain 𝒪] [Module.Free ℤ 𝒪] [Module.Finite ℤ 𝒪] {K : Type u_2} [CommRing K] [Algebra 𝒪 K] [IsFractionRing 𝒪 K] (𝔟 : FractionalIdeal (nonZeroDivisors 𝒪) K) : fractionalIdealNorm 𝔟 = FractionalIdeal.absNorm 𝔟

The fractional ideal norm defined here agrees with Mathlib's FractionalIdeal.absNorm.

theorem FractionalIdealNorm.fractionalIdealNorm_eq {𝒪 : Type u_1} [CommRing 𝒪] [IsDedekindDomain 𝒪] [Module.Free ℤ 𝒪] [Module.Finite ℤ 𝒪] {K : Type u_2} [CommRing K] [Algebra 𝒪 K] [IsFractionRing 𝒪 K] (𝔟 : FractionalIdeal (nonZeroDivisors 𝒪) K) : fractionalIdealNorm 𝔟 = ↑(Ideal.absNorm 𝔟.num) / ↑|(Algebra.norm ℤ) ↑𝔟.den|

Definitional unfolding of fractionalIdealNorm.

theorem nsmul_mem_of_card_quotient {M : Type u_1} [AddCommGroup M] [Module ℤ M] (N : Submodule ℤ M) (x : M) : Nat.card (M ⧸ N) • x ∈ N

For any ℤ-submodule N of M, the cardinality of M/N (as a natural number) times x lies in N, for every x ∈ M.

theorem zsmul_mem_of_card_quotient {M : Type u_1} [AddCommGroup M] [Module ℤ M] (N : Submodule ℤ M) (x : M) : ↑(Nat.card (M ⧸ N)) • x ∈ N

Integer-scalar version of nsmul_mem_of_card_quotient.

theorem nsmul_top_eq_pi (n : ℤ) : Submodule.map (n • LinearMap.id) ⊤ = Submodule.pi Set.univ fun (x : Fin 2) => ℤ ∙ n

For n : ℤ, the image n · (Fin 2 → ℤ) under scalar multiplication equals the product of singleton spans Π i, ⟨n⟩.

theorem nat_card_int_quotient_span (n : ℕ) : Nat.card (ℤ ⧸ ℤ ∙ ↑n) = n

The cardinality of ℤ / ⟨n⟩ equals n (for a natural number n).

theorem nat_card_quotient_nsmul (n : ℕ) : Nat.card ((Fin 2 → ℤ) ⧸ Submodule.map (↑n • LinearMap.id) ⊤) = n ^ 2

The cardinality of (Fin 2 → ℤ) / n·(Fin 2 → ℤ) equals n².

theorem nsmul_le_of_card_quotient (N : Submodule ℤ (Fin 2 → ℤ)) (n : ℕ) (hindex : Nat.card ((Fin 2 → ℤ) ⧸ N) = n) : Submodule.map (↑n • LinearMap.id) ⊤ ≤ N

For a sublattice N of (Fin 2 → ℤ) of index n, the sublattice n·(Fin 2 → ℤ) is contained in N.

theorem sublattice_index_nsmul (N : Submodule ℤ (Fin 2 → ℤ)) (n : ℕ) (hn : 0 < n) (hindex : Nat.card ((Fin 2 → ℤ) ⧸ N) = n) : Nat.card ↥(Submodule.map (Submodule.map (↑n • LinearMap.id) ⊤).mkQ N) = n

For a sublattice N of (Fin 2 → ℤ) of index n > 0, the image of N in (Fin 2 → ℤ) / n·(Fin 2 → ℤ) also has cardinality n.

theorem ComplexLattice.endomorphismRing_eq_of_homothetic {L L' : ComplexLattice} (h : L.IsHomothetic L') : L'.endomorphismRing = L.endomorphismRing

The endomorphism ring of a complex lattice is invariant under homothety: if L and L' are homothetic, then End(L) = End(L').

theorem ComplexLattice.IsProperIdeal.of_homothetic {𝒪 : Subring ℂ} {L L' : ComplexLattice} (hL : IsProperIdeal 𝒪 L) (hom : L.IsHomothetic L') : IsProperIdeal 𝒪 L'

Being a proper 𝒪-ideal is preserved under homothety of lattices.

theorem ComplexLattice.isProperIdeal_iff_of_homothetic {𝒪 : Subring ℂ} {L L' : ComplexLattice} (hom : L.IsHomothetic L') : IsProperIdeal 𝒪 L ↔ IsProperIdeal 𝒪 L'

Equivalence: L is a proper 𝒪-ideal iff its homothetic image L' is.

structure ImagQuadDiscriminant.ImaginaryQuadraticOrder : Type

An imaginary quadratic order, presented by a trace t and a norm n such that the discriminant t² - 4n is negative and ≡ 0 or 1 (mod 4).

• t : ℤ
• n : ℤ
• hdisc_neg : self.t ^ 2 - 4 * self.n < 0
• hdisc_mod : (self.t ^ 2 - 4 * self.n) % 4 = 0 ∨ (self.t ^ 2 - 4 * self.n) % 4 = 1

def ImagQuadDiscriminant.ImaginaryQuadraticOrder.discriminant (𝒪 : ImaginaryQuadraticOrder) : ℤ

The discriminant t² - 4n of an imaginary quadratic order.

def ImagQuadDiscriminant.ImaginaryQuadraticOrder.SameOrder (𝒪₁ 𝒪₂ : ImaginaryQuadraticOrder) : Prop

Two imaginary quadratic orders agree (define the same order) when they have the same discriminant and the same trace parity.

theorem ImagQuadDiscriminant.sq_mod_four_iff (t : ℤ) : t % 2 = 0 ∧ t ^ 2 % 4 = 0 ∨ t % 2 = 1 ∧ t ^ 2 % 4 = 1

Case split for t² (mod 4): either t is even and t² ≡ 0 (mod 4), or t is odd and t² ≡ 1 (mod 4).

theorem ImagQuadDiscriminant.mod_two_eq_of_sq_mod_four_eq {t₁ t₂ : ℤ} (h : t₁ ^ 2 % 4 = t₂ ^ 2 % 4) : t₁ % 2 = t₂ % 2

If t₁² ≡ t₂² (mod 4), then t₁ and t₂ have the same parity.

theorem ImagQuadDiscriminant.trace_parity_eq_of_disc_eq {t₁ n₁ t₂ n₂ : ℤ} (heq : t₁ ^ 2 - 4 * n₁ = t₂ ^ 2 - 4 * n₂) : t₁ % 2 = t₂ % 2

If two trace-norm pairs (t₁, n₁) and (t₂, n₂) have the same discriminant, then their traces have the same parity.

theorem ImagQuadDiscriminant.existence (D : ℤ) (hD : ImaginaryQuadraticDiscriminant.IsImaginaryQuadraticDiscriminant D) : ∃ (𝒪 : ImaginaryQuadraticOrder), 𝒪.discriminant = D

Existence: every imaginary quadratic discriminant D arises from some ImaginaryQuadraticOrder.

theorem ImagQuadDiscriminant.uniqueness (𝒪₁ 𝒪₂ : ImaginaryQuadraticOrder) (hD : 𝒪₁.discriminant = 𝒪₂.discriminant) : 𝒪₁.SameOrder 𝒪₂

Uniqueness: two ImaginaryQuadraticOrders with the same discriminant satisfy SameOrder.

def ImagQuadDiscriminant.orderFromDecomposition {D : ℤ} (dec : ImaginaryQuadraticDiscriminant.ImaginaryQuadraticDiscriminantDecomposition D) : ImaginaryQuadraticOrder

Construct an ImaginaryQuadraticOrder of discriminant D = u² · D_K from the decomposition dec into a conductor u and a fundamental discriminant D_K.

theorem ImagQuadDiscriminant.orderFromDecomposition_disc {D : ℤ} (dec : ImaginaryQuadraticDiscriminant.ImaginaryQuadraticDiscriminantDecomposition D) : (orderFromDecomposition dec).discriminant = D

The order built by orderFromDecomposition has discriminant equal to D.

def ImagQuadDiscriminant.maximalOrder (D_K : ℤ) (hfund : ImaginaryQuadraticDiscriminant.IsFundamentalImaginaryQuadraticDiscriminant D_K) : ImaginaryQuadraticOrder

The maximal order of an imaginary quadratic field with fundamental discriminant D_K, constructed as an ImaginaryQuadraticOrder.

theorem ImagQuadDiscriminant.maximalOrder_disc (D_K : ℤ) (hfund : ImaginaryQuadraticDiscriminant.IsFundamentalImaginaryQuadraticDiscriminant D_K) : (maximalOrder D_K hfund).discriminant = D_K

The maximal order constructed by maximalOrder has the prescribed discriminant D_K.

theorem ImagQuadDiscriminant.conductor_eq {D : ℤ} (dec : ImaginaryQuadraticDiscriminant.ImaginaryQuadraticDiscriminantDecomposition D) : (orderFromDecomposition dec).discriminant = dec.u ^ 2 * (maximalOrder dec.D_K ⋯).discriminant

The conductor relation: the discriminant of orderFromDecomposition dec is u² times the discriminant of the maximal order with fundamental discriminant D_K.

theorem ImagQuadDiscriminant.exists_unique_order (D : ℤ) (hD : ImaginaryQuadraticDiscriminant.IsImaginaryQuadraticDiscriminant D) : ∃ (u : ℤ) (D_K : ℤ), u ≥ 1 ∧ ImaginaryQuadraticDiscriminant.IsFundamentalImaginaryQuadraticDiscriminant D_K ∧ D = u ^ 2 * D_K ∧ ∃ (𝒪_K : ImaginaryQuadraticOrder), 𝒪_K.discriminant = D_K ∧ ∃ (𝒪 : ImaginaryQuadraticOrder), 𝒪.discriminant = D ∧ 𝒪.discriminant = u ^ 2 * 𝒪_K.discriminant ∧ ∀ (𝒪' : ImaginaryQuadraticOrder), 𝒪'.discriminant = D → 𝒪.SameOrder 𝒪'

Existence and uniqueness: every imaginary quadratic discriminant D factors uniquely as u² · D_K, giving rise to a maximal order 𝒪_K and a unique (up to SameOrder) order 𝒪 of discriminant D.

def ImagQuadDiscriminant.ImaginaryQuadraticOrder.IsSuborderOfIndex (𝒪 𝒪_K : ImaginaryQuadraticOrder) (u : ℤ) : Prop

𝒪 is a suborder of 𝒪_K with index u if its discriminant is u² times that of 𝒪_K and the traces satisfy 𝒪.t = 2a + u · 𝒪_K.t for some integer a.

theorem ImagQuadDiscriminant.conductor_is_lattice_index {D : ℤ} (dec : ImaginaryQuadraticDiscriminant.ImaginaryQuadraticDiscriminantDecomposition D) : (orderFromDecomposition dec).IsSuborderOfIndex (maximalOrder dec.D_K ⋯) dec.u

The order constructed from a decomposition is a suborder of index u of the maximal order of D_K.

theorem ImagQuadDiscriminant.exists_unique_order_conductor_index (D : ℤ) (hD : ImaginaryQuadraticDiscriminant.IsImaginaryQuadraticDiscriminant D) : ∃ (u : ℤ) (D_K : ℤ) (𝒪_K : ImaginaryQuadraticOrder) (𝒪 : ImaginaryQuadraticOrder), u ≥ 1 ∧ ImaginaryQuadraticDiscriminant.IsFundamentalImaginaryQuadraticDiscriminant D_K ∧ 𝒪_K.discriminant = D_K ∧ 𝒪.discriminant = D ∧ 𝒪.IsSuborderOfIndex 𝒪_K u ∧ ∀ (𝒪' : ImaginaryQuadraticOrder), 𝒪'.discriminant = D → 𝒪.SameOrder 𝒪'

Refined existence-uniqueness statement: every imaginary quadratic discriminant D gives rise to a unique pair (𝒪_K, 𝒪) with 𝒪 ⊂ 𝒪_K of conductor index u.

def ProperIdealInvertible.idealOrder {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] (I : FractionalIdeal (nonZeroDivisors R) K) : Set K

The order (multiplier ring) of a fractional ideal I in K: the set of x : K such that x · I ⊆ I.

def ProperIdealInvertible.IsProper {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] (I : FractionalIdeal (nonZeroDivisors R) K) : Prop

A fractional ideal I is proper if its order equals the image of R in K, i.e. its multiplier ring is exactly R itself.

theorem ProperIdealInvertible.algebraMap_range_subset_idealOrder {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] (I : FractionalIdeal (nonZeroDivisors R) K) : Set.range ⇑(algebraMap R K) ⊆ idealOrder I

R always sits inside the order of any fractional ideal: R ⊆ idealOrder I.

theorem ProperIdealInvertible.isProper_iff_order_subset {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] (I : FractionalIdeal (nonZeroDivisors R) K) : IsProper I ↔ idealOrder I ⊆ Set.range ⇑(algebraMap R K)

Reformulation of IsProper: properness is equivalent to the reverse inclusion idealOrder I ⊆ R.

theorem ProperIdealInvertible.idealOrder_mul_unit {R : Type u_1} [CommRing R] [IsDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (u : (FractionalIdeal (nonZeroDivisors R) K)ˣ) (I : FractionalIdeal (nonZeroDivisors R) K) : idealOrder (↑u * I) = idealOrder I

Multiplying by an invertible fractional ideal does not change the order: idealOrder (u · I) = idealOrder I for a unit u.

theorem ProperIdealInvertible.isProper_mul_unit_iff {R : Type u_1} [CommRing R] [IsDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (u : (FractionalIdeal (nonZeroDivisors R) K)ˣ) (I : FractionalIdeal (nonZeroDivisors R) K) : IsProper (↑u * I) ↔ IsProper I

Properness is preserved under multiplication by a unit: IsProper (u · I) ↔ IsProper I.

theorem ProperIdealInvertible.isProper_of_isUnit {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (I : FractionalIdeal (nonZeroDivisors R) K) (hI : IsUnit I) : IsProper I

Every invertible (unit) fractional ideal is proper.

noncomputable def ProperIdealInvertible.zsqrtdLinearEquivFin2 (d : ℤ) : ℤ√d ≃ₗ[ℤ] Fin 2 → ℤ

The canonical ℤ-linear equivalence ℤ√d ≃ₗ[ℤ] (Fin 2 → ℤ) sending α to ![α.re, α.im]. Exhibits ℤ√d as a free ℤ-module of rank 2.

instance ProperIdealInvertible.instModuleFreeZsqrtd {d : ℤ} : Module.Free ℤ (ℤ√d)

ℤ√d is free as a ℤ-module, via the equivalence with Fin 2 → ℤ.

instance ProperIdealInvertible.instModuleFiniteZsqrtd {d : ℤ} : Module.Finite ℤ (ℤ√d)

ℤ√d is finitely generated as a ℤ-module (in fact rank 2).

def ProperIdealInvertible.conjIdeal {d : ℤ} (I : Ideal (ℤ√d)) : Ideal (ℤ√d)

The conjugate of an ideal I ⊆ ℤ√d: the image of I under the conjugation ring homomorphism star.

theorem ProperIdealInvertible.mem_conjIdeal {d : ℤ} {I : Ideal (ℤ√d)} {x : ℤ√d} (hx : x ∈ I) : star x ∈ conjIdeal I

If x ∈ I, then star x ∈ conjIdeal I.

theorem ProperIdealInvertible.conjIdeal_conjIdeal {d : ℤ} (I : Ideal (ℤ√d)) : conjIdeal (conjIdeal I) = I

Conjugation of ideals is an involution: conjIdeal (conjIdeal I) = I.

noncomputable def ProperIdealInvertible.idealNormZsqrtd {d : ℤ} (I : Ideal (ℤ√d)) : ℕ

The ideal norm in ℤ√d, given by the cardinality of the quotient (ℤ√d) / I.

theorem ProperIdealInvertible.conjProduct_eq_norm_principal {d : ℤ} (hd : d < 0) [IsDomain (ℤ√d)] (K : Type u_1) [Field K] [Algebra (ℤ√d) K] [IsFractionRing (ℤ√d) K] (I : Ideal (ℤ√d)) (hI : I ≠ ⊥) (hP : IsProper ↑I) : I * conjIdeal I = Ideal.span {↑(idealNormZsqrtd I)}

For a proper, nonzero ideal I ⊆ ℤ√d (with d < 0), the product I · conjIdeal I is the principal ideal generated by the norm N(I) ∈ ℤ√d.

theorem ProperIdealInvertible.isUnit_coeIdeal_of_mul_eq_span {d : ℤ} [IsDomain (ℤ√d)] (K' : Type u_1) [Field K'] [Algebra (ℤ√d) K'] [IsFractionRing (ℤ√d) K'] (J J' : Ideal (ℤ√d)) (n : ℤ√d) (hn : n ≠ 0) (h : J * J' = Ideal.span {n}) : IsUnit ↑J

If J · J' = (n) with n ≠ 0, then J is invertible as a fractional ideal in the field of fractions.

theorem ProperIdealInvertible.isProper_iff_isUnit_quadratic {d : ℤ} (hd : d < 0) [IsDomain (ℤ√d)] (K : Type u_1) [Field K] [Algebra (ℤ√d) K] [IsFractionRing (ℤ√d) K] (I : FractionalIdeal (nonZeroDivisors (ℤ√d)) K) (hI : I ≠ 0) : IsProper I ↔ IsUnit I

Characterisation of properness for nonzero fractional ideals of ℤ√d (imaginary quadratic case): I is proper iff I is invertible.

theorem ProperIdealInvertible.inverse_eq_conj_div_norm {d : ℤ} (hd : d < 0) [IsDomain (ℤ√d)] (K : Type u_1) [Field K] [Algebra (ℤ√d) K] [IsFractionRing (ℤ√d) K] (I : Ideal (ℤ√d)) (hI : IsUnit ↑I) : ↑hI.unit⁻¹ = FractionalIdeal.spanSingleton (nonZeroDivisors (ℤ√d)) ((algebraMap (ℤ√d) K) ↑(idealNormZsqrtd I))⁻¹ * ↑(conjIdeal I)

Explicit formula for the inverse of a proper/invertible ideal in ℤ√d: I⁻¹ = (1/N(I)) · conjIdeal I.

noncomputable def ProperIdealInvertible.fractionalIdealNormZsqrtd {d : ℤ} (hd : d < 0) [IsDomain (ℤ√d)] (K : Type u_1) [Field K] [Algebra (ℤ√d) K] [IsFractionRing (ℤ√d) K] (𝔞 : FractionalIdeal (nonZeroDivisors (ℤ√d)) K) : ℚ

Norm of a fractional ideal in ℤ√d: N(𝔞) = N(𝔞.num) / |N(𝔞.den)|, as a rational number.

theorem ProperIdealInvertible.fractionalIdealNormZsqrtd_mul {d : ℤ} (hd : d < 0) [IsDomain (ℤ√d)] (K : Type u_1) [Field K] [Algebra (ℤ√d) K] [IsFractionRing (ℤ√d) K] (𝔞 𝔟 : FractionalIdeal (nonZeroDivisors (ℤ√d)) K) (h𝔞 : IsProper 𝔞) (h𝔟 : IsProper 𝔟) : fractionalIdealNormZsqrtd hd K (𝔞 * 𝔟) = fractionalIdealNormZsqrtd hd K 𝔞 * fractionalIdealNormZsqrtd hd K 𝔟

Multiplicativity of the fractional ideal norm in ℤ√d on proper ideals: N(𝔞 · 𝔟) = N(𝔞) · N(𝔟).

@[reducible, inline]

abbrev IdealClassGroup.InvertibleFractionalIdeals (R : Type u_1) [CommRing R] (K : Type u_2) [Field K] [Algebra R K] : Type u_2

The group of invertible fractional ideals of R in its field of fractions K.

@[reducible, inline]

abbrev IdealClassGroup.PrincipalFractionalIdeals (R : Type u_1) [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : Subgroup (FractionalIdeal (nonZeroDivisors R) K)ˣ

The subgroup of principal invertible fractional ideals (image of K* under toPrincipalIdeal).

instance IdealClassGroup.instNormalUnitsFractionalIdealNonZeroDivisorsPrincipalFractionalIdeals (R : Type u_1) [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : (PrincipalFractionalIdeals R K).Normal

The subgroup of principal fractional ideals is normal in the group of invertible fractional ideals (the ambient group is abelian).

noncomputable def IdealClassGroup.classGroup_mulEquiv (R : Type u_1) [CommRing R] [IsDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : InvertibleFractionalIdeals R K ⧸ PrincipalFractionalIdeals R K ≃* ClassGroup R

Identification of the quotient InvertibleFractionalIdeals / PrincipalFractionalIdeals with the ideal class group Cl(R) (via Mathlib's ClassGroup.equiv).

@[implicit_reducible]

noncomputable instance IdealClassGroup.instCommGroupQuotient (R : Type u_1) [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : CommGroup (InvertibleFractionalIdeals R K ⧸ PrincipalFractionalIdeals R K)

The quotient of invertible fractional ideals by principal ones inherits an abelian group structure.

@[implicit_reducible]

noncomputable instance IdealClassGroup.instCommGroupClassGroup_atlas (R : Type u_1) [CommRing R] [IsDomain R] : CommGroup (ClassGroup R)

The class group Cl(R) is an abelian group.

theorem IdealClassGroup.proper_iff_invertible_quadratic {d : ℤ} (hd : d < 0) [IsDomain (ℤ√d)] (K : Type u_1) [Field K] [Algebra (ℤ√d) K] [IsFractionRing (ℤ√d) K] (I : FractionalIdeal (nonZeroDivisors (ℤ√d)) K) (hI : I ≠ 0) : ProperIdealInvertible.IsProper I ↔ IsUnit I

For ℤ√d with d < 0, properness of a nonzero fractional ideal is equivalent to invertibility.

theorem IdealClassGroup.isProper_of_isUnit_quadratic {R : Type u_1} [CommRing R] [IsDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (I : FractionalIdeal (nonZeroDivisors R) K) (hI : IsUnit I) : ProperIdealInvertible.IsProper I

Every invertible fractional ideal (in the imaginary quadratic case) is proper.

noncomputable def IdealClassGroup.classGroupQuotient_imaginaryQuadratic {d : ℤ} [IsDomain (ℤ√d)] (K : Type u_1) [Field K] [Algebra (ℤ√d) K] [IsFractionRing (ℤ√d) K] : (FractionalIdeal (nonZeroDivisors (ℤ√d)) K)ˣ ⧸ (toPrincipalIdeal (ℤ√d) K).range ≃* ClassGroup (ℤ√d)

Identification of the quotient InvertibleFractionalIdeals(ℤ√d) / PrincipalFractionalIdeals(ℤ√d) with the class group Cl(ℤ√d) (in the imaginary quadratic case).

noncomputable def IdealClassGroup.classGroupMulEquivQuotient_imagQuad (𝒪 : Subring ℂ) (h𝒪 : ComplexLattice.IsImagQuadOrder 𝒪) (K : Type u_1) [Field K] [Algebra (↥𝒪) K] [IsFractionRing (↥𝒪) K] : have x := ComplexLattice.IdealClassGroup.commGroup 𝒪; ComplexLattice.IdealClassGroup 𝒪 ≃* (FractionalIdeal (nonZeroDivisors ↥𝒪) K)ˣ ⧸ (toPrincipalIdeal (↥𝒪) K).range

For an imaginary quadratic order 𝒪 ⊂ ℂ, the geometric ideal class group of 𝒪 (defined via complex lattices) is isomorphic to the quotient (FractionalIdeal 𝒪 K)ˣ / Principal.

theorem IdealClassGroup.cl_is_commGroup_imagQuad (𝒪 : Subring ℂ) [IsDomain ↥𝒪] (h𝒪 : ComplexLattice.IsImagQuadOrder 𝒪) : Nonempty (CommGroup (ComplexLattice.IdealClassGroup 𝒪))

The geometric ideal class group of an imaginary quadratic order 𝒪 ⊂ ℂ carries the structure of a (commutative) group.

noncomputable def IdealClassGroup.classGroupQuotient_Zsqrtd (d : ℤ) [IsDomain (ℤ√d)] (K : Type u_1) [Field K] [Algebra (ℤ√d) K] [IsFractionRing (ℤ√d) K] : (FractionalIdeal (nonZeroDivisors (ℤ√d)) K)ˣ ⧸ (toPrincipalIdeal (ℤ√d) K).range ≃* ClassGroup (ℤ√d)

Specialised version for 𝒪 = ℤ√d: the quotient (FractionalIdeal (ℤ√d) K)ˣ / Principal is Cl(ℤ√d).

def IdealTorsion.idealTorsion {𝒪 : Type u_1} [CommRing 𝒪] {E : Type u_2} [AddCommGroup E] [Module 𝒪 E] (𝔞 : Ideal 𝒪) : Submodule 𝒪 E

The 𝔞-torsion submodule of an 𝒪-module E: the set of P ∈ E such that α · P = 0 for every α ∈ 𝔞.

@[simp]

theorem IdealTorsion.mem_idealTorsion_iff {𝒪 : Type u_1} [CommRing 𝒪] {E : Type u_2} [AddCommGroup E] [Module 𝒪 E] (𝔞 : Ideal 𝒪) (P : E) : P ∈ idealTorsion 𝔞 ↔ ∀ α ∈ 𝔞, α • P = 0

Defining property of idealTorsion: P ∈ idealTorsion 𝔞 iff α · P = 0 for all α ∈ 𝔞.

@[simp]

theorem IdealTorsion.idealTorsion_eq_torsionBySet {𝒪 : Type u_1} [CommRing 𝒪] {E : Type u_2} [AddCommGroup E] [Module 𝒪 E] (𝔞 : Ideal 𝒪) : idealTorsion 𝔞 = Submodule.torsionBySet 𝒪 E ↑𝔞

The bespoke idealTorsion agrees with Mathlib's Submodule.torsionBySet.

def IdealTorsion.idealTorsionAddSubgroup {𝒪 : Type u_1} [CommRing 𝒪] {E : Type u_2} [AddCommGroup E] [Module 𝒪 E] (𝔞 : Ideal 𝒪) : AddSubgroup E

The 𝔞-torsion submodule viewed as an additive subgroup of E.

class CMTorsorAction.IsCMModule (𝒪 : Type u_2) [CommRing 𝒪] (E : Type u_3) [AddCommGroup E] [Module 𝒪 E] : Type (max u_2 u_3)

A CM-module over 𝒪 is an 𝒪-module E together with the data of an ideal latticeIdeal ⊆ 𝒪 and an 𝒪-linear equivalence E ≃ₗ[𝒪] 𝒪 / latticeIdeal.

• latticeIdeal : Ideal 𝒪
• linearEquiv : E ≃ₗ[𝒪] 𝒪 ⧸ latticeIdeal E

structure CMTorsorAction.CMIsogenyData (𝒪 : Type u_2) [CommRing 𝒪] (𝔟 𝔞 : Ideal 𝒪) : Type u_2

Data describing a CM-isogeny 𝒪/𝔟 → 𝒪/targetIdeal corresponding to multiplication by an ideal 𝔞: includes the target ideal (the colon ideal (𝔟 : 𝔞)) and the relation 𝔞 · targetIdeal = 𝔟.

• targetIdeal : Ideal 𝒪
• le_target : 𝔟 ≤ self.targetIdeal
• ideal_mul_target_le : 𝔞 * self.targetIdeal ≤ 𝔟
• target_eq_colon : self.targetIdeal = Submodule.colon 𝔟 ↑𝔞
• ideal_mul_target_eq : 𝔞 * self.targetIdeal = 𝔟

noncomputable def CMTorsorAction.CMIsogenyData.toLinearMap {𝒪 : Type u_1} [CommRing 𝒪] {𝔟 𝔞 : Ideal 𝒪} (φ : CMIsogenyData 𝒪 𝔟 𝔞) : 𝒪 ⧸ 𝔟 →ₗ[𝒪] 𝒪 ⧸ φ.targetIdeal

The 𝒪-linear map 𝒪/𝔟 → 𝒪/targetIdeal underlying a CMIsogenyData.

theorem CMTorsorAction.CMIsogenyData.toLinearMap_surjective {𝒪 : Type u_1} [CommRing 𝒪] {𝔟 𝔞 : Ideal 𝒪} (φ : CMIsogenyData 𝒪 𝔟 𝔞) : Function.Surjective ⇑φ.toLinearMap

The linear map associated to a CMIsogenyData is surjective.

theorem CMTorsorAction.CMIsogenyData.ker_toLinearMap {𝒪 : Type u_1} [CommRing 𝒪] {𝔟 𝔞 : Ideal 𝒪} (φ : CMIsogenyData 𝒪 𝔟 𝔞) : φ.toLinearMap.ker = Submodule.map (Submodule.mkQ 𝔟) φ.targetIdeal

The kernel of φ.toLinearMap is the image of the target ideal inside 𝒪/𝔟.

noncomputable def CMTorsorAction.degIsogeny {𝒪 : Type u_1} [CommRing 𝒪] {𝔟 𝔞 : Ideal 𝒪} (φ : CMIsogenyData 𝒪 𝔟 𝔞) : ℕ

The degree of the CM-isogeny φ, defined as the cardinality of its kernel.

theorem CMTorsorAction.degIsogeny_eq_idealNorm {𝒪 : Type u_1} [CommRing 𝒪] {𝔟 𝔞 : Ideal 𝒪} [IsDedekindDomain 𝒪] [Module.Free ℤ 𝒪] [Module.Finite ℤ 𝒪] (φ : CMIsogenyData 𝒪 𝔟 𝔞) (h𝔠_ne : φ.targetIdeal ≠ ⊥) : degIsogeny φ = NormTrace.idealNorm 𝔞

The degree of the CM-isogeny equals the ideal norm of 𝔞, provided the target ideal is nonzero (so that the quotient is finite).

theorem CMIdealIsogeny.isogeny_degree_eq_idealNorm {𝒪 : Type u_1} [CommRing 𝒪] {𝔟 𝔞 : Ideal 𝒪} [IsDedekindDomain 𝒪] [Module.Free ℤ 𝒪] [Module.Finite ℤ 𝒪] (φ : CMTorsorAction.CMIsogenyData 𝒪 𝔟 𝔞) (h𝔠_ne : φ.targetIdeal ≠ ⊥) : CMTorsorAction.degIsogeny φ = NormTrace.idealNorm 𝔞

Restatement: the degree of a CM-isogeny coincides with the ideal norm of the acting ideal.

theorem CMIdealIsogeny.cm_curves_same_endRing_isogenous {𝒪 : Type u_2} [CommRing 𝒪] (𝔟₁ 𝔟₂ : Ideal 𝒪) : ∃ (𝔞 : Ideal 𝒪) (φ : CMTorsorAction.CMIsogenyData 𝒪 𝔟₁ 𝔞), φ.targetIdeal = 𝔟₂

Any two CM elliptic curves with the same endomorphism ring 𝒪 are linked by a CM ideal isogeny: for any two ideals 𝔟₁, 𝔟₂ there exists an ideal 𝔞 and a CMIsogenyData 𝒪 𝔟₁ 𝔞 whose target equals 𝔟₂.