Base change preserves finite limits and étale covering sieves. The covering statement follows from base change on the localized big étale sites, using the description of the small topology through the forgetful functors to over categories.
Base change of an étale scheme along an arbitrary morphism of schemes.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)def etaleBaseChange : Y.Etale ⥤ X.EtaleSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)instance : PreservesFiniteLimits (etaleBaseChange f)Base change preserves covering sieves for the actual small étale topology.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)lemma etaleBaseChange_coverPreserving :
CoverPreserving Y.smallEtaleTopology X.smallEtaleTopology (etaleBaseChange f) where
cover_preserve {U} {S} hS := by
let : (Scheme.Etale.forget Y).LocallyCoverDense (Scheme.etaleTopology.over Y) :=
inferInstanceAs ((MorphismProperty.Over.forget
(show MorphismProperty Scheme.{u} from @Etale) ⊤ Y).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 Y).restrictedTopology
(Scheme.etaleTopology.over Y) U at hS
change S.functorPushforward (etaleBaseChange f) ∈
(Scheme.Etale.forget X).restrictedTopology
(Scheme.etaleTopology.over X) ((etaleBaseChange f).obj U)
rw [CategoryTheory.Functor.mem_restrictedTopology_iff] at hS ⊢
rw [← Sieve.functorPushforward_comp]
change S.functorPushforward
(Scheme.Etale.forget Y ⋙ CategoryTheory.Over.pullback f) ∈
(Scheme.etaleTopology.over X) _
rw [Sieve.functorPushforward_comp]
exact CoverPreserving.cover_preserve
(GrothendieckTopology.coverPreserving_overPullback Scheme.etaleTopology f) hSSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y)instance : (etaleBaseChange f).IsContinuous Y.smallEtaleTopology X.smallEtaleTopology