Theorems · Theorem · algebraic geometry
PrimeSpectrum.preimage_comap_zeroLocus
∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S) (s : Set R),
PrimeSpectrum.comap f ⁻¹' PrimeSpectrum.zeroLocus s = PrimeSpectrum.zeroLocus (⇑f '' s)- Cited by
- 7 results in Mathlib
- Foundations
- Depth 33 from the axioms · uses propext, Quot.sound
- Assumes
- CommSemiringCommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Setstatement and proof · cited by 53,352
- CommSemiringstatement and proof · cited by 10,911
- RingHomstatement and proof · cited by 10,189
- Set.imagestatement · cited by 5,609
- Set.preimagestatement · cited by 4,946
- PrimeSpectrumstatement · cited by 625
- PrimeSpectrum.comapstatement · cited by 199
- PrimeSpectrum.zeroLocusstatement · cited by 164
- PrimeSpectrum.preimage_comap_zeroLocus_auxproof · cited by 2
Cited by7
Results whose statement or proof uses this declaration.
- PrimeSpectrum.comap_isInducing_of_surjectiveproof · cited by 2
- PrimeSpectrum.closure_image_comap_zeroLocusproof · cited by 1
- AlgebraicGeometry.eq_top_of_sigmaSpec_subset_of_isCompactproof · cited by 1
- PrimeSpectrum.BasicConstructibleSetData.toSet_mapproof · cited by 1
- PrimeSpectrum.localization_comap_isInducingproof · cited by 1
- Localization.exists_finite_awayMapₐ_of_surjective_awayMapₐproof · cited by 1
- chevalley_mvPolynomial_mvPolynomialproof · cited by 0