5.3. The site
Before we define the pro-étale site, we recall a few standard definitions.
- Lemma 5.1.1
- Definition 5.2.1
- Lemma 5.2.2
- Lemma 5.2.3
- Lemma 5.2.4
- 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
- No associated Lean code or declarations.
A jointly surjective family (f_i \colon Y_i \to X)_{i \in I} of morphisms of
schemes is quasi-compact if for every affine open U of X there exist
quasi-compact opens V_i in Y_i such that
U = \bigcup_{i \in I} f_i(V_i).
- Lemma 5.1.1
- Definition 5.2.1
- Lemma 5.2.2
- Lemma 5.2.3
- Lemma 5.2.4
- Definition 5.3.1
- 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
Let (f_i \colon Y_i \to X)_{i \in I} be a jointly-surjective family of
morphisms of schemes. If f_i is flat and locally of finite presentation for
every i \in I, the family is quasi-compact.
Lean code for Lemma5.3.2●1 theorem
Associated Lean declarations
-
theoremdefined in Proetale/Mathlib/AlgebraicGeometry/Cover/QuasiCompact.leancomplete
theorem AlgebraicGeometry.QuasiCompactCover.of_flat_locallyOfFinitePresentation.{u, u_1} {S : AlgebraicGeometry.Scheme} {K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover K S) [AlgebraicGeometry.Scheme.JointlySurjective K] [∀ (i : 𝒰.I₀), AlgebraicGeometry.Flat (𝒰.f i)] [∀ (i : 𝒰.I₀), AlgebraicGeometry.LocallyOfFinitePresentation (𝒰.f i)] : AlgebraicGeometry.QuasiCompactCover 𝒰.toPreZeroHypercover
theorem AlgebraicGeometry.QuasiCompactCover.of_flat_locallyOfFinitePresentation.{u, u_1} {S : AlgebraicGeometry.Scheme} {K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover K S) [AlgebraicGeometry.Scheme.JointlySurjective K] [∀ (i : 𝒰.I₀), AlgebraicGeometry.Flat (𝒰.f i)] [∀ (i : 𝒰.I₀), AlgebraicGeometry.LocallyOfFinitePresentation (𝒰.f i)] : AlgebraicGeometry.QuasiCompactCover 𝒰.toPreZeroHypercover
A jointly surjective family of flat morphisms locally of finite presentation is quasi-compact.
In this case, every f_i is an open map, from which the claim easily follows.
- Lemma 5.1.1
- 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.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
- No associated Lean code or declarations.
Let \mathcal{P} be a morphism property of schemes and X be a scheme. The
small \mathcal{P}-site of X is the category of X-schemes with
structure morphism satisfying \mathcal{P} and with covers given by
quasi-compact, jointly surjective families of morphisms satisfying
\mathcal{P}.
If we let \mathcal{P} be flat morphisms of schemes, we obtain the fpqc site:
- Lemma 5.1.1
- 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
- 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
- No associated Lean code or declarations.
Let X be a scheme. The fpqc site of X, denoted by \fpqc{X}, is the
\mathcal{P}-site of X with \mathcal{P} = \text{flat}.
For us, the main relevant property of the fpqc site is that it is subcanonical:
- Lemma 5.1.1
- 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
- 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
- No associated Lean code or declarations.
The fpqc site is subcanonical, i.e., every representable presheaf is a sheaf.
Analogous to the familiar criterion for fpqc sheaves, we have a generalization
for the small \mathcal{P}-site of a scheme.
- Lemma 5.1.1
- 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
- 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
- No associated Lean code or declarations.
Let F be a presheaf on the small \mathcal{P}-site. Then F is a sheaf
if and only if it is a sheaf in the Zariski topology and satisfies the sheaf
property for \{V \to U\} with V, U affine and V \to U satisfying
\mathcal{P}.
We can now define the main object of this chapter:
- Lemma 5.1.1
- 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
- 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
- No associated Lean code or declarations.
Let X be a scheme. The pro-étale site of X, denoted by \proet{X},
is the \mathcal{P}-site of X with
\mathcal{P} = \text{weakly étale}.
(Bhatt–Scholze, Definition 4.1.1)
Despite the name pro-étale, Definition 5.3.7 does not mention pro-étale morphisms. The name is justified by Theorem 2.6.1 (see also Proposition 5.3.1.4).
- Lemma 5.1.1
- 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
- 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
- No associated Lean code or declarations.
The site \proet{X} is subcanonical.
(Bhatt–Scholze, Lemma 4.2.4)
Follows from Theorem 5.3.5, since every pro-étale sheaf is an fpqc-sheaf.
5.3.1. Affine covers
- Lemma 5.1.1
- 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
- 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
-
AlgebraicGeometry.Scheme.AffineProEt[complete]
An object U of \proet{X} is called a pro-étale affine if it can be
written as U = \lim U_i over a small cofiltered diagram i \mapsto U_i of
affine schemes étale over X. The subcategory of pro-étale affines in
\proet{X} is denoted by \affproet{X}.
(Bhatt–Scholze, Definition 4.2.1)
Lean code for Definition5.3.1.1●1 definition
Associated Lean declarations
-
AlgebraicGeometry.Scheme.AffineProEt[complete]
-
AlgebraicGeometry.Scheme.AffineProEt[complete]
-
defdefined in Proetale/Topology/Comparison/Affine.leancomplete
def AlgebraicGeometry.Scheme.AffineProEt.{u} (S : AlgebraicGeometry.Scheme) : Type (u + 1)
def AlgebraicGeometry.Scheme.AffineProEt.{u} (S : AlgebraicGeometry.Scheme) : Type (u + 1)
The pro-étale affine site is the full subcategory of the pro-étale site where every object can be written as a cofiltered limit of affine étale schemes over `S`.
- Lemma 5.1.1
- 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
- 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
- No associated Lean code or declarations.
The category \affproet{X} admits limits indexed by a connected diagram and
the forgetful functor to \mathrm{Sch} / X preserves them. If X is affine,
\affproet{X} has all small limits.
(Bhatt–Scholze, Remark 4.2.3)
- Lemma 5.1.1
- 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
- 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
-
AlgebraicGeometry.Scheme.AffineProEt[complete]
Let X be affine. The affine pro-étale site of X is the category
\affproet{X}. The covering families are the quasi-compact covers.
Lean code for Definition5.3.1.3●1 definition
Associated Lean declarations
-
AlgebraicGeometry.Scheme.AffineProEt[complete]
-
AlgebraicGeometry.Scheme.AffineProEt[complete]
-
defdefined in Proetale/Topology/Comparison/Affine.leancomplete
def AlgebraicGeometry.Scheme.AffineProEt.{u} (S : AlgebraicGeometry.Scheme) : Type (u + 1)
def AlgebraicGeometry.Scheme.AffineProEt.{u} (S : AlgebraicGeometry.Scheme) : Type (u + 1)
The pro-étale affine site is the full subcategory of the pro-étale site where every object can be written as a cofiltered limit of affine étale schemes over `S`.
In other words, \affproet{X} carries the topology induced by the inclusion
functor \affproet{X} \to \proet{X}. Although the objects of \proet{X} are
weakly étale X-schemes, by Theorem 2.6.1 the
topology of \proet{X} is still generated by objects in \affproet{X}:
- Lemma 5.1.1
- 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
- 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
The inclusion \affproet{X} \to \proet{X} is cover dense, i.e. for every
object Y of \proet{X}, there exists a cover \{U_i \to Y\}_{i \in I}
with U_i in \affproet{X}.
(Bhatt–Scholze, Lemma 4.2.4)
Lean code for Proposition5.3.1.4●1 theorem
Associated Lean declarations
-
theoremdefined in Proetale/Topology/Comparison/Affine.leancomplete
theorem AlgebraicGeometry.Scheme.AffineProEt.isCoverDense_toProEt.{u} {S : AlgebraicGeometry.Scheme} : (AlgebraicGeometry.Scheme.AffineProEt.toProEt S).IsCoverDense (AlgebraicGeometry.Scheme.ProEt.topology S)
theorem AlgebraicGeometry.Scheme.AffineProEt.isCoverDense_toProEt.{u} {S : AlgebraicGeometry.Scheme} : (AlgebraicGeometry.Scheme.AffineProEt.toProEt S).IsCoverDense (AlgebraicGeometry.Scheme.ProEt.topology S)
The affine pro-étale site embeds densely in the pro-étale site. The key ingredient of the proof is the commutative algebra lemma `RingHom.WeaklyEtale.exists_indEtale_comp`.
Let f\colon Y \to X be a weakly étale morphism and let \{U_i \to X\} be
an affine open cover of X. If we prove the lemma for each U_i and the
weakly étale morphism f^{-1}(U_i) \to U_i, the lemma follows for f by
taking the joint cover. Thus we may assume that X = \spec{A} is affine.
Now let \{U_i \to Y\} be an affine open cover. Again, if we prove the lemma
for each U_i and the composition U_i \to Y \to X, the claim follows by
joining the covers. Hence we may assume that Y = \spec{B} is affine.
We now have A \to B weakly étale, so by
Theorem 2.6.1 there exists an ind-étale and faithfully
flat B \to B' such that A \to B \to B' is ind-étale. The cover
\{ \spec{B'} \to \spec{B} \} concludes the proof.
- Lemma 5.1.1
- 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.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
Restriction along the inclusion \affproet{X} \to \proet{X} induces an
equivalence of categories \shv{\proet{X}} \to \shv{\affproet{X}}.
Lean code for Corollary5.3.1.5●1 theorem
Associated Lean declarations
-
theoremdefined in Proetale/Topology/Comparison/Affine.leancomplete
theorem AlgebraicGeometry.Scheme.AffineProEt.isEquivalence_sheafPushforwardContinuous_toProEt.{u, v_1, u_2} (S : AlgebraicGeometry.Scheme) {A : Type u_2} [CategoryTheory.Category.{v_1, u_2} A] [CategoryTheory.Limits.HasLimitsOfSize.{u, u + 1, v_1, u_2} A] : ((AlgebraicGeometry.Scheme.AffineProEt.toProEt S).sheafPushforwardContinuous A (AlgebraicGeometry.Scheme.AffineProEt.topology S) (AlgebraicGeometry.Scheme.ProEt.topology S)).IsEquivalence
theorem AlgebraicGeometry.Scheme.AffineProEt.isEquivalence_sheafPushforwardContinuous_toProEt.{u, v_1, u_2} (S : AlgebraicGeometry.Scheme) {A : Type u_2} [CategoryTheory.Category.{v_1, u_2} A] [CategoryTheory.Limits.HasLimitsOfSize.{u, u + 1, v_1, u_2} A] : ((AlgebraicGeometry.Scheme.AffineProEt.toProEt S).sheafPushforwardContinuous A (AlgebraicGeometry.Scheme.AffineProEt.topology S) (AlgebraicGeometry.Scheme.ProEt.topology S)).IsEquivalence
Restriction along inclusion of the affine pro-étale site into the pro-étale site induces an equivalence of categories of sheaves of `Ab.{u + 1}`, or more generally any category having large enough limits.
The functor \affproet{X} \to \proet{X} is fully faithful and makes
\affproet{X} a dense subsite of \proet{X} by
Proposition 5.3.1.4. Thus the claim follows from the
comparison lemma for sites.
- Lemma 5.1.1
- 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
- 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
- No associated Lean code or declarations.
Restriction along the inclusion \affproet{X} \to \proet{X} commutes with
sheafification.
This follows immediately from Corollary 5.3.1.5.
We can also compare \affproet{X} to \affet{X}.
- Lemma 5.1.1
- 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.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
- No associated Lean code or declarations.
The canonical functor \affet{X} \to \affproet{X} induces an equivalence of
categories \pro{\affet{X}} \to \affproet{X}.
By Proposition 4.4, it suffices to show that for every U in
\affet{X}, the image of U in \affproet{X} is co-finitely-presentable.
This follows from the fact that étale morphisms are finitely presented.
5.3.2. Repleteness
An important property of the pro-étale site is the following:
- Lemma 5.1.1
- 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
- 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
- No associated Lean code or declarations.
The category of sheaves on \proet{X} has enough weakly contractible
objects.
(Bhatt–Scholze, Proposition 4.2.8)
TBA.
- Lemma 5.1.1
- 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
- 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
- No associated Lean code or declarations.
The category of sheaves on \proet{X} is replete.