Theorems · Definition · algebraic geometry
PrimeSpectrum.comap
{R : Type u_1} →
{S : Type u_2} → [inst : CommSemiring R] → [inst_1 : CommSemiring S] → (R →+* S) → PrimeSpectrum S → PrimeSpectrum RThe pullback of an element of PrimeSpectrum S along a ring homomorphism f : R →+* S.
The bundled continuous version is PrimeSpectrum.comap.
- Cited by
- 199 results in Mathlib
- Foundations
- Depth 31 from the axioms, rests on 295 definitions · uses propext, Quot.sound
- Assumes
- CommSemiringCommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- RingHomstatement and proof · cited by 10,189
- PrimeSpectrumstatement and proof · cited by 625
- Ideal.comapproof · cited by 443
- PrimeSpectrum.asIdealproof · cited by 333
Cited by218
Results whose statement or proof uses this declaration.
- PrimeSpectrum.continuous_comapstatement and proof · cited by 19
- PrimeSpectrum.localization_away_comap_rangestatement · cited by 17
- AlgebraicGeometry.StructureSheaf.comapstatement and proof · cited by 15
- AlgebraicGeometry.Spec.topMapproof · cited by 13
- PrimeSpectrum.sigmaToPiproof · cited by 10
- range_comap_of_surjectivestatement and proof · cited by 9
- PrimeSpectrum.preimageEquivFiberstatement and proof · cited by 8
- PrimeSpectrum.primesOverOrderIsoFiberproof · cited by 8
- PrimeSpectrum.preimage_comap_zeroLocusstatement · cited by 7
- AlgebraicGeometry.Scheme.Hom.finrank_SpecMap_eq_finrankproof · cited by 6
- AlgebraicGeometry.Scheme.Hom.support_kerproof · cited by 6
- PrimeSpectrum.isClosed_image_of_stableUnderSpecializationstatement and proof · cited by 6
Showing the 200 most cited of 218.