Documentation

Mathlib.RingTheory.FractionalIdeal.Norm

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 #

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|

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

Equations
Instances For
    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) :
    FractionalIdeal.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₀) :
    FractionalIdeal.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 FractionalIdeal.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] :
    FractionalIdeal.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] :
    FractionalIdeal.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] [NoZeroDivisors K] {I : FractionalIdeal (nonZeroDivisors R) K} :
    FractionalIdeal.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) :
    FractionalIdeal.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] [NoZeroDivisors K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b : Basis ι R) (I : FractionalIdeal (nonZeroDivisors R) K) (bI : Basis ι I) :
    |(Basis.localizationLocalization (nonZeroDivisors ) K b).det (Subtype.val bI)| = FractionalIdeal.absNorm I