Theorems · Theorem · number theory

NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm

∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ)
  (e : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K) ≃ Module.Free.ChooseBasisIndex ℤ ↥↑↑I),
  |(NumberField.mixedEmbedding.latticeBasis K).det
        (⇑(NumberField.mixedEmbedding K) ∘ ⇑(NumberField.basisOfFractionalIdeal K I) ∘ ⇑e)| =
    ↑(FractionalIdeal.absNorm ↑I)

The generalized index of the lattice generated by I in the lattice generated by 𝓞 K is equal to the norm of the ideal I. The result is stated in terms of base change determinant and is the translation of NumberField.det_basisOfFractionalIdeal_eq_absNorm in the mixed space. This is useful, in particular, to prove that the family obtained from the ℤ-basis of I is actually an ℝ-basis of the mixed space, see fractionalIdealLatticeBasis.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Cited by

1 results in Mathlib

Foundations

Depth 306 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNumberField