Fractional ideal norms

This file defines the absolute ideal norm of a fractional ideal I : FractionalIdeal R⁰ K where K is a fraction field of R. The norm is defined by FractionalIdeal.absNorm I = Ideal.absNorm I.num / |Algebra.norm ℤ I.den| where I.num is an ideal of R and I.den an element of R⁰ such that I.den • I = I.num.

Main definitions and results

• FractionalIdeal.absNorm: the norm as a zero-preserving morphism with values in ℚ.
• FractionalIdeal.absNorm_eq': the value of the norm does not depend on the choice of I.num and I.den.
• FractionalIdeal.abs_det_basis_change: the norm is given by the determinant of the basis change matrix.
• FractionalIdeal.absNorm_span_singleton: the norm of a principal fractional ideal is the norm of its generator

theorem FractionalIdeal.absNorm_div_norm_eq_absNorm_div_norm {R : Type u_1} [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] {K : Type u_2} [CommRing K] [Algebra R K] [IsFractionRing R K] {I : FractionalIdeal (nonZeroDivisors R) K} (a : ↥(nonZeroDivisors R)) (I₀ : Ideal R) (h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀) : ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den| = ↑(Ideal.absNorm I₀) / ↑|(Algebra.norm ℤ) ↑a|

noncomputable def FractionalIdeal.absNorm {R : Type u_1} [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] {K : Type u_2} [CommRing K] [Algebra R K] [IsFractionRing R K] : FractionalIdeal (nonZeroDivisors R) K →*₀ ℚ

The absolute norm of the fractional ideal I extending by multiplicativity the absolute norm on (integral) ideals.

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

theorem FractionalIdeal.absNorm_eq' {R : Type u_1} [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] {K : Type u_2} [CommRing K] [Algebra R K] [IsFractionRing R K] {I : FractionalIdeal (nonZeroDivisors R) K} (a : ↥(nonZeroDivisors R)) (I₀ : Ideal R) (h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀) : absNorm I = ↑(Ideal.absNorm I₀) / ↑|(Algebra.norm ℤ) ↑a|

theorem FractionalIdeal.absNorm_nonneg {R : Type u_1} [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] {K : Type u_2} [CommRing K] [Algebra R K] [IsFractionRing R K] (I : FractionalIdeal (nonZeroDivisors R) K) : 0 ≤ absNorm I

theorem FractionalIdeal.absNorm_bot {R : Type u_1} [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] {K : Type u_2} [CommRing K] [Algebra R K] [IsFractionRing R K] : absNorm ⊥ = 0

theorem FractionalIdeal.absNorm_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] {K : Type u_2} [CommRing K] [Algebra R K] [IsFractionRing R K] : absNorm 1 = 1

theorem FractionalIdeal.absNorm_eq_zero_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] {K : Type u_2} [CommRing K] [Algebra R K] [IsFractionRing R K] [IsDomain K] {I : FractionalIdeal (nonZeroDivisors R) K} : absNorm I = 0 ↔ I = 0

theorem FractionalIdeal.coeIdeal_absNorm {R : Type u_1} [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] {K : Type u_2} [CommRing K] [Algebra R K] [IsFractionRing R K] (I₀ : Ideal R) : absNorm ↑I₀ = ↑(Ideal.absNorm I₀)

theorem FractionalIdeal.abs_det_basis_change {R : Type u_1} [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] {K : Type u_2} [CommRing K] [Algebra R K] [IsFractionRing R K] [IsLocalization (Algebra.algebraMapSubmonoid R (nonZeroDivisors ℤ)) K] [Algebra ℚ K] [IsDomain K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℤ R) (I : FractionalIdeal (nonZeroDivisors R) K) (bI : Module.Basis ι ℤ ↥↑I) : |(Module.Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) K b).det (Subtype.val ∘ ⇑bI)| = absNorm I

@[simp]

theorem FractionalIdeal.absNorm_span_singleton (R : Type u_1) [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] {K : Type u_2} [CommRing K] [Algebra R K] [IsFractionRing R K] [IsLocalization (Algebra.algebraMapSubmonoid R (nonZeroDivisors ℤ)) K] [Algebra ℚ K] [Module.Finite ℚ K] (x : K) : absNorm (spanSingleton (nonZeroDivisors R) x) = |(Algebra.norm ℚ) x|