The existing category FiniteEtale X embeds fully faithfully into sheaves of sets on the actual small étale site. The geometric stalk of the represented sheaf is naturally isomorphic to the underlying finite set of EFG's geometric fiber functor FiniteEtale.fiber.
The comparison uses the ordinary colimit definition of a stalk, the map/pullback adjunction on slice categories, and the existing equivalence between finite étale schemes over a separably closed field and finite sets. No connectedness hypothesis is imposed on X.
This supplies the represented-sheaf and fiber comparison needed for https://stacks.math.columbia.edu/tag/09Y8 . The converse representability of finite locally constant sheaves is a subsequent step.
A finite étale cover is an object of the small étale site.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Limits
universe u v
namespace EtaleCohomologydef finiteEtaleToEtale (X : Scheme.{u}) : FiniteEtale X ⥤ X.EtaleThe sheaf represented by a finite étale cover.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Limits
universe u v
namespace EtaleCohomologydef finiteEtaleSheaf (X : Scheme.{u}) :
FiniteEtale X ⥤ Sheaf X.smallEtaleTopology (Type u)Maps of represented étale sheaves are exactly maps of finite étale covers.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Limits
universe u v
namespace EtaleCohomologydef finiteEtaleSheafFullyFaithful (X : Scheme.{u}) :
(finiteEtaleSheaf X).FullyFaithfulSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Limits
universe u v
namespace EtaleCohomologydef representableSheafFiberIso {C : Type v} [Category.{u} C]
{J : GrothendieckTopology C} [J.Subcanonical] (Φ : J.Point.{u}) :
J.yoneda ⋙ Φ.sheafFiber ≅ Φ.fiberThe stalk of the represented sheaf consists of geometric points of the cover.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Limits
universe u v
namespace EtaleCohomologydef finiteEtaleSheafStalkIso {X : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
(s : Spec (.of Ω) ⟶ X) :
finiteEtaleSheaf X ⋙ (Scheme.pointSmallEtale s).sheafFiber ≅
finiteEtaleToEtale X ⋙ (Scheme.pointSmallEtale s).fiberSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Limits
universe u v
namespace EtaleCohomologydef finiteEtalePoint (Ω : Type u) [Field Ω] : FiniteEtale (Spec (.of Ω))Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Limits
universe u v
namespace EtaleCohomologydef finiteEtaleSectionEquivPoints {Ω : Type u} [Field Ω] [IsSepClosed Ω]
(W : FiniteEtale (Spec (.of Ω))) :
(finiteEtalePoint Ω ⟶ W) ≃ W.leftSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Limits
universe u v
namespace EtaleCohomologydef finiteEtaleGeometricHomEquivFiber {X : Scheme.{u}} {Ω : Type u}
[Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X) (W : FiniteEtale X) :
(Over.mk s ⟶ (FiniteEtale.forget X).obj W) ≃ (FiniteEtale.fiber s).obj WSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Limits
universe u v
namespace EtaleCohomologylemma finiteEtaleGeometricHomEquivFiber_apply {X : Scheme.{u}} {Ω : Type u}
[Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X) (W : FiniteEtale X)
(a : Over.mk s ⟶ (FiniteEtale.forget X).obj W) :
finiteEtaleGeometricHomEquivFiber s W a =
(pullback.lift (f := ((FiniteEtale.forget X).obj W).hom) (g := s)
a.left (𝟙 (Spec (.of Ω)))
((Over.w a).trans (Category.id_comp s).symm)) (default : Spec (.of Ω))Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Limits
universe u v
namespace EtaleCohomologydef finiteEtaleGeometricFiberIso {X : Scheme.{u}} {Ω : Type u}
[Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ X) :
finiteEtaleToEtale X ⋙ (Scheme.pointSmallEtale s).fiber ≅
FiniteEtale.fiber s ⋙ forget FintypeCatThe geometric stalk of a finite étale represented sheaf is naturally the underlying finite set of the existing EFG fiber functor.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Limits
universe u v
namespace EtaleCohomologydef finiteEtaleSheafFiberIso {X : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
(s : Spec (.of Ω) ⟶ X) :
finiteEtaleSheaf X ⋙ (Scheme.pointSmallEtale s).sheafFiber ≅
FiniteEtale.fiber s ⋙ forget FintypeCat