Theorems · Definition · algebraic geometry
AlgebraicGeometry.Spec.map
{R S : CommRingCat} → (R ⟶ S) → (AlgebraicGeometry.Spec S ⟶ AlgebraicGeometry.Spec R)The induced map of a ring homomorphism on the ring spectra, as a morphism of schemes.
- Defined in
- Mathlib.AlgebraicGeometry.Scheme
- Cited by
- 332 results in Mathlib
- Foundations
- Depth 129 from the axioms, rests on 5,165 definitions · uses propext, Classical.choice, Quot.sound
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.
- Quiver.Homstatement and proof · cited by 32,603
- AlgebraicGeometry.Schemestatement · cited by 2,540
- CommRingCatstatement and proof · cited by 2,333
- AlgebraicGeometry.Specstatement · cited by 626
- AlgebraicGeometry.Spec.locallyRingedSpaceMapproof · cited by 7
Cited by376
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.Specproof · cited by 57
- AlgebraicGeometry.Scheme.fromSpecResidueFieldproof · cited by 47
- AlgebraicGeometry.Scheme.Opens.toSpecΓproof · cited by 39
- AlgebraicGeometry.Spec.map_compstatement · cited by 33
- AlgebraicGeometry.Scheme.Hom.toNormalizationproof · cited by 28
- AlgebraicGeometry.pullbackSpecIsostatement · cited by 26
- AlgebraicGeometry.Spec.map_surjectivestatement · cited by 25
- AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjιproof · cited by 20
- AlgebraicGeometry.HasRingHomProperty.Spec_iffstatement and proof · cited by 19
- AlgebraicGeometry.IsAffineOpen.basicOpenproof · cited by 19
- AlgebraicGeometry.Spec.map_idstatement · cited by 18
- AlgebraicGeometry.Spec.map_comp_assocstatement and proof · cited by 14
Showing the 200 most cited of 376.