Theorems · Definition · algebraic geometry
AlgebraicGeometry.IsAffineOpen
{X : AlgebraicGeometry.Scheme} → X.Opens → PropAn open subset of a scheme is affine if the open subscheme is affine.
- Defined in
- Mathlib.AlgebraicGeometry.AffineScheme
- Cited by
- 222 results in Mathlib
- Foundations
- Depth 137 from the axioms, rests on 5,516 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 and proof · cited by 2,540
- AlgebraicGeometry.Scheme.Opensstatement and proof · cited by 1,149
- AlgebraicGeometry.Scheme.Opens.toSchemeproof · cited by 433
- AlgebraicGeometry.IsAffineproof · cited by 159
Cited by260
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.affineOpensproof · cited by 220
- AlgebraicGeometry.IsAffineOpen.fromSpecstatement and proof · cited by 65
- AlgebraicGeometry.IsAffineOpen.isoSpecstatement and proof · cited by 48
- AlgebraicGeometry.Scheme.AffineZariskiSiteproof · cited by 30
- AlgebraicGeometry.isAffineOpen_topstatement and proof · cited by 26
- AlgebraicGeometry.IsAffineOpen.basicOpenstatement and proof · cited by 19
- AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpenstatement and proof · cited by 18
- AlgebraicGeometry.IsAffineOpen.isCompactstatement and proof · cited by 17
- AlgebraicGeometry.IsAffineOpen.preimagestatement and proof · cited by 17
- AlgebraicGeometry.IsAffineOpen.primeIdealOfstatement and proof · cited by 15
- AlgebraicGeometry.isAffineOpen_opensRangestatement · cited by 13
- AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_selfstatement and proof · cited by 10
Showing the 200 most cited of 260.