Documentation

Mathlib.RingTheory.Ideal.Norm.RelNorm

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 #

Main results #

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
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] :
    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} :
    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 ∈ 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} :
    spanNorm R (span {r}) = 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] :
    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) :
    map f (spanNorm R I) = 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) :
    spanNorm R I ≤ 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ₘ] :
    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] {S : Type u_2} [CommRing S] [Algebra R 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] {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) :
    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
    @[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) :
    spanNorm K (I * J) = spanNorm K I * 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) :
    spanNorm R (I * J) = spanNorm R I * 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
    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) :
      (relNorm R) I = 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) :
      spanNorm R I = (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] :
      (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] :
      (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} :
      (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 ∈ (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) :
      (relNorm R) (span {r}) = 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) :
      map f ((relNorm R) I) = 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) :
      (relNorm R) I ≤ (relNorm R) J