ModuleStalkObjectSpreading.lean
Nyll.EtaleFundamentalGroups.FiniteEtale.StalkObjectSpreading
4 declarations indexed from sourceView source ↗ Module documentation
Finite-etale covers spread from an actual stalk
The stalk is the colimit of the rings of sections on open neighborhoods. Finite-etale inverse-limit descent supplies a cover of the spectrum of one such ring. Pulling it back by the neighborhood's affinization gives an actual cover of that neighborhood, retaining the native stalk comparison.
This is the object-spreading step in Stacks 0BPA and 0BQ5. It does not assume that the base is affine, quasi-compact, or quasi-separated.
Declarations
AlgebraicGeometry.FiniteEtale.finiteEtaleOverCategoryStalkSpreading
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
AlgebraicGeometry.FiniteEtale.finiteEtaleHasPullbacksAlongStalkSpreading
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryStalkSpreading (X : Scheme.{u}) :
Category (MorphismProperty.Over
(@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
AlgebraicGeometry.FiniteEtale.finiteEtaleStableUnderBaseChangeAlongStalkSpreading
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryStalkSpreading (X : Scheme.{u}) :
Category (MorphismProperty.Over
(@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongStalkSpreading
{X Y : Scheme.{u}} (f : X ⟶ Y) :
MorphismProperty.HasPullbacksAlong
(@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
⟨fun _ _ ↦ inferInstance⟩
AlgebraicGeometry.FiniteEtale.exists_open_model_fromSpecStalk
DocumentationEvery finite-etale cover of the actual local spectrum comes from a finite-etale cover of an open neighborhood, with its literal native pullback isomorphic to the supplied cover.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryStalkSpreading (X : Scheme.{u}) :
Category (MorphismProperty.Over
(@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongStalkSpreading
{X Y : Scheme.{u}} (f : X ⟶ Y) :
MorphismProperty.HasPullbacksAlong
(@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongStalkSpreading
{X Y : Scheme.{u}} (f : X ⟶ Y) :
MorphismProperty.IsStableUnderBaseChangeAlong
(@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
⟨fun h hf ↦ MorphismProperty.of_isPullback
(P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩