The index of one fractional ideal in another

An invertible fractional ideal of a number field K is a full ℤ-lattice in K. If J ≤ I are two such ideals, the index of J in I is the ratio of their absolute norms. The index is computed from the determinant formula NumberField.det_basisOfFractionalIdeal_eq_absNorm and AddSubgroup.relIndex_eq_abs_det.

Main results

• NumberField.relIndex_fractionalIdeal_eq_absNorm_div_absNorm: the index of J in I, as additive subgroups of K, is absNorm J / absNorm I.

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

The index of a fractional ideal in a larger one is the ratio of the norms. For invertible fractional ideals J ≤ I of a number field, the index of J in I, as additive subgroups of the field, is absNorm J / absNorm I.