The Zariski topology on the prime spectrum of a commutative (semi)ring #
Conventions #
We denote subsets of (semi)rings with s, s', etc...
whereas we denote subsets of prime spectra with t, t', etc...
Inspiration/contributors #
The contents of this file draw inspiration from https://github.com/ramonfmir/lean-scheme which has contributions from Ramon Fernandez Mir, Kevin Buzzard, Kenny Lau, and Chris Hughes (on an earlier repository).
The Zariski topology on the prime spectrum of a commutative (semi)ring is defined via the closed sets of the topology: they are exactly those sets that are the zero locus of a subset of the ring.
theorem
PrimeSpectrum.isClosed_iff_zeroLocus
{R : Type u}
[CommSemiring R]
(Z : Set (PrimeSpectrum R))
:
IsClosed Z ↔ ∃ (s : Set R), Z = PrimeSpectrum.zeroLocus s
theorem
PrimeSpectrum.isClosed_iff_zeroLocus_ideal
{R : Type u}
[CommSemiring R]
(Z : Set (PrimeSpectrum R))
:
IsClosed Z ↔ ∃ (I : Ideal R), Z = PrimeSpectrum.zeroLocus ↑I
theorem
PrimeSpectrum.isClosed_iff_zeroLocus_radical_ideal
{R : Type u}
[CommSemiring R]
(Z : Set (PrimeSpectrum R))
:
theorem
PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure
{R : Type u}
[CommSemiring R]
(t : Set (PrimeSpectrum R))
:
theorem
PrimeSpectrum.vanishingIdeal_closure
{R : Type u}
[CommSemiring R]
(t : Set (PrimeSpectrum R))
:
theorem
PrimeSpectrum.closure_singleton
{R : Type u}
[CommSemiring R]
(x : PrimeSpectrum R)
:
closure {x} = PrimeSpectrum.zeroLocus ↑x.asIdeal
theorem
PrimeSpectrum.isClosed_singleton_iff_isMaximal
{R : Type u}
[CommSemiring R]
(x : PrimeSpectrum R)
:
theorem
PrimeSpectrum.isRadical_vanishingIdeal
{R : Type u}
[CommSemiring R]
(s : Set (PrimeSpectrum R))
:
(PrimeSpectrum.vanishingIdeal s).IsRadical
theorem
PrimeSpectrum.zeroLocus_eq_iff
{R : Type u}
[CommSemiring R]
{I J : Ideal R}
:
PrimeSpectrum.zeroLocus ↑I = PrimeSpectrum.zeroLocus ↑J ↔ I.radical = J.radical
theorem
PrimeSpectrum.vanishingIdeal_anti_mono_iff
{R : Type u}
[CommSemiring R]
{s t : Set (PrimeSpectrum R)}
(ht : IsClosed t)
:
theorem
PrimeSpectrum.vanishingIdeal_strict_anti_mono_iff
{R : Type u}
[CommSemiring R]
{s t : Set (PrimeSpectrum R)}
(hs : IsClosed s)
(ht : IsClosed t)
:
The antitone order embedding of closed subsets of Spec R into ideals of R.
Equations
- PrimeSpectrum.closedsEmbedding R = OrderEmbedding.ofMapLEIff (fun (s : (TopologicalSpace.Closeds (PrimeSpectrum R))ᵒᵈ) => PrimeSpectrum.vanishingIdeal ↑(OrderDual.ofDual s)) ⋯
Instances For
theorem
PrimeSpectrum.t1Space_iff_isField
{R : Type u}
[CommSemiring R]
[IsDomain R]
:
T1Space (PrimeSpectrum R) ↔ IsField R
theorem
PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radical
{R : Type u}
[CommSemiring R]
(I : Ideal R)
(hI : I.IsRadical)
:
IsIrreducible (PrimeSpectrum.zeroLocus ↑I) ↔ I.IsPrime
theorem
PrimeSpectrum.isIrreducible_zeroLocus_iff
{R : Type u}
[CommSemiring R]
(I : Ideal R)
:
IsIrreducible (PrimeSpectrum.zeroLocus ↑I) ↔ I.radical.IsPrime
theorem
PrimeSpectrum.isIrreducible_iff_vanishingIdeal_isPrime
{R : Type u}
[CommSemiring R]
{s : Set (PrimeSpectrum R)}
:
IsIrreducible s ↔ (PrimeSpectrum.vanishingIdeal s).IsPrime
theorem
PrimeSpectrum.vanishingIdeal_isIrreducible
{R : Type u}
[CommSemiring R]
:
PrimeSpectrum.vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsIrreducible s} = {P : Ideal R | P.IsPrime}
theorem
PrimeSpectrum.vanishingIdeal_isClosed_isIrreducible
{R : Type u}
[CommSemiring R]
:
PrimeSpectrum.vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s} = {P : Ideal R | P.IsPrime}
The prime spectrum of a commutative (semi)ring is a compact topological space.
theorem
PrimeSpectrum.discreteTopology_iff_finite_and_isPrime_imp_isMaximal
{R : Type u}
[CommSemiring R]
:
DiscreteTopology (PrimeSpectrum R) ↔ Finite (PrimeSpectrum R) ∧ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal
The prime spectrum of a semiring has discrete Zariski topology iff it is finite and all primes are maximal.
theorem
PrimeSpectrum.discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical
{R : Type u}
[CommSemiring R]
:
DiscreteTopology (PrimeSpectrum R) ↔ Finite ↑{I : Ideal R | I.IsMaximal} ∧ sInf {I : Ideal R | I.IsMaximal} ≤ nilradical R
The prime spectrum of a semiring has discrete Zariski topology iff there are only finitely many maximal ideals and their intersection is contained in the nilradical.
theorem
PrimeSpectrum.discreteTopology_of_toLocalization_surjective
{R : Type u}
[CommSemiring R]
(surj : Function.Surjective ⇑(PrimeSpectrum.toPiLocalization R))
:
The continuous function between prime spectra of commutative (semi)rings induced by a ring homomorphism.
Equations
- PrimeSpectrum.comap f = { toFun := f.specComap, continuous_toFun := ⋯ }
Instances For
@[simp]
theorem
PrimeSpectrum.comap_asIdeal
{R : Type u}
{S : Type v}
[CommSemiring R]
[CommSemiring S]
(f : R →+* S)
(y : PrimeSpectrum S)
:
((PrimeSpectrum.comap f) y).asIdeal = Ideal.comap f y.asIdeal
@[simp]
@[simp]
theorem
PrimeSpectrum.comap_comp
{R : Type u}
{S : Type v}
[CommSemiring R]
[CommSemiring S]
{S' : Type u_1}
[CommSemiring S']
(f : R →+* S)
(g : S →+* S')
:
PrimeSpectrum.comap (g.comp f) = (PrimeSpectrum.comap f).comp (PrimeSpectrum.comap g)
theorem
PrimeSpectrum.comap_comp_apply
{R : Type u}
{S : Type v}
[CommSemiring R]
[CommSemiring S]
{S' : Type u_1}
[CommSemiring S']
(f : R →+* S)
(g : S →+* S')
(x : PrimeSpectrum S')
:
(PrimeSpectrum.comap (g.comp f)) x = (PrimeSpectrum.comap f) ((PrimeSpectrum.comap g) x)
@[simp]
theorem
PrimeSpectrum.preimage_comap_zeroLocus
{R : Type u}
{S : Type v}
[CommSemiring R]
[CommSemiring S]
(f : R →+* S)
(s : Set R)
:
⇑(PrimeSpectrum.comap f) ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus (⇑f '' s)
theorem
PrimeSpectrum.comap_injective_of_surjective
{R : Type u}
{S : Type v}
[CommSemiring R]
[CommSemiring S]
(f : R →+* S)
(hf : Function.Surjective ⇑f)
:
theorem
PrimeSpectrum.localization_comap_isInducing
{R : Type u}
(S : Type v)
[CommSemiring R]
[CommSemiring S]
[Algebra R S]
(M : Submonoid R)
[IsLocalization M S]
:
@[deprecated PrimeSpectrum.localization_comap_isInducing (since := "2024-10-28")]
theorem
PrimeSpectrum.localization_comap_inducing
{R : Type u}
(S : Type v)
[CommSemiring R]
[CommSemiring S]
[Algebra R S]
(M : Submonoid R)
[IsLocalization M S]
:
theorem
PrimeSpectrum.localization_comap_injective
{R : Type u}
(S : Type v)
[CommSemiring R]
[CommSemiring S]
[Algebra R S]
(M : Submonoid R)
[IsLocalization M S]
:
theorem
PrimeSpectrum.localization_comap_isEmbedding
{R : Type u}
(S : Type v)
[CommSemiring R]
[CommSemiring S]
[Algebra R S]
(M : Submonoid R)
[IsLocalization M S]
:
@[deprecated PrimeSpectrum.localization_comap_isEmbedding (since := "2024-10-26")]
theorem
PrimeSpectrum.localization_comap_embedding
{R : Type u}
(S : Type v)
[CommSemiring R]
[CommSemiring S]
[Algebra R S]
(M : Submonoid R)
[IsLocalization M S]
:
theorem
PrimeSpectrum.localization_comap_range
{R : Type u}
(S : Type v)
[CommSemiring R]
[CommSemiring S]
[Algebra R S]
(M : Submonoid R)
[IsLocalization M S]
:
Set.range ⇑(PrimeSpectrum.comap (algebraMap R S)) = {p : PrimeSpectrum R | Disjoint ↑M ↑p.asIdeal}
theorem
PrimeSpectrum.comap_isInducing_of_surjective
{R : Type u}
(S : Type v)
[CommSemiring R]
[CommSemiring S]
(f : R →+* S)
(hf : Function.Surjective ⇑f)
:
@[deprecated PrimeSpectrum.comap_isInducing_of_surjective (since := "2024-10-28")]
theorem
PrimeSpectrum.comap_inducing_of_surjective
{R : Type u}
(S : Type v)
[CommSemiring R]
[CommSemiring S]
(f : R →+* S)
(hf : Function.Surjective ⇑f)
:
The comap of a surjective ring homomorphism is a closed embedding between the prime spectra.
theorem
PrimeSpectrum.comap_singleton_isClosed_of_surjective
{R : Type u}
(S : Type v)
[CommRing R]
[CommRing S]
(f : R →+* S)
(hf : Function.Surjective ⇑f)
(x : PrimeSpectrum S)
(hx : IsClosed {x})
:
IsClosed {(PrimeSpectrum.comap f) x}
theorem
PrimeSpectrum.image_comap_zeroLocus_eq_zeroLocus_comap
{R : Type u}
(S : Type v)
[CommRing R]
[CommRing S]
(f : R →+* S)
(hf : Function.Surjective ⇑f)
(I : Ideal S)
:
⇑(PrimeSpectrum.comap f) '' PrimeSpectrum.zeroLocus ↑I = PrimeSpectrum.zeroLocus ↑(Ideal.comap f I)
theorem
PrimeSpectrum.range_comap_of_surjective
{R : Type u}
(S : Type v)
[CommRing R]
[CommRing S]
(f : R →+* S)
(hf : Function.Surjective ⇑f)
:
theorem
PrimeSpectrum.isClosed_range_comap_of_surjective
{R : Type u}
(S : Type v)
[CommRing R]
[CommRing S]
(f : R →+* S)
(hf : Function.Surjective ⇑f)
:
IsClosed (Set.range ⇑(PrimeSpectrum.comap f))
theorem
PrimeSpectrum.isClosedEmbedding_comap_of_surjective
{R : Type u}
(S : Type v)
[CommRing R]
[CommRing S]
(f : R →+* S)
(hf : Function.Surjective ⇑f)
:
@[deprecated PrimeSpectrum.isClosedEmbedding_comap_of_surjective (since := "2024-10-20")]
theorem
PrimeSpectrum.closedEmbedding_comap_of_surjective
{R : Type u}
(S : Type v)
[CommRing R]
[CommRing S]
(f : R →+* S)
(hf : Function.Surjective ⇑f)
:
Alias of PrimeSpectrum.isClosedEmbedding_comap_of_surjective.
theorem
PrimeSpectrum.primeSpectrumProd_symm_inl
{R : Type u}
{S : Type v}
[CommRing R]
[CommRing S]
(x : PrimeSpectrum R)
:
(PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inl x) = (PrimeSpectrum.comap (RingHom.fst R S)) x
theorem
PrimeSpectrum.primeSpectrumProd_symm_inr
{R : Type u}
{S : Type v}
[CommRing R]
[CommRing S]
(x : PrimeSpectrum S)
:
(PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inr x) = (PrimeSpectrum.comap (RingHom.snd R S)) x
noncomputable def
PrimeSpectrum.primeSpectrumProdHomeo
{R : Type u}
{S : Type v}
[CommRing R]
[CommRing S]
:
PrimeSpectrum (R × S) ≃ₜ PrimeSpectrum R ⊕ PrimeSpectrum S
The prime spectrum of R × S is homeomorphic
to the disjoint union of PrimeSpectrum R and PrimeSpectrum S.
Equations
- PrimeSpectrum.primeSpectrumProdHomeo = ((PrimeSpectrum.primeSpectrumProd R S).symm.toHomeomorphOfIsInducing ⋯).symm
Instances For
basicOpen r is the open subset containing all prime ideals not containing r.
Equations
- PrimeSpectrum.basicOpen r = { carrier := {x : PrimeSpectrum R | r ∉ x.asIdeal}, is_open' := ⋯ }
Instances For
@[simp]
theorem
PrimeSpectrum.mem_basicOpen
{R : Type u}
[CommSemiring R]
(f : R)
(x : PrimeSpectrum R)
:
x ∈ PrimeSpectrum.basicOpen f ↔ f ∉ x.asIdeal
@[simp]
theorem
PrimeSpectrum.basicOpen_eq_zeroLocus_compl
{R : Type u}
[CommSemiring R]
(r : R)
:
↑(PrimeSpectrum.basicOpen r) = (PrimeSpectrum.zeroLocus {r})ᶜ
@[simp]
@[simp]
theorem
PrimeSpectrum.basicOpen_le_basicOpen_iff
{R : Type u}
[CommSemiring R]
(f g : R)
:
PrimeSpectrum.basicOpen f ≤ PrimeSpectrum.basicOpen g ↔ f ∈ (Ideal.span {g}).radical
@[simp]
theorem
PrimeSpectrum.isTopologicalBasis_basic_opens
{R : Type u}
[CommSemiring R]
:
TopologicalSpace.IsTopologicalBasis (Set.range fun (r : R) => ↑(PrimeSpectrum.basicOpen r))
@[simp]
theorem
PrimeSpectrum.localization_away_comap_range
{R : Type u}
[CommSemiring R]
(S : Type v)
[CommSemiring S]
[Algebra R S]
(r : R)
[IsLocalization.Away r S]
:
Set.range ⇑(PrimeSpectrum.comap (algebraMap R S)) = ↑(PrimeSpectrum.basicOpen r)
theorem
PrimeSpectrum.localization_away_isOpenEmbedding
{R : Type u}
[CommSemiring R]
(S : Type v)
[CommSemiring S]
[Algebra R S]
(r : R)
[IsLocalization.Away r S]
:
@[deprecated PrimeSpectrum.localization_away_isOpenEmbedding (since := "2024-10-18")]
theorem
PrimeSpectrum.localization_away_openEmbedding
{R : Type u}
[CommSemiring R]
(S : Type v)
[CommSemiring S]
[Algebra R S]
(r : R)
[IsLocalization.Away r S]
:
theorem
PrimeSpectrum.comap_basicOpen
{R : Type u}
{S : Type v}
[CommSemiring R]
[CommSemiring S]
(f : R →+* S)
(x : R)
:
theorem
PrimeSpectrum.iSup_basicOpen_eq_top_iff
{R : Type u}
[CommSemiring R]
{ι : Type u_1}
{f : ι → R}
:
⨆ (i : ι), PrimeSpectrum.basicOpen (f i) = ⊤ ↔ Ideal.span (Set.range f) = ⊤
theorem
PrimeSpectrum.iSup_basicOpen_eq_top_iff'
{R : Type u}
[CommSemiring R]
{s : Set R}
:
⨆ i ∈ s, PrimeSpectrum.basicOpen i = ⊤ ↔ Ideal.span s = ⊤
theorem
PrimeSpectrum.isLocalization_away_iff_atPrime_of_basicOpen_eq_singleton
{R : Type u}
{S : Type v}
[CommSemiring R]
[CommSemiring S]
[Algebra R S]
{f : R}
{p : PrimeSpectrum R}
(h : (PrimeSpectrum.basicOpen f).carrier = {p})
:
IsLocalization.Away f S ↔ IsLocalization.AtPrime S p.asIdeal
def
PrimeSpectrum.MaximalSpectrum.toPiLocalizationEquivtoLocalizationEquiv
(R : Type u)
[CommSemiring R]
[DiscreteTopology (PrimeSpectrum R)]
:
If the prime spectrum of a commutative semiring R has discrete Zariski topology, then R is canonically isomorphic to the product of its localizations at the (finitely many) maximal ideals.
Stacks Tag 00JA (See also PrimeSpectrum.discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical.)
Equations
Instances For
The specialization order #
We endow PrimeSpectrum R with a partial order, where x ≤ y if and only if y ∈ closure {x}.
def
PrimeSpectrum.nhdsOrderEmbedding
{R : Type u}
[CommSemiring R]
:
PrimeSpectrum R ↪o Filter (PrimeSpectrum R)
nhds as an order embedding.
Instances For
@[simp]
theorem
PrimeSpectrum.nhdsOrderEmbedding_apply
{R : Type u}
[CommSemiring R]
(x : PrimeSpectrum R)
:
def
PrimeSpectrum.localizationMapOfSpecializes
{R : Type u}
[CommSemiring R]
{x y : PrimeSpectrum R}
(h : x ⤳ y)
:
Localization.AtPrime y.asIdeal →+* Localization.AtPrime x.asIdeal
If x specializes to y, then there is a natural map from the localization of y to the
localization of x.
Instances For
theorem
PrimeSpectrum.isClosed_range_of_stableUnderSpecialization
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
(f : R →+* S)
(hf : StableUnderSpecialization (Set.range ⇑(PrimeSpectrum.comap f)))
:
IsClosed (Set.range ⇑(PrimeSpectrum.comap f))
theorem
PrimeSpectrum.isClosed_image_of_stableUnderSpecialization
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
(f : R →+* S)
(Z : Set (PrimeSpectrum S))
(hZ : IsClosed Z)
(hf : StableUnderSpecialization (⇑(PrimeSpectrum.comap f) '' Z))
:
IsClosed (⇑(PrimeSpectrum.comap f) '' Z)
theorem
PrimeSpectrum.stableUnderSpecialization_image_iff
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
(f : R →+* S)
(Z : Set (PrimeSpectrum S))
(hZ : IsClosed Z)
:
StableUnderSpecialization (⇑(PrimeSpectrum.comap f) '' Z) ↔ IsClosed (⇑(PrimeSpectrum.comap f) '' Z)
theorem
PrimeSpectrum.vanishingIdeal_range_comap
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
(f : R →+* S)
:
PrimeSpectrum.vanishingIdeal (Set.range ⇑(PrimeSpectrum.comap f)) = (RingHom.ker f).radical
theorem
PrimeSpectrum.denseRange_comap_iff_ker_le_nilRadical
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
(f : R →+* S)
:
DenseRange ⇑(PrimeSpectrum.comap f) ↔ RingHom.ker f ≤ nilradical R
theorem
PrimeSpectrum.denseRange_comap_iff_minimalPrimes
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
(f : R →+* S)
:
DenseRange ⇑(PrimeSpectrum.comap f) ↔ ∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range ⇑(PrimeSpectrum.comap f)
Zero loci of prime ideals are closed irreducible sets in the Zariski topology and any closed irreducible set is a zero locus of some prime ideal.
Equations
- PrimeSpectrum.pointsEquivIrreducibleCloseds R = { toEquiv := irreducibleSetEquivPoints.symm.trans OrderDual.toDual, map_rel_iff' := ⋯ }
Instances For
theorem
PrimeSpectrum.stableUnderSpecialization_singleton
{R : Type u}
[CommSemiring R]
{x : PrimeSpectrum R}
:
StableUnderSpecialization {x} ↔ x.asIdeal.IsMaximal
theorem
PrimeSpectrum.isMin_iff
{R : Type u}
[CommSemiring R]
{x : PrimeSpectrum R}
:
IsMin x ↔ x.asIdeal ∈ minimalPrimes R
theorem
PrimeSpectrum.stableUnderGeneralization_singleton
{R : Type u}
[CommSemiring R]
{x : PrimeSpectrum R}
:
StableUnderGeneralization {x} ↔ x.asIdeal ∈ minimalPrimes R
theorem
PrimeSpectrum.isCompact_isOpen_iff
{R : Type u}
[CommSemiring R]
{s : Set (PrimeSpectrum R)}
:
theorem
PrimeSpectrum.isCompact_isOpen_iff_ideal
{R : Type u}
[CommSemiring R]
{s : Set (PrimeSpectrum R)}
:
theorem
PrimeSpectrum.basicOpen_injOn_isIdempotentElem
{R : Type u}
[CommSemiring R]
:
Set.InjOn PrimeSpectrum.basicOpen {e : R | IsIdempotentElem e}
theorem
PrimeSpectrum.existsUnique_idempotent_basicOpen_eq_of_isClopen
{R : Type u}
[CommSemiring R]
{s : Set (PrimeSpectrum R)}
(hs : IsClopen s)
:
∃! e : R, IsIdempotentElem e ∧ s = ↑(PrimeSpectrum.basicOpen e)
theorem
PrimeSpectrum.exists_idempotent_basicOpen_eq_of_isClopen
{R : Type u}
[CommSemiring R]
{s : Set (PrimeSpectrum R)}
(hs : IsClopen s)
:
∃ (e : R), IsIdempotentElem e ∧ s = ↑(PrimeSpectrum.basicOpen e)
@[deprecated PrimeSpectrum.exists_idempotent_basicOpen_eq_of_isClopen (since := "2024-11-11")]
theorem
PrimeSpectrum.exists_idempotent_basicOpen_eq_of_is_clopen
{R : Type u}
[CommSemiring R]
{s : Set (PrimeSpectrum R)}
(hs : IsClopen s)
:
∃ (e : R), IsIdempotentElem e ∧ s = ↑(PrimeSpectrum.basicOpen e)
Alias of PrimeSpectrum.exists_idempotent_basicOpen_eq_of_isClopen.
theorem
PrimeSpectrum.isClosed_comap_singleton_of_isIntegral
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
(f : R →+* S)
(hf : f.IsIntegral)
(x : PrimeSpectrum S)
(hx : IsClosed {x})
:
IsClosed {(PrimeSpectrum.comap f) x}
theorem
PrimeSpectrum.closure_image_comap_zeroLocus
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
(f : R →+* S)
(I : Ideal S)
:
closure (⇑(PrimeSpectrum.comap f) '' PrimeSpectrum.zeroLocus ↑I) = PrimeSpectrum.zeroLocus ↑(Ideal.comap f I)
theorem
PrimeSpectrum.isIntegral_of_isClosedMap_comap_mapRingHom
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
(f : R →+* S)
(h : IsClosedMap ⇑(PrimeSpectrum.comap (Polynomial.mapRingHom f)))
:
f.IsIntegral
def
PrimeSpectrum.primeSpectrum_unique_of_localization_at_minimal
{R : Type u}
[CommSemiring R]
{I : Ideal R}
[hI : I.IsPrime]
(h : I ∈ minimalPrimes R)
:
Localizations at minimal primes have single-point prime spectra.
Equations
- PrimeSpectrum.primeSpectrum_unique_of_localization_at_minimal h = { default := { asIdeal := IsLocalRing.maximalIdeal (Localization I.primeCompl), isPrime := ⋯ }, uniq := ⋯ }
Instances For
def
minimalPrimes.equivIrreducibleComponents
(R : Type u)
[CommSemiring R]
:
↑(minimalPrimes R) ≃o (↑(irreducibleComponents (PrimeSpectrum R)))ᵒᵈ
Stacks: Lemma 00ES (3)
Zero loci of minimal prime ideals of R are irreducible components in Spec R and any
irreducible component is a zero locus of some minimal prime ideal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
PrimeSpectrum.vanishingIdeal_mem_minimalPrimes
{R : Type u}
[CommSemiring R]
{s : Set (PrimeSpectrum R)}
:
theorem
PrimeSpectrum.zeroLocus_ideal_mem_irreducibleComponents
{R : Type u}
[CommSemiring R]
{I : Ideal R}
:
PrimeSpectrum.zeroLocus ↑I ∈ irreducibleComponents (PrimeSpectrum R) ↔ I.radical ∈ minimalPrimes R
The closed point in the prime spectrum of a local ring.
Equations
- IsLocalRing.closedPoint R = { asIdeal := IsLocalRing.maximalIdeal R, isPrime := ⋯ }
Instances For
theorem
IsLocalRing.isLocalHom_iff_comap_closedPoint
{R : Type u}
[CommSemiring R]
[IsLocalRing R]
{S : Type v}
[CommSemiring S]
[IsLocalRing S]
(f : R →+* S)
:
@[deprecated IsLocalRing.isLocalHom_iff_comap_closedPoint (since := "2024-10-10")]
theorem
IsLocalRing.isLocalRingHom_iff_comap_closedPoint
{R : Type u}
[CommSemiring R]
[IsLocalRing R]
{S : Type v}
[CommSemiring S]
[IsLocalRing S]
(f : R →+* S)
:
@[simp]
theorem
IsLocalRing.comap_closedPoint
{R : Type u}
[CommSemiring R]
[IsLocalRing R]
{S : Type v}
[CommSemiring S]
[IsLocalRing S]
(f : R →+* S)
[IsLocalHom f]
:
theorem
IsLocalRing.specializes_closedPoint
{R : Type u}
[CommSemiring R]
[IsLocalRing R]
(x : PrimeSpectrum R)
:
theorem
IsLocalRing.closedPoint_mem_iff
{R : Type u}
[CommSemiring R]
[IsLocalRing R]
(U : TopologicalSpace.Opens (PrimeSpectrum R))
:
IsLocalRing.closedPoint R ∈ U ↔ U = ⊤
theorem
IsLocalRing.closed_point_mem_iff
{R : Type u}
[CommSemiring R]
[IsLocalRing R]
{U : TopologicalSpace.Opens (PrimeSpectrum R)}
:
IsLocalRing.closedPoint R ∈ U ↔ U = ⊤
@[simp]
theorem
IsLocalRing.PrimeSpectrum.comap_residue
(T : Type u)
[CommRing T]
[IsLocalRing T]
(x : PrimeSpectrum (IsLocalRing.ResidueField T))
:
@[deprecated IsLocalRing.closedPoint (since := "2024-11-11")]
Alias of IsLocalRing.closedPoint.
The closed point in the prime spectrum of a local ring.
Instances For
@[deprecated IsLocalRing.isLocalHom_iff_comap_closedPoint (since := "2024-11-11")]
theorem
LocalRing.isLocalHom_iff_comap_closedPoint
{R : Type u}
[CommSemiring R]
[IsLocalRing R]
{S : Type v}
[CommSemiring S]
[IsLocalRing S]
(f : R →+* S)
:
@[deprecated IsLocalRing.comap_closedPoint (since := "2024-11-11")]
theorem
LocalRing.comap_closedPoint
{R : Type u}
[CommSemiring R]
[IsLocalRing R]
{S : Type v}
[CommSemiring S]
[IsLocalRing S]
(f : R →+* S)
[IsLocalHom f]
:
Alias of IsLocalRing.comap_closedPoint.
@[deprecated IsLocalRing.specializes_closedPoint (since := "2024-11-11")]
theorem
LocalRing.specializes_closedPoint
{R : Type u}
[CommSemiring R]
[IsLocalRing R]
(x : PrimeSpectrum R)
:
Alias of IsLocalRing.specializes_closedPoint.
@[deprecated IsLocalRing.closedPoint_mem_iff (since := "2024-11-11")]
theorem
LocalRing.closedPoint_mem_iff
{R : Type u}
[CommSemiring R]
[IsLocalRing R]
(U : TopologicalSpace.Opens (PrimeSpectrum R))
:
IsLocalRing.closedPoint R ∈ U ↔ U = ⊤
Alias of IsLocalRing.closedPoint_mem_iff.
@[deprecated IsLocalRing.closed_point_mem_iff (since := "2024-11-11")]
theorem
LocalRing.closed_point_mem_iff
{R : Type u}
[CommSemiring R]
[IsLocalRing R]
{U : TopologicalSpace.Opens (PrimeSpectrum R)}
:
IsLocalRing.closedPoint R ∈ U ↔ U = ⊤
Alias of IsLocalRing.closed_point_mem_iff.
@[deprecated IsLocalRing.PrimeSpectrum.comap_residue (since := "2024-11-11")]
theorem
LocalRing.PrimeSpectrum.comap_residue
(T : Type u)
[CommRing T]
[IsLocalRing T]
(x : PrimeSpectrum (IsLocalRing.ResidueField T))
:
Alias of IsLocalRing.PrimeSpectrum.comap_residue.
theorem
PrimeSpectrum.basicOpen_eq_zeroLocus_of_isIdempotentElem
{R : Type u}
[CommRing R]
(e : R)
(he : IsIdempotentElem e)
:
↑(PrimeSpectrum.basicOpen e) = PrimeSpectrum.zeroLocus {1 - e}
theorem
PrimeSpectrum.zeroLocus_eq_basicOpen_of_isIdempotentElem
{R : Type u}
[CommRing R]
(e : R)
(he : IsIdempotentElem e)
:
PrimeSpectrum.zeroLocus {e} = ↑(PrimeSpectrum.basicOpen (1 - e))
theorem
PrimeSpectrum.isClopen_iff
{R : Type u}
[CommRing R]
{s : Set (PrimeSpectrum R)}
:
IsClopen s ↔ ∃ (e : R), IsIdempotentElem e ∧ s = ↑(PrimeSpectrum.basicOpen e)
theorem
PrimeSpectrum.isClopen_iff_zeroLocus
{R : Type u}
[CommRing R]
{s : Set (PrimeSpectrum R)}
:
IsClopen s ↔ ∃ (e : R), IsIdempotentElem e ∧ s = PrimeSpectrum.zeroLocus {e}
def
PrimeSpectrum.isIdempotentElemEquivClopens
{R : Type u}
[CommRing R]
:
↑{e : R | IsIdempotentElem e} ≃ TopologicalSpace.Clopens (PrimeSpectrum R)
Clopen subsets in the prime spectrum of a commutative ring are in 1-1 correspondence with idempotent elements in the ring.
Equations
- PrimeSpectrum.isIdempotentElemEquivClopens = Equiv.ofBijective (fun (e : ↑{e : R | IsIdempotentElem e}) => { carrier := ↑(PrimeSpectrum.basicOpen ↑e), isClopen' := ⋯ }) ⋯
Instances For
theorem
PrimeSpectrum.basicOpen_isIdempotentElemEquivClopens_symm
{R : Type u}
[CommRing R]
(s : TopologicalSpace.Clopens (PrimeSpectrum R))
:
PrimeSpectrum.basicOpen ↑(PrimeSpectrum.isIdempotentElemEquivClopens.symm s) = s.toOpens
theorem
PrimeSpectrum.coe_isIdempotentElemEquivClopens_apply
{R : Type u}
[CommRing R]
(e : ↑{e : R | IsIdempotentElem e})
:
↑(PrimeSpectrum.isIdempotentElemEquivClopens e) = ↑(PrimeSpectrum.basicOpen ↑e)
theorem
PrimeSpectrum.isIdempotentElemEquivClopens_apply_toOpens
{R : Type u}
[CommRing R]
(e : ↑{e : R | IsIdempotentElem e})
:
(PrimeSpectrum.isIdempotentElemEquivClopens e).toOpens = PrimeSpectrum.basicOpen ↑e
theorem
PrimeSpectrum.isIdempotentElemEquivClopens_mul
{R : Type u}
[CommRing R]
(e₁ e₂ : ↑{e : R | IsIdempotentElem e})
:
theorem
PrimeSpectrum.isIdempotentElemEquivClopens_one_sub
{R : Type u}
[CommRing R]
(e : ↑{e : R | IsIdempotentElem e})
:
theorem
PrimeSpectrum.isIdempotentElemEquivClopens_symm_inf
{R : Type u}
[CommRing R]
(s₁ s₂ : TopologicalSpace.Clopens (PrimeSpectrum R))
:
PrimeSpectrum.isIdempotentElemEquivClopens.symm (s₁ ⊓ s₂) = ⟨↑(PrimeSpectrum.isIdempotentElemEquivClopens.symm s₁) * ↑(PrimeSpectrum.isIdempotentElemEquivClopens.symm s₂), ⋯⟩
theorem
PrimeSpectrum.isIdempotentElemEquivClopens_symm_compl
{R : Type u}
[CommRing R]
(s : TopologicalSpace.Clopens (PrimeSpectrum R))
:
PrimeSpectrum.isIdempotentElemEquivClopens.symm sᶜ = ⟨1 - ↑(PrimeSpectrum.isIdempotentElemEquivClopens.symm s), ⋯⟩
theorem
PrimeSpectrum.isIdempotentElemEquivClopens_symm_top
{R : Type u}
[CommRing R]
:
PrimeSpectrum.isIdempotentElemEquivClopens.symm ⊤ = ⟨1, ⋯⟩
theorem
PrimeSpectrum.isIdempotentElemEquivClopens_symm_bot
{R : Type u}
[CommRing R]
:
PrimeSpectrum.isIdempotentElemEquivClopens.symm ⊥ = ⟨0, ⋯⟩
theorem
PrimeSpectrum.isIdempotentElemEquivClopens_symm_sup
{R : Type u}
[CommRing R]
(s₁ s₂ : TopologicalSpace.Clopens (PrimeSpectrum R))
:
PrimeSpectrum.isIdempotentElemEquivClopens.symm (s₁ ⊔ s₂) = ⟨↑(PrimeSpectrum.isIdempotentElemEquivClopens.symm s₁) + ↑(PrimeSpectrum.isIdempotentElemEquivClopens.symm s₂) - ↑(PrimeSpectrum.isIdempotentElemEquivClopens.symm s₁) * ↑(PrimeSpectrum.isIdempotentElemEquivClopens.symm s₂),
⋯⟩