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

source

def Ideal.spanNorm (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] (I : Ideal S) :

Ideal R

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

See also Ideal.relNorm.

Equations

Ideal.spanNorm R I = Ideal.span (⇑(Algebra.norm R) '' ↑I)

Instances For

source

@[simp]

theorem Ideal.spanNorm_bot (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Nontrivial S] [Module.Free R S] [Module.Finite R S] :

Ideal.spanNorm R ⊥ = ⊥

source

@[simp]

theorem Ideal.spanNorm_eq_bot_iff {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [Module.Free R S] [Module.Finite R S] {I : Ideal S} :

Ideal.spanNorm R I = ⊥ ↔ I = ⊥

source

theorem Ideal.norm_mem_spanNorm (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] {I : Ideal S} (x : S) (hx : x ∈ I) :

(Algebra.norm R) x ∈ Ideal.spanNorm R I

source

@[simp]

theorem Ideal.spanNorm_singleton (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] {r : S} :

Ideal.spanNorm R (Ideal.span {r}) = Ideal.span {(Algebra.norm R) r}

source

@[simp]

theorem Ideal.spanNorm_top (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] :

Ideal.spanNorm R ⊤ = ⊤

source

theorem Ideal.map_spanNorm (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] (I : Ideal S) {T : Type u_3} [CommRing T] (f : R →+* T) :

Ideal.map f (Ideal.spanNorm R I) = Ideal.span (⇑f ∘ ⇑(Algebra.norm R) '' ↑I)

source

theorem Ideal.spanNorm_mono (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] {I J : Ideal S} (h : I ≤ J) :

Ideal.spanNorm R I ≤ Ideal.spanNorm R J

source

theorem Ideal.spanNorm_localization (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] (I : Ideal S) [Module.Finite R S] [Module.Free R S] (M : Submonoid R) {Rₘ : Type u_3} (Sₘ : Type u_4) [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ₘ] :

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

source

theorem Ideal.spanNorm_mul_spanNorm_le (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] (I J : Ideal S) :

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

source

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

Ideal.spanNorm R (I * J) = Ideal.spanNorm R I * Ideal.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

@[simp]

theorem Ideal.spanNorm_mul_of_field {S : Type u_2} [CommRing S] {K : Type u_3} [Field K] [Algebra K S] [IsDomain S] [Module.Finite K S] (I J : Ideal S) :

Ideal.spanNorm K (I * J) = Ideal.spanNorm K I * Ideal.spanNorm K J

source

theorem Ideal.spanNorm_mul (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] (I J : Ideal S) :

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

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

source

def Ideal.relNorm (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R 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' := ⋯ }

Instances For

source

theorem Ideal.relNorm_apply (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] (I : Ideal S) :

(Ideal.relNorm R) I = Ideal.span (⇑(Algebra.norm R) '' ↑I)

source

@[simp]

theorem Ideal.spanNorm_eq (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] (I : Ideal S) :

Ideal.spanNorm R I = (Ideal.relNorm R) I

source

@[simp]

theorem Ideal.relNorm_bot (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] :

(Ideal.relNorm R) ⊥ = ⊥

source

@[simp]

theorem Ideal.relNorm_top (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] :

(Ideal.relNorm R) ⊤ = ⊤

source

@[simp]

theorem Ideal.relNorm_eq_bot_iff {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] {I : Ideal S} :

(Ideal.relNorm R) I = ⊥ ↔ I = ⊥

source

theorem Ideal.norm_mem_relNorm (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] (I : Ideal S) {x : S} (hx : x ∈ I) :

(Algebra.norm R) x ∈ (Ideal.relNorm R) I

source

@[simp]

theorem Ideal.relNorm_singleton (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] (r : S) :

(Ideal.relNorm R) (Ideal.span {r}) = Ideal.span {(Algebra.norm R) r}

source

theorem Ideal.map_relNorm (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] (I : Ideal S) {T : Type u_3} [CommRing T] (f : R →+* T) :

Ideal.map f ((Ideal.relNorm R) I) = Ideal.span (⇑f ∘ ⇑(Algebra.norm R) '' ↑I)

source

theorem Ideal.relNorm_mono (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [Module.Free R S] {I J : Ideal S} (h : I ≤ J) :

(Ideal.relNorm R) I ≤ (Ideal.relNorm R) J

Documentation

Mathlib.RingTheory.Ideal.Norm.RelNorm

Ideal norms #

Main definitions #

Main results #