Theorems · Definition · algebraic geometry
AlgebraicGeometry.Scheme.affineOpenCover
(X : AlgebraicGeometry.Scheme) → X.AffineOpenCover
A choice of an affine open cover of a scheme.
- Defined in
- Mathlib.AlgebraicGeometry.Cover.Open
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 142 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopCat.carrierproof · cited by 3,184
- AlgebraicGeometry.Schemestatement and proof · cited by 2,540
- AlgebraicGeometry.PresheafedSpace.carrierproof · cited by 2,020
- AlgebraicGeometry.SheafedSpace.toPresheafedSpaceproof · cited by 1,988
- AlgebraicGeometry.LocallyRingedSpace.toSheafedSpaceproof · cited by 1,892
- AlgebraicGeometry.Scheme.toLocallyRingedSpaceproof · cited by 1,734
- CategoryTheory.PreZeroHypercover.I₀proof · cited by 763
- CategoryTheory.PreZeroHypercover.fproof · cited by 542
- CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercoverproof · cited by 469
- AlgebraicGeometry.LocallyRingedSpace.toTopCatproof · cited by 128
- AlgebraicGeometry.Scheme.affineCoverproof · cited by 61
- AlgebraicGeometry.Scheme.AffineOpenCoverstatement · cited by 4
Cited by9
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.Hom.finrankproof · cited by 11
- AlgebraicGeometry.Scheme.Hom.finrank_comp_left_of_isIsoproof · cited by 7
- AlgebraicGeometry.Scheme.exists_Spec_apply_eqproof · cited by 4
- AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullbackproof · cited by 0
- AlgebraicGeometry.Scheme.affineOpenCover_I₀statement and proof · cited by 0
- AlgebraicGeometry.Scheme.affineOpenCover_Xstatement and proof · cited by 0
- AlgebraicGeometry.Scheme.affineOpenCover_fstatement and proof · cited by 0
- AlgebraicGeometry.Scheme.affineOpenCover_idxstatement and proof · cited by 0
- AlgebraicGeometry.Scheme.openCover_affineOpenCoverstatement · cited by 0