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

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

@[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 ⊥ = ⊥

@[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 = ⊥

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

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

@[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}

@[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 ⊤ = ⊤

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)

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

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)

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)

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.

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

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).

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)

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.

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

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

• Ideal.relNorm R = { toFun := Ideal.spanNorm R, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

theorem Ideal.relNorm_apply (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 : Ideal S) : (relNorm R) I = span (⇑(Algebra.intNorm R S) '' ↑I)

@[simp]

theorem Ideal.spanNorm_eq (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 : Ideal S) : spanNorm R I = (relNorm R) I

@[simp]

theorem Ideal.relNorm_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)] [IsDedekindDomain R] [IsDedekindDomain S] : (relNorm R) ⊥ = ⊥

@[simp]

theorem Ideal.relNorm_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)] [IsDedekindDomain R] [IsDedekindDomain S] : (relNorm R) ⊤ = ⊤

@[simp]

theorem Ideal.relNorm_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)] [IsDedekindDomain R] [IsDedekindDomain S] {I : Ideal S} : (relNorm R) I = ⊥ ↔ I = ⊥

theorem Ideal.norm_mem_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] [Module.Free R S] (I : Ideal S) {x : S} (hx : x ∈ I) : (Algebra.norm R) x ∈ (relNorm R) I

@[simp]

theorem Ideal.relNorm_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)] [IsDedekindDomain R] [IsDedekindDomain S] (r : S) : (relNorm R) (span {r}) = span {(Algebra.intNorm R S) r}

theorem Ideal.map_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] (I : Ideal S) {T : Type u_4} [Semiring T] (f : R →+* T) : map f ((relNorm R) I) = span (⇑f ∘ ⇑(Algebra.intNorm R S) '' ↑I)

theorem Ideal.relNorm_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)] [IsDedekindDomain R] [IsDedekindDomain S] {I J : Ideal S} (h : I ≤ J) : (relNorm R) I ≤ (relNorm R) J

@[simp]

theorem Ideal.relNorm_map_algEquiv {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] {T : Type u_4} [CommRing T] [IsDedekindDomain T] [IsIntegrallyClosed T] [Algebra R T] [Module.Finite R T] [NoZeroSMulDivisors R T] [Algebra.IsSeparable (FractionRing R) (FractionRing T)] (σ : S ≃ₐ[R] T) (I : Ideal S) : (relNorm R) (map σ I) = (relNorm R) I

@[simp]

theorem Ideal.relNorm_comap_algEquiv {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] {T : Type u_4} [CommRing T] [IsDedekindDomain T] [IsIntegrallyClosed T] [Algebra R T] [Module.Finite R T] [NoZeroSMulDivisors R T] [Algebra.IsSeparable (FractionRing R) (FractionRing T)] (σ : S ≃ₐ[R] T) (I : Ideal T) : (relNorm R) (comap σ I) = (relNorm R) I

@[simp]

theorem Ideal.relNorm_smul (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] {G : Type u_4} [Group G] [MulSemiringAction G S] [SMulCommClass G R S] (g : G) (I : Ideal S) : (relNorm R) (g • I) = (relNorm R) I

theorem Ideal.relNorm_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)] [IsDedekindDomain R] [IsDedekindDomain S] (I : Ideal S) : (relNorm R) I ≤ comap (algebraMap R S) I

theorem Ideal.relNorm_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] (T : Type u_4) [CommRing T] [IsDedekindDomain T] [IsIntegrallyClosed T] [Algebra R T] [Algebra T S] [IsScalarTower R T S] [Module.Finite R T] [Module.Finite T S] [NoZeroSMulDivisors R T] [NoZeroSMulDivisors T S] [Algebra.IsSeparable (FractionRing R) (FractionRing T)] [Algebra.IsSeparable (FractionRing T) (FractionRing S)] (I : Ideal S) : (relNorm R) ((relNorm T) I) = (relNorm R) I

theorem Ideal.relNorm_algebraMap {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 : Ideal R) : (relNorm R) (map (algebraMap R S) I) = I ^ Module.finrank (FractionRing R) (FractionRing S)

theorem Ideal.relNorm_algebraMap' (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] {R' : Type u_4} [CommRing R'] (I : Ideal R') [Algebra R' R] [Algebra R' S] [IsScalarTower R' R S] : (relNorm R) (map (algebraMap R' S) I) = map (algebraMap R' R) I ^ Module.finrank (FractionRing R) (FractionRing S)

A version of relNorm_algebraMap involving a tower of algebras S/R/R'.