Theorems · Definition · algebraic geometry
AlgebraicGeometry.Scheme.OpenCover
AlgebraicGeometry.Scheme → Type (max (v + 1) (u + 1))
An open cover of a scheme X is a cover where all component maps are open immersions.
- Defined in
- Mathlib.AlgebraicGeometry.Cover.Open
- Cited by
- 207 results in Mathlib
- Foundations
- Depth 105 from the axioms, rests on 1,370 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.IsOpenImmersionproof · cited by 476
- AlgebraicGeometry.Scheme.precoverageproof · cited by 336
- AlgebraicGeometry.Scheme.Coverproof · cited by 88
Cited by295
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.affineCoverstatement · cited by 61
- AlgebraicGeometry.Scheme.Pullback.vstatement and proof · cited by 34
- AlgebraicGeometry.Scheme.Pullback.gluingstatement and proof · cited by 30
- AlgebraicGeometry.Scheme.Cover.ColimitGluingDatastatement · cited by 26
- AlgebraicGeometry.Scheme.Pullback.fVstatement and proof · cited by 21
- AlgebraicGeometry.Scheme.Pullback.t'statement and proof · cited by 20
- AlgebraicGeometry.Scheme.Cover.hom_extstatement and proof · cited by 18
- AlgebraicGeometry.Scheme.Pullback.p1statement and proof · cited by 18
- AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functorstatement and proof · cited by 18
- AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCoverstatement and proof · cited by 18
- AlgebraicGeometry.Scheme.AffineOpenCover.openCoverstatement · cited by 17
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.coconestatement and proof · cited by 16
Showing the 200 most cited of 295.