Localization of ideals and submodules

DefinitionSaturation of a submodule at a submonoid#✓fully proved

Let \(A\) be a commutative ring, \(V\) an \(A\)-module, \(M\) a submodule of \(V\) and \(S\) a submonoid of \(A\). The saturation of \(M\) at \(S\) is the submodule of \(V\) consisting of the elements \(v \in V\) such that \(s v \in M\) for some \(s \in S\).

Writing \(S^{-1}V\) for the localization of \(V\) at \(S\) and \(S^{-1}M \subseteq S^{-1}V\) for that of \(M\), it is the preimage of \(S^{-1}M\) under the localization map \(V \to S^{-1}V\), that is, the contraction to \(V\) of the extension of \(M\) to the localization at \(S\).

def localizedAt (M : Submodule A V) (S : Submonoid A) : Submodule A V where
  carrier := {v | ∃ s ∈ S, s • v ∈ M}
  add_mem' := by
    rintro a b ⟨s₁, hs₁, h₁⟩ ⟨s₂, hs₂, h₂⟩
    refine ⟨s₁ * s₂, S.mul_mem hs₁ hs₂, ?_⟩
    have h : (s₁ * s₂) • (a + b) = s₂ • (s₁ • a) + s₁ • (s₂ • b) := by
      rw [smul_add, mul_smul, mul_smul, smul_comm s₁ s₂ a, smul_comm s₁ s₂ b]
    rw [h]
    exact M.add_mem (M.smul_mem _ h₁) (M.smul_mem _ h₂)
  zero_mem' := ⟨1, S.one_mem, by simp⟩
  smul_mem' := by
    rintro c v ⟨s, hs, h⟩
    exact ⟨s, hs, by rw [smul_comm]; exact M.smul_mem _ h⟩
Used by 8
Used byThe image of an ideal in the fraction field is the intersection of its localizations at maximal ideals · A submodule is the intersection of its saturations at the maximal ideals · Intersections of saturations over maximal and over prime ideals agree · The image of an ideal in the fraction field is the intersection of its localizations at prime ideals · A submodule is the intersection of its saturations at the prime ideals · Membership in the saturation · Membership is detected at the maximal ideals · Membership is detected at the prime ideals

TheoremMembership in the saturation#✓fully proved

Let \(A\) be a commutative ring, \(V\) an \(A\)-module, \(M\) a submodule of \(V\) and \(S\) a submonoid of \(A\). An element \(v \in V\) lies in the saturation of \(M\) at \(S\) if and only if \(s v \in M\) for some \(s \in S\).

theorem mem_localizedAt {M : Submodule A V} {S : Submonoid A} {v : V} :
    v ∈ M.localizedAt S ↔ ∃ s ∈ S, s • v ∈ M
Uses 1
Statement usesSaturation of a submodule at a submonoid

TheoremMembership is detected at the maximal ideals#✓fully proved

Let \(A\) be a commutative ring, \(V\) an \(A\)-module, \(M\) a submodule of \(V\) and \(v \in V\). Suppose that for every maximal ideal \(\mathfrak m\) of \(A\), \(v\) lies in the saturation of \(M\) at \(A \setminus \mathfrak m\), that is, \(s v \in M\) for some \(s \in A \setminus \mathfrak m\). Then \(v \in M\).

theorem mem_of_forall_mem_localizedAt_maximal (M : Submodule A V) {v : V}
    (h : ∀ 𝔪 : MaximalSpectrum A, v ∈ M.localizedAt 𝔪.asIdeal.primeCompl) :
    v ∈ M
Sources
  • ATLAS NumberTheoryI, Section 2.3, Proposition 2.6, element form.
Uses 1 · Used by 2
Statement usesSaturation of a submodule at a submonoid
Used byA submodule is the intersection of its saturations at the maximal ideals · Membership is detected at the prime ideals

TheoremMembership is detected at the prime ideals#✓fully proved

Let \(A\) be a commutative ring, \(V\) an \(A\)-module, \(M\) a submodule of \(V\) and \(v \in V\). Suppose that for every prime ideal \(\mathfrak p\) of \(A\), \(v\) lies in the saturation of \(M\) at \(A \setminus \mathfrak p\), that is, \(s v \in M\) for some \(s \in A \setminus \mathfrak p\). Then \(v \in M\).

theorem mem_of_forall_mem_localizedAt_prime (M : Submodule A V) {v : V}
    (h : ∀ 𝔭 : PrimeSpectrum A, v ∈ M.localizedAt 𝔭.asIdeal.primeCompl) :
    v ∈ M
Sources
  • ATLAS NumberTheoryI, Section 2.3, Proposition 2.6, element form.
Uses 2 · Used by 1
Statement usesSaturation of a submodule at a submonoid
Proof usesMembership is detected at the maximal ideals
Used byA submodule is the intersection of its saturations at the prime ideals

TheoremA submodule is the intersection of its saturations at the maximal ideals#✓fully proved

Let \(A\) be a commutative ring, \(V\) an \(A\)-module and \(M\) a submodule of \(V\). For a maximal ideal \(\mathfrak m\) of \(A\), let \(M_{\mathfrak m}\) be the saturation of \(M\) at \(A \setminus \mathfrak m\), that is, the set of \(v \in V\) with \(s v \in M\) for some \(s \in A \setminus \mathfrak m\). Then \(M\) is the intersection of the submodules \(M_{\mathfrak m}\) over all maximal ideals \(\mathfrak m\) of \(A\).

theorem eq_iInf_localizedAt_maximal (M : Submodule A V) :
    (⨅ 𝔪 : MaximalSpectrum A, M.localizedAt 𝔪.asIdeal.primeCompl) = M
Sources
  • ATLAS NumberTheoryI, Section 2.3, Proposition 2.6, maximal-ideal form.
Uses 2 · Used by 2
Statement usesSaturation of a submodule at a submonoid
Proof usesMembership is detected at the maximal ideals
Used byThe image of an ideal in the fraction field is the intersection of its localizations at maximal ideals · Intersections of saturations over maximal and over prime ideals agree

TheoremA submodule is the intersection of its saturations at the prime ideals#✓fully proved

Let \(A\) be a commutative ring, \(V\) an \(A\)-module and \(M\) a submodule of \(V\). For a prime ideal \(\mathfrak p\) of \(A\), let \(M_{\mathfrak p}\) be the saturation of \(M\) at \(A \setminus \mathfrak p\), that is, the set of \(v \in V\) with \(s v \in M\) for some \(s \in A \setminus \mathfrak p\). Then \(M\) is the intersection of the submodules \(M_{\mathfrak p}\) over all prime ideals \(\mathfrak p\) of \(A\).

theorem eq_iInf_localizedAt_prime (M : Submodule A V) :
    (⨅ 𝔭 : PrimeSpectrum A, M.localizedAt 𝔭.asIdeal.primeCompl) = M
Sources
  • ATLAS NumberTheoryI, Section 2.3, Proposition 2.6, prime-ideal form.
Uses 2 · Used by 2
Statement usesSaturation of a submodule at a submonoid
Proof usesMembership is detected at the prime ideals
Used byIntersections of saturations over maximal and over prime ideals agree · The image of an ideal in the fraction field is the intersection of its localizations at prime ideals

TheoremIntersections of saturations over maximal and over prime ideals agree#✓fully proved

Let \(A\) be a commutative ring, \(V\) an \(A\)-module and \(M\) a submodule of \(V\). For a prime ideal \(\mathfrak p\) of \(A\), let \(M_{\mathfrak p}\) be the saturation of \(M\) at \(A \setminus \mathfrak p\), that is, the set of \(v \in V\) with \(s v \in M\) for some \(s \in A \setminus \mathfrak p\). Then the intersection of the \(M_{\mathfrak m}\) over all maximal ideals \(\mathfrak m\) of \(A\) equals the intersection of the \(M_{\mathfrak p}\) over all prime ideals \(\mathfrak p\) of \(A\).

theorem eq_iInf_localizedAt_maximal_eq_prime (M : Submodule A V) :
    (⨅ 𝔪 : MaximalSpectrum A, M.localizedAt 𝔪.asIdeal.primeCompl) =
    (⨅ 𝔭 : PrimeSpectrum A, M.localizedAt 𝔭.asIdeal.primeCompl)
Uses 3
Statement usesSaturation of a submodule at a submonoid
Proof usesA submodule is the intersection of its saturations at the maximal ideals · A submodule is the intersection of its saturations at the prime ideals

TheoremAn ideal is the intersection of its contracted localizations at maximal ideals#✓fully proved

Let \(A\) be a commutative ring and \(I\) an ideal of \(A\). For a maximal ideal \(\mathfrak{m}\) of \(A\), let \(\varphi_{\mathfrak{m}} \colon A \to A_{\mathfrak{m}}\) be the canonical map to the localization of \(A\) at \(\mathfrak{m}\). Then \(I = \bigcap_{\mathfrak{m}} \varphi_{\mathfrak{m}}^{-1}(I A_{\mathfrak{m}})\), the intersection over all maximal ideals \(\mathfrak{m}\) of \(A\): an ideal is the intersection of the contractions to \(A\) of its extensions to the localizations at the maximal ideals.

theorem eq_iInf_comap_map_localization_maximal (I : Ideal A) :
    (⨅ 𝔪 : MaximalSpectrum A,
      (I.map (algebraMap A (Localization 𝔪.asIdeal.primeCompl))).comap
        (algebraMap A (Localization 𝔪.asIdeal.primeCompl))) = I
Used by 2
Used byAn ideal is the intersection of its contracted localizations at prime ideals · Contracted localizations of an ideal: the maximal and prime intersections agree

TheoremAn ideal is the intersection of its contracted localizations at prime ideals#✓fully proved

Let \(A\) be a commutative ring and \(I\) an ideal of \(A\). For a prime ideal \(\mathfrak{p}\) of \(A\), let \(\varphi_{\mathfrak{p}} \colon A \to A_{\mathfrak{p}}\) be the canonical map to the localization of \(A\) at \(\mathfrak{p}\). Then \(I = \bigcap_{\mathfrak{p}} \varphi_{\mathfrak{p}}^{-1}(I A_{\mathfrak{p}})\), the intersection over all prime ideals \(\mathfrak{p}\) of \(A\): an ideal is the intersection of the contractions to \(A\) of its extensions to the localizations at the prime ideals.

theorem eq_iInf_comap_map_localization_prime (I : Ideal A) :
    (⨅ 𝔭 : PrimeSpectrum A,
      (I.map (algebraMap A (Localization 𝔭.asIdeal.primeCompl))).comap
        (algebraMap A (Localization 𝔭.asIdeal.primeCompl))) = I
Uses 1 · Used by 1
Proof usesAn ideal is the intersection of its contracted localizations at maximal ideals
Used byContracted localizations of an ideal: the maximal and prime intersections agree

TheoremContracted localizations of an ideal: the maximal and prime intersections agree#✓fully proved

Let \(A\) be a commutative ring and \(I\) an ideal of \(A\). For a prime ideal \(\mathfrak{p}\) of \(A\), let \(\varphi_{\mathfrak{p}} \colon A \to A_{\mathfrak{p}}\) be the canonical map to the localization of \(A\) at \(\mathfrak{p}\). Then \(\bigcap_{\mathfrak{m}} \varphi_{\mathfrak{m}}^{-1}(I A_{\mathfrak{m}}) = \bigcap_{\mathfrak{p}} \varphi_{\mathfrak{p}}^{-1}(I A_{\mathfrak{p}})\), where the left intersection runs over all maximal ideals \(\mathfrak{m}\) of \(A\) and the right one over all prime ideals \(\mathfrak{p}\) of \(A\).

theorem iInf_comap_map_localization_maximal_eq_prime (I : Ideal A) :
    (⨅ 𝔪 : MaximalSpectrum A,
      (I.map (algebraMap A (Localization 𝔪.asIdeal.primeCompl))).comap
        (algebraMap A (Localization 𝔪.asIdeal.primeCompl))) =
    (⨅ 𝔭 : PrimeSpectrum A,
      (I.map (algebraMap A (Localization 𝔭.asIdeal.primeCompl))).comap
        (algebraMap A (Localization 𝔭.asIdeal.primeCompl)))
Uses 2
Proof usesAn ideal is the intersection of its contracted localizations at maximal ideals · An ideal is the intersection of its contracted localizations at prime ideals

TheoremThe image of an ideal in the fraction field is the intersection of its localizations at maximal ideals#✓fully proved

The image of an ideal in the fraction field is the intersection of its localizations at maximal ideals. Let \(A\) be an integral domain with fraction field \(K\), let \(I\) be an ideal of \(A\), and let \(M \subseteq K\) be the image of \(I\) under the canonical map \(A \to K\), an \(A\)-submodule of \(K\). For a maximal ideal \(\mathfrak{m}\) of \(A\), let \(M_{\mathfrak{m}}\) be the localization of \(M\) at \(\mathfrak{m}\): the set of \(x \in K\) such that \(s x \in M\) for some \(s \in A \setminus \mathfrak{m}\). Then \(M = \bigcap_{\mathfrak{m}} M_{\mathfrak{m}}\), the intersection over all maximal ideals \(\mathfrak{m}\) of \(A\), taken inside \(K\).

theorem eq_iInf_localizedAt_maximal [IsDomain A] (K : Type*)
    [Field K] [Algebra A K] [IsFractionRing A K] (I : Ideal A) :
    (⨅ 𝔪 : MaximalSpectrum A,
      (Submodule.map (Algebra.linearMap A K) I).localizedAt
        𝔪.asIdeal.primeCompl) =
    Submodule.map (Algebra.linearMap A K) I
Sources
  • ATLAS NumberTheoryI, Section 2.3, Corollary 2.7, maximal-ideal form.
Uses 2
Statement usesSaturation of a submodule at a submonoid
Proof usesA submodule is the intersection of its saturations at the maximal ideals

TheoremThe image of an ideal in the fraction field is the intersection of its localizations at prime ideals#✓fully proved

The image of an ideal in the fraction field is the intersection of its localizations at prime ideals. Let \(A\) be an integral domain with fraction field \(K\), let \(I\) be an ideal of \(A\), and let \(M \subseteq K\) be the image of \(I\) under the canonical map \(A \to K\), an \(A\)-submodule of \(K\). For a prime ideal \(\mathfrak{p}\) of \(A\), let \(M_{\mathfrak{p}}\) be the localization of \(M\) at \(\mathfrak{p}\): the set of \(x \in K\) such that \(s x \in M\) for some \(s \in A \setminus \mathfrak{p}\). Then \(M = \bigcap_{\mathfrak{p}} M_{\mathfrak{p}}\), the intersection over all prime ideals \(\mathfrak{p}\) of \(A\), taken inside \(K\).

theorem eq_iInf_localizedAt_prime [IsDomain A] (K : Type*)
    [Field K] [Algebra A K] [IsFractionRing A K] (I : Ideal A) :
    (⨅ 𝔭 : PrimeSpectrum A,
      (Submodule.map (Algebra.linearMap A K) I).localizedAt
        𝔭.asIdeal.primeCompl) =
    Submodule.map (Algebra.linearMap A K) I
Sources
  • ATLAS NumberTheoryI, Section 2.3, Corollary 2.7, prime-ideal form.
Uses 2
Statement usesSaturation of a submodule at a submonoid
Proof usesA submodule is the intersection of its saturations at the prime ideals
12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.