Composition with an étale morphism defines a continuous functor of small étale sites. Its adjunction with scheme base change identifies actual inverse image of set-valued sheaves with restriction of their underlying presheaves. This makes local representers on an étale trivializing cover available for effective descent, with their ordinary functorial sections.
Postcomposition with an étale morphism on the small sites.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {U X : Scheme.{u}} (f : U ⟶ X) [hf : Etale f]def etalePostcompose : U.Etale ⥤ X.EtalePostcomposition and scheme base change are adjoint.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {U X : Scheme.{u}} (f : U ⟶ X) [hf : Etale f]def etalePostcomposeBaseChangeAdjunction : etalePostcompose f ⊣ etaleBaseChange fPostcomposition does not change the covering property of a family.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {U X : Scheme.{u}} (f : U ⟶ X) [hf : Etale f]lemma etalePostcompose_coverPreserving :
CoverPreserving U.smallEtaleTopology X.smallEtaleTopology (etalePostcompose f) where
cover_preserve {V} {S} hS := by
let : (Scheme.Etale.forget U).LocallyCoverDense (Scheme.etaleTopology.over U) :=
inferInstanceAs ((MorphismProperty.Over.forget
(show MorphismProperty Scheme.{u} from @Etale) ⊤ U).LocallyCoverDense _)
let : (Scheme.Etale.forget X).LocallyCoverDense (Scheme.etaleTopology.over X) :=
inferInstanceAs ((MorphismProperty.Over.forget
(show MorphismProperty Scheme.{u} from @Etale) ⊤ X).LocallyCoverDense _)
change S ∈ (Scheme.Etale.forget U).restrictedTopology
(Scheme.etaleTopology.over U) V at hS
change S.functorPushforward (etalePostcompose f) ∈
(Scheme.Etale.forget X).restrictedTopology
(Scheme.etaleTopology.over X) ((etalePostcompose f).obj V)
rw [CategoryTheory.Functor.mem_restrictedTopology_iff] at hS ⊢
rw [← Sieve.functorPushforward_comp]
change S.functorPushforward
(Scheme.Etale.forget U ⋙ CategoryTheory.Over.map f) ∈
(Scheme.etaleTopology.over X) _
rw [Sieve.functorPushforward_comp]
exact (GrothendieckTopology.over_map_coverPreserving Scheme.etaleTopology f).cover_preserve hSSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {U X : Scheme.{u}} (f : U ⟶ X) [hf : Etale f]instance : PreservesLimitsOfShape WalkingCospan (etalePostcompose f)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {U X : Scheme.{u}} (f : U ⟶ X) [hf : Etale f]instance : (etalePostcompose f).IsContinuous U.smallEtaleTopology X.smallEtaleTopologyRestriction of sheaves by precomposition with the étale postcomposition functor.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {U X : Scheme.{u}} (f : U ⟶ X) [hf : Etale f]
variable (A : Type v) [Category.{w} A]def etaleRestriction : Sheaf X.smallEtaleTopology A ⥤ Sheaf U.smallEtaleTopology ARestriction along an étale morphism is left adjoint to direct image.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {U X : Scheme.{u}} (f : U ⟶ X) [hf : Etale f]
variable (A : Type v) [Category.{w} A]def etaleRestrictionPushforwardAdjunction :
etaleRestriction f A ⊣ (etaleBaseChange f).sheafPushforwardContinuous A
X.smallEtaleTopology U.smallEtaleTopologyThe constructed inverse image is naturally isomorphic to ordinary restriction.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {U X : Scheme.{u}} (f : U ⟶ X) [hf : Etale f]
variable (A : Type v) [Category.{w} A]def etaleSetPullbackRestrictionIso : etaleSetPullback f ≅ etaleRestriction f (Type u)