Ideals in localizations of commutative rings #
Implementation notes #
See Mathlib/RingTheory/Localization/Basic.lean for a design overview.
Tags #
localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions
theorem
IsLocalization.mk'_mem_iff
{R : Type u_1}
[CommSemiring R]
{M : Submonoid R}
{S : Type u_2}
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
{x : R}
{y : ↥M}
{I : Ideal S}
:
theorem
IsLocalization.mem_map_algebraMap_iff
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
{I : Ideal R}
{z : S}
:
z ∈ Ideal.map (algebraMap R S) I ↔ ∃ (x : ↥I × ↥M), z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1
theorem
IsLocalization.mk'_mem_map_algebraMap_iff
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
(I : Ideal R)
(x : R)
(s : ↥M)
:
theorem
IsLocalization.algebraMap_mem_map_algebraMap_iff
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
(I : Ideal R)
(x : R)
:
theorem
IsLocalization.map_algebraMap_ne_top_iff_disjoint
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
(I : Ideal R)
:
theorem
IsLocalization.map_inf
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
(I J : Ideal R)
:
def
IsLocalization.mapFrameHom
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
:
IsLocalization.map_inf as an FrameHom.
Equations
Instances For
@[simp]
theorem
IsLocalization.mapFrameHom_apply
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
(I : Ideal R)
:
theorem
IsLocalization.map_comap
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
(J : Ideal S)
:
theorem
IsLocalization.comap_map_of_isPrimary_disjoint
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
{I : Ideal R}
(hI : I.IsPrimary)
(hM : Disjoint ↑M ↑I)
:
theorem
IsLocalization.comap_map_of_isPrime_disjoint
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
{I : Ideal R}
(hI : I.IsPrime)
(hM : Disjoint ↑M ↑I)
:
def
IsLocalization.orderEmbedding
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
:
If S is the localization of R at a submonoid, the ordering of ideals of S is
embedded in the ordering of ideals of R.
Equations
Instances For
theorem
IsLocalization.isPrime_iff_isPrime_disjoint
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
(J : Ideal S)
:
J.IsPrime ↔ (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
If R is a ring, then prime ideals in the localization at M
correspond to prime ideals in the original ring R that are disjoint from M.
This lemma gives the particular case for an ideal and its comap,
see le_rel_iso_of_prime for the more general relation isomorphism
theorem
IsLocalization.isPrime_of_isPrime_disjoint
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
(I : Ideal R)
(hp : I.IsPrime)
(hd : Disjoint ↑M ↑I)
:
(Ideal.map (algebraMap R S) I).IsPrime
If R is a ring, then prime ideals in the localization at M
correspond to prime ideals in the original ring R that are disjoint from M.
This lemma gives the particular case for an ideal and its map,
see le_rel_iso_of_prime for the more general relation isomorphism, and the reverse implication
theorem
IsLocalization.disjoint_comap_iff
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
(J : Ideal S)
:
def
IsLocalization.orderIsoOfPrime
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
:
If R is a ring, then prime ideals in the localization at M
correspond to prime ideals in the original ring R that are disjoint from M
Equations
Instances For
@[simp]
theorem
IsLocalization.orderIsoOfPrime_symm_apply_coe
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
(p : { p : Ideal R // p.IsPrime ∧ Disjoint ↑M ↑p })
:
@[simp]
theorem
IsLocalization.orderIsoOfPrime_apply_coe
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
(p : { p : Ideal S // p.IsPrime })
:
def
IsLocalization.primeSpectrumOrderIso
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
:
The prime spectrum of the localization of a ring at a submonoid M are in
order-preserving bijection with subset of the prime spectrum of the ring consisting of
prime ideals disjoint from M.
Equations
Instances For
@[simp]
theorem
IsLocalization.coe_primeSpectrumOrderIso_symm_apply_asIdeal
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
(a✝ : { p : PrimeSpectrum R // Disjoint ↑M ↑p.asIdeal })
:
↑((RelIso.symm (primeSpectrumOrderIso M S)) a✝).asIdeal = ⋂ (s : Submodule S S), ⋂ (_ : ↑(↑a✝).asIdeal ⊆ ⇑(algebraMap R S) ⁻¹' ↑s), ↑s
@[simp]
theorem
IsLocalization.coe_primeSpectrumOrderIso_apply_coe_asIdeal
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
(a✝ : PrimeSpectrum S)
:
theorem
IsLocalization.map_radical
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
(I : Ideal R)
:
theorem
IsLocalization.ideal_eq_iInf_comap_map_away
{R : Type u_1}
[CommSemiring R]
{S : Finset R}
(hS : Ideal.span ↑S = ⊤)
(I : Ideal R)
:
I = ⨅ f ∈ S, Ideal.comap (algebraMap R (Localization.Away f)) (Ideal.map (algebraMap R (Localization.Away f)) I)
theorem
IsLocalization.surjective_quotientMap_of_maximal_of_localization
{R : Type u_1}
[CommRing R]
(M : Submonoid R)
(S : Type u_2)
[CommRing S]
[Algebra R S]
[IsLocalization M S]
{I : Ideal S}
[I.IsPrime]
{J : Ideal R}
{H : J ≤ Ideal.comap (algebraMap R S) I}
(hI : (Ideal.comap (algebraMap R S) I).IsMaximal)
:
Function.Surjective ⇑(Ideal.quotientMap I (algebraMap R S) H)
quotientMap applied to maximal ideals of a localization is surjective.
The quotient by a maximal ideal is a field, so inverses to elements already exist,
and the localization necessarily maps the equivalence class of the inverse in the localization
theorem
IsLocalization.bot_lt_comap_prime
{R : Type u_1}
[CommRing R]
(M : Submonoid R)
(S : Type u_2)
[CommRing S]
[Algebra R S]
[IsLocalization M S]
[IsDomain R]
(hM : M ≤ nonZeroDivisors R)
(p : Ideal S)
[hpp : p.IsPrime]
(hp0 : p ≠ ⊥)
:
theorem
Module.IsTorsionFree.of_isLocalization
(R : Type u_1)
[CommRing R]
(S : Type u_2)
[CommRing S]
[Algebra R S]
[IsDomain R]
[IsDomain S]
{Rₚ : Type u_3}
{Sₚ : Type u_4}
[CommRing Rₚ]
[IsDomain Rₚ]
[CommRing Sₚ]
[Algebra R Rₚ]
[Algebra R Sₚ]
[Algebra S Sₚ]
[Algebra Rₚ Sₚ]
[IsScalarTower R S Sₚ]
[IsScalarTower R Rₚ Sₚ]
{M : Submonoid R}
(hM : M ≤ nonZeroDivisors R)
[IsLocalization M Rₚ]
[IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ]
[IsTorsionFree R S]
:
IsTorsionFree Rₚ Sₚ
theorem
IsLocalization.of_surjective
{R : Type u_1}
[CommRing R]
(M : Submonoid R)
(S : Type u_2)
[CommRing S]
[Algebra R S]
[IsLocalization M S]
{R' : Type u_3}
{S' : Type u_4}
[CommRing R']
[CommRing S']
[Algebra R' S']
(f : R →+* R')
(hf : Function.Surjective ⇑f)
(g : S →+* S')
(hg : Function.Surjective ⇑g)
(H : g.comp (algebraMap R S) = (algebraMap R' S').comp f)
(H' : RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f))
:
IsLocalization (Submonoid.map f M) S'