The index of one ideal lattice in another

An invertible fractional ideal I of a number field K is a full ℤ-lattice in K, and its image mixedEmbedding.idealLattice K I is a full lattice in the mixed space. If J ≤ I are two such ideals, the index of J in I is the ratio of their absolute norms. This is the lattice-theoretic meaning of the norm of a fractional ideal: for an integral ideal 𝔞, the lattice of I * 𝔞 has index N 𝔞 in the lattice of I, which is how congruence conditions modulo 𝔞 are counted among the lattice points of I.

The index is computed in K by NumberField.relIndex_fractionalIdeal_eq_absNorm_div_absNorm, and transported to the mixed space along the injective embedding.

Main results

• NumberField.mixedEmbedding.relIndex_idealLattice: the index of the lattice of J in the lattice of I is absNorm J / absNorm I.
• NumberField.mixedEmbedding.relIndex_idealLattice_mul_mk0: the lattice of I * 𝔞 has index N 𝔞 in the lattice of I.
• NumberField.mixedEmbedding.covolume_idealLattice_mul_mk0: the covolume of the lattice of I * 𝔞 is N 𝔞 times the covolume of the lattice of I.

theorem NumberField.mixedEmbedding.idealLattice_toAddSubgroup {K : Type u_1} [Field K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : (idealLattice K I).toAddSubgroup = AddSubgroup.map (mixedEmbedding K).toAddMonoidHom (↑↑I).toAddSubgroup

The ideal lattice of I is the image of I under the mixed embedding, as an additive subgroup.

theorem NumberField.mixedEmbedding.relIndex_idealLattice {K : Type u_1} [Field K] [NumberField K] {I J : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ} (hJI : ↑J ≤ ↑I) : ↑((idealLattice K J).toAddSubgroup.relIndex (idealLattice K I).toAddSubgroup) = FractionalIdeal.absNorm ↑J / FractionalIdeal.absNorm ↑I

The index of one ideal lattice in another is the ratio of the norms. For invertible fractional ideals J ≤ I of a number field, the lattice of J has index absNorm J / absNorm I in the lattice of I.

theorem NumberField.mixedEmbedding.relIndex_idealLattice_mul_mk0 {K : Type u_1} [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (𝔞 : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) : (idealLattice K (I * (FractionalIdeal.mk0 K) 𝔞)).toAddSubgroup.relIndex (idealLattice K I).toAddSubgroup = Ideal.absNorm ↑𝔞

The index of the lattice of I * 𝔞. For an integral ideal 𝔞, the lattice of I * 𝔞 has index N 𝔞 in the lattice of I.

theorem NumberField.mixedEmbedding.covolume_idealLattice_mul_mk0 {K : Type u_1} [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (𝔞 : ↥(nonZeroDivisors (Ideal (RingOfIntegers K)))) : ZLattice.covolume (idealLattice K (I * (FractionalIdeal.mk0 K) 𝔞)) MeasureTheory.volume = ↑(Ideal.absNorm ↑𝔞) * ZLattice.covolume (idealLattice K I) MeasureTheory.volume

The covolume of the lattice of I * 𝔞 is N 𝔞 times the covolume of the lattice of I.