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 ofI.numandI.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₀)
:
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]
:
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)
:
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₀)
:
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)
:
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]
:
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]
:
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}
:
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)
:
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)
: