Theorems · Definition · algebraic geometry
AlgebraicGeometry.Scheme.overPretopology
(P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) →
(S : AlgebraicGeometry.Scheme) →
[P.IsStableUnderBaseChange] →
[P.IsMultiplicative] → [P.RespectsIso] → CategoryTheory.Pretopology (CategoryTheory.Over S)The pretopology on Over S induced by P where coverings are given by P-covers
of S-schemes.
- Defined in
- Mathlib.AlgebraicGeometry.Sites.Small
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 197 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.ofPredproof · cited by 6,101
- AlgebraicGeometry.Schemestatement and proof · cited by 2,540
- CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
- CategoryTheory.Overstatement and proof · cited by 935
- CategoryTheory.Over.leftproof · cited by 541
- CategoryTheory.Presieveproof · cited by 449
- AlgebraicGeometry.Scheme.precoverageproof · cited by 336
- CategoryTheory.MorphismProperty.IsMultiplicativestatement and proof · cited by 332
- CategoryTheory.MorphismProperty.RespectsIsostatement and proof · cited by 248
- CategoryTheory.MorphismProperty.IsStableUnderBaseChangestatement and proof · cited by 131
- AlgebraicGeometry.Scheme.Coverproof · cited by 88
- CategoryTheory.Pretopologystatement · cited by 32
Cited by2
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.mem_overGrothendieckTopologyproof · cited by 1
- AlgebraicGeometry.Scheme.overGrothendieckTopology_eq_toGrothendieck_overPretopologystatement and proof · cited by 1