The congruence lattice of a modulus

Let 𝔪 be a modulus of a number field K with finite part 𝔪₀, and let I be an invertible fractional ideal. Under the mixed embedding K → ℝ^r₁ × ℂ^r₂, the ideal I becomes the full lattice mixedEmbedding.idealLattice K I. The congruence lattice congruenceLattice 𝔪 I is the sublattice coming from I * 𝔪₀: the elements of I congruent to 0 modulo I * 𝔪₀.

Counting the elements of I in a region that satisfy a congruence x ≡ a mod I * 𝔪₀ is counting the points of one coset of this sublattice, which is itself a translate of a full lattice. The index computation below says that there are exactly N 𝔪₀ such cosets, and the covolume grows by the factor N 𝔪₀. These are the lattice inputs to counting integral ideals in a ray class.

Only the finite part 𝔪₀ enters the lattice: the infinite part of 𝔪 plays no role here, and the sign conditions at the real places of 𝔪.infinitePart are imposed by the region, not by the sublattice.

Main definitions

• TauCeti.GlobalNumberFields.congruenceLattice: the lattice of I * 𝔪₀ in the mixed space.

Main results

• TauCeti.GlobalNumberFields.mem_congruenceLattice_iff: its points are the images of the elements of I * 𝔪₀.
• TauCeti.GlobalNumberFields.coe_congruenceLattice_mk0_eq_image: for an integral ideal 𝔞, the same description over 𝔞 * 𝔪₀.
• TauCeti.GlobalNumberFields.congruenceLattice_le_idealLattice: it is a sublattice of the ideal lattice of I.
• TauCeti.GlobalNumberFields.relIndex_congruenceLattice: its index in the ideal lattice of I is the absolute norm of 𝔪₀.
• TauCeti.GlobalNumberFields.covolume_congruenceLattice: its covolume is N 𝔪₀ times the covolume of the ideal lattice of I.
• TauCeti.GlobalNumberFields.covolume_congruenceLattice_div_absNorm: its covolume divided by N I is N 𝔪₀ · √|d_K| / 2 ^ r₂.
• TauCeti.GlobalNumberFields.congruenceLattice_eq_of_finitePart_eq: it depends only on the finite part of the modulus.
• TauCeti.GlobalNumberFields.congruenceLattice_eq_idealLattice_of_finitePart_eq_top: for a modulus with trivial finite part it is the ideal lattice itself; congruenceLattice_one and congruenceLattice_narrowModulus are the cases of the trivial and the narrow modulus.

References

• S. Lang, Algebraic Number Theory, Chapter VI, §3.
• J. Neukirch, Algebraic Number Theory, Chapter VI, §1.

noncomputable def TauCeti.GlobalNumberFields.congruenceLattice {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) : Submodule ℤ (NumberField.mixedEmbedding.mixedSpace K)

The congruence lattice of a modulus 𝔪 inside the ideal lattice of I: the image in the mixed space of the fractional ideal I * 𝔪₀, whose elements are those of I congruent to 0 modulo I * 𝔪₀, where 𝔪₀ is the finite part of 𝔪.

Equations

• TauCeti.GlobalNumberFields.congruenceLattice 𝔪 I = NumberField.mixedEmbedding.idealLattice K (I * (FractionalIdeal.mk0 K) ⟨𝔪.finitePart, ⋯⟩)

theorem TauCeti.GlobalNumberFields.congruenceLattice_def {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) : congruenceLattice 𝔪 I = NumberField.mixedEmbedding.idealLattice K (I * (FractionalIdeal.mk0 K) ⟨𝔪.finitePart, ⋯⟩)

The congruence lattice is the ideal lattice of I * 𝔪₀.

instance TauCeti.GlobalNumberFields.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntCongruenceLattice {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) : DiscreteTopology ↥(congruenceLattice 𝔪 I)

The congruence lattice is a discrete subgroup of the mixed space.

instance TauCeti.GlobalNumberFields.instIsZLatticeRealMixedSpaceCongruenceLattice {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) : IsZLattice ℝ (congruenceLattice 𝔪 I)

The congruence lattice is a full ℤ-lattice in the mixed space.

@[simp]

theorem TauCeti.GlobalNumberFields.mem_congruenceLattice_iff {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ} {x : NumberField.mixedEmbedding.mixedSpace K} : x ∈ congruenceLattice 𝔪 I ↔ ∃ y ∈ ↑I * ↑𝔪.finitePart, (NumberField.mixedEmbedding K) y = x

The points of the congruence lattice are the images of the elements of I * 𝔪₀.

theorem TauCeti.GlobalNumberFields.congruenceLattice_le_idealLattice {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) : congruenceLattice 𝔪 I ≤ NumberField.mixedEmbedding.idealLattice K I

The congruence lattice is a sublattice of the ideal lattice of I.

@[simp]

theorem TauCeti.GlobalNumberFields.relIndex_congruenceLattice {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) : (congruenceLattice 𝔪 I).toAddSubgroup.relIndex (NumberField.mixedEmbedding.idealLattice K I).toAddSubgroup = Ideal.absNorm 𝔪.finitePart

The index of the congruence lattice. The congruence lattice of 𝔪 has index N 𝔪₀ in the ideal lattice of I, so it has exactly N 𝔪₀ cosets there, one for each residue class modulo I * 𝔪₀.

@[simp]

theorem TauCeti.GlobalNumberFields.covolume_congruenceLattice {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) : ZLattice.covolume (congruenceLattice 𝔪 I) MeasureTheory.volume = ↑(Ideal.absNorm 𝔪.finitePart) * ZLattice.covolume (NumberField.mixedEmbedding.idealLattice K I) MeasureTheory.volume

The covolume of the congruence lattice is N 𝔪₀ times the covolume of the ideal lattice of I.

theorem TauCeti.GlobalNumberFields.covolume_congruenceLattice_div_absNorm {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) : ZLattice.covolume (congruenceLattice 𝔪 I) MeasureTheory.volume / ↑(FractionalIdeal.absNorm ↑I) = ↑(Ideal.absNorm 𝔪.finitePart) * √|↑(NumberField.discr K)| / 2 ^ NumberField.InfinitePlace.nrComplexPlaces K

The covolume of the congruence lattice, per unit norm. For an invertible fractional ideal I, the covolume of the congruence lattice of 𝔪 at I, divided by N I, is N 𝔪₀ · √|d_K| / 2 ^ r₂, where d_K is the discriminant and r₂ the number of complex places of K; in particular it does not depend on I.

theorem TauCeti.GlobalNumberFields.congruenceLattice_eq_of_finitePart_eq {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪.finitePart = 𝔫.finitePart) (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) : congruenceLattice 𝔪 I = congruenceLattice 𝔫 I

The congruence lattice depends only on the finite part of the modulus.

theorem TauCeti.GlobalNumberFields.congruenceLattice_eq_idealLattice_of_finitePart_eq_top {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} (h : 𝔪.finitePart = ⊤) (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) : congruenceLattice 𝔪 I = NumberField.mixedEmbedding.idealLattice K I

For a modulus with trivial finite part the congruence lattice is the whole ideal lattice.

@[simp]

theorem TauCeti.GlobalNumberFields.congruenceLattice_one {K : Type u_1} [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) : congruenceLattice (Modulus.one K) I = NumberField.mixedEmbedding.idealLattice K I

For the trivial modulus the congruence lattice is the whole ideal lattice.

@[simp]

theorem TauCeti.GlobalNumberFields.congruenceLattice_narrowModulus {K : Type u_1} [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) : congruenceLattice (narrowModulus K) I = NumberField.mixedEmbedding.idealLattice K I

For the narrow modulus the congruence lattice is the whole ideal lattice.

@[simp]

theorem TauCeti.GlobalNumberFields.coe_congruenceLattice_mk0_eq_image {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (𝔞 : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) : ↑(congruenceLattice 𝔪 ((FractionalIdeal.mk0 K) 𝔞)) = (fun (y : NumberField.RingOfIntegers K) => (NumberField.mixedEmbedding K) ↑y) '' ↑(↑𝔞 * 𝔪.finitePart)

The congruence lattice of an integral ideal, upstairs. For a nonzero integral ideal 𝔞, the congruence lattice of 𝔪 at mk0 𝔞 is the image under mixedEmbedding of the ideal 𝔞 * 𝔪₀ of 𝓞 K.