Documentation

Mathlib.RingTheory.Ideal.Norm

Ideal norms #

This file defines the absolute ideal norm Ideal.absNorm (I : Ideal R) : ℕ as the cardinality of the quotient R ⧸ I (setting it to 0 if the cardinality is infinite), and 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 #

noncomputable def Submodule.cardQuot {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) :

The cardinality of (M ⧸ S), if (M ⧸ S) is finite, and 0 otherwise. This is used to define the absolute ideal norm Ideal.absNorm.

Equations
Instances For
    @[simp]
    theorem Submodule.cardQuot_apply {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) [h : Fintype (M S)] :
    @[simp]
    theorem Submodule.cardQuot_bot (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] [Infinite M] :
    @[simp]
    theorem Submodule.cardQuot_eq_one_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {P : Submodule R M} :

    Multiplicity of the ideal norm, for coprime ideals. This is essentially just a repackaging of the Chinese Remainder Theorem.

    theorem Ideal.mul_add_mem_pow_succ_inj {S : Type u_1} [CommRing S] (P : Ideal S) {i : } (a : S) (d : S) (d' : S) (e : S) (e' : S) (a_mem : a P ^ i) (e_mem : e P ^ (i + 1)) (e'_mem : e' P ^ (i + 1)) (h : d - d' P) :
    a * d + e - (a * d' + e') P ^ (i + 1)

    If the d from Ideal.exists_mul_add_mem_pow_succ is unique, up to P, then so are the cs, up to P ^ (i + 1). Inspired by [Neukirch], proposition 6.1

    theorem Ideal.exists_mul_add_mem_pow_succ {S : Type u_1} [CommRing S] {P : Ideal S} [P_prime : Ideal.IsPrime P] (hP : P ) [IsDedekindDomain S] {i : } (a : S) (c : S) (a_mem : a P ^ i) (a_not_mem : aP ^ (i + 1)) (c_mem : c P ^ i) :
    ∃ (d : S), ∃ e ∈ P ^ (i + 1), a * d + e = c

    If a ∈ P^i \ P^(i+1) and c ∈ P^i, then a * d + e = c for e ∈ P^(i+1). Ideal.mul_add_mem_pow_succ_unique shows the choice of d is unique, up to P. Inspired by [Neukirch], proposition 6.1

    theorem Ideal.mem_prime_of_mul_mem_pow {S : Type u_1} [CommRing S] [IsDedekindDomain S] {P : Ideal S} [P_prime : Ideal.IsPrime P] (hP : P ) {i : } {a : S} {b : S} (a_not_mem : aP ^ (i + 1)) (ab_mem : a * b P ^ (i + 1)) :
    b P
    theorem Ideal.mul_add_mem_pow_succ_unique {S : Type u_1} [CommRing S] {P : Ideal S} [P_prime : Ideal.IsPrime P] (hP : P ) [IsDedekindDomain S] {i : } (a : S) (d : S) (d' : S) (e : S) (e' : S) (a_not_mem : aP ^ (i + 1)) (e_mem : e P ^ (i + 1)) (e'_mem : e' P ^ (i + 1)) (h : a * d + e - (a * d' + e') P ^ (i + 1)) :
    d - d' P

    The choice of d in Ideal.exists_mul_add_mem_pow_succ is unique, up to P. Inspired by [Neukirch], proposition 6.1

    theorem cardQuot_pow_of_prime {S : Type u_1} [CommRing S] [IsDomain S] {P : Ideal S} [P_prime : Ideal.IsPrime P] (hP : P ) [IsDedekindDomain S] [Module.Finite S] [Module.Free S] {i : } :

    Multiplicity of the ideal norm, for powers of prime ideals.

    Multiplicativity of the ideal norm in number rings.

    The absolute norm of the ideal I : Ideal R is the cardinality of the quotient R ⧸ I.

    Equations
    • Ideal.absNorm = { toZeroHom := { toFun := Submodule.cardQuot, map_zero' := }, map_one' := , map_mul' := }
    Instances For
      @[simp]
      theorem Ideal.absNorm_bot {S : Type u_1} [CommRing S] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free S] [Module.Finite S] :
      Ideal.absNorm = 0
      @[simp]
      theorem Ideal.absNorm_top {S : Type u_1} [CommRing S] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free S] [Module.Finite S] :
      Ideal.absNorm = 1
      @[simp]
      theorem Ideal.absNorm_eq_one_iff {S : Type u_1} [CommRing S] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free S] [Module.Finite S] {I : Ideal S} :
      Ideal.absNorm I = 1 I =
      theorem Ideal.absNorm_ne_zero_iff {S : Type u_1} [CommRing S] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free S] [Module.Finite S] (I : Ideal S) :
      Ideal.absNorm I 0 Finite (S I)
      theorem Ideal.natAbs_det_equiv {S : Type u_1} [CommRing S] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free S] [Module.Finite S] (I : Ideal S) {E : Type u_2} [EquivLike E S I] [AddEquivClass E S I] (e : E) :
      Int.natAbs (LinearMap.det ( (Submodule.subtype I) ∘ₗ AddMonoidHom.toIntLinearMap e)) = Ideal.absNorm I

      Let e : S ≃ I be an additive isomorphism (therefore a -linear equiv). Then an alternative way to compute the norm of I is given by taking the determinant of e. See natAbs_det_basis_change for a more familiar formulation of this result.

      theorem Ideal.natAbs_det_basis_change {S : Type u_1} [CommRing S] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free S] [Module.Finite S] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Basis ι S) (I : Ideal S) (bI : Basis ι I) :
      Int.natAbs ((Basis.det b) (Subtype.val bI)) = Ideal.absNorm I

      Let b be a basis for S over and bI a basis for I over of the same dimension. Then an alternative way to compute the norm of I is given by taking the determinant of bI over b.

      @[simp]
      theorem Ideal.absNorm_dvd_absNorm_of_le {S : Type u_1} [CommRing S] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free S] [Module.Finite S] {I : Ideal S} {J : Ideal S} (h : J I) :
      Ideal.absNorm I Ideal.absNorm J
      theorem Ideal.absNorm_dvd_norm_of_mem {S : Type u_1} [CommRing S] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free S] [Module.Finite S] {I : Ideal S} {x : S} (h : x I) :
      (Ideal.absNorm I) (Algebra.norm ) x
      @[simp]
      theorem Ideal.absNorm_span_insert {S : Type u_1} [CommRing S] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free S] [Module.Finite S] (r : S) (s : Set S) :
      Ideal.absNorm (Ideal.span (insert r s)) gcd (Ideal.absNorm (Ideal.span s)) (Int.natAbs ((Algebra.norm ) r))
      theorem Ideal.absNorm_eq_zero_iff {S : Type u_1} [CommRing S] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free S] [Module.Finite S] {I : Ideal S} :
      Ideal.absNorm I = 0 I =
      theorem Ideal.prime_of_irreducible_absNorm_span {S : Type u_1} [CommRing S] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free S] [Module.Finite S] {a : S} (ha : a 0) (hI : Irreducible (Ideal.absNorm (Ideal.span {a}))) :
      theorem Ideal.absNorm_mem {S : Type u_1} [CommRing S] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free S] [Module.Finite S] (I : Ideal S) :
      (Ideal.absNorm I) I
      theorem Ideal.span_singleton_absNorm_le {S : Type u_1} [CommRing S] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free S] [Module.Finite S] (I : Ideal S) :
      Ideal.span {(Ideal.absNorm I)} I
      theorem Ideal.span_singleton_absNorm {S : Type u_1} [CommRing S] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free S] [Module.Finite S] {I : Ideal S} (hI : Nat.Prime (Ideal.absNorm I)) :
      Ideal.span {(Ideal.absNorm I)} = Ideal.comap (algebraMap S) I
      theorem Ideal.finite_setOf_absNorm_eq {S : Type u_1} [CommRing S] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free S] [Module.Finite S] [CharZero S] {n : } (hn : 0 < n) :
      Set.Finite {I : Ideal S | Ideal.absNorm I = n}
      theorem Ideal.norm_dvd_iff {S : Type u_1} [CommRing S] [IsDomain S] [Nontrivial S] [IsDedekindDomain S] [Module.Free S] [Module.Finite S] {x : S} (hx : Prime ((Algebra.norm ) x)) {y : } :
      (Algebra.norm ) x y x y
      def Ideal.spanNorm (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] (I : Ideal S) :

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

      See also Ideal.relNorm.

      Equations
      Instances For
        @[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] :
        @[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} :
        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) :
        @[simp]
        theorem Ideal.spanNorm_singleton (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] {r : S} :
        @[simp]
        theorem Ideal.spanNorm_top (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] :
        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) :
        theorem Ideal.spanNorm_mono (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] {I : Ideal S} {J : Ideal S} (h : I J) :
        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ₘ] :
        theorem Ideal.spanNorm_mul_spanNorm_le (R : Type u_1) [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] (I : Ideal S) (J : Ideal S) :
        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 : Ideal S) (J : Ideal S) :

        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.

        @[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 : Ideal S) (J : Ideal S) :
        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 : Ideal S) (J : Ideal S) :

        Multiplicativity of Ideal.spanNorm. simp-normal form is map_mul (Ideal.relNorm 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
          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) :
          @[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) :
          @[simp]
          @[simp]
          @[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} :
          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) :
          @[simp]
          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)
          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 : Ideal S} {J : Ideal S} (h : I J) :