Theorems · Definition · algebraic geometry
AlgebraicGeometry.Spec
CommRingCat → AlgebraicGeometry.Scheme
The spectrum of a commutative ring, as a scheme.
- Defined in
- Mathlib.AlgebraicGeometry.Scheme
- Cited by
- 626 results in Mathlib
- Foundations
- Depth 128 from the axioms, rests on 5,159 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AlgebraicGeometry.Schemestatement · cited by 2,540
- CommRingCatstatement and proof · cited by 2,333
- AlgebraicGeometry.LocallyRingedSpaceproof · cited by 205
- AlgebraicGeometry.Spec.locallyRingedSpaceObjproof · cited by 57
Cited by758
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Spec.mapstatement · cited by 332
- AlgebraicGeometry.Scheme.ΓSpecIsostatement · cited by 106
- AlgebraicGeometry.IsAffineOpen.fromSpecstatement · cited by 65
- AlgebraicGeometry.Scheme.affineCoverproof · cited by 61
- AlgebraicGeometry.Scheme.toSpecΓstatement · cited by 59
- AlgebraicGeometry.Scheme.Specproof · cited by 57
- AlgebraicGeometry.Scheme.isoSpecstatement · cited by 56
- AlgebraicGeometry.AffineSpaceproof · cited by 51
- AlgebraicGeometry.IsAffineOpen.isoSpecstatement · cited by 48
- AlgebraicGeometry.Scheme.fromSpecResidueFieldstatement · cited by 47
- AlgebraicGeometry.Scheme.fromSpecStalkstatement · cited by 43
- AlgebraicGeometry.Scheme.Opens.toSpecΓstatement · cited by 39
Showing the 200 most cited of 758.