Theorems · Definition · algebraic geometry
AlgebraicGeometry.Scheme.ProEt
AlgebraicGeometry.Scheme → Type (u + 1)
The (small) pro-étale site of a scheme S: Its objects are the schemes weakly étale over S.
We prefer to work with weakly étale morphisms instead of pro-étale morphisms, since the property
of being pro-étale is not well-behaved: it is not local on the target.
[Definition 4.1.1][proetale2015]
- Defined in
- Mathlib.AlgebraicGeometry.Sites.Proetale
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 100 from the axioms · 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.
- Top.topproof · cited by 9,680
- AlgebraicGeometry.Schemestatement and proof · cited by 2,540
- CategoryTheory.MorphismProperty.Overproof · cited by 94
- AlgebraicGeometry.WeaklyEtaleproof · cited by 14
Cited by13
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.ProEt.topologystatement · cited by 4
- AlgebraicGeometry.Scheme.ProEt.mkstatement · cited by 3
- AlgebraicGeometry.Scheme.ProEt.forgetstatement · cited by 3
- AlgebraicGeometry.Scheme.ProEt.precoveragestatement · cited by 1
- AlgebraicGeometry.Scheme.ellAdicSheafstatement · cited by 1
- AlgebraicGeometry.Scheme.ProEt.topology_eq_top_of_isEmptystatement and proof · cited by 1
- AlgebraicGeometry.Scheme.ProEt.bot_mem_topologystatement and proof · cited by 1
- AlgebraicGeometry.Scheme.ProEt.forget_mapstatement · cited by 0
- AlgebraicGeometry.Scheme.ProEt.forget_objstatement · cited by 0
- AlgebraicGeometry.Scheme.isZero_ellAdicSheaf_of_isEmptystatement · cited by 0
- AlgebraicGeometry.Scheme.ProEt.topology_eq_inducedTopologystatement · cited by 0
- AlgebraicGeometry.Scheme.ProEt.equivOfIsEmptystatement · cited by 0