5.1. Preliminaries about the étale topology
Before going to the pro-étale case, we recall a few preliminary results about
the étale site that we will need in the sequel. Let X be a scheme. By
\et{X} we denote the étale site of X and by \affet{X} the affine étale
site. \affet{X} consists of affine schemes étale over X.
Lemma5.1.1
Group: The pro-étale site of a scheme and its basic properties, including the comparison with étale cohomology, following Sections 4 and 5 of Bhatt–Scholze. (36)
- Definition 5.2.1
- Lemma 5.2.2
- Lemma 5.2.3
- Lemma 5.2.4
- Definition 5.3.1
- Lemma 5.3.2
- Definition 5.3.3
- Definition 5.3.4
- Theorem 5.3.5
- Proposition 5.3.6
- Definition 5.3.7
- Proposition 5.3.8
- Definition 5.3.1.1
- Lemma 5.3.1.2
- Definition 5.3.1.3
- Proposition 5.3.1.4
- Corollary 5.3.1.5
- Corollary 5.3.1.6
- Proposition 5.3.1.7
- Proposition 5.3.2.1
- Corollary 5.3.2.2
- Definition 5.4.1
- Lemma 5.4.2
- Lemma 5.4.3
- Lemma 5.4.4
- Proposition 5.4.5
- Corollary 5.4.6
- Corollary 5.4.7
- Corollary 5.4.8
- Definition 5.4.9
- Corollary 5.4.10
- Lemma 5.4.11
- Proposition 5.4.12
- Corollary 5.4.13
- Definition 5.4.14
- Theorem 5.4.15
Lean status
- No associated Lean code or declarations.
The inclusion functor \affet{X} \to \et{X} is cover dense, i.e. for every
Y in \et{X} there exists a cover \{U_i \to Y\} with U_i in
\affet{X}.
Proof for Lemma 5.1.1
uses 0
This is immediate, because open immersions are étale and étale is stable under composition.