5.4. Comparison with étale cohomology
Let X be a scheme. Since an étale map is also weakly étale by
Lemma 5.2.3 we may define:
- 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
- Corollary 5.3.2.2
- 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.toProEtale[complete]
We denote by \nu = \nu_X the morphism of sites \proet{X} \to \et{X}
induced by the functor from \et{X} to \proet{X} given by
(U \to X) \mapsto (U \to X).
Lean code for Definition5.4.1●1 definition
Associated Lean declarations
-
AlgebraicGeometry.Scheme.toProEtale[complete]
-
AlgebraicGeometry.Scheme.toProEtale[complete]
-
defdefined in Definitions.leancomplete
def AlgebraicGeometry.Scheme.toProEtale.{u} (S : AlgebraicGeometry.Scheme) : CategoryTheory.Functor S.Etale S.ProEt
def AlgebraicGeometry.Scheme.toProEtale.{u} (S : AlgebraicGeometry.Scheme) : CategoryTheory.Functor S.Etale S.ProEt
The inclusion of the étale site into the pro-étale 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
- 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.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 morphism of sites \nu is continuous.
Lean code for Lemma5.4.2●1 theorem
Associated Lean declarations
-
theoremdefined in Definitions.leancomplete
theorem AlgebraicGeometry.Scheme.isContinuous_toProEtale.{u} (S : AlgebraicGeometry.Scheme) : S.toProEtale.IsContinuous S.smallEtaleTopology (AlgebraicGeometry.Scheme.ProEt.topology S)
theorem AlgebraicGeometry.Scheme.isContinuous_toProEtale.{u} (S : AlgebraicGeometry.Scheme) : S.toProEtale.IsContinuous S.smallEtaleTopology (AlgebraicGeometry.Scheme.ProEt.topology S)
The inclusion of the étale site into the pro-étale site is continuous.
This follows from the definitions, because every étale covering is a quasi-compact covering by Lemma 5.3.2.
We denote by \nu_{p}\colon \preshv{\proet{X}} \to \preshv{\et{X}} and
\nu^{p}\colon \preshv{\et{X}} \to \preshv{\proet{X}} the pushforward and
pullback functors on the level of presheaves.
- 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
- Corollary 5.3.2.2
- Definition 5.4.1
- Lemma 5.4.2
- 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 be a presheaf on \et{X}. Then (\nu^p F)|_{\affproet{X}}
preserves filtered colimits.
Lean code for Lemma5.4.3●1 theorem, incomplete
Associated Lean declarations
-
theoremdefined in Proetale/Topology/Comparison/Affine.leancontains sorry
theorem AlgebraicGeometry.Scheme.ProEt.preservesFilteredColimitsOfSize_lan_toProEtale.{u} (S : AlgebraicGeometry.Scheme) (F : CategoryTheory.Functor S.Etaleᵒᵖ Ab) : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u + 1, u + 1, u + 2} ((AlgebraicGeometry.Scheme.AffineProEt.toProEt S).op.comp (S.toProEtale.op.lan.obj F))
theorem AlgebraicGeometry.Scheme.ProEt.preservesFilteredColimitsOfSize_lan_toProEtale.{u} (S : AlgebraicGeometry.Scheme) (F : CategoryTheory.Functor S.Etaleᵒᵖ Ab) : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u + 1, u + 1, u + 2} ((AlgebraicGeometry.Scheme.AffineProEt.toProEt S).op.comp (S.toProEtale.op.lan.obj F))
Let U = \lim_{\lambda} U_{\lambda} be a cofiltered limit. By definition of
\affproet{X} and because pro-pro-étale is pro-étale, we may assume that the
U_{\lambda} are étale over X. Then
(\nu^p F)|_{\affproet{X}}(\lim U_{\lambda}) = \colim_{\mu} F(V_{\mu}),
where the V_{\mu} run over factorisations
U = \lim U_{\lambda} \to V_{\mu} \to X where V_{\mu} \to X is étale.
Since the U_{\lambda} are locally of finite presentation over X, they
are finitely presented in the categorical sense. Hence, for every such
factorisation there exists a \lambda such that
U = \lim U_{\lambda} \to V_{\mu} factors via U_{\lambda}. This shows
that the U_{\lambda} lie cofinal in all V_{\mu}, so we obtain
\colim_{\mu} F(V_{\mu}) = \colim_{\lambda} F(U_{\lambda}) = \colim_{\lambda} (\nu^p F)|_{\affproet{X}}(U_{\lambda}).
- 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
- Corollary 5.3.2.2
- Definition 5.4.1
- Lemma 5.4.2
- Lemma 5.4.3
- 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 topology on \affproet{X} is generated by relatively pro-representable
one-hypercovers with respect to the inclusion \affet{X} \to \affproet{X}.
The topology on \affproet{X} is generated by surjections V \to U in
\affproet{X} and finite standard Zariski coverings. Both of these can be
relatively pro-represented by Proposition 4.2 (see also
Lemma 4.3).
Further denote by \nu_{*} \colon \shv{\proet{X}} \to \shv{\et{X}} and
\nu^* \colon \shv{\et{X}} \to \shv{\proet{X}} the corresponding pushforward
and pullback functors. Since \nu^* is exact, we have R \nu^* = \nu^* by
abuse of notation and we simply write \nu^* everywhere. In contrast to
Bhatt–Scholze, we write R \nu_{*} for the derived functor of \nu_{*}.
- 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
- Corollary 5.3.2.2
- Definition 5.4.1
- Lemma 5.4.2
- Lemma 5.4.3
- Lemma 5.4.4
- 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 be a sheaf on \et{X}. Then (\nu^p F)|_{\affproet{X}} is a
sheaf. In particular,
(\nu^*F)|_{\affproet{X}} \cong (\nu^p F)|_{\affproet{X}}.
Lean code for Proposition5.4.5●2 declarations
Associated Lean declarations
-
theoremdefined in Proetale/Topology/Comparison/Affine.leancomplete
theorem AlgebraicGeometry.Scheme.isSheaf_lan_toProEtale.{u} (S : AlgebraicGeometry.Scheme) (F : CategoryTheory.Functor S.Etaleᵒᵖ Ab) (hF : CategoryTheory.Presheaf.IsSheaf S.smallEtaleTopology F) : CategoryTheory.Presheaf.IsSheaf (AlgebraicGeometry.Scheme.AffineProEt.topology S) ((AlgebraicGeometry.Scheme.AffineProEt.toProEt S).op.comp (S.toProEtale.op.lan.obj F))
theorem AlgebraicGeometry.Scheme.isSheaf_lan_toProEtale.{u} (S : AlgebraicGeometry.Scheme) (F : CategoryTheory.Functor S.Etaleᵒᵖ Ab) (hF : CategoryTheory.Presheaf.IsSheaf S.smallEtaleTopology F) : CategoryTheory.Presheaf.IsSheaf (AlgebraicGeometry.Scheme.AffineProEt.topology S) ((AlgebraicGeometry.Scheme.AffineProEt.toProEt S).op.comp (S.toProEtale.op.lan.obj F))
If `F` is a sheaf on the small étale site, the presheaf pullback of `F` to the small pro-étale site (i.e., the left Kan extension) is a sheaf when restricted to the small affine pro-étale site.
-
defdefined in Proetale/Topology/Comparison/Affine.leancomplete
def AlgebraicGeometry.Scheme.ProEt.sheafPullbackCompIso.{u} (S : AlgebraicGeometry.Scheme) : (AlgebraicGeometry.Scheme.ProEt.sheafPullback S Ab).comp (((AlgebraicGeometry.Scheme.AffineProEt.toProEt S).sheafPushforwardContinuous Ab (AlgebraicGeometry.Scheme.AffineProEt.topology S) (AlgebraicGeometry.Scheme.ProEt.topology S)).comp (CategoryTheory.sheafToPresheaf (AlgebraicGeometry.Scheme.AffineProEt.topology S) Ab)) ≅ (CategoryTheory.sheafToPresheaf S.smallEtaleTopology Ab).comp (S.toProEtale.op.lan.comp ((CategoryTheory.Functor.whiskeringLeft S.AffineProEtᵒᵖ S.ProEtᵒᵖ Ab).obj (AlgebraicGeometry.Scheme.AffineProEt.toProEt S).op))
def AlgebraicGeometry.Scheme.ProEt.sheafPullbackCompIso.{u} (S : AlgebraicGeometry.Scheme) : (AlgebraicGeometry.Scheme.ProEt.sheafPullback S Ab).comp (((AlgebraicGeometry.Scheme.AffineProEt.toProEt S).sheafPushforwardContinuous Ab (AlgebraicGeometry.Scheme.AffineProEt.topology S) (AlgebraicGeometry.Scheme.ProEt.topology S)).comp (CategoryTheory.sheafToPresheaf (AlgebraicGeometry.Scheme.AffineProEt.topology S) Ab)) ≅ (CategoryTheory.sheafToPresheaf S.smallEtaleTopology Ab).comp (S.toProEtale.op.lan.comp ((CategoryTheory.Functor.whiskeringLeft S.AffineProEtᵒᵖ S.ProEtᵒᵖ Ab).obj (AlgebraicGeometry.Scheme.AffineProEt.toProEt S).op))
The pullback of an étale sheaf `F` to the pro-étale site is isomorphic to the presheaf-pullback of `F` (i.e., left Kan extension) after restricting to the affine pro-étale site.
By Lemma 5.4.4 and
Lemma 5.4.3, this follows
from Proposition 4.2.3. Hence we have
the following chain of isomorphisms
(\nu^*F)|_{\affproet{X}} \cong (\nu^pF)^{\#}|_{\affproet{X}} \cong ((\nu^pF)|_{\affproet{X}})^{\#} \cong (\nu^pF)|_{\affproet{X}}.
The second isomorphism is Corollary 5.3.1.6 and
the last is the first part of this proposition.
- 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
- 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.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 sheaf on \et{X} and U = \lim_i U_i in \affproet{X}.
Then \nu^*F(U) = \colim_i F(U_i).
(Bhatt–Scholze, Lemma 5.1.1)
By Proposition 5.4.5 we have
(\nu^*F)|_{\affproet{X}} \cong (\nu^p F)|_{\affproet{X}}. The claim now
follows from Lemma 5.4.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
- 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.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
For any F \in \shv{\et{X}}, the unit F \to \nu_{*} \nu^{*} F is an
isomorphism.
Lean code for Corollary5.4.7●1 theorem
Associated Lean declarations
-
theoremdefined in Proetale/Topology/Comparison/Affine.leancomplete
theorem AlgebraicGeometry.Scheme.ProEt.isIso_unit_sheafAdjunction.{u} (S : AlgebraicGeometry.Scheme) : CategoryTheory.IsIso (AlgebraicGeometry.Scheme.ProEt.sheafAdjunction S Ab).unit
theorem AlgebraicGeometry.Scheme.ProEt.isIso_unit_sheafAdjunction.{u} (S : AlgebraicGeometry.Scheme) : CategoryTheory.IsIso (AlgebraicGeometry.Scheme.ProEt.sheafAdjunction S Ab).unit
By Lemma 5.1.1, we may check this on any affine U étale
over X. Since U = \lim U, the formula of
Corollary 5.4.6 shows the desired isomorphism.
- 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
- 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
- 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
\nu^* is fully faithful.
(Bhatt–Scholze, Lemma 5.1.2, fully faithful part)
Lean code for Corollary5.4.8●2 theorems
Associated Lean declarations
-
theoremdefined in Proetale/Topology/Comparison/Affine.leancomplete
theorem AlgebraicGeometry.Scheme.ProEt.faithful_sheafPullback.{u} (S : AlgebraicGeometry.Scheme) : (AlgebraicGeometry.Scheme.ProEt.sheafPullback S Ab).Faithful
theorem AlgebraicGeometry.Scheme.ProEt.faithful_sheafPullback.{u} (S : AlgebraicGeometry.Scheme) : (AlgebraicGeometry.Scheme.ProEt.sheafPullback S Ab).Faithful
-
theoremdefined in Proetale/Topology/Comparison/Affine.leancomplete
theorem AlgebraicGeometry.Scheme.ProEt.full_sheafPullback.{u} (S : AlgebraicGeometry.Scheme) : (AlgebraicGeometry.Scheme.ProEt.sheafPullback S Ab).Full
theorem AlgebraicGeometry.Scheme.ProEt.full_sheafPullback.{u} (S : AlgebraicGeometry.Scheme) : (AlgebraicGeometry.Scheme.ProEt.sheafPullback S Ab).Full
Follows formally from Corollary 5.4.7.
- 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
- 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
- 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 sheaf F in \shv{\proet{X}} is called classical if it lies in the
essential image of \nu^{*}.
We can recognize the classical sheaves among all pro-étale sheaves by checking if they preserve affine filtered colimits:
- 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
- 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
- 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 sheaf F in \shv{\proet{X}} is classical if and only if for any
U \in \affproet{X} with presentation U = \lim U_i, it holds that
F(U) = \colim F(U_i).
(Bhatt–Scholze, Lemma 5.1.2, essential image part)
The only if part follows directly from
Corollary 5.4.6. Conversely, let F be in
\shv{\proet{X}} and suppose F satisfies the formula in the statement.
Then \nu^* \nu_{*} F \to F is an isomorphism. Indeed, by
Corollary 5.3.1.5, it suffices to check this after
restricting to \affproet{X}. Let U = \lim U_i be in \affproet{X}.
Then again by Corollary 5.4.6
\nu^* \nu_{*} F (U) = \colim \nu_{*} F(U_i) = \colim F(U_i) = F(U).
- 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
- 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
- Proposition 5.4.12
- Corollary 5.4.13
- Definition 5.4.14
- Theorem 5.4.15
- No associated Lean code or declarations.
Let K be in D^+(\et{X}) and U = \lim_i U_i in \affproet{X}. Then
R \Gamma(U, \nu^*K) = \colim_i R\Gamma(U_i, K).
(Bhatt–Scholze, Lemma 5.1.6)
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
- 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
- Corollary 5.4.13
- Definition 5.4.14
- Theorem 5.4.15
- No associated Lean code or declarations.
For any K in D^{+}(\et{X}) the unit K \to R \nu_{*} \nu^* K is an
isomorphism.
(Bhatt–Scholze, Corollary 5.1.6)
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
- 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
- Definition 5.4.14
- Theorem 5.4.15
- No associated Lean code or declarations.
Let K be in D^{+}(\et{X}). Then
R \Gamma(\et{X}, K) \cong R \Gamma(\proet{X}, \nu^{*} K).
By Proposition 5.4.12, we have
R \Gamma(\et{X}, K) \cong R \Gamma(\et{X}, R \nu_{*}\nu^*K). Since
\nu_* maps injective sheaves to acyclic ones by general theory, we have
R \Gamma(\et{X}, -) \circ R\nu_{*} = R (\Gamma(\et{X}, -) \circ \nu_*) = R \Gamma(\proet{X}, -).
So the claim 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.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
- Theorem 5.4.15
- No associated Lean code or declarations.
Denote by
\gammacont(X, -)\colon \mathrm{Ab}(\et{X})^{\N} \to \mathrm{Ab} the functor
\left( F_n \right)_{n \in \N} \mapsto \Gamma\left(X, \lim F_n\right).
For an inverse system (F_n)_{n \in \N}, we call the cohomology groups
H^i \mathrm{R} \gammacont\left(X, -\right)\left( \left( F_{n} \right)_{n \in \N} \right),
denoted by H^i_{\mathrm{cont}}(\et{X}, (F_{n})_{n \in \N}), the
continuous étale cohomology of X with coefficients in
\left( F_n \right)_{n \in \N}.
(Jannsen, §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
- 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
- No associated Lean code or declarations.
Let (F_n)_{n \in \N} be an inverse system of abelian sheaves on \et{X}
with epimorphic transition maps. Then there exists a canonical identification
R \gammacont(X, (F_n)_n) \cong R \Gamma(\proet{X}, \lim \nu^* F_n).
In particular, for every i \ge 0 we have
H^i_{\mathrm{cont}}(\et{X}, (F_n)_n) \cong H^i(\proet{X}, \lim \nu^* F_n).
(Bhatt–Scholze, Proposition 5.6.2)
We repeatedly use the fact that \Gamma commutes with inverse limits both on
\et{X} and \proet{X}. Then we have
\begin{aligned} R \gammacont(X, (F_n)_n) &\cong R \left( \Gamma(\et{X}, -) \circ \lim \right) ( (F_n)_n ) \\ &\cong R \left( \lim \circ \Gamma(\et{X}, -) \right) ( (F_n)_n ) \\ &\cong R \lim ( R \Gamma(\et{X}, F_n)) \\ &\cong R \lim ( R \Gamma(\proet{X}, \nu^{*} F_n)) \\ &\cong R \left( \lim \circ \Gamma(\proet{X}, -) \right) ( (\nu^* F_n)_n ) \\ &\cong R \left( \Gamma(\proet{X}, -) \circ \lim \right) ( (\nu^* F_n)_n ) \\ &\cong R \Gamma(\proet{X}, R \lim \nu^* F_n) \\ &\cong R \Gamma(\proet{X}, \lim \nu^* F_n) \end{aligned}
The fourth isomorphism is
Corollary 5.4.13 and the last is
Proposition 3.4.