Ideal norms #

This file defines the relative ideal norm Ideal.spanNorm R (I : Ideal S) : Ideal S as the ideal spanned by the norms of elements in I.

Main definitions #

Ideal.spanNorm R (I : Ideal S): the ideal spanned by the norms of elements in I. This is used to define Ideal.relNorm.
Ideal.relNorm R (I : Ideal S): the relative ideal norm as a bundled monoid-with-zero morphism, defined as the ideal spanned by the norms of elements in I.

Main results #

map_mul Ideal.relNorm: multiplicativity of the relative ideal norm
relNorm_relNorm: transitivity of the relative ideal norm

source

noncomputable def Ideal.spanNorm (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_3} [CommRing S] [IsDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (I : Ideal S) :

Ideal R

Ideal.spanNorm R (I : Ideal S) is the ideal generated by mapping Algebra.intNorm R S over I.

See also Ideal.relNorm.

Equations

Ideal.spanNorm R I = Ideal.map (Algebra.intNorm R S) I

Instances For

source

@[simp]

theorem Ideal.spanNorm_bot (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_3} [CommRing S] [IsDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] :

spanNorm R ⊥ = ⊥

source

@[simp]

theorem Ideal.spanNorm_eq_bot_iff {R : Type u_1} [CommRing R] [IsDomain R] {S : Type u_3} [CommRing S] [IsDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] {I : Ideal S} :

spanNorm R I = ⊥ ↔ I = ⊥

source

theorem Ideal.intNorm_mem_spanNorm (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_3} [CommRing S] [IsDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] {I : Ideal S} {x : S} (hx : x ∈ I) :

(Algebra.intNorm R S) x ∈ spanNorm R I

source

theorem Ideal.norm_mem_spanNorm (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_3} [CommRing S] [IsDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] [Module.Free R S] {I : Ideal S} (x : S) (hx : x ∈ I) :

(Algebra.norm R) x ∈ spanNorm R I

source

@[simp]

theorem Ideal.spanNorm_singleton (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_3} [CommRing S] [IsDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] {r : S} :

spanNorm R (span {r}) = span {(Algebra.intNorm R S) r}

source

@[simp]

theorem Ideal.spanNorm_top (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_3} [CommRing S] [IsDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] :

spanNorm R ⊤ = ⊤

source

theorem Ideal.map_spanIntNorm (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_3} [CommRing S] [IsDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (I : Ideal S) {T : Type u_4} [Semiring T] (f : R →+* T) :

map f (spanNorm R I) = span (⇑f ∘ ⇑(Algebra.intNorm R S) '' ↑I)

source

theorem Ideal.spanNorm_mono (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_3} [CommRing S] [IsDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] {I J : Ideal S} (h : I ≤ J) :

spanNorm R I ≤ spanNorm R J

source

theorem Ideal.spanIntNorm_localization (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_3} [CommRing S] [IsDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (I : Ideal S) (M : Submonoid R) (hM : M ≤ nonZeroDivisors R) {Rₘ : Type u_4} (Sₘ : Type u_5) [CommRing Rₘ] [Algebra R Rₘ] [CommRing Sₘ] [Algebra S Sₘ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [IsLocalization M Rₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] [IsIntegrallyClosed Rₘ] [IsDomain Rₘ] [IsDomain Sₘ] [NoZeroSMulDivisors Rₘ Sₘ] [Module.Finite Rₘ Sₘ] [IsIntegrallyClosed Sₘ] [Algebra.IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)] :

spanNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanNorm R I)

source

theorem Ideal.spanNorm_mul_spanNorm_le (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_3} [CommRing S] [IsDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (I J : Ideal S) :

spanNorm R I * spanNorm R J ≤ spanNorm R (I * J)

source

theorem Ideal.spanNorm_mul_of_bot_or_top (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_3} [CommRing S] [IsDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤) (I J : Ideal S) :

spanNorm R (I * J) = spanNorm R I * spanNorm R J

This condition eq_bot_or_top is equivalent to being a field. However, Ideal.spanNorm_mul_of_field is harder to apply since we'd need to upgrade a CommRing R instance to a Field R instance.

source

theorem Ideal.spanNorm_le_comap (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_3} [CommRing S] [IsDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (I : Ideal S) :

spanNorm R I ≤ comap (algebraMap R S) I

source

theorem Ideal.spanNorm_mul (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_3} [CommRing S] [IsDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] [IsDedekindDomain R] [IsDedekindDomain S] (I J : Ideal S) :

spanNorm R (I * J) = spanNorm R I * spanNorm R J

Multiplicativity of Ideal.spanNorm. simp-normal form is map_mul (Ideal.relNorm R).

source

theorem Ideal.le_spanNorm_spanNorm (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_3} [CommRing S] [IsDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (T : Type u_4) [CommRing T] [IsDomain T] [IsIntegrallyClosed T] [Algebra R T] [Algebra T S] [Module.Finite R T] [Module.Finite T S] [NoZeroSMulDivisors R T] [NoZeroSMulDivisors T S] [IsScalarTower R T S] [Algebra.IsSeparable (FractionRing R) (FractionRing T)] [Algebra.IsSeparable (FractionRing T) (FractionRing S)] (I : Ideal S) :

spanNorm R I ≤ spanNorm R (spanNorm T I)

source

theorem Ideal.spanNorm_spanNorm_of_bot_or_top (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_3} [CommRing S] [IsDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (T : Type u_4) [CommRing T] [IsDomain T] [IsIntegrallyClosed T] [Algebra R T] [Algebra T S] [Module.Finite R T] [Module.Finite T S] [NoZeroSMulDivisors R T] [NoZeroSMulDivisors T S] [IsScalarTower R T S] [Algebra.IsSeparable (FractionRing R) (FractionRing T)] [Algebra.IsSeparable (FractionRing T) (FractionRing S)] (eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤) (I : Ideal S) :

spanNorm R (spanNorm T I) = spanNorm R I

This condition eq_bot_or_top is equivalent to being a field. However, Ideal.spanNorm_spanNorm_of_field would be harder to apply since we'd need to upgrade a CommRing R instance to a Field R instance.

source

theorem Ideal.spanNorm_spanNorm (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_3} [CommRing S] [IsDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (T : Type u_4) [CommRing T] [IsDomain T] [IsIntegrallyClosed T] [Algebra R T] [Algebra T S] [Module.Finite R T] [Module.Finite T S] [NoZeroSMulDivisors R T] [NoZeroSMulDivisors T S] [IsScalarTower R T S] [Algebra.IsSeparable (FractionRing R) (FractionRing T)] [Algebra.IsSeparable (FractionRing T) (FractionRing S)] [IsDedekindDomain R] [IsDedekindDomain T] [IsDedekindDomain S] (I : Ideal S) :

spanNorm R (spanNorm T I) = spanNorm R I

source

noncomputable def Ideal.relNorm (R : Type u_1) [CommRing R] [IsDomain R] {S : Type u_3} [CommRing S] [IsDomain S] [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] [IsDedekindDomain R] [IsDedekindDomain S] :

Ideal S →*₀ Ideal R

The relative norm Ideal.relNorm R (I : Ideal S), where R and S are Dedekind domains, and S is an extension of R that is finite and free as a module.

Equations