59.70 Extension by zero to 59.74 Constructible sheaves on…

Section59.70 Extension by zero#

Section 59.70 of the Stacks Project, Tag 03S2. 10 tags here are carried by 51 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03S3, a definition

Tag 03S3 in the Stacks Project.

Stacks.EtaleCohomology.extensionByZeroSets, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZero/Basic.lean, line 308. The attribute's comment: “sets: the left adjoint of restriction”.

Stacks Project, Tag 03S3 (1). Extension by zero j_!^{Sh} on sheaves of sets of the small étale sites of an étale morphism j : U ⟶ X: the left adjoint of restriction, realised as the sheafification of the left Kan extension along composition with j.

abbrev extensionByZeroSets :
    Sheaf U.smallEtaleTopology (Type (max (u + 1) v)) ⥤
      Sheaf X.smallEtaleTopology (Type (max (u + 1) v))

Stacks.EtaleCohomology.extensionByZeroSetsAdj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZero/Basic.lean, line 317. The attribute's comment: “sets: the left adjoint of restriction”.

Stacks Project, Tag 03S3 (1). Extension by zero is left adjoint to restriction, on sheaves of sets.

def extensionByZeroSetsAdj :
    extensionByZeroSets.{u, v} j ⊣ etaleRestrictionSets.{u, v} j

Stacks.EtaleCohomology.extensionByZero, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZero/Basic.lean, line 351. The attribute's comment: “abelian: the left adjoint of restriction”.

Stacks Project, Tag 03S3 (2). Extension by zero j_! on abelian sheaves of the small étale sites of an étale morphism j : U ⟶ X: the left adjoint of restriction, realised as the sheafification of the left Kan extension along composition with j.

abbrev extensionByZero [HasSheafify X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}] :
    Sheaf U.smallEtaleTopology AddCommGrpCat.{max (u + 1) v} ⥤
      Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}

Stacks.EtaleCohomology.extensionByZeroAdj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZero/Basic.lean, line 360. The attribute's comment: “abelian: the left adjoint of restriction”.

Stacks Project, Tag 03S3 (2). Extension by zero is left adjoint to restriction, on abelian sheaves.

def extensionByZeroAdj [HasSheafify X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}] :
    extensionByZero.{u, v} j ⊣ etaleRestriction.{u, v} j

AlgebraicGeometry.abelianExtensionByZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/Adjunction.lean, line 91. The attribute's comment: “abelian_extension_by_zero”.

Stacks 03S3, part (2). Extension by zero of abelian étale sheaves along the étale morphism U ⟶ X: the sheafification of V ↦ ⨁_{V → U} F(V → U), realised as the sheaf pullback of the continuous site functor AlgebraicGeometry.smallEtalePostcompose.

public def abelianExtensionByZero :
    Sheaf (SmallEtale.topology B U.obj.left.1 U.obj.left.property)
        AddCommGrpCat.{u + 1} ⥤
      Sheaf (SmallEtale.topology B X hX) AddCommGrpCat.{u + 1}

AlgebraicGeometry.abelianExtensionByZeroAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/Adjunction.lean, line 106. The attribute's comment: “abelian_extension_by_zero”. References: SGA 4 XVII (6.2.11), “f_! ⊣ f^* (abelian)”; SGA 4 IV (11.3.1), “étale site, Ab”.

Stacks 03S3, part (2). Extension by zero is left adjoint to restriction, which is the property characterising it.

public def abelianExtensionByZeroAdjunction :
    abelianExtensionByZero B X hX U ⊣ abelianRestriction B X hX U

AlgebraicGeometry.moduleExtensionByZeroAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/Adjunction.lean, line 171. The attribute's comment: “module_extension_by_zero”. References: SGA 4 XVII (6.2.11), “f_! ⊣ f^* (Λ-modules)”; SGA 4 IV (11.3.1), “étale site, Λ-modules”.

Stacks 03S3, part (3). Extension by zero of sheaves of modules is left adjoint to restriction.

public def moduleExtensionByZeroAdjunction :
    moduleExtensionByZero B X hX U Λ ⊣ moduleRestriction B X hX U Λ

AlgebraicGeometry.moduleOpenExtensionByZeroAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/OpenImmersion.lean, line 147. The attribute's comment: “module_extension_by_zero”.

Extension by zero along an open immersion is left adjoint to restriction.

public def moduleOpenExtensionByZeroAdjunction
    [HasWeakSheafify (SmallEtale.topology B X hX) (ModuleCat.{w} Λ)] :
    moduleOpenExtensionByZero B X hX U Λ ⊣ moduleRestriction B X hX U Λ

AlgebraicGeometry.setExtensionByEmpty, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/Sets.lean, line 85. The attribute's comment: “sheaves_of_sets”.

Stacks 03S3, part (1). Extension by the empty set of étale sheaves of sets along the étale morphism U ⟶ X: the sheafification of V ↦ ⨿_{V → U} F(V → U), realised as the sheaf pullback of the continuous site functor AlgebraicGeometry.smallEtalePostcompose.

public def setExtensionByEmpty :
    Sheaf (SmallEtale.topology B U.obj.left.1 U.obj.left.property)
        (Type (max (u + 1) v)) ⥤
      Sheaf (SmallEtale.topology B X hX) (Type (max (u + 1) v))

AlgebraicGeometry.setExtensionByEmptyAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/Sets.lean, line 99. The attribute's comment: “sheaves_of_sets”.

Stacks 03S3, part (1). Restriction of étale sheaves of sets along U ⟶ X has a left adjoint, namely extension by the empty set. This adjunction is the property characterising it.

public def setExtensionByEmptyAdjunction :
    setExtensionByEmpty.{u, v} B X hX U ⊣ setRestriction.{u, v} B X hX U

AlgebraicGeometry.Space.abelianEtaleExtensionByZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleAbelianExtensionByZero.lean, line 71. The attribute's comment: “extension by zero of abelian sheaves”.

Extension by zero of abelian étale sheaves along an étale morphism f : X ⟶ Y of algebraic spaces: the left adjoint of restriction, constructed as the sheafification of the left Kan extension along postcomposition.

def abelianEtaleExtensionByZero (f : X ⟶ Y) (hf : IsEtale B S hS f.hom) :
    Sheaf (SmallEtale.topology B S hS X.1) AddCommGrpCat.{u} ⥤
      Sheaf (SmallEtale.topology B S hS Y.1) AddCommGrpCat.{u}

AlgebraicGeometry.Space.abelianEtaleExtensionByZeroAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleAbelianExtensionByZero.lean, line 80. The attribute's comment: “the adjunction”.

Extension by zero is left adjoint to restriction for abelian étale sheaves along an étale morphism of algebraic spaces.

def abelianEtaleExtensionByZeroAdjunction (f : X ⟶ Y) (hf : IsEtale B S hS f.hom) :
    abelianEtaleExtensionByZero B S hS f hf ⊣ abelianEtaleRestriction B S hS f hf

Tag 0F4K, an equation

Tag 0F4K in the Stacks Project.

Stacks.EtaleCohomology.isIso_sigmaDesc_extensionByZeroSummandInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZero/Formula.lean, line 376. The attribute's comment: “the presheaf formula (j_{p!} F)(V) = ⨁_{φ : V → U} F(V →^φ U)”.

Stacks Project, Tag 0F4K. The sections of the presheaf j_{p!} F over a scheme V étale over X are the direct sum, over the morphisms φ : V ⟶ U over X, of the sections of F over V regarded as étale over U through φ; the comparison map is the one induced on each summand by the Kan extension unit.

theorem isIso_sigmaDesc_extensionByZeroSummandInclusion (F : (U.Etale)ᵒᵖ ⥤ A) (V : X.Etale) :
    IsIso (Sigma.desc
      (f := fun φ : V ⟶ smallEtaleSource j => F.obj (op (sourceDescend j φ)))
      (P := (extensionByZeroPresheaf j F).obj (op V))
      (fun φ => extensionByZeroSummandInclusion j F φ))

Stacks.EtaleCohomology.extensionByZeroPresheafSectionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZero/Formula.lean, line 411. The attribute's comment: “the presheaf formula (j_{p!} F)(V) = ⨁_{φ : V → U} F(V →^φ U)”.

Stacks Project, Tag 0F4K. The direct-sum formula for the sections of the presheaf j_{p!} F over a scheme V étale over X, as an isomorphism.

def extensionByZeroPresheafSectionIso (F : (U.Etale)ᵒᵖ ⥤ A) (V : X.Etale) :
    (∐ fun φ : V ⟶ smallEtaleSource j => F.obj (op (sourceDescend j φ))) ≅
      (extensionByZeroPresheaf j F).obj (op V)

Stacks.EtaleCohomology.extensionByZero_obj_eq_sheafify, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZero/Formula.lean, line 458. The attribute's comment: “j_! F is the sheafification of j_{p!} F”.

Stacks Project, Tag 0F4K. Extension by zero of an abelian sheaf is the sheafification of the presheaf j_{p!} F whose sections are given by the direct-sum formula.

theorem extensionByZero_obj_eq_sheafify
    [HasSheafify X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}]
    (F : Sheaf U.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}) :
    (extensionByZero.{u, v} j).obj F =
      (presheafToSheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}).obj
        (extensionByZeroPresheaf j F.obj)

Stacks.Sites.ExtensionByZero.isIso_lanSigmaDesc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/ExtensionByZeroExactness.lean, line 110.

Stacks 0F4K. The left Kan extension along (Over.forget U).op is, over V, the coproduct of the values of F at the objects φ : V ⟶ U of C/U, the comparison map being the one induced by the Kan extension unit on each summand. Applied to the small étale site of a scheme and an étale U ⟶ X, this is the presheaf extension by zero along U ⟶ X: its sections over V are the direct sum of the sections of F over the lifts V ⟶ U.

theorem isIso_lanSigmaDesc
    {C : Type u} [Category.{u} C] (U : C)
    [∀ F : (Over U)ᵒᵖ ⥤ AddCommGrpCat.{u}, (Over.forget U).op.HasLeftKanExtension F]
    (F : (Over U)ᵒᵖ ⥤ AddCommGrpCat.{u}) (V : C) :
    IsIso (Sigma.desc
      (f := fun φ : V ⟶ U => F.obj (op (Over.mk φ)))
      (P := (((Over.forget U).op.lan.obj F).obj (op V)))
      (fun φ => (((Over.forget U).op.lanUnit.app F).app (op (Over.mk φ)))))

Tag 03S4, an exercise

Tag 03S4 in the Stacks Project.

Stacks.EtaleCohomology.extensionByZeroDirectSumAdj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZero/FormulaAdjunction.lean, line 202. The attribute's comment: “the sheafification of the direct-sum presheaf j_{p!} is a left adjoint of j^{-1}”.

Stacks Project, Tag 03S4. Extension by zero, defined as the sheafification of the presheaf j_{p!} whose sections over a scheme V étale over X are the direct sum ⨁_{φ : V → U} F(V →^φ U) of Stacks Tag 0F4K, is a left adjoint of the restriction functor j^{-1} on abelian sheaves of the small étale sites of an étale morphism j : U ⟶ X of schemes.

def extensionByZeroDirectSumAdj :
    sheafToPresheaf U.smallEtaleTopology AddCommGrpCat.{max (u + 1) v} ⋙
        extensionByZeroDirectSum j (A := AddCommGrpCat.{max (u + 1) v}) ⋙
        presheafToSheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v} ⊣
      etaleRestriction.{u, v} j

Tag 03S5, a proposition

Tag 03S5 in the Stacks Project.

AlgebraicGeometry.abelianExtensionByZero_preservesFiniteLimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/DerivedLowerShriekQuasiFinite.lean, line 105. The attribute's comment: “left exactness of j_! in a big étale site”.

Extension by zero of abelian étale sheaves preserves finite limits.

public instance abelianExtensionByZero_preservesFiniteLimits :
    PreservesFiniteLimits (abelianExtensionByZero B X hX U)

AlgebraicGeometry.abelianExtensionByZero_preservesFiniteColimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/DerivedLowerShriekQuasiFinite.lean, line 111. The attribute's comment: “right exactness of j_! in a big étale site”.

Extension by zero of abelian étale sheaves preserves finite colimits.

public instance abelianExtensionByZero_preservesFiniteColimits :
    PreservesFiniteColimits (abelianExtensionByZero B X hX U)

Stacks.EtaleCohomology.etaleModuleExtensionByZero_preservesFiniteLimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/CompactlySupportedCohomologyZero.lean, line 224. The attribute's comment: “left exactness of j_! for module coefficients”.

Stacks Project, Tag 03S5 for module coefficients: extension by zero of sheaves of Λ-modules on small étale sites preserves finite limits. It is additive, preserves monomorphisms and preserves all colimits, hence preserves homology, hence finite limits.

instance etaleModuleExtensionByZero_preservesFiniteLimits :
    PreservesFiniteLimits (etaleModuleExtensionByZero.{u, r} Λ j)

Stacks.EtaleCohomology.extensionByZero_preservesFiniteLimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZero/Exactness.lean, line 212. The attribute's comment: “left exactness of j_!”.

Extension by zero preserves finite limits.

instance extensionByZero_preservesFiniteLimits
    [HasSheafify U.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}] :
    PreservesFiniteLimits (extensionByZero.{u, v} j)

Stacks.EtaleCohomology.extensionByZero_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZero/Exactness.lean, line 222. The attribute's comment: “j_! is an exact functor”.

Extension by zero along an étale morphism of schemes is an exact functor on abelian sheaves of the small étale sites.

theorem extensionByZero_exact
    [HasSheafify U.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}] :
    exactFunctor _ _ (extensionByZero.{u, v} j)

AlgebraicGeometry.moduleExtensionByZero_preservesFiniteLimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/ModuleExactness.lean, line 106. The attribute's comment: “left exactness of j_! for sheaves of modules on the small etale sites of Tag 021B”.

Stacks 03S5 for sheaves of modules, on the sites of Tag 021B. Extension by zero of sheaves of Λ-modules along an object U of the small étale site of X preserves finite limits. Together with the finite colimits it preserves as a left adjoint, extension by zero is exact.

The small étale site of U has fibre products and equalizers, and composition with U ⟶ X preserves both, so Tag 04BH for module coefficients applies.

public instance moduleExtensionByZero_preservesFiniteLimits :
    PreservesFiniteLimits (moduleExtensionByZero B X hX U Λ)

AlgebraicGeometry.stalkExtensionByZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroStalk.lean, line 535. The attribute's comment: “stalk formula”.

Stacks 03S5. The stalk at a geometric point x of X of the extension by zero of an abelian étale sheaf on U is the direct sum of its stalks at the lifts of x to U.

public def stalkExtensionByZeroIso
    (F : Sheaf (SmallEtale.topology B U.obj.left.1 U.obj.left.property) AddCommGrpCat.{u + 1}) :
    etaleStalk B X hX x ((abelianExtensionByZero B X hX U).obj F).obj ≅
      (∐ fun p : geometricPointLifts B X hX U x => liftedStalk B X hX U x F p)

AlgebraicGeometry.stalkExtensionByZeroIso_germ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroStalk.lean, line 546. The attribute's comment: “germ computation”.

Stacks 03S5. The stalk isomorphism sends the germ of a section over an étale neighbourhood W ⟶ U, viewed in the extension by zero through the adjunction unit, to its germ at the induced lift, in the corresponding summand of the direct sum. This formula characterises the isomorphism.

public theorem stalkExtensionByZeroIso_germ
    (F : Sheaf (SmallEtale.topology B U.obj.left.1 U.obj.left.property) AddCommGrpCat.{u + 1})
    (W : SmallEtale B U.obj.left.1 U.obj.left.property)
    (p : geometricPointLifts B X hX U x)
    (w : (geometricPointFiber B U.obj.left.1 U.obj.left.property
      (geometricPointOfLift B X hX U x p)).obj W)
    (q : (geometricPointFiber B X hX x).obj ((smallEtalePostcompose B X hX U).obj W))
    (hq : q.1 = w.1) (s : F.obj.obj (op W)) :
    (stalkExtensionByZeroIso B X hX U x F).hom
      ((colimit.ι ((CategoryOfElements.π (geometricPointFiber B X hX x)).op ⋙
          ((abelianExtensionByZero B X hX U).obj F).obj)
          (op (Functor.elementsMk _ ((smallEtalePostcompose B X hX U).obj W) q)))
        (((abelianExtensionByZeroAdjunction B X hX U).unit.app F).hom.app (op W) s)) =
      (Sigma.ι (fun p : geometricPointLifts B X hX U x => liftedStalk B X hX U x F p) p)
        ((colimit.ι ((CategoryOfElements.π (geometricPointFiber B U.obj.left.1
            U.obj.left.property (geometricPointOfLift B X hX U x p))).op ⋙ F.obj)
          (op (Functor.elementsMk _ W w))) s)

AlgebraicGeometry.stalkExtensionByZeroIso_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroStalk.lean, line 577. The attribute's comment: “naturality”.

Stacks 03S5. The stalk decomposition of extension by zero is natural in the abelian sheaf.

public theorem stalkExtensionByZeroIso_naturality
    {F G : Sheaf (SmallEtale.topology B U.obj.left.1 U.obj.left.property) AddCommGrpCat.{u + 1}}
    (f : F ⟶ G) :
    colimMap (Functor.whiskerLeft (CategoryOfElements.π (geometricPointFiber B X hX x)).op
        ((abelianExtensionByZero B X hX U).map f).hom) ≫
        (stalkExtensionByZeroIso B X hX U x G).hom =
      (stalkExtensionByZeroIso B X hX U x F).hom ≫
        Limits.Sigma.map (fun p : geometricPointLifts B X hX U x =>
          colimMap (Functor.whiskerLeft (CategoryOfElements.π (geometricPointFiber
            B U.obj.left.1 U.obj.left.property (geometricPointOfLift B X hX U x p))).op f.hom))

AlgebraicGeometry.abelianExtensionByZero_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroStalk.lean, line 594. The attribute's comment: “exactness”.

Stacks 03S5. Extension by zero of abelian sheaves along an étale morphism is exact. Under the equivalence of the small étale site of U with the localization of the small étale site of X at U, extension by zero becomes lower shriek along Over.forget U, which is exact.

public theorem abelianExtensionByZero_exact :
    exactFunctor _ _ (abelianExtensionByZero B X hX U)

Tag 0F70, a lemma

Tag 0F70 in the Stacks Project.

Stacks.EtaleCohomology.directImageRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZero/Exactness.lean, line 263. The attribute's comment: “the isomorphism j^{-1} j_* F → F”.

For an étale monomorphism j : U ⟶ X, the natural isomorphism j^{-1} j_* F ≅ F for abelian sheaves F on the small étale site of U, given by the counit of j^{-1} ⊣ j_*.

def directImageRestrictionIso :
    etaleDirectImage.{u, v} j ⋙ etaleRestriction.{u, v} j ≅ 𝟭 _

AlgebraicGeometry.abelianDirectImageAdjunction_counit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/DirectImage.lean, line 90. The attribute's comment: “direct_image_counit”.

Stacks 0F70. Along an open immersion U ⟶ X the counit of the adjunction between restriction and direct image is an isomorphism: an abelian étale sheaf on U is recovered from its direct image by restricting back to U. Composition with U ⟶ X is continuous, cocontinuous, and — because the structure morphism of U is a monomorphism — fully faithful, which is exactly the situation of Stacks 00XT.

public theorem abelianDirectImageAdjunction_counit_isIso :
    IsIso (abelianDirectImageAdjunction B X hX U).counit

AlgebraicGeometry.abelianExtensionByZeroAdjunction_unit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/OpenImmersion.lean, line 63. The attribute's comment: “extension_by_zero_unit”.

Along an open immersion U ⟶ X the unit of the extension-by-zero adjunction is an isomorphism: an abelian étale sheaf on U is recovered from its extension by zero by restricting back to U.

public theorem abelianExtensionByZeroAdjunction_unit_isIso
    (F : Sheaf (SmallEtale.topology B U.obj.left.1 U.obj.left.property) AddCommGrpCat.{u + 1}) :
    IsIso ((abelianExtensionByZeroAdjunction B X hX U).unit.app F)

AlgebraicGeometry.abelianExtensionByZeroAdjunction_hom_isIso_of_stalk_isZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroCharacterization.lean, line 226. The attribute's comment: “extension_by_zero_characterization: uniqueness”.

Stacks 0F70. An abelian étale sheaf on X whose restriction to the open subscheme U is identified with F and whose stalks at the geometric points of X outside U vanish is canonically the extension by zero of F: the map from j_!F adjoint to the given identification is an isomorphism. Together with the vanishing of the stalks of j_!F outside U this is the uniqueness assertion of the source.

public theorem abelianExtensionByZeroAdjunction_hom_isIso_of_stalk_isZero
    [IsOpenImmersion (B.inclusion.map U.obj.hom)]
    (F : Sheaf (SmallEtale.topology B U.obj.left.1 U.obj.left.property) AddCommGrpCat.{u + 1})
    (G : Sheaf (SmallEtale.topology B X hX) AddCommGrpCat.{u + 1})
    (e : F ≅ (abelianRestriction B X hX U).obj G)
    (hG : ∀ x : GeometricPoint X,
      x.hom default ∉ Set.range (B.inclusion.map U.obj.hom).base →
        IsZero (etaleStalk B X hX x G.obj)) :
    IsIso (((abelianExtensionByZeroAdjunction B X hX U).homEquiv F G).symm e.hom)

AlgebraicGeometry.abelianExtensionByZero_stalk_isZero_of_not_mem_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroStalk.lean, line 677. The attribute's comment: “extension_by_zero_characterization: zero stalks”.

Stacks 0F70. The extension by zero of an abelian étale sheaf on U has zero stalk at every geometric point of X outside the image of U: by the stalk formula the stalk is the direct sum over the lifts of that point, and there are none.

public theorem abelianExtensionByZero_stalk_isZero_of_not_mem_range
    (F : Sheaf (SmallEtale.topology B U.obj.left.1 U.obj.left.property) AddCommGrpCat.{u + 1})
    (hx : x.hom default ∉ Set.range (B.inclusion.map U.obj.hom).base) :
    IsZero (etaleStalk B X hX x ((abelianExtensionByZero B X hX U).obj F).obj)

AlgebraicGeometry.abelianExtensionByZero_stalk_isZero_of_not_mem_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroStalk.lean, line 677. The attribute's comment: “extension_by_zero_characterization”.

Stacks 0F70. The extension by zero of an abelian étale sheaf on U has zero stalk at every geometric point of X outside the image of U: by the stalk formula the stalk is the direct sum over the lifts of that point, and there are none.

public theorem abelianExtensionByZero_stalk_isZero_of_not_mem_range
    (F : Sheaf (SmallEtale.topology B U.obj.left.1 U.obj.left.property) AddCommGrpCat.{u + 1})
    (hx : x.hom default ∉ Set.range (B.inclusion.map U.obj.hom).base) :
    IsZero (etaleStalk B X hX x ((abelianExtensionByZero B X hX U).obj F).obj)

Tag 03S6, a lemma

Tag 03S6 in the Stacks Project.

AlgebraicGeometry.abelianExtensionByZeroBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange.lean, line 182. The attribute's comment: “abelian sheaves”.

Stacks 03S6, abelian sheaves. Extension by zero of abelian étale sheaves commutes with base change: for f : Y ⟶ X and j : V ⟶ X étale with base change j' : V' ⟶ Y and f' : V' ⟶ V, one has j'_! ∘ f'^{-1} ≅ f^{-1} ∘ j_!, naturally in the sheaf.

public noncomputable def abelianExtensionByZeroBaseChangeIso
    (B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : Y ⟶ X)
    (U : SmallEtale B X.1 X.property) :
    (smallEtaleBaseChange B (baseChangedEtaleProjection B f U)).sheafPullback
        AddCommGrpCat.{u + 1}
        (SmallEtale.topology B U.obj.left.1 U.obj.left.property)
        (SmallEtale.topology B
          ((smallEtaleBaseChange B f).obj U).obj.left.1
          ((smallEtaleBaseChange B f).obj U).obj.left.property) ⋙
      abelianExtensionByZero B Y.1 Y.property
        ((smallEtaleBaseChange B f).obj U) ≅
    abelianExtensionByZero B X.1 X.property U ⋙
      (smallEtaleBaseChange B f).sheafPullback AddCommGrpCat.{u + 1}
        (SmallEtale.topology B X.1 X.property)
        (SmallEtale.topology B Y.1 Y.property)

AlgebraicGeometry.moduleExtensionByZeroBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange.lean, line 214. The attribute's comment: “sheaves of modules”.

Stacks 03S6, sheaves of modules. Extension by zero of étale sheaves of Λ-modules commutes with base change, by the same adjunction argument as for abelian sheaves.

public noncomputable def moduleExtensionByZeroBaseChangeIso
    (B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : Y ⟶ X)
    (U : SmallEtale B X.1 X.property) (Λ : Type v) [Ring Λ] :
    (smallEtaleBaseChange B (baseChangedEtaleProjection B f U)).sheafPullback
        (ModuleCat.{max (u + 1) v} Λ)
        (SmallEtale.topology B U.obj.left.1 U.obj.left.property)
        (SmallEtale.topology B
          ((smallEtaleBaseChange B f).obj U).obj.left.1
          ((smallEtaleBaseChange B f).obj U).obj.left.property) ⋙
      moduleExtensionByZero B Y.1 Y.property
        ((smallEtaleBaseChange B f).obj U) Λ ≅
    moduleExtensionByZero B X.1 X.property U Λ ⋙
      (smallEtaleBaseChange B f).sheafPullback (ModuleCat.{max (u + 1) v} Λ)
        (SmallEtale.topology B X.1 X.property)
        (SmallEtale.topology B Y.1 Y.property)

Tag 0F4L, a lemma

Tag 0F4L in the Stacks Project.

AlgebraicGeometry.abelianExtensionByZeroToPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/Pushforward.lean, line 887. The attribute's comment: “abelian natural map”.

The canonical map from extension by zero to the direct image of abelian sheaves along the étale morphism U ⟶ X. On the summand of the presheaf extension indexed by φ : V ⟶ U it extends a section by zero along the open and closed graph of φ; that requires U ⟶ X to be separated, and off the separated locus the map is zero.

public noncomputable def abelianExtensionByZeroToPushforward :
    let := smallEtaleBaseChange_isContinuous B U.obj.hom
    abelianExtensionByZero B X hX U ⟶
      (smallEtaleBaseChange B U.obj.hom).sheafPushforwardContinuous
        AddCommGrpCat.{u + 1}
        (SmallEtale.topology B X hX)
        (SmallEtale.topology B U.obj.left.1 U.obj.left.property)

AlgebraicGeometry.abelianExtensionByZeroToPushforward_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/Pushforward.lean, line 924. The attribute's comment: “abelian injectivity”.

For a separated étale morphism, every component of the canonical map from extension by zero to the direct image of abelian sheaves is a monomorphism.

public theorem abelianExtensionByZeroToPushforward_mono
    (F : Sheaf (SmallEtale.topology B U.obj.left.1 U.obj.left.property)
      AddCommGrpCat.{u + 1}) :
    Mono ((abelianExtensionByZeroToPushforward B X hX U).app F)

AlgebraicGeometry.abelianExtensionByZeroToPushforward_graph, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/Pushforward.lean, line 946. The attribute's comment: “abelian graph restriction”.

On the summand indexed by W ⟶ U, the canonical map restricts along the graph W ⟶ W ×_X U to the original section.

public theorem abelianExtensionByZeroToPushforward_graph
    (F : Sheaf (SmallEtale.topology B U.obj.left.1 U.obj.left.property)
      AddCommGrpCat.{u + 1})
    (W : SmallEtale B U.obj.left.1 U.obj.left.property)
    (s : F.obj.obj (Opposite.op W)) :
    let V := (smallEtalePostcompose B X hX U).obj W
    (F.obj.map (smallEtaleGraph B X hX U W).op)
      (((abelianExtensionByZeroToPushforward B X hX U).app F).hom.app
        (Opposite.op V)
        (((abelianExtensionByZeroAdjunction
          B X hX U).unit.app F).hom.app (Opposite.op W) s)) = s

AlgebraicGeometry.abelianExtensionByZeroToPushforward_graph_compl, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/Pushforward.lean, line 967. The attribute's comment: “abelian complementary vanishing”.

The image of the summand indexed by W ⟶ U restricts to zero along every morphism into W ×_X U whose image avoids the graph of W.

public theorem abelianExtensionByZeroToPushforward_graph_compl
    (F : Sheaf (SmallEtale.topology B U.obj.left.1 U.obj.left.property)
      AddCommGrpCat.{u + 1})
    (W T : SmallEtale B U.obj.left.1 U.obj.left.property)
    (g : T ⟶ (smallEtaleBaseChange B U.obj.hom).obj
      ((smallEtalePostcompose B X hX U).obj W))
    (hg : disjointFromSmallEtaleGraph B X hX U W T g)
    (s : F.obj.obj (Opposite.op W)) :
    let V := (smallEtalePostcompose B X hX U).obj W
    (F.obj.map g.op)
      (((abelianExtensionByZeroToPushforward B X hX U).app F).hom.app
        (Opposite.op V)
        (((abelianExtensionByZeroAdjunction
          B X hX U).unit.app F).hom.app (Opposite.op W) s)) = 0

AlgebraicGeometry.moduleExtensionByZeroToPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/Pushforward.lean, line 993. The attribute's comment: “module natural map”.

The canonical map from extension by zero to the direct image of sheaves of Λ-modules along the étale morphism U ⟶ X, constructed exactly as in the abelian case.

public noncomputable def moduleExtensionByZeroToPushforward
    (Λ : Type v) [Ring Λ] :
    let := smallEtaleBaseChange_isContinuous B U.obj.hom
    moduleExtensionByZero B X hX U Λ ⟶
      (smallEtaleBaseChange B U.obj.hom).sheafPushforwardContinuous
        (ModuleCat.{max (u + 1) v} Λ)
        (SmallEtale.topology B X hX)
        (SmallEtale.topology B U.obj.left.1 U.obj.left.property)

AlgebraicGeometry.moduleExtensionByZeroToPushforward_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/Pushforward.lean, line 1032. The attribute's comment: “module injectivity”.

For a separated étale morphism, every component of the canonical map from extension by zero to the direct image of sheaves of Λ-modules is a monomorphism.

public theorem moduleExtensionByZeroToPushforward_mono
    (Λ : Type v) [Ring Λ]
    (F : Sheaf (SmallEtale.topology B U.obj.left.1 U.obj.left.property)
      (ModuleCat.{max (u + 1) v} Λ)) :
    Mono ((moduleExtensionByZeroToPushforward B X hX U Λ).app F)

AlgebraicGeometry.moduleExtensionByZeroToPushforward_graph, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/Pushforward.lean, line 1064. The attribute's comment: “module graph restriction”.

On the summand indexed by W ⟶ U, the canonical map for sheaves of modules restricts along the graph W ⟶ W ×_X U to the original section.

public theorem moduleExtensionByZeroToPushforward_graph
    (Λ : Type v) [Ring Λ]
    (F : Sheaf (SmallEtale.topology B U.obj.left.1 U.obj.left.property)
      (ModuleCat.{max (u + 1) v} Λ))
    (W : SmallEtale B U.obj.left.1 U.obj.left.property)
    (s : F.obj.obj (Opposite.op W)) :
    let V := (smallEtalePostcompose B X hX U).obj W
    (F.obj.map (smallEtaleGraph B X hX U W).op)
      (((moduleExtensionByZeroToPushforward B X hX U Λ).app F).hom.app
        (Opposite.op V)
      (((moduleExtensionByZeroAdjunction
          B X hX U Λ).unit.app F).hom.app (Opposite.op W) s)) = s

AlgebraicGeometry.moduleExtensionByZeroToPushforward_graph_compl, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/Pushforward.lean, line 1086. The attribute's comment: “module complementary vanishing”.

The image of the summand indexed by W ⟶ U restricts to zero along every morphism into W ×_X U whose image avoids the graph of W, for sheaves of modules.

public theorem moduleExtensionByZeroToPushforward_graph_compl
    (Λ : Type v) [Ring Λ]
    (F : Sheaf (SmallEtale.topology B U.obj.left.1 U.obj.left.property)
      (ModuleCat.{max (u + 1) v} Λ))
    (W T : SmallEtale B U.obj.left.1 U.obj.left.property)
    (g : T ⟶ (smallEtaleBaseChange B U.obj.hom).obj
      ((smallEtalePostcompose B X hX U).obj W))
    (hg : disjointFromSmallEtaleGraph B X hX U W T g)
    (s : F.obj.obj (Opposite.op W)) :
    let V := (smallEtalePostcompose B X hX U).obj W
    (F.obj.map g.op)
      (((moduleExtensionByZeroToPushforward B X hX U Λ).app F).hom.app
        (Opposite.op V)
      (((moduleExtensionByZeroAdjunction
          B X hX U Λ).unit.app F).hom.app (Opposite.op W) s)) = 0

Tag 03S7, a lemma

Tag 03S7 in the Stacks Project.

AlgebraicGeometry.abelianExtensionByZeroToPushforward_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/FinitePushforward.lean, line 272. The attribute's comment: “abelian sheaves”.

Stacks 03S7. For a finite étale morphism, the canonical map from extension by zero to the direct image is an isomorphism on abelian sheaves.

public theorem abelianExtensionByZeroToPushforward_isIso :
    IsIso (abelianExtensionByZeroToPushforward B X hX U)

AlgebraicGeometry.moduleExtensionByZeroToPushforward_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/FinitePushforward.lean, line 322. The attribute's comment: “sheaves of modules”.

Stacks 03S7. For a finite étale morphism, the canonical map from extension by zero to the direct image is an isomorphism on sheaves of Λ-modules.

public theorem moduleExtensionByZeroToPushforward_isIso (Λ : Type v) [Ring Λ] :
    IsIso (moduleExtensionByZeroToPushforward B X hX U Λ)

Tag 095L, a lemma

Tag 095L in the Stacks Project.

Stacks.EtaleCohomology.openClosedShortComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZero/ClosedComplement.lean, line 46. The attribute's comment: “the canonical short complex”.

The short complex j_! j^{-1} F ⟶ F ⟶ i_* i^{-1} F built from the counit of j_! ⊣ j^{-1} and the unit of i^{-1} ⊣ i_*, for a closed subscheme i : Z ⟶ X and the open immersion j : U ⟶ X of its complement.

def openClosedShortComplex :
    ShortComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})

Stacks.EtaleCohomology.openClosedShortComplex_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZero/ClosedComplement.lean, line 57. The attribute's comment: “short exactness”.

For a closed immersion i : Z ⟶ X and the open immersion j : U ⟶ X of its complement, the short complex 0 ⟶ j_! j^{-1} F ⟶ F ⟶ i_* i^{-1} F ⟶ 0 is short exact.

theorem openClosedShortComplex_shortExact :
    (openClosedShortComplex.{u, v} i j hij F).ShortExact

Stacks.EtaleCohomology.shortExact_etaleModuleExtensionByZero_directImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZero/ModuleOpenClosedTriangle.lean, line 256. The attribute's comment: “module coefficients”. References: SGA 4 IV (14.6), “(14.6.1)”; SGA 4 VIII (6.5), “partial”.

Stacks Project, Tag 095L for module coefficients. Let X be a scheme, let i : Z ⟶ X be a closed immersion and let j : U ⟶ X be an open immersion whose image is the complement of the image of i, and let Λ be a ring. For every sheaf ℱ of Λ-modules on the small étale site of X the counit of j_! ⊣ j^{-1} and the unit of i^{-1} ⊣ i_* form a short exact sequence 0 → j_! j^{-1} ℱ → ℱ → i_* i^{-1} ℱ → 0 of sheaves of Λ-modules on X_étale.

theorem shortExact_etaleModuleExtensionByZero_directImage (Λ : Type r) [Ring Λ]
    {Z U X : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i] (j : U ⟶ X) [IsOpenImmersion j]
    (hij : Set.range j.base = (Set.range i.base)ᶜ) (F : EtaleModules.{u, r} Λ X) :
    ∃ h : (etaleModuleExtensionByZeroAdj.{u, r} Λ j).counit.app F ≫
        (etaleModuleInverseImageAdj.{u, r} Λ i).unit.app F = 0,
      (ShortComplex.mk ((etaleModuleExtensionByZeroAdj.{u, r} Λ j).counit.app F)
        ((etaleModuleInverseImageAdj.{u, r} Λ i).unit.app F) h).ShortExact

Stacks.EtaleCohomology.shortExact_extensionByZero_etaleAbelianDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZero/OpenClosedSequence.lean, line 400. References: SGA 4 VIII (6.5), “partial”.

Stacks Project, Tag 095L. Let X be a scheme, let i : Z ⟶ X be a closed immersion and let j : U ⟶ X be an open immersion whose image is the complement of the image of i. For every abelian sheaf F on the small étale site of X the counit of j_! ⊣ j^{-1} and the unit of i^{-1} ⊣ i_* form a short exact sequence 0 → j_! j^{-1} F → F → i_* i^{-1} F → 0 of abelian sheaves on X_étale.

theorem shortExact_extensionByZero_etaleAbelianDirectImage {Z U X : Scheme.{u}} (i : Z ⟶ X)
    [IsClosedImmersion i] (j : U ⟶ X) [IsOpenImmersion j]
    (hij : Set.range j.base = (Set.range i.base)ᶜ)
    (F : Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}) :
    ∃ h : (extensionByZeroAdj.{u, v} j).counit.app F ≫
        (etaleAbelianInverseImageDirectImageAdj.{u, v} i).unit.app F = 0,
      (ShortComplex.mk ((extensionByZeroAdj.{u, v} j).counit.app F)
        ((etaleAbelianInverseImageDirectImageAdj.{u, v} i).unit.app F) h).ShortExact

Tag 0GJ1, a lemma

Tag 0GJ1 in the Stacks Project.

Stacks.EtaleCohomology.directImageExtensionByZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZero/FiniteDirectImage.lean, line 136. The attribute's comment: “at the coefficients AddCommGrpCat.{u+1}, on Mathlib's small etale sites”.

Stacks Project, Tag 0GJ1. For a cartesian square j' ≫ f = g ≫ j of schemes with f finite and j an open immersion, f_* ∘ j'_! ≅ j_! ∘ g_* as functors from abelian sheaves on U_étale to abelian sheaves on Y_étale.

def directImageExtensionByZeroIso :
    extensionByZero.{u, 0} j' ⋙ etaleAbelianDirectImage.{u, 0} f ≅
      etaleAbelianDirectImage.{u, 0} g ⋙ extensionByZero.{u, 0} j

AlgebraicGeometry.extensionByZeroFinitePushforwardCartesianIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroFinitePushforwardCartesian.lean, line 186.

Stacks 0GJ1. For a cartesian square g ≫ j = j' ≫ f of schemes of a big étale site with f finite and j : V ⟶ Y an open immersion, the functors j_! ∘ g_* and f_* ∘ j'_! from abelian sheaves on the small étale site of U to abelian sheaves on the small étale site of Y are naturally isomorphic.

The isomorphism is the mate, along the two extension-by-zero adjunctions, of the base change identification AlgebraicGeometry.abelianRestrictionPushforwardCartesianIso of the restriction functors; it is an isomorphism by the uniqueness characterisation of extension by zero, whose stalk hypothesis is AlgebraicGeometry.etaleStalk_pushforward_extensionByZero_isZero, where finiteness of f is used. The cartesian square is used twice: once for the base change identification, and once to see that j' is an open immersion.

public def extensionByZeroFinitePushforwardCartesianIso [IsFinite (B.inclusion.map f)]
    [IsOpenImmersion (B.inclusion.map V.obj.hom)]
    (sq : IsPullback (B.inclusion.map U.obj.hom) (B.inclusion.map g) (B.inclusion.map f)
      (B.inclusion.map V.obj.hom)) :
    B.smallPushforward g AddCommGrpCat.{u + 1} ⋙
        abelianExtensionByZero B Y.1 Y.property V ≅
      abelianExtensionByZero B X.1 X.property U ⋙
        B.smallPushforward f AddCommGrpCat.{u + 1}

Sources

• Section 59.70, Tag 03S2
• AxiomMath/Stacks at 5ed82d14

LeanStacks.EtaleCohomology.extensionByZeroSets · Stacks.EtaleCohomology.extensionByZeroSetsAdj · Stacks.EtaleCohomology.extensionByZero · Stacks.EtaleCohomology.extensionByZeroAdj · AlgebraicGeometry.abelianExtensionByZero · AlgebraicGeometry.abelianExtensionByZeroAdjunction · AlgebraicGeometry.moduleExtensionByZeroAdjunction · AlgebraicGeometry.moduleOpenExtensionByZeroAdjunction

Section59.71 Constructible sheaves#

Section 59.71 of the Stacks Project, Tag 05BE. 10 tags here are carried by 35 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03RW, a definition

Tag 03RW in the Stacks Project.

AlgebraicGeometry.IsConstructibleSetSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible.lean, line 104. The attribute's comment: “part (1)”. References: SGA 4 IX (2.3), “sheaves of sets”.

A constructible sheaf of sets on the small étale site.

public abbrev IsConstructibleSetSheaf (B : BigEtaleSite.{u}) (X : B.Scheme)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1))) : Prop

AlgebraicGeometry.IsConstructibleAbelianSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible.lean, line 110. The attribute's comment: “part (2)”. References: SGA 4½ Arcata (4.3.2), “(i)”; SGA 4 IX (2.3), “sheaves of groups”.

A constructible sheaf of abelian groups on the small étale site.

public abbrev IsConstructibleAbelianSheaf (B : BigEtaleSite.{u}) (X : B.Scheme)
    [∀ (S T : B.Scheme) (f : T ⟶ S),
      ((smallEtaleBaseChange B f).sheafPushforwardContinuous AddCommGrpCat.{w}
        (SmallEtale.topology B S.obj S.property)
        (SmallEtale.topology B T.obj T.property)).IsRightAdjoint]
    [∀ (T : B.Scheme) (V : SmallEtale B T.obj T.property),
      HasWeakSheafify ((SmallEtale.topology B T.obj T.property).over V) AddCommGrpCat.{w}]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{w}) : Prop

AlgebraicGeometry.IsConstructibleModuleSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible.lean, line 175. The attribute's comment: “part (3)”. References: SGA 4 IX (2.3), “A-modules, A noetherian”.

A constructible sheaf of modules over a Noetherian ring: on a finite constructible stratification of every affine open, it is locally constant of finite type.

public abbrev IsConstructibleModuleSheaf (B : BigEtaleSite.{u}) (X : B.Scheme)
    (R : Type r) [Ring R]
    [∀ (S T : B.Scheme) (f : T ⟶ S),
      ((smallEtaleBaseChange B f).sheafPushforwardContinuous (ModuleCat.{w} R)
        (SmallEtale.topology B S.obj S.property)
        (SmallEtale.topology B T.obj T.property)).IsRightAdjoint]
    [∀ (T : B.Scheme) (V : SmallEtale B T.obj T.property),
      HasWeakSheafify ((SmallEtale.topology B T.obj T.property).over V) (ModuleCat.{w} R)]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{w} R)) : Prop

AlgebraicGeometry.IsConstructibleAbelianEtaleSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/Definition.lean, line 85. The attribute's comment: “part (2)”. References: SGA 4 IX (2.3), “special case”; SGA 4½ Arcata (4.3.2).

Stacks 03RW (2). A sheaf of abelian groups F on the small étale site of X is constructible if for every affine open U ⊆ X there is a finite decomposition U = ∐ᵢ Uᵢ into constructible locally closed subschemes such that F|_{Uᵢ} is finite locally constant for all i.

public abbrev IsConstructibleAbelianEtaleSheaf
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) w}) : Prop

AlgebraicGeometry.IsConstructibleModuleEtaleSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/Definition.lean, line 99. The attribute's comment: “part (3)”.

Stacks 03RW (3). Let Λ be a Noetherian ring. A sheaf of Λ-modules F on the small étale site of X is constructible if for every affine open U ⊆ X there is a finite decomposition U = ∐ᵢ Uᵢ into constructible locally closed subschemes such that F|_{Uᵢ} is of finite type and locally constant for all i.

public abbrev IsConstructibleModuleEtaleSheaf (Λ : Type r) [CommRing Λ] [IsNoetherianRing Λ]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{max (u + 1) w} Λ)) : Prop

Tag 095E, a lemma

Tag 095E in the Stacks Project.

AlgebraicGeometry.isConstructibleFiniteSheaf_iff_exists_stratification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/GlobalStratification.lean, line 142. The attribute's comment: “finite sheaves, stratification”. References: SGA 4 IX (2.4), “(i)”.

Stacks 095E, sets and abelian groups: the equivalence of (1) and (3). On a quasi-compact quasi-separated scheme, a sheaf with values in a concrete category is constructible exactly when there is one finite partition of the whole scheme by constructible locally closed subschemes on each of which its inverse image is finite locally constant.

public theorem isConstructibleFiniteSheaf_iff_exists_stratification
    (F : Sheaf (SmallEtale.topology B X.obj X.property) D) :
    IsConstructibleFiniteSheaf B X F ↔
      ∃ s : ConstructibleStratification B X ⊤,
        ∀ i, Stacks.ConstantSheaf.IsFiniteLocallyConstant
          (SmallEtale.topology B (s.piece i).obj (s.piece i).property)
          (((smallEtaleBaseChange B (s.inclusion i)).sheafPullback D
            (SmallEtale.topology B X.obj X.property)
            (SmallEtale.topology B (s.piece i).obj (s.piece i).property)).obj F)

AlgebraicGeometry.isConstructibleModuleSheaf_iff_exists_stratification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/GlobalStratification.lean, line 188. The attribute's comment: “module sheaves, stratification”. References: SGA 4 IX (2.4), “(i), modules”.

Stacks 095E, modules: the equivalence of (1) and (3). On a quasi-compact quasi-separated scheme, a sheaf of modules over a commutative ring is constructible exactly when there is one finite partition of the whole scheme by constructible locally closed subschemes on each of which its inverse image is locally constant with finitely generated values.

public theorem isConstructibleModuleSheaf_iff_exists_stratification
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{w} R)) :
    IsConstructibleModuleSheaf B X R F ↔
      ∃ s : ConstructibleStratification B X ⊤,
        ∀ i, Stacks.ConstantSheaf.IsFiniteTypeLocallyConstant R
          (SmallEtale.topology B (s.piece i).obj (s.piece i).property)
          (((smallEtaleBaseChange B (s.inclusion i)).sheafPullback (ModuleCat.{w} R)
            (SmallEtale.topology B X.obj X.property)
            (SmallEtale.topology B (s.piece i).obj (s.piece i).property)).obj F)

AlgebraicGeometry.isConstructibleFiniteSheaf_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ZariskiLocal.lean, line 431. References: SGA 4 IX (2.4), “(i), (ii)”.

Stacks 095E for sheaves of sets and of abelian groups. For a sheaf on the small étale site of a quasi-compact quasi-separated scheme the following are equivalent: it is constructible; it is constructible after restriction to each member of some open cover; and there is one constructible stratification of the whole scheme on each stratum of which its inverse image is finite locally constant.

Finite local constancy is closed under isomorphism and stable under inverse image along an arbitrary morphism of small étale sites, by AlgebraicGeometry.isFiniteLocallyConstant_smallEtaleSheafPullback_of_overPost, which is Tag 093R, so AlgebraicGeometry.isStratifiedSheaf_tfae applies to it.

public theorem isConstructibleFiniteSheaf_tfae (Z : B.Scheme)
    [CompactSpace Z.obj] [QuasiSeparatedSpace Z.obj]
    (G : Sheaf (SmallEtale.topology B Z.obj Z.property) A) :
    List.TFAE
      [ IsConstructibleFiniteSheaf B Z G,
        ∃ (J : Type (u + 1)) (Y : J → B.Scheme) (g : ∀ j, Y j ⟶ Z),
          (∀ j, IsOpenImmersion (B.inclusion.map (g j))) ∧
          (Set.univ = ⋃ j, Set.range (B.inclusion.map (g j)).base) ∧
          ∀ j, IsConstructibleFiniteSheaf B (Y j)
            (((smallEtaleBaseChange B (g j)).sheafPullback A
              (SmallEtale.topology B Z.obj Z.property)
              (SmallEtale.topology B (Y j).obj (Y j).property)).obj G),
        ∃ s : ConstructibleStratification B Z ⊤, ∀ i,
          Stacks.ConstantSheaf.IsFiniteLocallyConstant (FD := FA) (CD := CA)
            (SmallEtale.topology B (s.piece i).obj (s.piece i).property)
            (((smallEtaleBaseChange B (s.inclusion i)).sheafPullback A
              (SmallEtale.topology B Z.obj Z.property)
              (SmallEtale.topology B (s.piece i).obj (s.piece i).property)).obj G) ]

AlgebraicGeometry.isConstructibleModuleSheaf_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ZariskiLocal.lean, line 483. References: SGA 4 IX (2.4), “special case”.

For a sheaf of modules over a Noetherian ring on the small étale site of a quasi-compact quasi-separated scheme the following are equivalent: it is constructible; it is constructible after restriction to each member of some open cover; and there is one constructible stratification of the whole scheme on each stratum of which its inverse image is locally constant with finitely generated values.

public theorem isConstructibleModuleSheaf_tfae (Z : B.Scheme)
    [CompactSpace Z.obj] [QuasiSeparatedSpace Z.obj]
    (G : Sheaf (SmallEtale.topology B Z.obj Z.property) (ModuleCat.{w} R)) :
    List.TFAE
      [ IsConstructibleModuleSheaf B Z R G,
        ∃ (J : Type (u + 1)) (Y : J → B.Scheme) (g : ∀ j, Y j ⟶ Z),
          (∀ j, IsOpenImmersion (B.inclusion.map (g j))) ∧
          (Set.univ = ⋃ j, Set.range (B.inclusion.map (g j)).base) ∧
          ∀ j, IsConstructibleModuleSheaf B (Y j) R
            (((smallEtaleBaseChange B (g j)).sheafPullback (ModuleCat.{w} R)
              (SmallEtale.topology B Z.obj Z.property)
              (SmallEtale.topology B (Y j).obj (Y j).property)).obj G),
        ∃ s : ConstructibleStratification B Z ⊤, ∀ i,
          Stacks.ConstantSheaf.IsFiniteTypeLocallyConstant R
            (SmallEtale.topology B (s.piece i).obj (s.piece i).property)
            (((smallEtaleBaseChange B (s.inclusion i)).sheafPullback (ModuleCat.{w} R)
              (SmallEtale.topology B Z.obj Z.property)
              (SmallEtale.topology B (s.piece i).obj (s.piece i).property)).obj G) ]

Tag 09YR, a lemma

Tag 09YR in the Stacks Project.

AlgebraicGeometry.isConstructibleFiniteSheaf_of_constructible_immersion_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ImmersionCover.lean, line 310. The attribute's comment: “sets and abelian groups”.

Stacks 09YR, for sheaves of sets and of abelian groups. On a quasi-compact quasi-separated scheme, a sheaf with values in a concrete category is constructible as soon as there are constructible locally closed subschemes covering the scheme on each of which its inverse image is constructible.

public theorem isConstructibleFiniteSheaf_of_constructible_immersion_cover
    (F : Sheaf (SmallEtale.topology B X.obj X.property) D)
    {I : Type*} (T : I → B.Scheme) (j : ∀ i, T i ⟶ X)
    (hj : ∀ i, IsImmersion (B.inclusion.map (j i)))
    (hc : ∀ i, Topology.IsConstructible (Set.range (B.inclusion.map (j i)).base))
    (hcover : (Set.univ : Set X.obj) = ⋃ i, Set.range (B.inclusion.map (j i)).base)
    (hF : ∀ i, IsConstructibleFiniteSheaf B (T i)
      (((smallEtaleBaseChange B (j i)).sheafPullback D
        (SmallEtale.topology B X.obj X.property)
        (SmallEtale.topology B (T i).obj (T i).property)).obj F)) :
    IsConstructibleFiniteSheaf B X F

AlgebraicGeometry.isConstructibleModuleSheaf_of_constructible_immersion_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ImmersionCover.lean, line 361. The attribute's comment: “modules over a Noetherian ring”.

Stacks 09YR, for sheaves of modules over a Noetherian ring. On a quasi-compact quasi-separated scheme, a sheaf of modules over a Noetherian ring is constructible as soon as there are constructible locally closed subschemes covering the scheme on each of which its inverse image is constructible.

public theorem isConstructibleModuleSheaf_of_constructible_immersion_cover
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{w} R))
    {I : Type*} (T : I → B.Scheme) (j : ∀ i, T i ⟶ X)
    (hj : ∀ i, IsImmersion (B.inclusion.map (j i)))
    (hc : ∀ i, Topology.IsConstructible (Set.range (B.inclusion.map (j i)).base))
    (hcover : (Set.univ : Set X.obj) = ⋃ i, Set.range (B.inclusion.map (j i)).base)
    (hF : ∀ i, IsConstructibleModuleSheaf B (T i) R
      (((smallEtaleBaseChange B (j i)).sheafPullback (ModuleCat.{w} R)
        (SmallEtale.topology B X.obj X.property)
        (SmallEtale.topology B (T i).obj (T i).property)).obj F)) :
    IsConstructibleModuleSheaf B X R F

Tag 095F, a lemma

Tag 095F in the Stacks Project.

AlgebraicGeometry.isConstructibleFiniteSheaf_of_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ZariskiDescent.lean, line 125. The attribute's comment: “sets and abelian groups”.

Stacks 095F for sheaves of sets and of abelian groups. Let X be a scheme covered by the images of open immersions U k ⟶ X. A sheaf with values in a concrete category whose restriction to every U k is constructible is constructible.

public theorem isConstructibleFiniteSheaf_of_openCover (X : B.Scheme)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) D)
    {I : Type*} (U : I → B.Scheme) (j : ∀ k, U k ⟶ X)
    (hj : ∀ k, IsOpenImmersion (B.inclusion.map (j k)))
    (hcover : Set.univ = ⋃ k, Set.range (B.inclusion.map (j k)).base)
    (hlocal : ∀ k, IsConstructibleFiniteSheaf B (U k)
      (((smallEtaleBaseChange B (j k)).sheafPullback D
        (SmallEtale.topology B X.obj X.property)
        (SmallEtale.topology B (U k).obj (U k).property)).obj F)) :
    IsConstructibleFiniteSheaf B X F

AlgebraicGeometry.isConstructibleModuleSheaf_of_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ZariskiDescent.lean, line 195. The attribute's comment: “modules over a Noetherian ring”.

Stacks 095F for sheaves of modules over a Noetherian ring. Let X be a scheme covered by the images of open immersions U k ⟶ X. A sheaf of modules over a Noetherian ring whose restriction to every U k is constructible is constructible.

public theorem isConstructibleModuleSheaf_of_openCover (X : B.Scheme)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{w} R))
    {I : Type*} (U : I → B.Scheme) (j : ∀ k, U k ⟶ X)
    (hj : ∀ k, IsOpenImmersion (B.inclusion.map (j k)))
    (hcover : Set.univ = ⋃ k, Set.range (B.inclusion.map (j k)).base)
    (hlocal : ∀ k, IsConstructibleModuleSheaf B (U k) R
      (((smallEtaleBaseChange B (j k)).sheafPullback (ModuleCat.{w} R)
        (SmallEtale.topology B X.obj X.property)
        (SmallEtale.topology B (U k).obj (U k).property)).obj F)) :
    IsConstructibleModuleSheaf B X R F

Declarations registered for the tag:

• AlgebraicGeometry.isConstructibleFiniteSheaf_iff_forall_restrict, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ZariskiLocalCriterionTag.lean, line 22 (StacksFrontier): “sets and abelian groups: constructible iff constructible on every member of any open covering”.
• AlgebraicGeometry.isConstructibleModuleSheaf_iff_forall_restrict, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ZariskiLocalCriterionTag.lean, line 26 (StacksFrontier): “Noetherian-ring modules: constructible iff constructible on every member of any open covering”.

Tag 095G, a lemma

Tag 095G in the Stacks Project.

AlgebraicGeometry.isConstructibleFiniteSheaf_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/InverseImage.lean, line 259. The attribute's comment: “sets and abelian groups”.

Stacks 095G for sheaves of sets and of abelian groups. The inverse image of a constructible sheaf with values in a concrete category along an arbitrary morphism of schemes is constructible.

public theorem isConstructibleFiniteSheaf_pullback {X Y : B.Scheme} (f : X ⟶ Y)
    (F : Sheaf (SmallEtale.topology B Y.obj Y.property) D)
    (hF : IsConstructibleFiniteSheaf B Y F) :
    IsConstructibleFiniteSheaf B X
      (((smallEtaleBaseChange B f).sheafPullback D
        (SmallEtale.topology B Y.obj Y.property)
        (SmallEtale.topology B X.obj X.property)).obj F)

AlgebraicGeometry.isConstructibleModuleSheaf_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/InverseImage.lean, line 302. The attribute's comment: “modules over a Noetherian ring”.

Stacks 095G for sheaves of modules over a Noetherian ring. The inverse image of a constructible sheaf of modules over a Noetherian ring along an arbitrary morphism of schemes is constructible.

public theorem isConstructibleModuleSheaf_pullback {X Y : B.Scheme} (f : X ⟶ Y)
    (F : Sheaf (SmallEtale.topology B Y.obj Y.property) (ModuleCat.{w} R))
    (hF : IsConstructibleModuleSheaf B Y R F) :
    IsConstructibleModuleSheaf B X R
      (((smallEtaleBaseChange B f).sheafPullback (ModuleCat.{w} R)
        (SmallEtale.topology B Y.obj Y.property)
        (SmallEtale.topology B X.obj X.property)).obj F)

Tag 03RZ, a lemma

Tag 03RZ in the Stacks Project.

AlgebraicGeometry.isConstructibleSetSheaf_limit_colimit_and_isWeakSerreClass_abelian_and_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/FiniteLimitsAndWeakSerre.lean, line 85. The attribute's comment: “the whole tag: part (1) finite limits and finite colimits of constructible sheaves of sets are constructible, part (2) the constructible abelian sheaves are a weak Serre subcategory, part (3) the constructible sheaves of modules over a Noetherian ring are a weak Serre subcategory. Unconditional: no hypothesis on the scheme and no instance the source does not name; part (3)'s ring is a Ring rather than a CommRing, which is more general than the source, and its Noetherian hypothesis is used by part (3) alone. The four component registrations are retained.”. References: SGA 4 IX (2.6).

Stacks 03RZ. Let X be a scheme of a big étale site and Λ a Noetherian ring. Then

1. a finite limit and a finite colimit of constructible sheaves of sets on the small étale site of X are constructible;
2. the constructible abelian sheaves on that site form a weak Serre subcategory of all abelian sheaves on it; and
3. the constructible sheaves of Λ-modules on that site form a weak Serre subcategory of all sheaves of Λ-modules on it.

This is the whole tag in one statement, under no hypothesis on X and none on Λ beyond the source's own Noetherianness, which part (3) alone uses. Each part is proved by the theorem that states it alone: AlgebraicGeometry.isConstructibleSetSheaf_limit and AlgebraicGeometry.isConstructibleSetSheaf_colimit for part (1), AlgebraicGeometry.constructibleAbelianSheaf_isWeakSerreClass for part (2), and AlgebraicGeometry.SmallEtale.isWeakSerreClass_isConstructibleModuleSheaf for part (3). Those four registrations are retained, each stating its own part.

The three parts are independent facts and not a chain: part (1) is about sheaves of sets and is not used for parts (2) and (3), which reduce to Tag 093U (2) and Tag 093U (3) respectively, so the conjunction asserts strictly more than any one of them.

public theorem isConstructibleSetSheaf_limit_colimit_and_isWeakSerreClass_abelian_and_module
    (B : BigEtaleSite.{u}) (X : B.Scheme) (Λ : Type r) [Ring Λ] [IsNoetherianRing Λ] :
    (∀ (I : Type v) [SmallCategory I] [FinCategory I]
        (F : I ⥤ Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1))),
        (∀ i, IsConstructibleSetSheaf B X (F.obj i)) →
          IsConstructibleSetSheaf B X (limit F) ∧
            IsConstructibleSetSheaf B X (colimit F)) ∧
      ObjectProperty.IsWeakSerreClass
        (fun F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1} =>
          IsConstructibleAbelianSheaf B X F) ∧
      ObjectProperty.IsWeakSerreClass
        (fun F : Sheaf (SmallEtale.topology B X.obj X.property)
          (ModuleCat.{max (u + 1) w} Λ) => IsConstructibleModuleSheaf B X Λ F)

AlgebraicGeometry.isConstructibleSetSheaf_limit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/FiniteLimitsSets.lean, line 135. The attribute's comment: “constructible_sets_finite_limits_colimits”. References: SGA 4 IX (2.6), “(i bis) finite limits”.

Stacks 03RZ for sheaves of sets, finite limits. A finite limit of constructible sheaves of sets on the small étale site of a scheme is constructible.

public theorem isConstructibleSetSheaf_limit
    (F : I ⥤ Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1)))
    (hF : ∀ i, IsConstructibleSetSheaf B X (F.obj i)) :
    IsConstructibleSetSheaf B X (limit F)

AlgebraicGeometry.isConstructibleSetSheaf_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/FiniteLimitsSets.lean, line 148. The attribute's comment: “constructible_sets_finite_limits_colimits”. References: SGA 4 IX (2.6), “(i bis) finite colimits”.

Stacks 03RZ for sheaves of sets, finite colimits. A finite colimit of constructible sheaves of sets on the small étale site of a scheme is constructible.

public theorem isConstructibleSetSheaf_colimit
    (F : I ⥤ Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1)))
    (hF : ∀ i, IsConstructibleSetSheaf B X (F.obj i)) :
    IsConstructibleSetSheaf B X (colimit F)

AlgebraicGeometry.SmallEtale.isWeakSerreClass_isConstructibleModuleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/FiniteLimitsSets.lean, line 213. The attribute's comment: “constructible_modules_weak_serre”. References: SGA 4 IX (2.6).

Stacks 03RZ (3). For Λ a Noetherian ring, the constructible sheaves of Λ-modules on the small étale site of a scheme form a weak Serre subcategory of all sheaves of Λ-modules on that site. There is no hypothesis on the scheme.

The proof is the five term form of the weak Serre condition, CategoryTheory.ObjectProperty.isWeakSerreClass_iff_prop_obj₂_of_exact. Given an exact ℱ₀ ⟶ ℱ₁ ⟶ ℱ₂ ⟶ ℱ₃ ⟶ ℱ₄ with the four outer terms constructible, fix an affine open and stratify all four of them on one constructible stratification of it with AlgebraicGeometry.exists_stratification_isStratifiedSheaf_forall. Inverse image to a stratum is exact by AlgebraicGeometry.preservesFiniteLimits_smallEtaleSheafPullback_moduleCat, so the restricted five term sequence is still exact, and on a stratum constructibility is local constancy of finite type, which is a weak Serre condition by Tag 093U (3). Hence the restriction of ℱ₂ to each stratum is locally constant of finite type, which is constructibility of ℱ₂.

public theorem SmallEtale.isWeakSerreClass_isConstructibleModuleSheaf :
    ObjectProperty.IsWeakSerreClass
      (fun F : Sheaf (SmallEtale.topology B X.obj X.property)
        (ModuleCat.{max (u + 1) w} Λ) => IsConstructibleModuleSheaf B X Λ F)

AlgebraicGeometry.constructibleAbelianSheaf_isWeakSerreClass, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/WeakSerreAbelian.lean, line 213. The attribute's comment: “constructible_abelian_weak_serre”. References: SGA 4 IX (2.6), “(ii)+ker/coker abelian”.

Stacks 03RZ for abelian sheaves. The constructible sheaves of abelian groups on the small étale site of a scheme form a weak Serre subcategory of all abelian sheaves on that site.

public instance constructibleAbelianSheaf_isWeakSerreClass :
    ObjectProperty.IsWeakSerreClass
      (fun F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1} =>
        IsConstructibleAbelianSheaf B X F)

Tag 09YS, a lemma

Tag 09YS in the Stacks Project.

AlgebraicGeometry.isConstructible_setOf_surjective_etaleStalk_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StalkLocus.lean, line 385. The attribute's comment: “part (1), surjectivity”.

Stacks 09YS, part (1), surjectivity. Let X be a quasi-compact quasi-separated scheme. For a map of constructible sheaves of sets on the small étale site of X, the set of points of X at which the induced map of geometric stalks is surjective is constructible.

public theorem isConstructible_setOf_surjective_etaleStalk_map
    (X : B.Scheme) [CompactSpace X.obj] [QuasiSeparatedSpace X.obj]
    {F G : Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1))} (φ : F ⟶ G)
    (hF : IsConstructibleSetSheaf B X F) (hG : IsConstructibleSetSheaf B X G) :
    IsConstructible {x : X.obj | ∃ t : GeometricPoint X.obj, t.LiesOver x ∧
      Function.Surjective
        ((etaleStalkPresheafFunctor B X.obj X.property t (Type (u + 1))).map φ.hom)}

AlgebraicGeometry.isConstructible_setOf_injective_etaleStalk_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StalkLocus.lean, line 400. The attribute's comment: “part (1), injectivity”.

Stacks 09YS, part (1), injectivity. Let X be a quasi-compact quasi-separated scheme. For a map of constructible sheaves of sets on the small étale site of X, the set of points of X at which the induced map of geometric stalks is injective is constructible.

public theorem isConstructible_setOf_injective_etaleStalk_map
    (X : B.Scheme) [CompactSpace X.obj] [QuasiSeparatedSpace X.obj]
    {F G : Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1))} (φ : F ⟶ G)
    (hF : IsConstructibleSetSheaf B X F) (hG : IsConstructibleSetSheaf B X G) :
    IsConstructible {x : X.obj | ∃ t : GeometricPoint X.obj, t.LiesOver x ∧
      Function.Injective
        ((etaleStalkPresheafFunctor B X.obj X.property t (Type (u + 1))).map φ.hom)}

AlgebraicGeometry.isConstructible_setOf_etaleStalk_map_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StalkLocus.lean, line 416. The attribute's comment: “part (1), isomorphic to a given map of sets”.

Stacks 09YS, part (1), prescribed isomorphism class. Let X be a quasi-compact quasi-separated scheme and let m₀ be a map of sets. For a map of constructible sheaves of sets on the small étale site of X, the set of points of X at which the induced map of geometric stalks is isomorphic to m₀ is constructible.

public theorem isConstructible_setOf_etaleStalk_map_iso {A₀ : Type v} {C₀ : Type w}
    (m₀ : A₀ → C₀) (X : B.Scheme) [CompactSpace X.obj] [QuasiSeparatedSpace X.obj]
    {F G : Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1))} (φ : F ⟶ G)
    (hF : IsConstructibleSetSheaf B X F) (hG : IsConstructibleSetSheaf B X G) :
    IsConstructible {x : X.obj | ∃ t : GeometricPoint X.obj, t.LiesOver x ∧
      ∃ (b : (etaleStalkPresheafFunctor B X.obj X.property t (Type (u + 1))).obj F.obj ≃ A₀)
        (d : (etaleStalkPresheafFunctor B X.obj X.property t (Type (u + 1))).obj G.obj ≃ C₀),
        ∀ z, d ((etaleStalkPresheafFunctor B X.obj X.property t (Type (u + 1))).map φ.hom z) =
          m₀ (b z)}

AlgebraicGeometry.isConstructible_supportSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StalkLocus.lean, line 541. The attribute's comment: “part (2)”.

Stacks 09YS, part (2). Let X be a quasi-compact quasi-separated scheme. The support of a constructible abelian sheaf on the small étale site of X is constructible.

public theorem isConstructible_supportSheaf (B : BigEtaleSite.{u}) (X : B.Scheme)
    [CompactSpace X.obj] [QuasiSeparatedSpace X.obj] [UnivLE.{u, w}]
    [∀ (Z : B.Scheme) (V : SmallEtale B Z.obj Z.property),
      HasWeakSheafify ((SmallEtale.topology B Z.obj Z.property).over V) AddCommGrpCat.{w}]
    [∀ (Z : B.Scheme) (V : SmallEtale B Z.obj Z.property),
      ((SmallEtale.topology B Z.obj Z.property).over V).WEqualsLocallyBijective
        AddCommGrpCat.{w}]
    [∀ (Y Z : B.Scheme) (f : Z ⟶ Y),
      ((smallEtaleBaseChange B f).sheafPushforwardContinuous AddCommGrpCat.{w}
        (SmallEtale.topology B Y.obj Y.property)
        (SmallEtale.topology B Z.obj Z.property)).IsRightAdjoint]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{w})
    (hF : IsConstructibleAbelianSheaf B X F) :
    IsConstructible (supportSheaf B X.obj X.property F)

AlgebraicGeometry.isConstructible_support_moduleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StalkLocus.lean, line 573. The attribute's comment: “part (3)”.

Stacks 09YS, part (3). Let X be a quasi-compact quasi-separated scheme and let Λ be a Noetherian ring. The support of a constructible sheaf of Λ-modules on the small étale site of X — the set of points carrying a nonzero geometric stalk — is constructible.

public theorem isConstructible_support_moduleSheaf (B : BigEtaleSite.{u}) (X : B.Scheme)
    [CompactSpace X.obj] [QuasiSeparatedSpace X.obj] (Λ : Type r) [CommRing Λ]
    [IsNoetherianRing Λ] [UnivLE.{u, w}]
    [PreservesFilteredColimitsOfSize.{max u w, max u w} (forget (ModuleCat.{max u w} Λ))]
    [∀ (Z : B.Scheme) (V : SmallEtale B Z.obj Z.property),
      HasWeakSheafify ((SmallEtale.topology B Z.obj Z.property).over V) (ModuleCat.{max u w} Λ)]
    [∀ (Z : B.Scheme) (V : SmallEtale B Z.obj Z.property),
      ((SmallEtale.topology B Z.obj Z.property).over V).WEqualsLocallyBijective
        (ModuleCat.{max u w} Λ)]
    [∀ (Y Z : B.Scheme) (f : Z ⟶ Y),
      ((smallEtaleBaseChange B f).sheafPushforwardContinuous (ModuleCat.{max u w} Λ)
        (SmallEtale.topology B Y.obj Y.property)
        (SmallEtale.topology B Z.obj Z.property)).IsRightAdjoint]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{max u w} Λ))
    (hF : IsConstructibleModuleSheaf B X Λ F) :
    IsConstructible {x : X.obj | ∃ t : GeometricPoint X.obj, t.LiesOver x ∧
      ¬ IsZero (etaleStalk B X.obj X.property t F.obj)}

AlgebraicGeometry.isConstructible_etaleStalk_map_loci_and_supports, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StalkLocusLociAndSupports.lean, line 68. The attribute's comment: “parts (1), (2) and (3), as the conjunction of the three constructibility claims”.

Stacks 09YS. Let X be a quasi-compact quasi-separated scheme.

1. For a map φ : F ⟶ G of constructible sheaves of sets on the small étale site of X, each of the three sets of points of X at which the induced map of geometric stalks is surjective, is injective, or is isomorphic to a prescribed map of sets m₀, is constructible.
2. The support of a constructible abelian sheaf on the small étale site of X is constructible.
3. For Λ a Noetherian ring, the support of a constructible sheaf of Λ-modules on the small étale site of X is constructible.

Sheaves of sets have values in the universe u + 1 of the site; abelian sheaves, resp. sheaves of Λ-modules for Λ : Type r, have values in any universe containing that of the site, resp. that of the site and of Λ. The statement has no hypothesis beyond the source's: every coefficient condition the general parts isConstructible_supportSheaf and isConstructible_support_moduleSheaf assume is proved at these universes inside the proof.

Part (1) is isConstructible_setOf_surjective_etaleStalk_map, isConstructible_setOf_injective_etaleStalk_map and isConstructible_setOf_etaleStalk_map_iso, part (2) is isConstructible_supportSheaf and part (3) is isConstructible_support_moduleSheaf.

public theorem isConstructible_etaleStalk_map_loci_and_supports (B : BigEtaleSite.{u})
    (X : B.Scheme) [CompactSpace X.obj] [QuasiSeparatedSpace X.obj] :
    (∀ (F G : Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1))) (φ : F ⟶ G),
        IsConstructibleSetSheaf B X F → IsConstructibleSetSheaf B X G →
        IsConstructible {x : X.obj | ∃ t : GeometricPoint X.obj, t.LiesOver x ∧
            Function.Surjective
              ((etaleStalkPresheafFunctor B X.obj X.property t (Type (u + 1))).map φ.hom)} ∧
          IsConstructible {x : X.obj | ∃ t : GeometricPoint X.obj, t.LiesOver x ∧
            Function.Injective
              ((etaleStalkPresheafFunctor B X.obj X.property t (Type (u + 1))).map φ.hom)} ∧
          ∀ (A₀ : Type v) (C₀ : Type w₀) (m₀ : A₀ → C₀),
            IsConstructible {x : X.obj | ∃ t : GeometricPoint X.obj, t.LiesOver x ∧
              ∃ (b : (etaleStalkPresheafFunctor B X.obj X.property t
                  (Type (u + 1))).obj F.obj ≃ A₀)
                (d : (etaleStalkPresheafFunctor B X.obj X.property t
                  (Type (u + 1))).obj G.obj ≃ C₀),
                ∀ z, d ((etaleStalkPresheafFunctor B X.obj X.property t
                  (Type (u + 1))).map φ.hom z) = m₀ (b z)}) ∧
      (∀ F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{max (u + 1) w},
          IsConstructibleAbelianSheaf B X F →
            IsConstructible (supportSheaf B X.obj X.property F)) ∧
      ∀ (Λ : Type r) [CommRing Λ] [IsNoetherianRing Λ]
        (F : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{max (u + 1) r w} Λ)),
        IsConstructibleModuleSheaf B X Λ F →
          IsConstructible {x : X.obj | ∃ t : GeometricPoint X.obj, t.LiesOver x ∧
            ¬ IsZero (etaleStalk B X.obj X.property t F.obj)}

Tag 095P, a lemma

Tag 095P in the Stacks Project.

AlgebraicGeometry.exists_isEssentiallyConstantWith_of_isConstructibleAbelianSheaf_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/AbelianEssentiallyConstantColimit.lean, line 109. The attribute's comment: “part (2), sheaves of abelian groups”.

Stacks 095P, part (2). Let X be a quasi-compact quasi-separated scheme and let F = colim_{i ∈ I} F_i be a filtered colimit of abelian sheaves on X_étale. If F and all the F_i are constructible, then the ind-object F_i is essentially constant with value F.

Nothing is assumed. Abelian groups are ULift ℤ-modules, a ring which is Noetherian and lives in the coefficient universe, so the system is carried to one of sheaves of modules by AlgebraicGeometry.isConstructibleModuleSheaf_uliftIntEquivalence, part (3) of the tag applies to it with nothing assumed, and the witness is brought back along the equivalence of sheaf categories, which preserves the colimit and is fully faithful.

public theorem exists_isEssentiallyConstantWith_of_isConstructibleAbelianSheaf_colimit
    (X : B.Scheme) [CompactSpace X.1] [QuasiSeparatedSpace X.1]
    {I : Type v} [Category.{v'} I] [IsFiltered I] [EssentiallySmall.{u + 1} I]
    (F : I ⥤ Sheaf (SmallEtale.topology B X.1 X.property) AddCommGrpCat.{u + 1})
    (t : Cocone F) (ht : IsColimit t)
    (hF : ∀ i, IsConstructibleAbelianSheaf B X (F.obj i))
    (hcolim : IsConstructibleAbelianSheaf B X t.pt) :
    ∃ (i : I) (r : t.pt ⟶ F.obj i),
      EssentiallyConstantInd.IsEssentiallyConstantWith F t i r

AlgebraicGeometry.isEssentiallyConstantWith_of_isConstructibleAbelianSheaf_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/EssentiallyConstantColimit.lean, line 126. The attribute's comment: “part (2), sheaves of abelian groups”.

Stacks 095P, part (2). Let X be a quasi-compact quasi-separated scheme and let F = colim_{i ∈ I} F_i be a filtered colimit of abelian sheaves on X_étale. If F and all the F_i are constructible, then the ind-object F_i is essentially constant with value F.

Nothing beyond the instance hypotheses is assumed: the input of the sheaves-of-abelian-groups case of Stacks 09Z4, Stacks 095N for ℤ-modules, is AlgebraicGeometry.hasFiniteShriekPresentation_of_isConstructibleModuleSheaf_int.

public theorem isEssentiallyConstantWith_of_isConstructibleAbelianSheaf_colimit
    (B : BigEtaleSite.{u}) (X : B.Scheme) [CompactSpace X.1] [QuasiSeparatedSpace X.1]
    [∀ (S T : B.Scheme) (f : T ⟶ S),
      ((smallEtaleBaseChange B f).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
        (SmallEtale.topology B S.1 S.property)
        (SmallEtale.topology B T.1 T.property)).IsRightAdjoint]
    [∀ (T : B.Scheme) (V : SmallEtale B T.1 T.property),
      HasWeakSheafify ((SmallEtale.topology B T.1 T.property).over V) AddCommGrpCat.{u + 1}]
    [∀ (S T : B.Scheme) (f : T ⟶ S),
      ((smallEtaleBaseChange B f).sheafPushforwardContinuous (ModuleCat.{u + 1} ℤ)
        (SmallEtale.topology B S.1 S.property)
        (SmallEtale.topology B T.1 T.property)).IsRightAdjoint]
    [∀ (T : B.Scheme) (V : SmallEtale B T.1 T.property),
      HasWeakSheafify ((SmallEtale.topology B T.1 T.property).over V) (ModuleCat.{u + 1} ℤ)]
    {I : Type v} [Category.{v'} I] [IsFiltered I] [EssentiallySmall.{u + 1} I]
    (F : I ⥤ Sheaf (SmallEtale.topology B X.1 X.property) AddCommGrpCat.{u + 1})
    (t : Cocone F) (ht : IsColimit t)
    (hF : ∀ i, IsConstructibleAbelianSheaf B X (F.obj i))
    (hcolim : IsConstructibleAbelianSheaf B X t.pt) :
    ∃ (i : I) (r : t.pt ⟶ F.obj i),
      EssentiallyConstantInd.IsEssentiallyConstantWith F t i r

AlgebraicGeometry.exists_isEssentiallyConstantWith_of_isConstructibleModuleSheaf_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ModuleEssentiallyConstantColimit.lean, line 43. The attribute's comment: “part (3), with 095N discharged”.

Let X be a quasi-compact quasi-separated scheme, let Λ be a Noetherian ring, and let F = colim_{i ∈ I} F_i be a filtered colimit of sheaves of Λ-modules on X_étale. If F and all the F_i are constructible, then the ind-object F_i is essentially constant with value F.

public theorem exists_isEssentiallyConstantWith_of_isConstructibleModuleSheaf_colimit
    (B : BigEtaleSite.{u}) (X : B.Scheme) (R : Type (u + 1)) [CommRing R] [IsNoetherianRing R]
    [CompactSpace X.1] [QuasiSeparatedSpace X.1]
    [∀ (S T : B.Scheme) (f : T ⟶ S),
      ((smallEtaleBaseChange B f).sheafPushforwardContinuous (ModuleCat.{u + 1} R)
        (SmallEtale.topology B S.1 S.property)
        (SmallEtale.topology B T.1 T.property)).IsRightAdjoint]
    [∀ (T : B.Scheme) (V : SmallEtale B T.1 T.property),
      HasWeakSheafify ((SmallEtale.topology B T.1 T.property).over V) (ModuleCat.{u + 1} R)]
    {I : Type v} [Category.{v'} I] [IsFiltered I] [EssentiallySmall.{u + 1} I]
    (F : I ⥤ Sheaf (SmallEtale.topology B X.1 X.property) (ModuleCat.{u + 1} R))
    (t : Cocone F) (ht : IsColimit t)
    (hF : ∀ i, IsConstructibleModuleSheaf B X R (F.obj i))
    (hcolim : IsConstructibleModuleSheaf B X R t.pt) :
    ∃ (i : I) (r : t.pt ⟶ F.obj i),
      EssentiallyConstantInd.IsEssentiallyConstantWith F t i r

AlgebraicGeometry.exists_isEssentiallyConstantWith_of_isConstructibleSetSheaf_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/SetEssentiallyConstantColimit.lean, line 45. The attribute's comment: “part (1), sheaves of sets”.

Let X be a quasi-compact quasi-separated scheme and let F = colim_{i ∈ I} F_i be a filtered colimit of sheaves of sets on X_étale. If F and all the F_i are constructible, then the ind-object F_i is essentially constant with value F.

public theorem exists_isEssentiallyConstantWith_of_isConstructibleSetSheaf_colimit
    (B : BigEtaleSite.{u}) (X : B.Scheme) [CompactSpace X.1] [QuasiSeparatedSpace X.1]
    {I : Type v} [Category.{v'} I] [IsFiltered I] [EssentiallySmall.{u + 1} I]
    (F : I ⥤ Sheaf (SmallEtale.topology B X.1 X.property) (Type (u + 1)))
    (t : Cocone F) (ht : IsColimit t)
    (hF : ∀ i, IsConstructibleSetSheaf B X (F.obj i))
    (hcolim : IsConstructibleSetSheaf B X t.pt) :
    ∃ (i : I) (r : t.pt ⟶ F.obj i),
      EssentiallyConstantInd.IsEssentiallyConstantWith F t i r

AlgebraicGeometry.exists_isEssentiallyConstantWith_of_isConstructibleModuleSheaf_colimit', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ShrinkCoefficients.lean, line 298. The attribute's comment: “part (3), for a Noetherian coefficient ring in any universe”.

Stacks 095P, part (3), for a coefficient ring in any universe. A filtered colimit of constructible sheaves of R-modules whose value is constructible is essentially constant as an ind-object.

The cocone is carried to Shrink.{u + 1} R-modules by the equivalence of sheaf categories, which preserves the colimit, and the witness found there is brought back by CategoryTheory.EssentiallyConstantInd.IsEssentiallyConstantWith.of_equivalence.

public theorem exists_isEssentiallyConstantWith_of_isConstructibleModuleSheaf_colimit'
    [IsNoetherianRing R] [CompactSpace X.1] [QuasiSeparatedSpace X.1]
    {I : Type v} [Category.{v₀} I] [IsFiltered I] [EssentiallySmall.{u + 1} I]
    (F : I ⥤ Sheaf (SmallEtale.topology B X.1 X.property) (ModuleCat.{u + 1} R))
    (t : Cocone F) (ht : IsColimit t)
    (hF : ∀ i, IsConstructibleModuleSheaf B X R (F.obj i))
    (hcolim : IsConstructibleModuleSheaf B X R t.pt) :
    ∃ (i : I) (r : t.pt ⟶ F.obj i),
      EssentiallyConstantInd.IsEssentiallyConstantWith F t i r

Tag 095I, a lemma

Tag 095I in the Stacks Project.

AlgebraicGeometry.isConstructibleModuleEtaleSheaf_tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/TensorProduct.lean, line 55.

Stacks 095I. Let X be a scheme and Λ a Noetherian ring. The tensor product of two constructible sheaves of Λ-modules on X_étale is a constructible sheaf of Λ-modules.

public theorem isConstructibleModuleEtaleSheaf_tensor (B : BigEtaleSite.{u}) (X : B.Scheme)
    (Λ : Type (max (u + 1) w)) [CommRing Λ] [IsNoetherianRing Λ]
    (F G : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{max (u + 1) w} Λ))
    (hF : IsConstructibleModuleEtaleSheaf B X Λ F) (hG : IsConstructibleModuleEtaleSheaf B X Λ G) :
    IsConstructibleModuleEtaleSheaf B X Λ (F ⊗ G)

Stacks.EtaleCohomology.isConstructibleModuleSheaf_tensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleSheaves/TensorProduct.lean, line 111.

Stacks 095I. The tensor product of two constructible sheaves of Λ-modules on the small étale site of a scheme, for Λ a Noetherian ring, is a constructible sheaf of Λ-modules.

theorem isConstructibleModuleSheaf_tensor (B : BigEtaleSite.{u}) (X : B.Scheme)
    (Λ : Type (max (u + 1) w)) [CommRing Λ] [IsNoetherianRing Λ]
    [∀ (S T : B.Scheme) (f : T ⟶ S),
      ((smallEtaleBaseChange B f).sheafPushforwardContinuous (ModuleCat.{max (u + 1) w} Λ)
        (SmallEtale.topology B S.obj S.property)
        (SmallEtale.topology B T.obj T.property)).IsRightAdjoint]
    (F G : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{max (u + 1) w} Λ))
    (hF : IsConstructibleModuleSheaf B X Λ F) (hG : IsConstructibleModuleSheaf B X Λ G) :
    IsConstructibleModuleSheaf B X Λ (F ⊗ G)

Tag 0GKB, a lemma

Tag 0GKB in the Stacks Project.

Stacks.EtaleCohomology.isConstructibleModuleSheaf_extendScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleSheaves/ExtensionOfScalars.lean, line 209.

Extension of scalars along a homomorphism of Noetherian rings preserves constructibility on the small étale site.

public theorem isConstructibleModuleSheaf_extendScalars
    (B : BigEtaleSite.{u}) (X : B.Scheme)
    (R : Type r) (S : Type s) [CommRing R] [CommRing S]
    [IsNoetherianRing R] [IsNoetherianRing S] (f : R →+* S)
    [HasWeakSheafify (SmallEtale.topology B X.1 X.property)
      (ModuleCat.{max r s w} S)]
    [∀ (A T : B.Scheme) (g : T ⟶ A),
      ((smallEtaleBaseChange B g).sheafPushforwardContinuous
        (ModuleCat.{max r s w} R)
        (SmallEtale.topology B A.1 A.property)
        (SmallEtale.topology B T.1 T.property)).IsRightAdjoint]
    [∀ (T : B.Scheme) (V : SmallEtale B T.1 T.property),
      HasWeakSheafify ((SmallEtale.topology B T.1 T.property).over V)
        (ModuleCat.{max r s w} R)]
    [∀ (A T : B.Scheme) (g : T ⟶ A),
      ((smallEtaleBaseChange B g).sheafPushforwardContinuous
        (ModuleCat.{max r s w} S)
        (SmallEtale.topology B A.1 A.property)
        (SmallEtale.topology B T.1 T.property)).IsRightAdjoint]
    [∀ (T : B.Scheme) (V : SmallEtale B T.1 T.property),
      HasWeakSheafify ((SmallEtale.topology B T.1 T.property).over V)
        (ModuleCat.{max r s w} S)]
    (F : Sheaf (SmallEtale.topology B X.1 X.property)
      (ModuleCat.{max r s w} R))
    (hF : IsConstructibleModuleSheaf B X R F) :
    IsConstructibleModuleSheaf B X S
      ((extendScalarsSheaf (SmallEtale.topology B X.1 X.property) R S f).obj F)

AlgebraicGeometry.SmallEtale.isConstructibleModuleSheaf_extendScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/ConstructibleExtendScalars.lean, line 279.

Stacks 0GKB. Extension of scalars along a homomorphism of Noetherian rings preserves constructibility of a sheaf of modules on the small étale site.

public theorem isConstructibleModuleSheaf_extendScalars
    (B : BigEtaleSite.{u}) (X : B.Scheme)
    (R : Type r) (S : Type s) [CommRing R] [CommRing S]
    [IsNoetherianRing R] [IsNoetherianRing S] (f : R →+* S)
    [HasWeakSheafify (SmallEtale.topology B X.obj X.property)
      (ModuleCat.{max r s w} S)]
    [∀ (A T : B.Scheme) (g : T ⟶ A),
      ((smallEtaleBaseChange B g).sheafPushforwardContinuous
        (ModuleCat.{max r s w} R)
        (SmallEtale.topology B A.obj A.property)
        (SmallEtale.topology B T.obj T.property)).IsRightAdjoint]
    [∀ (T : B.Scheme) (V : SmallEtale B T.obj T.property),
      HasWeakSheafify ((SmallEtale.topology B T.obj T.property).over V)
        (ModuleCat.{max r s w} R)]
    [∀ (A T : B.Scheme) (g : T ⟶ A),
      ((smallEtaleBaseChange B g).sheafPushforwardContinuous
        (ModuleCat.{max r s w} S)
        (SmallEtale.topology B A.obj A.property)
        (SmallEtale.topology B T.obj T.property)).IsRightAdjoint]
    [∀ (T : B.Scheme) (V : SmallEtale B T.obj T.property),
      HasWeakSheafify ((SmallEtale.topology B T.obj T.property).over V)
        (ModuleCat.{max r s w} S)]
    (F : Sheaf (SmallEtale.topology B X.obj X.property)
      (ModuleCat.{max r s w} R))
    (hF : IsConstructibleModuleSheaf B X R F) :
    IsConstructibleModuleSheaf B X S
      ((Sheaf.composeAndSheafify (SmallEtale.topology B X.obj X.property)
        (ModuleCat.extendScalars.{r, s, max r s w} f)).obj F)

Sources

• Section 59.71, Tag 05BE
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.IsConstructibleSetSheaf · AlgebraicGeometry.IsConstructibleAbelianSheaf · AlgebraicGeometry.IsConstructibleModuleSheaf · AlgebraicGeometry.IsConstructibleAbelianEtaleSheaf · AlgebraicGeometry.IsConstructibleModuleEtaleSheaf · AlgebraicGeometry.isConstructibleFiniteSheaf_iff_exists_stratification · AlgebraicGeometry.isConstructibleModuleSheaf_iff_exists_stratification · AlgebraicGeometry.isConstructibleFiniteSheaf_tfae

Section59.72 Auxiliary lemmas on morphisms#

Section 59.72 of the Stacks Project, Tag 095J. 3 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03S0, a lemma

Tag 03S0 in the Stacks Project.

AlgebraicGeometry.exists_constructible_partition_finite_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/FiniteEtaleStratification.lean, line 574.

Let f : U ⟶ X be an étale morphism of quasi-compact and quasi-separated schemes. Then X has a partition into constructible locally closed subschemes over each of which the base change of f is finite étale.

public theorem exists_constructible_partition_finite_etale
    {U X : Scheme.{u}} [CompactSpace U] [QuasiSeparatedSpace U]
    [CompactSpace X] [QuasiSeparatedSpace X] (f : U ⟶ X) [Etale f] :
    ∃ P : Set (Set X), IsTopologicalPartition P ∧
      (∀ S ∈ P, Topology.IsConstructible S) ∧
      (∀ S ∈ P, ∃ (Y : Scheme.{u}) (i : Y ⟶ X),
        IsImmersion i ∧ Set.range i.base = S ∧
          IsFinite (pullback.fst i f) ∧ Etale (pullback.fst i f))

Tag 03S1, a lemma

Tag 03S1 in the Stacks Project.

AlgebraicGeometry.finite_preimage_singleton_iff_exists_affine_open_isFinite_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/GenericallyFinite.lean, line 513. The attribute's comment: “forward direction over an affine open”.

Stacks Project, Tag 02NW, condition (4). For a quasi-compact and quasi-separated morphism locally of finite type, finiteness of the fibre over a generic point of an irreducible component is equivalent to finiteness over some affine neighbourhood of the point.

theorem finite_preimage_singleton_iff_exists_affine_open_isFinite_restrict
    {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [QuasiCompact f]
    [QuasiSeparated f] (η : Y) (hη : η ∈ genericPoints Y) :
    (f ⁻¹' {η}).Finite ↔
      ∃ V : Y.affineOpens, (η ∈ V.1) ∧ IsFinite (f ∣_ V.1)

Tag 095K, a lemma

Tag 095K in the Stacks Project.

AlgebraicGeometry.exists_finite_affine_stratification_split_reduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/BaseChangeDecomposition.lean, line 2088. The attribute's comment: “part (2)”.

A finite locally free cover of each affine stratum splits the reduced pullback into finitely many copies of the reduced covering scheme.

public theorem exists_finite_affine_stratification_split_reduction
    {Y X : Scheme.{u}} (f : Y ⟶ X) [IsAffine Y] [IsAffine X]
    [LocallyOfFiniteType f] [QuasiCompact f] [LocallyQuasiFinite f]
    (hfp : FinitePresentation f) :
    ∃ (n : ℕ) (S : Fin n → Scheme.{u}) (s : ∀ i, S i ⟶ X),
      (∀ i, IsAffine (S i) ∧ IsImmersion (s i) ∧
        IsLocallyClosed (Set.range (s i).base) ∧
        Topology.IsConstructible (Set.range (s i).base)) ∧
      (∀ i j, i ≠ j → Disjoint (Set.range (s i).base) (Set.range (s j).base)) ∧
      (⋃ i, Set.range (s i).base) = Set.univ ∧
      ∀ i, ∃ (S' : Scheme.{u}) (g : S' ⟶ S i),
        Surjective g ∧ Stacks.Morphisms.IsFiniteLocallyFree g ∧
        ∃ (m : ℕ)
          (q : (pullback f (g ≫ s i)).nilradical.subscheme ⟶
            S'.nilradical.subscheme)
          (e : (pullback f (g ≫ s i)).nilradical.subscheme ≅
            ∐ (fun _ : Fin m ↦ S'.nilradical.subscheme)),
          q ≫ S'.nilradical.subschemeι =
              (pullback f (g ≫ s i)).nilradical.subschemeι ≫
                pullback.snd f (g ≫ s i) ∧
          e.hom ≫ Sigma.desc (fun _ : Fin m ↦ 𝟙 S'.nilradical.subscheme) = q

AlgebraicGeometry.exists_surjective_affine_baseChange_thickening_finiteEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/QuasiFinite/BaseChangeDecomposition.lean, line 2150. The attribute's comment: “part (1)”.

After a surjective affine base change, the pullback contains a finite étale thickening.

public theorem exists_surjective_affine_baseChange_thickening_finiteEtale
    {Y X : Scheme.{u}} (f : Y ⟶ X) [IsAffine Y] [IsAffine X]
    [LocallyOfFiniteType f] [QuasiCompact f] [LocallyQuasiFinite f]
    (hfp : FinitePresentation f) :
    ∃ (X' : Scheme.{u}) (_ : IsAffine X') (g : X' ⟶ X),
      Surjective g ∧
      ∃ (Z' : Scheme.{u}) (i : Z' ⟶ pullback f g),
        Stacks.Thickenings.IsThickening i ∧
        IsFinite (i ≫ pullback.snd f g) ∧
        Etale (i ≫ pullback.snd f g)

Sources

• Section 59.72, Tag 095J
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.exists_constructible_partition_finite_etale · AlgebraicGeometry.finite_preimage_singleton_iff_exists_affine_open_isFinite_restrict · AlgebraicGeometry.exists_finite_affine_stratification_split_reduction · AlgebraicGeometry.exists_surjective_affine_baseChange_thickening_finiteEtale

Section59.73 More on constructible sheaves#

Section 59.73 of the Stacks Project, Tag 095M. 14 tags here are carried by 72 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03S8, a lemma

Tag 03S8 in the Stacks Project.

AlgebraicGeometry.isConstructibleAbelianSheaf_abelianShriekConstant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/AbelianShriekConstructible.lean, line 412. The attribute's comment: “part (2), abelian sheaves: an extension by zero of the constant sheaf at a finite abelian group at a quasi-compact quasi-separated etale object is a constructible abelian sheaf”.

Stacks 03S8, part (2). For an étale morphism j : U ⟶ X of quasi-compact and quasi-separated schemes, presented as an object U of the small étale site of X, and M a finite abelian group, the extension by zero j_!\underline{M} is a constructible abelian sheaf on X_étale.

By AlgebraicGeometry.abelianShriekConstantIsoCopower this sheaf is the copower sheaf by M on the sheaf h_U^# of sets, which is constructible by part (1) of the same tag; and the copower sheaf by a finite abelian group carries a constructible sheaf of sets to a constructible abelian sheaf. No input beyond part (1) of the tag is used.

public theorem isConstructibleAbelianSheaf_abelianShriekConstant [Finite M]
    [CompactSpace X.obj] [QuasiSeparatedSpace X.obj] (U : SmallEtale B X.obj X.property)
    [CompactSpace U.obj.left.obj] [QuasiSeparatedSpace U.obj.left.obj] :
    IsConstructibleAbelianSheaf B X
      ((abelianExtensionByZero B X.obj X.property U).obj
        ((constantSheaf (SmallEtale.topology B U.obj.left.obj U.obj.left.property)
          AddCommGrpCat.{u + 1}).obj M))

AlgebraicGeometry.abelianShriekZModIsConstructible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/AbelianShriekConstructible.lean, line 437. The attribute's comment: “part (2) at the finite groups Z/nZ, the form AbelianShriekZModIsConstructible”.

Stacks 03S8, part (2), at the finite abelian groups Z/nZ. The predicate AlgebraicGeometry.AbelianShriekZModIsConstructible holds: for every scheme Y of B that is quasi-compact and quasi-separated, every quasi-compact quasi-separated étale object U of Y_étale and every positive integer n, the abelian sheaf j_{U!}(Z/nZ) is constructible.

ZMod n is finite exactly because n is positive, so this is AlgebraicGeometry.isConstructibleAbelianSheaf_abelianShriekConstant at M = ULift (ZMod n).

public theorem abelianShriekZModIsConstructible : AbelianShriekZModIsConstructible B

AlgebraicGeometry.isConstructibleSetSheaf_sheafifiedYoneda, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/EtaleShriekConstructible.lean, line 141. The attribute's comment: “part (1), carrying the conclusion of Stacks 03S0 (an etale morphism of quasi-compact quasi-separated schemes becomes finite etale on the strata of a partition of its target into constructible locally closed subschemes) as the explicit hypothesis hstrat”.

Stacks 03S8, part (1). For an étale morphism of quasi-compact and quasi-separated schemes j : U ⟶ X, presented as an object U of the small étale site of X, the sheaf h_U represented by U is a constructible sheaf of sets on X_étale.

public theorem isConstructibleSetSheaf_sheafifiedYoneda (B : BigEtaleSite.{u}) (X : B.Scheme)
    [CompactSpace X.obj] [QuasiSeparatedSpace X.obj]
    (U : SmallEtale B X.obj X.property)
    [CompactSpace U.obj.left.obj] [QuasiSeparatedSpace U.obj.left.obj]
    (hstrat : HasFiniteEtaleStratification B X U) :
    IsConstructibleSetSheaf B X
      ((Sheaf.sheafifiedYoneda (SmallEtale.topology B X.obj X.property)).obj U)

AlgebraicGeometry.isConstructible_sheafifiedYoneda_and_abelianShriekConstant_and_moduleShriek_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ShriekAndRepresentableConstructible.lean, line 90. The attribute's comment: “the whole tag: part (1) the sheaf of sets represented by a quasi-compact quasi-separated etale object is constructible, part (2) an extension by zero of the constant sheaf at a finite abelian group is a constructible abelian sheaf, part (3) an extension by zero of the constant sheaf at a finite module over a Noetherian commutative ring is a constructible sheaf of modules. Unconditional: only the source's quasi-compactness and quasi-separatedness of X and of U, and part (3)'s own Noetherian commutative ring. No IsRightAdjoint or HasWeakSheafify assumption is carried, those being inferable here although the elaborated signatures of parts (2) and (3) assume them. All six component registrations are retained.”.

Stacks 03S8. Let X be a quasi-compact and quasi-separated scheme of a big étale site, R a Noetherian commutative ring and U a quasi-compact quasi-separated object of the small étale site of X, so that j : U ⟶ X is an étale morphism of quasi-compact quasi-separated schemes. Then

1. the sheaf h_U^# of sets represented by U is a constructible sheaf of sets on X_étale;
2. for every finite abelian group M the extension by zero j_!\underline{M} is a constructible abelian sheaf on X_étale; and
3. for every finite R-module M the extension by zero j_{U!}\underline{M} is a constructible sheaf of R-modules on X_étale.

This is the whole tag in one statement, under the source's quasi-compactness and quasi-separatedness of X and of U and no other hypothesis. Each part is proved by the theorem that states it alone: AlgebraicGeometry.isConstructibleSetSheaf_sheafifiedYoneda_of_qcqs for part (1), AlgebraicGeometry.isConstructibleAbelianSheaf_abelianShriekConstant for part (2), and AlgebraicGeometry.isConstructibleModuleSheaf_moduleShriek for part (3). All six existing registrations of the tag are retained, each stating its own part or a case of one.

The ring R, its commutativity and its Noetherianness are hypotheses of part (3) alone: parts (1) and (2) do not mention R and are proved without it. Part (1) is used in proving parts (2) and (3), so the conjunction asserts no more than parts (2) and (3) together do; it is the statement of the tag rather than a new fact.

No instance beyond the source's hypotheses is assumed, although the components appear to assume four families of them; see the implementation notes above.

public theorem isConstructible_sheafifiedYoneda_and_abelianShriekConstant_and_moduleShriek_of_qcqs
    (B : BigEtaleSite.{u}) (X : B.Scheme) (R : Type (u + 1)) [CommRing R] [IsNoetherianRing R]
    [CompactSpace X.obj] [QuasiSeparatedSpace X.obj] (U : SmallEtale B X.obj X.property)
    [CompactSpace U.obj.left.obj] [QuasiSeparatedSpace U.obj.left.obj] :
    IsConstructibleSetSheaf B X
        ((Sheaf.sheafifiedYoneda (SmallEtale.topology B X.obj X.property)).obj U) ∧
      (∀ (M : AddCommGrpCat.{u + 1}) [Finite M],
        IsConstructibleAbelianSheaf B X
          ((abelianExtensionByZero B X.obj X.property U).obj
            ((constantSheaf (SmallEtale.topology B U.obj.left.obj U.obj.left.property)
              AddCommGrpCat.{u + 1}).obj M))) ∧
      (∀ (M : ModuleCat.{u + 1} R) [Module.Finite R M],
        IsConstructibleModuleSheaf B X R (moduleShriek.{u, u + 1, u + 1} B X R U M))

AlgebraicGeometry.isConstructibleModuleSheaf_moduleShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ShriekFiniteModuleConstructible.lean, line 234. The attribute's comment: “part (3)”.

Stacks 03S8, part (3). Let X be a quasi-compact and quasi-separated scheme, Λ a Noetherian ring and M a finite Λ-module. For U a quasi-compact and quasi-separated object of the small étale site of X, the extension by zero j_{U!}\underline{M} is a constructible sheaf of Λ-modules on X_étale.

By ModuleCat.exists_cokernel_finFreeSigma_of_finite the module M is the cokernel of a map between finite direct sums of copies of Λ. Extension by zero of the constant sheaf is a left adjoint, so it carries that presentation to one of j_{U!}\underline{M} as the cokernel of a map between finite direct sums of copies of j_{U!}\underline{Λ}, which are constructible.

public theorem isConstructibleModuleSheaf_moduleShriek
    [CompactSpace X.obj] [QuasiSeparatedSpace X.obj] (U : SmallEtale B X.obj X.property)
    [CompactSpace U.obj.left.obj] [QuasiSeparatedSpace U.obj.left.obj]
    (M : ModuleCat.{u + 1} R) [Module.Finite R M] :
    IsConstructibleModuleSheaf B X R (moduleShriek.{u, u + 1, u + 1} B X R U M)

AlgebraicGeometry.isConstructibleSetSheaf_sheafifiedYoneda_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ShriekGeneratorConstructible.lean, line 136. The attribute's comment: “part (1), sheaves of sets”.

Stacks 03S8, part (1). For an étale morphism j : U ⟶ X of quasi-compact and quasi-separated schemes, presented as an object U of the small étale site of X, the sheaf h_U represented by U is a constructible sheaf of sets on X_étale.

This is AlgebraicGeometry.isConstructibleSetSheaf_sheafifiedYoneda with its hypothesis, the conclusion of Stacks 03S0, discharged by AlgebraicGeometry.hasFiniteEtaleStratification.

public theorem isConstructibleSetSheaf_sheafifiedYoneda_of_qcqs
    [CompactSpace X.obj] [QuasiSeparatedSpace X.obj] (U : SmallEtale B X.obj X.property)
    [CompactSpace U.obj.left.obj] [QuasiSeparatedSpace U.obj.left.obj] :
    IsConstructibleSetSheaf B X
      ((Sheaf.sheafifiedYoneda (SmallEtale.topology B X.obj X.property)).obj U)

AlgebraicGeometry.isConstructibleModuleSheaf_moduleShriekConstant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ShriekGeneratorConstructible.lean, line 200. The attribute's comment: “sheaves of modules over a Noetherian commutative ring in an arbitrary universe: an extension by zero of a constant free rank-one module sheaf at a quasi-compact quasi-separated etale object is constructible”.

Stacks 03S8 for sheaves of modules. For U a quasi-compact quasi-separated object of the small étale site of a quasi-compact quasi-separated scheme X and Λ a Noetherian commutative ring in an arbitrary universe r, the extension by zero j_{U!}\underline{\Lambda}_U of the constant free rank-one module sheaf is a constructible sheaf of Λ-modules in ModuleCat.{max (u + 1) r} Λ.

By AlgebraicGeometry.moduleShriekConstantIsoCopower this sheaf is the copower module sheaf by the free rank-one module on the sheaf h_U^# of sets, which is constructible as a sheaf of sets in the module universe by AlgebraicGeometry.isConstructibleFiniteSheaf_sheafifiedUliftYoneda_of_qcqs, part (1) of the same tag. The copower stands in for ModuleCat.free Λ, whose source Type r ⥤ ModuleCat.{r} Λ would force the ring into the module universe.

public theorem isConstructibleModuleSheaf_moduleShriekConstant
    [CompactSpace X.obj] [QuasiSeparatedSpace X.obj] (U : SmallEtale B X.obj X.property)
    [CompactSpace U.obj.left.obj] [QuasiSeparatedSpace U.obj.left.obj] :
    IsConstructibleModuleSheaf B X Λ (moduleShriekConstant.{u, r, r} B X Λ U)

Tag 03SA, a lemma

Tag 03SA in the Stacks Project.

AlgebraicGeometry.exists_isFilteredColimit_isConstructibleAbelianSheaf_of_torsionSheafProperty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/AbelianSurjectiveDescent.lean, line 242. The attribute's comment: “part (2), at the faithful local torsion notion; 093C and 03S8 (2) granted”.

The content of Stacks 03SA (2). Let X be a quasi-compact and quasi-separated scheme and let F be a torsion abelian sheaf on X_étale. Then F is a filtered colimit of constructible abelian sheaves.

This is the faithful restatement of AlgebraicGeometry.exists_isFilteredColimit_isConstructibleAbelianSheaf (Constructible/TorsionColimitOfConstructibles.lean), whose torsion hypothesis is AlgebraicGeometry.IsTorsionAbelianSheaf, the pointwise annihilation of every section over every étale object. That condition strengthens the hypothesis of the tag, whose "torsion abelian sheaf" is the local condition of Stacks 0DD7, here Stacks.Torsion.torsionSheafProperty; the two are not equivalent, the objects of X_étale not being quasi-compact.

The proof is the source's, and is the same as the pointwise version's: the presentation supplied by h093C writes F as a filtered colimit of the cokernels displayed by Stacks 09YT, and those cokernels are constructible by the library's Stacks 09YT, AlgebraicGeometry.isConstructibleAbelianSheaf_of_hasFiniteZModShriekPresentation, which rests on Stacks 03RZ (2).

Two statements of the source are hypotheses of this theorem rather than inputs it derives. Stacks 03S8 (2) at the finite groups ℤ/nℤ, as h03S8, is a theorem of the library — AlgebraicGeometry.abelianShriekZModIsConstructible of Constructible/AbelianShriekConstructible.lean proves AlgebraicGeometry.AbelianShriekZModIsConstructible outright — so any caller can supply it. Stacks 093C for torsion abelian sheaves at the local torsion notion, as h093C in the spelling AlgebraicGeometry.LocallyTorsionAbelianSheavesAreFilteredColimitsOfZModPresentations, is not: the library has no proof of it, and no caller can supply it, so the tag is registered with that one hypothesis named in its clause string.

public theorem exists_isFilteredColimit_isConstructibleAbelianSheaf_of_torsionSheafProperty
    (h093C : LocallyTorsionAbelianSheavesAreFilteredColimitsOfZModPresentations B X)
    (h03S8 : AbelianShriekZModIsConstructible B) (hXc : CompactSpace X.obj)
    (hXq : QuasiSeparatedSpace X.obj)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
    (hF : torsionSheafProperty (SmallEtale.topology B X.obj X.property) F) :
    ∃ (I : Type (u + 1)) (_ : SmallCategory I) (_ : IsFiltered I)
      (D : I ⥤ Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
      (ι : D ⟶ (Functor.const I).obj F), Nonempty (IsColimit (Cocone.mk F ι)) ∧
        ∀ i, IsConstructibleAbelianSheaf B X (D.obj i)

AlgebraicGeometry.exists_isFilteredColimit_isConstructibleSetSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ColimitOfConstructibles.lean, line 246. The attribute's comment: “part (1), granted Stacks 093C (1) in the coequalizer spelling as the hypothesis h093C and Stacks 03S0 as the hypothesis h03S0; Stacks 03S8 (1) and Stacks 03RZ (1) are discharged from the library”.

Stacks 03SA (1). Let X be a quasi-compact and quasi-separated scheme and F a sheaf of sets on X_étale. Then F is a filtered colimit of constructible sheaves of sets.

This is the source's own proof: Stacks 093C writes F as a filtered colimit of coequalizers of maps between finite coproducts of representables at quasi-compact quasi-separated objects, and AlgebraicGeometry.isConstructibleSetSheaf_of_presentation says those coequalizers are constructible. Of the three cited inputs, Stacks 03S8 (1) and Stacks 03RZ (1) are discharged from the library; what remains as hypotheses is Stacks 093C, and Stacks 03S0, which Stacks 03S8 (1) itself carries.

public theorem exists_isFilteredColimit_isConstructibleSetSheaf
    (h093C : SetSheavesAreFilteredColimitsOfPresentations B X)
    (h03S0 : EtaleFiniteStratificationExists B) (hXc : CompactSpace X.obj)
    (hXq : QuasiSeparatedSpace X.obj)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1))) :
    ∃ (I : Type (u + 1)) (_ : SmallCategory I) (_ : IsFiltered I)
      (D : I ⥤ Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1)))
      (ι : D ⟶ (Functor.const I).obj F), Nonempty (IsColimit (Cocone.mk F ι)) ∧
        ∀ i, IsConstructibleSetSheaf B X (D.obj i)

AlgebraicGeometry.exists_isFilteredColimit_isConstructibleModuleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ColimitOfConstructibles.lean, line 316. The attribute's comment: “part (3), granted Stacks 093C (2) in the shriek spelling as the hypothesis h093C and the sheaves-of-modules case of Stacks 03S8 as the hypothesis hshriek, which is the same hypothesis the library's Stacks 095N carries; Stacks 03RZ (3) is discharged from the library”.

Stacks 03SA (3). Let X be a quasi-compact and quasi-separated scheme, Λ a Noetherian ring and F a sheaf of Λ-modules on X_étale. Then F is a filtered colimit of constructible sheaves of Λ-modules.

This is the source's own proof: Stacks 093C writes F as a filtered colimit of cokernels of maps between finite direct sums of the sheaves j_{U!}Λ at quasi-compact quasi-separated objects, and the library's Stacks 095N says those cokernels are constructible once the generators are — that is AlgebraicGeometry.isConstructibleModuleSheaf_of_hasFiniteShriekPresentation. Stacks 03RZ (3) is discharged from the library; what remains as hypotheses is Stacks 093C and the sheaves-of-modules case of Stacks 03S8.

public theorem exists_isFilteredColimit_isConstructibleModuleSheaf
    (h093C : ModuleSheavesAreFilteredColimitsOfPresentations B X Λ)
    (hshriek : ∀ U : SmallEtale B X.obj X.property, IsQCQSEtaleObject B X U →
      IsConstructibleModuleSheaf B X Λ (moduleShriekConstant.{u, u + 1, u + 1} B X Λ U))
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} Λ)) :
    ∃ (I : Type (u + 1)) (_ : SmallCategory I) (_ : IsFiltered I)
      (D : I ⥤ Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} Λ))
      (ι : D ⟶ (Functor.const I).obj F), Nonempty (IsColimit (Cocone.mk F ι)) ∧
        ∀ i, IsConstructibleModuleSheaf B X Λ (D.obj i)

AlgebraicGeometry.exists_isFilteredColimit_isConstructibleAbelianSheaf_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/LocalTorsionColimitOfConstructibles.lean, line 452. The attribute's comment: “part (2), torsion abelian sheaves, torsion in the local sense of Stacks 0DD7”. References: SGA 4½ Arcata (4.3.3), “more general”.

Stacks 03SA (2). Let X be a quasi-compact and quasi-separated scheme and let F be a torsion abelian sheaf on X_étale. Then F is a filtered colimit of constructible abelian sheaves.

The torsion condition is the local one of Stacks 0DD7, Stacks.Torsion.torsionSheafProperty: every section is annihilated by a positive integer after restriction along the arrows of a covering sieve. The colimit is taken in the category of abelian sheaves on X_étale, over a small filtered index category, and the terms are constructible in the sense of Stacks 03RW (2). This is AlgebraicGeometry.ind_isConstructibleAbelianSheaf_of_torsionSheafProperty in the diagram-and-cocone spelling of parts (1) and (3).

public theorem exists_isFilteredColimit_isConstructibleAbelianSheaf_of_qcqs
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
    (hF : Stacks.Torsion.torsionSheafProperty (SmallEtale.topology B X.obj X.property) F) :
    ∃ (I : Type (u + 1)) (_ : SmallCategory I) (_ : IsFiltered I)
      (D : I ⥤ Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
      (ι : D ⟶ (Functor.const I).obj F), Nonempty (IsColimit (Cocone.mk F ι)) ∧
        ∀ i, IsConstructibleAbelianSheaf B X (D.obj i)

AlgebraicGeometry.exists_isFilteredColimit_isConstructibleSetSheaf_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ModuleColimitOfConstructibles.lean, line 94. The attribute's comment: “part (1), sheaves of sets, with 093C (1) and 03S0 discharged”.

Stacks 03SA, part (1). Let X be a quasi-compact and quasi-separated scheme and F a sheaf of sets on X_étale. Then F is a filtered colimit of constructible sheaves of sets.

This is AlgebraicGeometry.exists_isFilteredColimit_isConstructibleSetSheaf with both of its hypotheses discharged: Stacks 093C (1) by AlgebraicGeometry.setSheavesAreFilteredColimitsOfPresentations and Stacks 03S0 by AlgebraicGeometry.etaleFiniteStratificationExists.

public theorem exists_isFilteredColimit_isConstructibleSetSheaf_of_qcqs
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1))) :
    ∃ (I : Type (u + 1)) (_ : SmallCategory I) (_ : IsFiltered I)
      (D : I ⥤ Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1)))
      (ι : D ⟶ (Functor.const I).obj F), Nonempty (IsColimit (Cocone.mk F ι)) ∧
        ∀ i, IsConstructibleSetSheaf B X (D.obj i)

AlgebraicGeometry.exists_isFilteredColimit_isConstructibleModuleSheaf_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ModuleColimitOfConstructibles.lean, line 114. The attribute's comment: “part (3), sheaves of modules, with 093C (2) and 03S8 discharged”. References: SGA 4 XVII (5.5.25.4), “more general”.

Stacks 03SA, part (3). Let X be a quasi-compact and quasi-separated scheme, Λ a Noetherian ring and F a sheaf of Λ-modules on X_étale. Then F is a filtered colimit of constructible sheaves of Λ-modules.

This is AlgebraicGeometry.exists_isFilteredColimit_isConstructibleModuleSheaf with both of its hypotheses discharged: Stacks 093C (2) by AlgebraicGeometry.moduleSheavesAreFilteredColimitsOfPresentations and Stacks 03S8 for sheaves of modules by AlgebraicGeometry.isConstructibleModuleSheaf_moduleShriekConstant.

public theorem exists_isFilteredColimit_isConstructibleModuleSheaf_of_qcqs
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} Λ)) :
    ∃ (I : Type (u + 1)) (_ : SmallCategory I) (_ : IsFiltered I)
      (D : I ⥤ Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} Λ))
      (ι : D ⟶ (Functor.const I).obj F), Nonempty (IsColimit (Cocone.mk F ι)) ∧
        ∀ i, IsConstructibleModuleSheaf B X Λ (D.obj i)

AlgebraicGeometry.exists_isFilteredColimit_isConstructibleAbelianSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/TorsionColimitOfConstructibles.lean, line 185. The attribute's comment: “part (2), torsion abelian sheaves, granted Stacks 093C for torsion abelian sheaves in the Z/nZ-shriek spelling as the hypothesis h093C, which subsumes the source's reduction to part (3), and Stacks 03S8 (2) at the finite groups Z/nZ as the hypothesis h03S8; Stacks 03RZ (2) and Stacks 09YT are discharged from the library”.

Stacks 03SA (2). Let X be a quasi-compact and quasi-separated scheme and let F be a torsion abelian sheaf on X_étale. Then F is a filtered colimit of constructible abelian sheaves.

This is the source's own proof, organised as for parts (1) and (3): the granted presentation writes F as a filtered colimit of the cokernels displayed by Stacks 09YT, and those cokernels are constructible by the library's Stacks 09YT, AlgebraicGeometry.isConstructibleAbelianSheaf_of_hasFiniteZModShriekPresentation, which in turn rests on Stacks 03RZ for abelian sheaves (AlgebraicGeometry.Constructible.constructibleAbelianSheaf_isWeakSerreClass, an unconditional instance of this library). Of the inputs the source cites, Stacks 03RZ (2) is discharged from the library; what remains granted is Stacks 093C for torsion abelian sheaves, which subsumes the source's reduction to part (3), and Stacks 03S8 (2) at the finite groups ℤ/nℤ.

public theorem exists_isFilteredColimit_isConstructibleAbelianSheaf
    (h093C : TorsionAbelianSheavesAreFilteredColimitsOfZModPresentations B X)
    (h03S8 : AbelianShriekZModIsConstructible B) (hXc : CompactSpace X.obj)
    (hXq : QuasiSeparatedSpace X.obj)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
    (hF : IsTorsionAbelianSheaf B X F) :
    ∃ (I : Type (u + 1)) (_ : SmallCategory I) (_ : IsFiltered I)
      (D : I ⥤ Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
      (ι : D ⟶ (Functor.const I).obj F), Nonempty (IsColimit (Cocone.mk F ι)) ∧
        ∀ i, IsConstructibleAbelianSheaf B X (D.obj i)

Tag 095Q, a lemma

Tag 095Q in the Stacks Project.

AlgebraicGeometry.isConstructibleAbelianSheaf_pullback_iff_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/AbelianSurjectiveDescent.lean, line 609. The attribute's comment: “part (2), abelian sheaves”.

Stacks 095Q, part (2). Let f : X ⟶ Y be a surjective morphism of quasi-compact and quasi-separated schemes and let ℱ be an abelian sheaf on Y_étale — arbitrary, with no torsion assumption. Then ℱ is constructible if and only if f⁻¹ℱ is constructible.

The forward implication is Stacks 095G, AlgebraicGeometry.isConstructibleFiniteSheaf_pullback, and needs neither surjectivity of f nor quasi-compactness. The converse is carried out in the category of sheaves of ℤ-modules, where Stacks 095Q is already unconditional: AlgebraicGeometry.isConstructibleModuleSheaf_pullback_iff_of_surjective. Only the quasi-compactness and quasi-separatedness of X and Y, which the source's statement assumes, are hypotheses.

The passage between the two categories is the one place with content. Going out is immediate, AlgebraicGeometry.isConstructibleModuleSheaf_moduleCatIntEquivalence, a finite abelian group being a finitely generated ℤ-module; the module development is pinned to a Noetherian ring in Type (u + 1), so the descent happens at ULift ℤ and is transported back by AlgebraicGeometry.isConstructibleModuleSheaf_int_of_uliftIntRestrictScalars. Coming back is AlgebraicGeometry.isConstructibleAbelianSheaf_of_isConstructibleModuleSheaf_int, which needs ℱ to be torsion — and that is exactly what the constructibility of f⁻¹ℱ supplies, through the stalk criterion AlgebraicGeometry.torsionSheafProperty_of_isConstructibleAbelianSheaf_pullback. Stacks 093C for torsion abelian sheaves is not used: the module form of Stacks 093C, which the library proves, is what the descent above consumes.

public theorem isConstructibleAbelianSheaf_pullback_iff_of_surjective
    (hf : Function.Surjective (B.inclusion.map f).base)
    (F : Sheaf (SmallEtale.topology B Y.obj Y.property) AddCommGrpCat.{u + 1}) :
    IsConstructibleAbelianSheaf B Y F ↔
      IsConstructibleAbelianSheaf B X ((smallEtaleAbelianPullbackFunctor B f).obj F)

AlgebraicGeometry.isConstructibleAbelianSheaf_pullback_iff_of_surjective_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/AbelianSurjectiveDescentUnconditional.lean, line 178. The attribute's comment: “part (2), abelian sheaves”.

Let f : X ⟶ Y be a surjective morphism of quasi-compact and quasi-separated schemes and let ℱ be an abelian sheaf on Y_étale, with no torsion assumption. Then ℱ is constructible if and only if f⁻¹ℱ is constructible.

public theorem isConstructibleAbelianSheaf_pullback_iff_of_surjective_general
    (hf : Function.Surjective (B.inclusion.map f).base)
    (𝓕 : Sheaf (SmallEtale.topology B Y.obj Y.property) AddCommGrpCat.{u + 1}) :
    IsConstructibleAbelianSheaf B Y 𝓕 ↔
      IsConstructibleAbelianSheaf B X ((smallEtaleAbelianPullbackFunctor B f).obj 𝓕)

AlgebraicGeometry.isConstructibleModuleSheaf_pullback_iff_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ModuleSurjectiveDescent.lean, line 269. The attribute's comment: “sheaves of modules”.

Stacks 095Q for sheaves of modules. Let f : X ⟶ Y be a surjective morphism of quasi-compact and quasi-separated schemes, Λ a Noetherian ring and ℱ a sheaf of Λ-modules on Y_étale. Then ℱ is constructible if and only if f⁻¹ℱ is constructible.

The forward implication is Stacks 095G, AlgebraicGeometry.isConstructibleModuleSheaf_pullback, and needs neither surjectivity of f nor quasi-compactness. The converse is AlgebraicGeometry.isConstructibleModuleSheaf_of_isConstructibleModuleSheaf_pullback.

Nothing is granted. The two statements of the source that were once hypotheses here are both proved in the library, and both are supplied from hXc, hXq, hYc and hYq, the quasi-compactness and quasi-separatedness of X and Y that the source's statement assumes: Stacks 095N on the quasi-compact quasi-separated schemes of B, from the unconditional AlgebraicGeometry.isConstructibleModuleSheaf_iff_qcqsShriekPresentation, and Stacks 093C (2) on Y, from AlgebraicGeometry.moduleSheavesAreFilteredColimitsOfPresentations.

public theorem isConstructibleModuleSheaf_pullback_iff_of_surjective
    (hf : Function.Surjective (B.inclusion.map f).base)
    (F : Sheaf (SmallEtale.topology B Y.1 Y.property) (ModuleCat.{u + 1} Λ)) :
    IsConstructibleModuleSheaf B Y Λ F ↔
      IsConstructibleModuleSheaf B X Λ ((smallEtaleModulePullbackFunctor B Λ f).obj F)

AlgebraicGeometry.isConstructibleSetSheaf_pullback_iff_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/SurjectiveDescent.lean, line 352. The attribute's comment: “part (1), sheaves of sets”.

Stacks 095Q, part (1). Let f : X ⟶ Y be a surjective morphism of quasi-compact and quasi-separated schemes and let ℱ be a sheaf of sets on Y_étale. Then ℱ is constructible if and only if f⁻¹ℱ is constructible.

Nothing is assumed. The forward implication is Stacks 095G, AlgebraicGeometry.isConstructibleFiniteSheaf_pullback, and needs neither surjectivity of f nor quasi-compactness. The converse is AlgebraicGeometry.isConstructibleSetSheaf_of_isConstructibleSetSheaf_pullback, whose Stacks 09Y9 is supplied from isConstructibleSetSheaf_iff_hasFiniteQCSRepresentableCoequalizerPresentation_unconditional, which assumes nothing beyond quasi-compactness and quasi-separatedness of X and does not use Stacks 0245. Both hypotheses of the library's Stacks 03SA (1) are discharged as described above.

Parts (2) and (3) of the tag are not proved here.

public theorem isConstructibleSetSheaf_pullback_iff_unconditional
    (hf : Function.Surjective (B.inclusion.map f).base)
    (hXc : CompactSpace X.obj) (hXq : QuasiSeparatedSpace X.obj)
    (hYc : CompactSpace Y.obj) (hYq : QuasiSeparatedSpace Y.obj)
    (F : Sheaf (SmallEtale.topology B Y.obj Y.property) (Type (u + 1))) :
    IsConstructibleSetSheaf B Y F ↔
      IsConstructibleSetSheaf B X ((smallEtaleSetPullback B f).obj F)

Tag 095H, a lemma

Tag 095H in the Stacks Project.

AlgebraicGeometry.isConstructibleModuleSheaf_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/FiniteEtalePushforwardConstructible.lean, line 476. The attribute's comment: “sheaves of modules over a Noetherian ring; nothing granted, no hypothesis on S or T”. References: SGA 4 IX (2.14), “(i), special case”; SGA 5 I (1.14), “b)”.

Stacks 095H for sheaves of modules over a Noetherian ring. Let p : T ⟶ S be a finite étale morphism of a big étale site, let Λ be a Noetherian ring and let ℱ be a constructible sheaf of Λ-modules on T_étale. Then p_*ℱ is a constructible sheaf of Λ-modules on S_étale. No hypothesis is imposed on S or T, and nothing is granted.

By Stacks 095F constructibility may be checked on an open covering of S, and the affine opens of S are such a covering; the restriction of p_*ℱ to an affine open U is the direct image, along the base change of p to U, of the restriction of ℱ (AlgebraicGeometry.smallEtaleRestrictionPushforwardBaseChangeIso), that base change is again finite étale, the restriction of ℱ is constructible by Stacks 095G, and U is quasi-compact and quasi-separated, so AlgebraicGeometry.isConstructibleModuleSheaf_pushforward_of_compactSpace applies.

public theorem isConstructibleModuleSheaf_pushforward
    [IsFinite (B.inclusion.map p)] [Etale (B.inclusion.map p)]
    (F : Sheaf (SmallEtale.topology B T.1 T.property) (ModuleCat.{u + 1} Λ))
    (hF : IsConstructibleModuleSheaf B T Λ F) :
    IsConstructibleModuleSheaf B S Λ
      ((B.smallPushforward p (ModuleCat.{u + 1} Λ)).obj F)

AlgebraicGeometry.isConstructibleSetSheaf_pushforward_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/FiniteEtalePushforwardConstructibleUnconditional.lean, line 149. The attribute's comment: “sheaves of sets; nothing granted, no hypothesis on S or T”. References: SGA 4 IX (2.14), “(i), special case”; SGA 4 XIV (1.1), “special case”; SGA 4 XIV (1.11), “partial”; SGA 4 XIV (1.5), “special case”.

Let p : T ⟶ S be a finite étale morphism of a big étale site and let ℱ be a constructible sheaf of sets on T_étale. Then p_*ℱ is a constructible sheaf of sets on S_étale.

public theorem isConstructibleSetSheaf_pushforward_unconditional
    [IsFinite (B.inclusion.map p)] [Etale (B.inclusion.map p)]
    (F : Sheaf (SmallEtale.topology B T.1 T.property) (Type (u + 1)))
    (hF : IsConstructibleSetSheaf B T F) :
    IsConstructibleSetSheaf B S ((B.smallPushforward p (Type (u + 1))).obj F)

AlgebraicGeometry.isConstructibleAbelianSheaf_pushforward_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/FiniteEtalePushforwardConstructibleUnconditional.lean, line 226. The attribute's comment: “sheaves of abelian groups; nothing granted, no hypothesis on S or T”.

Let p : T ⟶ S be a finite étale morphism of a big étale site and let ℱ be a constructible abelian sheaf on T_étale. Then p_*ℱ is a constructible abelian sheaf on S_étale.

public theorem isConstructibleAbelianSheaf_pushforward_unconditional
    [IsFinite (B.inclusion.map p)] [Etale (B.inclusion.map p)]
    (F : Sheaf (SmallEtale.topology B T.1 T.property) AddCommGrpCat.{u + 1})
    (hF : IsConstructibleAbelianSheaf B T F) :
    IsConstructibleAbelianSheaf B S
      ((B.smallPushforward p AddCommGrpCat.{u + 1}).obj F)

Tag 09Y9, a lemma

Tag 09Y9 in the Stacks Project.

AlgebraicGeometry.isConstructibleSetSheaf_of_hasFiniteQCSRepresentableCoequalizerPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/CoequalizerPresentationConstructible.lean, line 88. The attribute's comment: “the implication from a finite coequalizer presentation by representables of quasi-compact quasi-separated etale objects to constructibility, for sheaves of sets; the reverse implication, from constructibility to the existence of such a presentation, is not part of this statement”. References: SGA 4 IX (2.7), “Sheaves of sets”; SGA 4 IX (2.7.1), “Sufficiency”.

Stacks 09Y9, the implication from a presentation to constructibility. Let X be a quasi-compact and quasi-separated scheme of a big étale site and let F be a sheaf of sets on X_étale which is a coequalizer of two maps between finite coproducts of sheaves represented by quasi-compact and quasi-separated objects of X_étale. Then F is a constructible sheaf of sets.

public theorem isConstructibleSetSheaf_of_hasFiniteQCSRepresentableCoequalizerPresentation
    (B : BigEtaleSite.{u}) (X : B.Scheme) [CompactSpace X.obj] [QuasiSeparatedSpace X.obj]
    {F : Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1))}
    (hF : HasFiniteQCSRepresentableCoequalizerPresentation B X F) :
    IsConstructibleSetSheaf B X F

AlgebraicGeometry.exists_finite_representable_epi_of_isConstructibleSetSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ConstructibleQuasiCompact.lean, line 328. The attribute's comment: “the surjection half: a constructible sheaf of sets on a quasi-compact quasi-separated scheme is the target of an epimorphism from a finite coproduct of sheaves represented by quasi-compact quasi-separated objects”.

Stacks 09Y9, the surjection half. A constructible sheaf of sets on the small étale site of a quasi-compact and quasi-separated scheme receives an epimorphism from a finite coproduct of sheaves represented by quasi-compact and quasi-separated objects of the site.

This is AlgebraicGeometry.isQuasiCompact_of_isConstructibleSetSheaf_unconditional followed by the presentation of a quasi-compact sheaf by finitely many affine representables; both the conservativity of geometric points and the finite affine covering it uses are theorems of the library, so nothing is assumed.

public theorem exists_finite_representable_epi_of_isConstructibleSetSheaf
    (B : BigEtaleSite.{u}) (X : B.Scheme) [CompactSpace X.obj] [QuasiSeparatedSpace X.obj]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1)))
    (hF : IsConstructibleSetSheaf B X F) :
    ∃ (n : ℕ) (U : Fin n → SmallEtale B X.obj X.property),
      (∀ i, CompactSpace ((SmallEtale.toScheme B X.obj X.property).obj (U i)) ∧
        QuasiSeparatedSpace ((SmallEtale.toScheme B X.obj X.property).obj (U i))) ∧
      ∃ p : (∐ fun i ↦ (Sheaf.sheafifiedYoneda
        (SmallEtale.topology B X.obj X.property)).obj (U i)) ⟶ F, Epi p

AlgebraicGeometry.isConstructibleSetSheaf_iff_hasFiniteQCSRepresentableCoequalizerPresentation_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ConstructibleQuasiCompact.lean, line 353. The attribute's comment: “both directions”. References: SGA 4 IX (2.7); SGA 4 IX (2.7.1), “Sufficiency”.

Stacks Project, Tag 09Y9. On a quasi-compact and quasi-separated scheme the constructible sheaves of sets on the small étale site are exactly the sheaves admitting a coequalizer presentation by finite coproducts of sheaves represented by quasi-compact and quasi-separated étale objects.

Nothing beyond quasi-compactness and quasi-separatedness of X is assumed. Stacks 03S0 is AlgebraicGeometry.etaleFiniteStratificationExists and the conservativity of geometric points of Stacks 03PU is AlgebraicGeometry.jointlyFaithful_smallEtaleSetPullback, both theorems of the library. Stacks 0245 is not used at all: the quasi-compactness step is AlgebraicGeometry.isQuasiCompact_of_isConstructibleSetSheaf_unconditional above, which refines the covering produced by étale-local representability instead of descending along it.

public theorem
    isConstructibleSetSheaf_iff_hasFiniteQCSRepresentableCoequalizerPresentation_unconditional
    (B : BigEtaleSite.{u}) (X : B.Scheme) [CompactSpace X.obj] [QuasiSeparatedSpace X.obj]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1))) :
    IsConstructibleSetSheaf B X F ↔
      HasFiniteQCSRepresentableCoequalizerPresentation B X F

Tag 095N, a lemma

Tag 095N in the Stacks Project.

AlgebraicGeometry.isConstructibleModuleSheaf_iff_hasFiniteShriekPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ModuleShriekCharacterization.lean, line 231. The attribute's comment: “quasi-compact quasi-separated presentation, carrying as explicit hypotheses the sheaves-of-modules case of Stacks 03S8 (hshriek), that an extension by zero of a constant free rank-one module sheaf is constructible, and the finite generation step of the proof (hgen), that a constructible sheaf of modules is a quotient of a finite direct sum of such sheaves”.

Stacks 095N, the quasi-compact quasi-separated presentation. Let X be a quasi-compact and quasi-separated scheme and Λ a Noetherian ring. A sheaf of Λ-modules on X_étale is constructible exactly when it is the cokernel of a map between finite direct sums of extensions by zero of constant free rank-one module sheaves at quasi-compact and quasi-separated objects of X_étale.

The hypotheses hshriek and hgen are carried; see the module documentation.

public theorem isConstructibleModuleSheaf_iff_hasFiniteShriekPresentation
    [CompactSpace X.1] [QuasiSeparatedSpace X.1]
    (hshriek : ∀ U : SmallEtale B X.1 X.property,
      CompactSpace ((SmallEtale.toScheme B X.1 X.property).obj U) →
      QuasiSeparatedSpace ((SmallEtale.toScheme B X.1 X.property).obj U) →
      IsConstructibleModuleSheaf B X R (moduleShriekConstant.{u, u + 1, u + 1} B X R U))
    (hgen : ∀ G : Sheaf (SmallEtale.topology B X.1 X.property) (ModuleCat.{u + 1} R),
      IsConstructibleModuleSheaf B X R G →
        ∃ (n : ℕ) (U : Fin n → SmallEtale B X.1 X.property),
          (∀ i, CompactSpace ((SmallEtale.toScheme B X.1 X.property).obj (U i)) ∧
            QuasiSeparatedSpace ((SmallEtale.toScheme B X.1 X.property).obj (U i))) ∧
          ∃ p : (∐ fun i => moduleShriekConstant.{u, u + 1, u + 1} B X R (U i)) ⟶ G, Epi p)
    (F : Sheaf (SmallEtale.topology B X.1 X.property) (ModuleCat.{u + 1} R)) :
    IsConstructibleModuleSheaf B X R F ↔
      HasFiniteShriekPresentation.{u, u + 1, u + 1} B X R
        (fun W ↦ CompactSpace ((SmallEtale.toScheme B X.1 X.property).obj W) ∧
          QuasiSeparatedSpace ((SmallEtale.toScheme B X.1 X.property).obj W)) F

AlgebraicGeometry.isConstructibleModuleSheaf_iff_affineShriekPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ModuleShriekCharacterization.lean, line 265. The attribute's comment: “affine presentation, carrying as explicit hypotheses the sheaves-of-modules case of Stacks 03S8 at affine objects (hshriek) and the finite generation step of the proof by affine objects (hgen)”.

Stacks 095N, the affine presentation. The étale objects of the presentation may be taken affine: a sheaf of Λ-modules on X_étale is constructible exactly when it is the cokernel of a map between finite direct sums of extensions by zero of constant free rank-one module sheaves at affine objects of X_étale.

The hypotheses hshriek and hgen are carried; see the module documentation. The refinement of a covering sieve of X_étale by a finite family with affine sources, which is what makes the affine form of hgen reachable, is AlgebraicGeometry.SmallEtale.exists_finite_affine_refinement_of_mem_topology.

public theorem isConstructibleModuleSheaf_iff_affineShriekPresentation
    [CompactSpace X.1] [QuasiSeparatedSpace X.1]
    (hshriek : ∀ U : SmallEtale B X.1 X.property, SmallEtale.IsAffine B X.1 X.property U →
      IsConstructibleModuleSheaf B X R (moduleShriekConstant.{u, u + 1, u + 1} B X R U))
    (hgen : ∀ G : Sheaf (SmallEtale.topology B X.1 X.property) (ModuleCat.{u + 1} R),
      IsConstructibleModuleSheaf B X R G →
        ∃ (n : ℕ) (U : Fin n → SmallEtale B X.1 X.property),
          (∀ i, SmallEtale.IsAffine B X.1 X.property (U i)) ∧
          ∃ p : (∐ fun i => moduleShriekConstant.{u, u + 1, u + 1} B X R (U i)) ⟶ G, Epi p)
    (F : Sheaf (SmallEtale.topology B X.1 X.property) (ModuleCat.{u + 1} R)) :
    IsConstructibleModuleSheaf B X R F ↔
      HasFiniteShriekPresentation.{u, u + 1, u + 1} B X R
        (SmallEtale.IsAffine B X.1 X.property) F

AlgebraicGeometry.isConstructibleModuleSheaf_iff_qcqsShriekPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ModuleShriekFiniteGeneration.lean, line 672. The attribute's comment: “quasi-compact quasi-separated presentation”. References: SGA 4 IX (2.7), “special case”; SGA 4 IX (2.9), “(ii)”.

Stacks 095N, the quasi-compact quasi-separated presentation. Let X be a quasi-compact and quasi-separated scheme and Λ a Noetherian ring. A sheaf of Λ-modules on X_étale is constructible exactly when it is the cokernel of a map between finite direct sums of extensions by zero of constant free rank-one module sheaves at quasi-compact and quasi-separated objects of X_étale.

Nothing is granted. The two inputs of AlgebraicGeometry.isConstructibleModuleSheaf_iff_hasFiniteShriekPresentation are discharged: constructibility of the generators is AlgebraicGeometry.isConstructibleModuleSheaf_moduleShriekConstant (Stacks 03S8 for modules) and the finite generation step of the proof is AlgebraicGeometry.exists_finite_epi_sigma_moduleShriekConstant_of_isConstructibleModuleSheaf.

public theorem isConstructibleModuleSheaf_iff_qcqsShriekPresentation
    (F : Sheaf (SmallEtale.topology B X.1 X.property) (ModuleCat.{u + 1} Λ)) :
    IsConstructibleModuleSheaf B X Λ F ↔
      HasFiniteShriekPresentation.{u, u + 1, u + 1} B X Λ
        (fun W ↦ CompactSpace ((SmallEtale.toScheme B X.1 X.property).obj W) ∧
          QuasiSeparatedSpace ((SmallEtale.toScheme B X.1 X.property).obj W)) F

AlgebraicGeometry.isConstructibleModuleSheaf_iff_hasFiniteAffineShriekPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ModuleShriekFiniteGeneration.lean, line 691. The attribute's comment: “affine presentation”. References: SGA 4 IX (2.7), “Module sheaves”; SGA 4 IX (2.9), “(ii)”.

Stacks 095N, the affine presentation. Let X be a quasi-compact and quasi-separated scheme and Λ a Noetherian ring. A sheaf of Λ-modules on X_étale is constructible exactly when it is the cokernel of a map between finite direct sums of extensions by zero of constant free rank-one module sheaves at affine objects of X_étale.

Nothing is granted: this is AlgebraicGeometry.isConstructibleModuleSheaf_iff_affineShriekPresentation_of_gen with its hypothesis discharged by the affine form of the finite generation step proved just above.

public theorem isConstructibleModuleSheaf_iff_hasFiniteAffineShriekPresentation
    (F : Sheaf (SmallEtale.topology B X.1 X.property) (ModuleCat.{u + 1} Λ)) :
    IsConstructibleModuleSheaf B X Λ F ↔
      HasFiniteShriekPresentation.{u, u + 1, u + 1} B X Λ
        (SmallEtale.IsAffine B X.1 X.property) F

AlgebraicGeometry.isConstructibleModuleSheaf_iff_affineShriekPresentation_of_gen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ShriekGeneratorConstructible.lean, line 255. The attribute's comment: “affine presentation, carrying as the only explicit hypothesis the finite generation step of the proof (hgen), that a constructible sheaf of modules is a quotient of a finite direct sum of extensions by zero of constant free rank-one module sheaves”.

Stacks 095N, the affine presentation, with hshriek discharged. Let X be a quasi-compact and quasi-separated scheme and Λ a Noetherian ring. A sheaf of Λ-modules on X_étale is constructible exactly when it is the cokernel of a map between finite direct sums of extensions by zero of constant free rank-one module sheaves at affine objects of X_étale.

Only the finite generation step hgen of the proof remains as a hypothesis; constructibility of the generators is AlgebraicGeometry.isConstructibleModuleSheaf_moduleShriekConstant.

public theorem isConstructibleModuleSheaf_iff_affineShriekPresentation_of_gen
    [CompactSpace X.obj] [QuasiSeparatedSpace X.obj]
    (hgen : ∀ G : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} R),
      IsConstructibleModuleSheaf B X R G →
        ∃ (n : ℕ) (U : Fin n → SmallEtale B X.obj X.property),
          (∀ i, SmallEtale.IsAffine B X.obj X.property (U i)) ∧
          ∃ p : (∐ fun i ↦ moduleShriekConstant.{u, u + 1, u + 1} B X R (U i)) ⟶ G, Epi p)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} R)) :
    IsConstructibleModuleSheaf B X R F ↔
      HasFiniteShriekPresentation.{u, u + 1, u + 1} B X R
        (SmallEtale.IsAffine B X.obj X.property) F

Tag 09YT, a lemma

Tag 09YT in the Stacks Project.

AlgebraicGeometry.isConstructibleAbelianSheaf_iff_hasFiniteZModShriekPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/AbelianShriekPresentation.lean, line 673. The attribute's comment: “a constructible abelian sheaf on a quasi-compact quasi-separated scheme is exactly a cokernel of a map between finite direct sums of the sheaves j_{U!}(Z/nZ) at quasi-compact quasi-separated etale objects and positive integers n”.

Stacks 09YT. Let X be a quasi-compact and quasi-separated scheme. An abelian sheaf on the small étale site of X is constructible exactly when it is of the form Coker(⨁_j j_{V_j!}(Z/m_jZ) → ⨁_i j_{U_i!}(Z/n_iZ)) with the V_j and U_i quasi-compact quasi-separated objects of X_étale and the m_j, n_i positive integers.

Both inclusions are proved. A cokernel of that form is constructible because constructibility of abelian sheaves is a weak Serre condition, Stacks 03RZ (2), and the summands are constructible by Stacks 03S8 (2) at the finite groups Z/nZ, which is AlgebraicGeometry.abelianShriekZModIsConstructible. Conversely a constructible abelian sheaf is annihilated by a positive integer N and has a presentation by extensions by zero of the constant sheaf ℤ from Stacks 095N at Λ = ℤ; quotienting that presentation by N turns it into one of the displayed form.

public theorem isConstructibleAbelianSheaf_iff_hasFiniteZModShriekPresentation
    (hXc : CompactSpace X.obj) (hXq : QuasiSeparatedSpace X.obj)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1}) :
    IsConstructibleAbelianSheaf B X F ↔
      HasFiniteZModShriekPresentation B X (IsQCQSEtaleObject B X) F

AlgebraicGeometry.isConstructibleAbelianSheaf_iff_affineZModShriekPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/AbelianShriekPresentation.lean, line 688. The attribute's comment: “the same characterization with the etale objects of the presentation affine, which is the tag's concluding sentence”.

Stacks 09YT, the affine form. "In fact, we can even assume U_i and V_j affine": the étale objects of the presentation of a constructible abelian sheaf may be taken affine, and a presentation by affine objects still has a constructible cokernel.

public theorem isConstructibleAbelianSheaf_iff_affineZModShriekPresentation
    (hXc : CompactSpace X.obj) (hXq : QuasiSeparatedSpace X.obj)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1}) :
    IsConstructibleAbelianSheaf B X F ↔
      HasFiniteZModShriekPresentation B X (SmallEtale.IsAffine B X.obj X.property) F

AlgebraicGeometry.isConstructibleAbelianSheaf_of_hasFiniteZModShriekPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ColimitOfConstructibles.lean, line 426. The attribute's comment: “the inclusion of the displayed cokernels at quasi-compact quasi-separated objects into the constructible abelian sheaves, granted Stacks 03S8 (2) at the finite groups Z/nZ as the hypothesis h03S8; the reverse inclusion needs Stacks 095N at Lambda = Z/nZ and is not proved here”.

Stacks 09YT, the inclusion of the displayed cokernels into the constructible abelian sheaves. Let X be quasi-compact and quasi-separated. Every abelian sheaf of the form Coker(⨁_j j_{V_j!}(Z/m_jZ) → ⨁_i j_{U_i!}(Z/n_iZ)), with the V_j and U_i quasi-compact quasi-separated objects of X_étale and the m_j, n_i positive, is a constructible abelian sheaf, granted Stacks 03S8 (2) for the summands.

The reverse inclusion — every constructible abelian sheaf has such a presentation — is the other half of the tag and is not proved here. The source deduces it from Stacks 095N at Λ = Z/nZ together with the omitted fact that on a quasi-compact X every constructible abelian sheaf is annihilated by some positive integer. Stacks 095N is now in the library, as AlgebraicGeometry.isConstructibleModuleSheaf_iff_hasFiniteShriekPresentation, but only for sheaves of modules over a single ring in the model Sheaf J (ModuleCat Λ), and three separate things are missing for the reduction: the global annihilation statement, whose absence this library already records in StacksFrontier.AlgebraicGeometry.EtaleCohomology.ProperBaseChange.PrimaryDevissage as waiting on this very tag; a comparison between abelian sheaves annihilated by n and sheaves of Z/nZ-modules, which CategoryTheory.Sheaf.coefficientEquivalence cannot supply because it needs an equivalence of coefficient categories and AddCommGrpCat is not equivalent to ModuleCat (ZMod n); and an identification of AlgebraicGeometry.moduleShriekConstant at Z/nZ with AlgebraicGeometry.abelianShriekZMod, which is not bookkeeping — the analogous comparison between extension by zero of modules and of the underlying abelian sheaves is not an isomorphism in general, by the counterexample Stacks.SheafOfModules.lowerShriekForget_not_isomorphic.

public theorem isConstructibleAbelianSheaf_of_hasFiniteZModShriekPresentation
    (h03S8 : AbelianShriekZModIsConstructible B) (hXc : CompactSpace X.obj)
    (hXq : QuasiSeparatedSpace X.obj)
    {F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1}}
    (hF : HasFiniteZModShriekPresentation B X (IsQCQSEtaleObject B X) F) :
    IsConstructibleAbelianSheaf B X F

AlgebraicGeometry.isConstructibleAbelianSheaf_of_affineZModShriekPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ColimitOfConstructibles.lean, line 441. The attribute's comment: “the same inclusion for the affine form of the displayed cokernels (the tag's concluding sentence), granted Stacks 03S8 (2) at the finite groups Z/nZ as the hypothesis h03S8”.

Stacks 09YT, the affine form of the same inclusion. "In fact, we can even assume U_i and V_j affine": for this inclusion that is a weakening of the hypothesis, since an affine scheme is quasi-compact and quasi-separated, so the affine cokernels are constructible as well.

public theorem isConstructibleAbelianSheaf_of_affineZModShriekPresentation
    (h03S8 : AbelianShriekZModIsConstructible B) (hXc : CompactSpace X.obj)
    (hXq : QuasiSeparatedSpace X.obj)
    {F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1}}
    (hF : HasFiniteZModShriekPresentation B X (SmallEtale.IsAffine B X.obj X.property) F) :
    IsConstructibleAbelianSheaf B X F

AlgebraicGeometry.isConstructibleAbelianSheaf_of_hasFiniteZModShriekPresentation_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ModuleColimitOfConstructibles.lean, line 145. The attribute's comment: “the inclusion of the displayed cokernels at quasi-compact quasi-separated etale objects into the constructible abelian sheaves, with Stacks 03S8 (2) at the finite groups Z/nZ discharged; the reverse inclusion needs Stacks 095N at Lambda = Z/nZ and is not proved here”.

Stacks 09YT, the inclusion of the displayed cokernels into the constructible abelian sheaves. Let X be quasi-compact and quasi-separated. Every abelian sheaf of the form Coker(⨁_j j_{V_j!}(Z/m_jZ) → ⨁_i j_{U_i!}(Z/n_iZ)), with the V_j and U_i quasi-compact quasi-separated objects of X_étale and the m_j, n_i positive, is a constructible abelian sheaf.

This is AlgebraicGeometry.isConstructibleAbelianSheaf_of_hasFiniteZModShriekPresentation with its one hypothesis discharged: Stacks 03S8 (2) at the finite groups Z/nZ by AlgebraicGeometry.abelianShriekZModIsConstructible.

The reverse inclusion — every constructible abelian sheaf has such a presentation — is the other half of the tag and is not proved; the three things it needs, and which two of them this library has, are listed on AlgebraicGeometry.isConstructibleAbelianSheaf_of_hasFiniteZModShriekPresentation.

public theorem isConstructibleAbelianSheaf_of_hasFiniteZModShriekPresentation_of_qcqs
    {F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1}}
    (hF : HasFiniteZModShriekPresentation B X (IsQCQSEtaleObject B X) F) :
    IsConstructibleAbelianSheaf B X F

AlgebraicGeometry.isConstructibleAbelianSheaf_of_affineZModShriekPresentation_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ModuleColimitOfConstructibles.lean, line 160. The attribute's comment: “the same inclusion for the affine form of the displayed cokernels (the tag's concluding sentence), with Stacks 03S8 (2) at the finite groups Z/nZ discharged”.

Stacks 09YT, the affine form of the same inclusion. "In fact, we can even assume U_i and V_j affine": for this inclusion that is a weakening of the hypothesis, since an affine scheme is quasi-compact and quasi-separated.

This is AlgebraicGeometry.isConstructibleAbelianSheaf_of_affineZModShriekPresentation with its one hypothesis discharged, by AlgebraicGeometry.abelianShriekZModIsConstructible.

public theorem isConstructibleAbelianSheaf_of_affineZModShriekPresentation_of_qcqs
    {F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1}}
    (hF : HasFiniteZModShriekPresentation B X (SmallEtale.IsAffine B X.obj X.property) F) :
    IsConstructibleAbelianSheaf B X F

Tag 09Z4, a lemma

Tag 09Z4 in the Stacks Project.

AlgebraicGeometry.IsConstructibleAbelianSheaf.isFinitelyPresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Restriction/CompactConstructibleAbelianViaShriekPresentation.lean, line 67. The attribute's comment: “sheaves of abelian groups”.

The sheaves-of-abelian-groups case of Stacks 09Z4. Let X be a quasi-compact and quasi-separated scheme and let F be a constructible abelian sheaf on X_étale. Then morphisms out of F commute with filtered colimits of abelian sheaves: Mor(F, colim G_i) = colim Mor(F, G_i).

A constructible abelian sheaf is a constructible sheaf of ℤ-modules and ℤ is Noetherian, so this is the module case at Λ = ℤ. Stacks 095N at ℤ, the presentation of a constructible sheaf of ℤ-modules as the cokernel of a map between finite direct sums of extensions by zero of the constant sheaf ℤ at quasi-compact and quasi-separated étale objects, is supplied by AlgebraicGeometry.hasFiniteShriekPresentation_of_isConstructibleModuleSheaf_int.

public theorem IsConstructibleAbelianSheaf.isFinitelyPresentable
    (B : BigEtaleSite.{u}) (X : B.Scheme) [CompactSpace X.1] [QuasiSeparatedSpace X.1]
    (F : Sheaf (SmallEtale.topology B X.1 X.property) AddCommGrpCat.{u + 1})
    (hF : IsConstructibleAbelianSheaf B X F) :
    IsFinitelyPresentable.{u + 1} F

AlgebraicGeometry.IsConstructibleModuleSheaf.isFinitelyPresentable_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Restriction/CompactConstructibleModulesUnconditional.lean, line 78. The attribute's comment: “sheaves of Λ-modules over an arbitrary Noetherian ring, with the inverse image along small étale base change and the sheafification on the slices proved rather than assumed”.

The sheaves-of-Λ-modules case of Stacks 09Z4, with nothing assumed. Let X be a quasi-compact and quasi-separated scheme, let Λ be a Noetherian ring and let F be a constructible sheaf of Λ-modules on X_étale. Then morphisms out of F commute with filtered colimits of sheaves of Λ-modules: Mor(F, colim G_i) = colim Mor(F, G_i).

The inverse image along small étale base change and the sheafification of presheaves of Λ-modules on the slices of the small étale sites, through which constructibility of a sheaf of Λ-modules is stated, are found here by instance search rather than taken as arguments.

public theorem IsConstructibleModuleSheaf.isFinitelyPresentable_unconditional
    (B : BigEtaleSite.{u}) (X : B.Scheme) (R : Type (u + 1)) [CommRing R] [IsNoetherianRing R]
    [CompactSpace X.1] [QuasiSeparatedSpace X.1]
    (F : Sheaf (SmallEtale.topology B X.1 X.property) (ModuleCat.{u + 1} R))
    (hF : IsConstructibleModuleSheaf B X R F) :
    IsFinitelyPresentable.{u + 1} F

AlgebraicGeometry.IsConstructibleModuleSheaf.isFinitelyPresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Restriction/CompactConstructibleModulesViaShriekPresentation.lean, line 71. The attribute's comment: “sheaves of Λ-modules”.

The sheaves-of-Λ-modules case of Stacks 09Z4. Let X be a quasi-compact and quasi-separated scheme, let Λ be a Noetherian ring and let F be a constructible sheaf of Λ-modules on X_étale. Then morphisms out of F commute with filtered colimits of sheaves of Λ-modules: Mor(F, colim G_i) = colim Mor(F, G_i).

Stacks 095N, the presentation of a constructible sheaf of Λ-modules as the cokernel of a map between finite direct sums of extensions by zero of constant free rank-one module sheaves at quasi-compact and quasi-separated étale objects, is supplied by AlgebraicGeometry.isConstructibleModuleSheaf_iff_qcqsShriekPresentation.

public theorem IsConstructibleModuleSheaf.isFinitelyPresentable
    (B : BigEtaleSite.{u}) (X : B.Scheme) (R : Type (u + 1)) [CommRing R] [IsNoetherianRing R]
    [CompactSpace X.1] [QuasiSeparatedSpace X.1]
    [∀ (S T : B.Scheme) (f : T ⟶ S),
      ((smallEtaleBaseChange B f).sheafPushforwardContinuous (ModuleCat.{u + 1} R)
        (SmallEtale.topology B S.1 S.property)
        (SmallEtale.topology B T.1 T.property)).IsRightAdjoint]
    [∀ (T : B.Scheme) (V : SmallEtale B T.1 T.property),
      HasWeakSheafify ((SmallEtale.topology B T.1 T.property).over V) (ModuleCat.{u + 1} R)]
    (F : Sheaf (SmallEtale.topology B X.1 X.property) (ModuleCat.{u + 1} R))
    (hF : IsConstructibleModuleSheaf B X R F) :
    IsFinitelyPresentable.{u + 1} F

AlgebraicGeometry.IsConstructibleSetSheaf.isFinitelyPresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Restriction/CompactConstructibleSetsViaPresentation.lean, line 59. The attribute's comment: “sheaves of sets”.

Let X be a quasi-compact and quasi-separated scheme and let F be a constructible sheaf of sets on X_étale. Then morphisms out of F commute with filtered colimits of sheaves of sets: Mor(F, colim G_i) = colim Mor(F, G_i).

public theorem IsConstructibleSetSheaf.isFinitelyPresentable
    (B : BigEtaleSite.{u}) (X : B.Scheme) [CompactSpace X.1] [QuasiSeparatedSpace X.1]
    (F : Sheaf (SmallEtale.topology B X.1 X.property) (Type (u + 1)))
    (hF : IsConstructibleSetSheaf B X F) :
    IsFinitelyPresentable.{u + 1} F

Tag 095R, a lemma

Tag 095R in the Stacks Project.

AlgebraicGeometry.isConstructibleSetSheaf_pushforward_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/FinitePresentationPushforward.lean, line 149. The attribute's comment: “sheaves of sets”. References: SGA 4 IX (2.14), “(i), sets variant”; SGA 4 XIV (1.1), “special case”; SGA 4 XIV (1.11), “partial”; SGA 4 XIV (1.5), “special case”.

Stacks 095R for sheaves of sets. Let p : T ⟶ S be a finite morphism of finite presentation of a big étale site and let ℱ be a constructible sheaf of sets on T_étale. Then p_*ℱ is a constructible sheaf of sets on S_étale. No hypothesis is imposed on S or T.

By Stacks 095F constructibility may be checked on the covering of S by its affine opens, and over an affine open U the restriction of p_*ℱ is the direct image of the restriction of ℱ along the base change of p to U, which is again finite and of finite presentation; there the source's reduction applies: base change along the surjection of Stacks 095K (1) (Stacks 095Q (1) and 0959), replace the pullback by its finite étale thickening (the unit of a finite universal homeomorphism is an isomorphism), and conclude by Stacks 095H.

public theorem isConstructibleSetSheaf_pushforward_of_isFinite {T S : B.Scheme} (p : T ⟶ S)
    [IsFinite (B.inclusion.map p)] (hfp : FinitePresentation (B.inclusion.map p))
    (F : Sheaf (SmallEtale.topology B T.1 T.property) (Type (u + 1)))
    (hF : IsConstructibleSetSheaf B T F) :
    IsConstructibleSetSheaf B S ((B.smallPushforward p (Type (u + 1))).obj F)

AlgebraicGeometry.isConstructibleAbelianSheaf_pushforward_of_isFinite_of_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/FinitePresentationPushforwardModules.lean, line 432. The attribute's comment: “abelian groups”.

[Stacks, Tag 095R], abelian sheaves. Let f : T ⟶ S be a finite and finitely presented morphism of a big étale site. If ℱ is a constructible abelian sheaf on T_étale, then f_*ℱ is a constructible abelian sheaf on S_étale.

theorem isConstructibleAbelianSheaf_pushforward_of_isFinite_of_finitePresentation {T S : B.Scheme}
    (f : T ⟶ S) [IsFinite (B.inclusion.map f)] (hfp : FinitePresentation (B.inclusion.map f))
    (F : Sheaf (SmallEtale.topology B T.1 T.property) AddCommGrpCat.{u + 1})
    (hF : IsConstructibleAbelianSheaf B T F) :
    IsConstructibleAbelianSheaf B S ((B.smallPushforward f AddCommGrpCat.{u + 1}).obj F)

AlgebraicGeometry.isConstructibleModuleSheaf_pushforward_of_isFinite_of_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/FinitePresentationPushforwardModules.lean, line 509. The attribute's comment: “sheaves of Λ-modules, Λ Noetherian”. References: SGA 4 IX (2.14), “(i), A-module variant”; SGA 5 I (1.14), “b)”.

[Stacks, Tag 095R], sheaves of modules. Let f : T ⟶ S be a finite and finitely presented morphism of a big étale site and let Λ be a Noetherian ring. If ℱ is a constructible sheaf of Λ-modules on T_étale, then f_*ℱ is a constructible sheaf of Λ-modules on S_étale.

theorem isConstructibleModuleSheaf_pushforward_of_isFinite_of_finitePresentation {T S : B.Scheme}
    (f : T ⟶ S) [IsFinite (B.inclusion.map f)] (hfp : FinitePresentation (B.inclusion.map f))
    (F : Sheaf (SmallEtale.topology B T.1 T.property) (ModuleCat.{u + 1} Λ))
    (hF : IsConstructibleModuleSheaf B T Λ F) :
    IsConstructibleModuleSheaf B S Λ ((B.smallPushforward f (ModuleCat.{u + 1} Λ)).obj F)

AlgebraicGeometry.isConstructibleSetSheaf_pushforward_of_universalHomeomorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/FiniteUniversalHomeomorphismPushforward.lean, line 269. The attribute's comment: “sheaves of sets, and only the case of a finite universal homeomorphism — equivalently of a finite, surjective and universally injective morphism; the finite presentation of the tag's hypothesis is not needed and is dropped. The general finite, finitely presented case is NOT proved: it needs the thickening reduction of Stacks 095K together with the equivalence of small étale topoi of Stacks 04DZ on the size-bounded site, which this library does not carry. Stacks 095Q (1)'s descent is granted as the only hypothesis, and nothing is assumed of S or T.”.

Stacks 095R for sheaves of sets and a finite universal homeomorphism. Let p : T ⟶ S be a finite morphism of a big étale site which is in addition a universal homeomorphism, and let ℱ be a constructible sheaf of sets on T_étale. Then p_*ℱ is a constructible sheaf of sets on S_étale. No hypothesis is imposed on S or T, and no finite presentation of p is needed.

By Stacks 095F constructibility may be checked on the covering of S by its affine opens, and over an affine open U the restriction of p_*ℱ is the direct image of the restriction of ℱ along the base change of p to U, which is again finite and a universal homeomorphism; the source of that base change is finite over the affine U, hence affine, so both are quasi-compact and quasi-separated and AlgebraicGeometry.isConstructibleSetSheaf_pushforward_of_universalHomeomorphism_of_compactSpace applies.

Stacks 095Q (1) is carried as the hypothesis h095Q, exactly as in that theorem; it quantifies over all morphisms of the site, so the Zariski reduction does not add to what is granted.

public theorem isConstructibleSetSheaf_pushforward_of_universalHomeomorphism
    [IsFinite (B.inclusion.map p)] [UniversalHomeomorphism (B.inclusion.map p)]
    (h095Q : SetConstructibilityDescendsAlongSurjective B)
    (F : Sheaf (SmallEtale.topology B T.1 T.property) (Type (u + 1)))
    (hF : IsConstructibleSetSheaf B T F) :
    IsConstructibleSetSheaf B S ((B.smallPushforward p (Type (u + 1))).obj F)

Stacks.EtaleCohomology.isConstructibleEtaleModule_directImage_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleSheaves/FiniteDirectImage.lean, line 241. The attribute's comment: “sheaves of Λ-modules, Λ a Noetherian ring in Type, on Mathlib's small étale site (IsBigSiteConstructibleEtaleModule); f finite and of finite presentation, no hypothesis on X or Y”.

Finite direct image preserves constructibility. Let Λ : Type be a Noetherian ring and f : X ⟶ Y a finite morphism of finite presentation of B. If ℱ is a constructible sheaf of Λ-modules on Mathlib's small étale site of X, then f_*ℱ is constructible.

theorem isConstructibleEtaleModule_directImage_of_isFinite {X Y : B.Scheme} (f : X ⟶ Y)
    [IsFinite (B.inclusion.map f)] [LocallyOfFinitePresentation (B.inclusion.map f)]
    {F : EtaleModules.{u, 0} Λ X.obj} (hF : IsBigSiteConstructibleEtaleModule B X Λ F) :
    IsBigSiteConstructibleEtaleModule B Y Λ
      ((etaleModuleDirectImage.{u, 0} Λ (B.inclusion.map f)).obj F)

Stacks.EtaleCohomology.isConstructibleEtaleModule_etaleModuleDirectImage_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LowerShriekAffineLine/ConstructibleDescent.lean, line 275. The attribute's comment: “sheaves of modules over a Noetherian ring”.

Stacks 095R for sheaves of modules, in the model EtaleModules. Let f : X ⟶ Y be a finite morphism of finite presentation, Λ a Noetherian ring and ℱ a constructible sheaf of Λ-modules on X_étale. Then f_* ℱ is constructible.

By Stacks 095F it suffices to work over the affine opens of Y, the direct image commuting with restriction to an open by Stacks 0959. Over an affine Y, Stacks 095K (1) gives a surjective affine Y' ⟶ Y and a thickening Z' ⊆ Y' ×_Y X with Z' ⟶ Y' finite étale; by Stacks 095Q and 0959 it suffices to treat the base change, where the direct image is that along the finite étale Z' ⟶ Y' of the inverse image to Z' (a thickening induces an equivalence of small étale topoi), constructible by Stacks 095H.

The coefficient ring lives in Type (u + 1), the universe of the library's Stacks 095Q and 095H for sheaves of modules.

theorem isConstructibleEtaleModule_etaleModuleDirectImage_of_isFinite {X Y : Scheme.{u}}
    (f : X ⟶ Y) [IsFinite f] (hfp : FinitePresentation f) (F : EtaleModules.{u, u + 1} Λ X)
    (hF : IsConstructibleEtaleModule Λ F) :
    IsConstructibleEtaleModule Λ ((etaleModuleDirectImage.{u, u + 1} Λ f).obj F)

Stacks.EtaleCohomology.isConstructibleEtaleAbelianSheaf_etaleAbelianDirectImage_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ProperBaseChange/AbelianConstructibleImages.lean, line 119. The attribute's comment: “sheaves of abelian groups”.

[Stacks, Tag 095R], for sheaves of abelian groups. Let f : X ⟶ Y be a finite morphism of finite presentation and F a constructible abelian sheaf on X_étale. Then f_* F is constructible.

As a sheaf of ULift ℤ-modules, F is constructible, so f_* F is a constructible sheaf of ULift ℤ-modules by the module case of the tag (Stacks.EtaleCohomology.isConstructibleEtaleModule_etaleModuleDirectImage_of_isFinite). It is moreover torsion: F is torsion, being constructible (Stacks.EtaleCohomology.torsionSheafProperty_of_isConstructibleEtaleAbelianSheaf), and the direct image along the quasi-compact quasi-separated f of a torsion sheaf is torsion (Stacks.EtaleCohomology.torsionSheafProperty_smallEtaleDirectImageAb, Tag 0DDD (1) in degree zero). A constructible torsion sheaf of ULift ℤ-modules has constructible underlying abelian sheaf. No torsion hypothesis is imposed on F.

theorem isConstructibleEtaleAbelianSheaf_etaleAbelianDirectImage_of_isFinite {X Y : Scheme.{u}}
    (f : X ⟶ Y) [IsFinite f] (hfp : FinitePresentation f)
    (F : Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1})
    (hF : _root_.Stacks.EtaleCohomology.IsConstructibleSmallEtaleAbelianSheaf.{u, 0} F) :
    _root_.Stacks.EtaleCohomology.IsConstructibleSmallEtaleAbelianSheaf.{u, 0}
      ((etaleAbelianDirectImage.{u, 0} f).obj F)

Tag 09YU, a lemma

Tag 09YU in the Stacks Project.

AlgebraicGeometry.smallEtaleStagesFull_isConstructibleAbelianSheaf_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/LimitCategory/AbelianLimit.lean, line 62. The attribute's comment: “clause (2), the fullness assertion”.

Stacks 09YU, clause (2), the fullness assertion.

theorem smallEtaleStagesFull_isConstructibleAbelianSheaf_unconditional (hc : IsLimit c)
    (haff : ∀ {p q : Iᵒᵖ} (e : p ⟶ q), IsAffineHom (B.inclusion.map (Dg.map e)))
    (hqc : ∀ p : I, CompactSpace (Dg.obj (op p)).obj)
    (hqs : ∀ p : I, QuasiSeparatedSpace (Dg.obj (op p)).obj) :
    SmallEtaleStagesFull B AddCommGrpCat.{u + 1} Dg c hX
      (fun Y => IsConstructibleAbelianSheaf B Y)

AlgebraicGeometry.smallEtaleStagesEssSurj_isConstructibleAbelianSheaf_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/LimitCategory/AbelianLimit.lean, line 77. The attribute's comment: “clause (2), the essential surjectivity assertion”.

Stacks 09YU, clause (2), the essential surjectivity assertion. Every constructible abelian sheaf on X_étale is isomorphic to the inverse image of a constructible abelian sheaf on some (X_i)_étale.

theorem smallEtaleStagesEssSurj_isConstructibleAbelianSheaf_unconditional (hc : IsLimit c)
    (haff : ∀ {p q : Iᵒᵖ} (e : p ⟶ q), IsAffineHom (B.inclusion.map (Dg.map e)))
    (hqc : ∀ p : I, CompactSpace (Dg.obj (op p)).obj)
    (hqs : ∀ p : I, QuasiSeparatedSpace (Dg.obj (op p)).obj) :
    SmallEtaleStagesEssSurj B AddCommGrpCat.{u + 1} Dg c hX
      (fun Y => IsConstructibleAbelianSheaf B Y)

AlgebraicGeometry.smallEtaleStagesColimit_isConstructibleAbelianSheaf_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/LimitCategory/AbelianLimit.lean, line 126. The attribute's comment: “clause (2)”.

Stacks 09YU, clause (2). Let X = lim X_i be the limit of a directed inverse system of schemes with affine transition morphisms, each X_i quasi-compact and quasi-separated. The category of constructible abelian sheaves on X_étale is the colimit of the categories of constructible abelian sheaves on the (X_i)_étale: the comparison is faithful, full and essentially surjective.

theorem smallEtaleStagesColimit_isConstructibleAbelianSheaf_unconditional (hc : IsLimit c)
    (haff : ∀ {p q : Iᵒᵖ} (e : p ⟶ q), IsAffineHom (B.inclusion.map (Dg.map e)))
    (hqc : ∀ p : I, CompactSpace (Dg.obj (op p)).obj)
    (hqs : ∀ p : I, QuasiSeparatedSpace (Dg.obj (op p)).obj) :
    SmallEtaleStagesColimit B AddCommGrpCat.{u + 1} Dg c hX
      (fun Y => IsConstructibleAbelianSheaf B Y)

AlgebraicGeometry.smallEtaleStagesEssSurj_isConstructibleModuleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/LimitCategory/ModuleEssSurj.lean, line 77. The attribute's comment: “clause (3), the essential surjectivity assertion”. References: SGA 4 IX (2.7.4), “partial, special case”.

Stacks 09YU, clause (3), the essential surjectivity assertion. Let X = lim X_i be the limit of a directed inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms and let Λ be a Noetherian ring. Every constructible sheaf of Λ-modules on X_étale is isomorphic to the inverse image of a constructible sheaf of Λ-modules on some (X_i)_étale.

A constructible sheaf is the cokernel of a map between finite direct sums of sheaves j_{U!}Λ with U affine (Stacks 095N); the affine U are base changed from a stage (Stacks 0EYL for objects, which is Stacks 01ZM and 07RP), extension by zero commutes with base change, and the map comes from a later stage by the fullness assertion; its cokernel there is constructible and pulls back to the given sheaf, inverse image being right exact.

theorem smallEtaleStagesEssSurj_isConstructibleModuleSheaf [IsNoetherianRing Λ] (hc : IsLimit c)
    (haff : ∀ {p q : Iᵒᵖ} (e : p ⟶ q), IsAffineHom (B.inclusion.map (Dg.map e)))
    (hqc : ∀ p : I, CompactSpace (Dg.obj (op p)).obj)
    (hqs : ∀ p : I, QuasiSeparatedSpace (Dg.obj (op p)).obj) :
    SmallEtaleStagesEssSurj B (ModuleCat.{u + 1} Λ) Dg c hX
      (fun Y => IsConstructibleModuleSheaf B Y Λ)

AlgebraicGeometry.smallEtaleStagesColimit_isConstructibleModuleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/LimitCategory/ModuleEssSurj.lean, line 173. The attribute's comment: “clause (3)”.

Stacks 09YU, clause (3). Let X = lim X_i be the limit of a directed inverse system of schemes with affine transition morphisms, each X_i quasi-compact and quasi-separated, and let Λ be a Noetherian ring. The category of constructible sheaves of Λ-modules on X_étale is the colimit of the categories of constructible sheaves of Λ-modules on the (X_i)_étale: the comparison, built from the inverse images and the canonical comparisons of iterated inverse images, is faithful, full and essentially surjective. For a directed index these three conditions are exactly the assertion that the canonical functor from the filtered colimit of the categories is an equivalence.

Nothing is assumed beyond the source's hypotheses: a nonempty directed index, a limit cone, affine transition morphisms, and quasi-compact quasi-separated stages.

theorem smallEtaleStagesColimit_isConstructibleModuleSheaf [IsNoetherianRing Λ] (hc : IsLimit c)
    (haff : ∀ {p q : Iᵒᵖ} (e : p ⟶ q), IsAffineHom (B.inclusion.map (Dg.map e)))
    (hqc : ∀ p : I, CompactSpace (Dg.obj (op p)).obj)
    (hqs : ∀ p : I, QuasiSeparatedSpace (Dg.obj (op p)).obj) :
    SmallEtaleStagesColimit B (ModuleCat.{u + 1} Λ) Dg c hX
      (fun Y => IsConstructibleModuleSheaf B Y Λ)

AlgebraicGeometry.smallEtaleStagesFull_isConstructibleModuleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/LimitCategory/ModuleFullness.lean, line 217. The attribute's comment: “clause (3), the fullness assertion”. References: SGA 4 IX (2.7.4), “partial”.

Stacks 09YU, clause (3), the fullness assertion. Let X = lim X_i be the limit of a directed inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms and let Λ be a Noetherian ring. Every map between the inverse images to X_étale of two constructible sheaves of Λ-modules on (X_i)_étale is the inverse image of a map at some later stage, read through the canonical comparison of inverse images.

A constructible sheaf is a quotient of a finite direct sum of sheaves j_{U!}Λ with U affine by Stacks 095N; the map on the sum comes from a stage by the degree zero case of Stacks 09YQ, its restriction to the kernel vanishes on X and hence, by the faithfulness assertion, at a later stage, where the map descends to the quotient.

theorem smallEtaleStagesFull_isConstructibleModuleSheaf [IsNoetherianRing Λ] (hc : IsLimit c)
    (haff : ∀ {p q : Iᵒᵖ} (e : p ⟶ q), IsAffineHom (B.inclusion.map (Dg.map e)))
    (hqc : ∀ p : I, CompactSpace (Dg.obj (op p)).obj)
    (hqs : ∀ p : I, QuasiSeparatedSpace (Dg.obj (op p)).obj) :
    SmallEtaleStagesFull B (ModuleCat.{u + 1} Λ) Dg c hX
      (fun Y => IsConstructibleModuleSheaf B Y Λ)

AlgebraicGeometry.smallEtaleStagesFaithful_isConstructibleAbelianSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StageColimitCompletion.lean, line 166. The attribute's comment: “clause (2), the faithfulness assertion”.

Stacks 09YU, clause (2), the faithfulness assertion. Let X = lim X_i be the limit of a directed inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms. Two maps of constructible sheaves of abelian groups on (X_i)_étale whose inverse images to X_étale agree agree after inverse image to some later stage.

The image of the difference of the two maps is constructible by Tag 03RZ, so the locus where it has a nonzero geometric stalk is constructible by Tag 09YS (2); inverse image to X is exact and kills the difference, hence the image, so by Tag 03Q1 that locus misses the image of X and by Tag 05F4 the image of a later stage, where Tag 03PU makes the inverse image of the image sheaf zero.

public theorem smallEtaleStagesFaithful_isConstructibleAbelianSheaf (hc : IsLimit c)
    (haff : ∀ {p q : Iᵒᵖ} (e : p ⟶ q), IsAffineHom (B.inclusion.map (Dg.map e)))
    (hqc : ∀ p : I, CompactSpace (Dg.obj (op p)).obj)
    (hqs : ∀ p : I, QuasiSeparatedSpace (Dg.obj (op p)).obj) :
    SmallEtaleStagesFaithful B AddCommGrpCat.{u + 1} Dg c hX
      (fun Y => IsConstructibleAbelianSheaf B Y)

AlgebraicGeometry.smallEtaleStagesEssSurj_isConstructibleSetSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StageConstructibleSetSheafDescent.lean, line 454. The attribute's comment: “clause (1), the essential surjectivity assertion”. References: SGA 4 IX (2.7.4), “partial, special case”.

Stacks 09YU, clause (1), the essential surjectivity assertion. Let X = lim X_i be the limit of a directed inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms inside a big étale site. Every constructible sheaf of sets on X_étale is isomorphic to the inverse image of a constructible sheaf of sets on (X_i)_étale for some i.

Tag 09Y9 presents the sheaf as a coequalizer of two maps between finite coproducts of sheaves represented by quasi-compact and quasi-separated objects; those coproducts are represented by the disjoint unions of the objects, so the two maps are a parallel pair of morphisms of the site, which descends to a stage by AlgebraicGeometry.exists_stage_smallEtaleModel_parallelPair_of_qcqs. The coequalizer of the descended pair of representable sheaves is constructible at that stage by Tag 03RZ and Tag 03S8 part (1), and inverse image, a left adjoint commuting with the sheafified Yoneda embedding, carries it to the given sheaf.

public theorem smallEtaleStagesEssSurj_isConstructibleSetSheaf (hc : IsLimit c)
    (haff : ∀ {p q : Iᵒᵖ} (e : p ⟶ q), IsAffineHom (B.inclusion.map (Dg.map e)))
    (hqc : ∀ p : I, CompactSpace (Dg.obj (op p)).obj)
    (hqs : ∀ p : I, QuasiSeparatedSpace (Dg.obj (op p)).obj) :
    SmallEtaleStagesEssSurj B (Type (u + 1)) Dg c hX
      (fun X => IsConstructibleSetSheaf B X)

AlgebraicGeometry.smallEtaleStagesFaithful_isConstructibleSetSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StageFaithfulness.lean, line 218. The attribute's comment: “clause (1), the faithfulness assertion”.

Stacks 09YU, clause (1), the faithfulness assertion. Let X = lim X_i be the limit of a directed inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms. Two maps of constructible sheaves of sets on (X_i)_étale whose inverse images to X_étale agree agree after inverse image to some later stage.

The locus in X_i where the two maps have the same geometric stalk is the locus where the geometric stalk of the inclusion of their equalizer is surjective; the equalizer is constructible by Tag 03RZ, so that locus is constructible by Tag 09YS and contains the image of X, hence by Tag 05F4 the image of a later stage, where Tag 03PU turns the inverse image of the inclusion into an isomorphism.

public theorem smallEtaleStagesFaithful_isConstructibleSetSheaf (hc : IsLimit c)
    (haff : ∀ {p q : Iᵒᵖ} (e : p ⟶ q), IsAffineHom (B.inclusion.map (Dg.map e)))
    (hqc : ∀ p : I, CompactSpace (Dg.obj (op p)).obj)
    (hqs : ∀ p : I, QuasiSeparatedSpace (Dg.obj (op p)).obj) :
    SmallEtaleStagesFaithful B (Type (u + 1)) Dg c hX
      (fun Y => IsConstructibleSetSheaf B Y)

AlgebraicGeometry.smallEtaleStagesFaithful_isConstructibleModuleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StageFaithfulnessModules.lean, line 172. The attribute's comment: “clause (3), the faithfulness assertion”.

Stacks 09YU, clause (3), the faithfulness assertion. Let X = lim X_i be the limit of a directed inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms and let Λ be a Noetherian ring. Two maps of constructible sheaves of Λ-modules on (X_i)_étale whose inverse images to X_étale agree agree after inverse image to some later stage.

The image of the difference of the two maps is constructible by Tag 03RZ (3), so its support is constructible by Tag 09YS (3); inverse image to X is exact and kills the difference, hence the image, so by Tag 03Q1 that support misses the image of X and by Tag 05F4 the image of a later stage, where Tag 03PU makes the inverse image of the image sheaf zero.

public theorem smallEtaleStagesFaithful_isConstructibleModuleSheaf (hc : IsLimit c)
    (haff : ∀ {p q : Iᵒᵖ} (e : p ⟶ q), IsAffineHom (B.inclusion.map (Dg.map e)))
    (hqc : ∀ p : I, CompactSpace (Dg.obj (op p)).obj)
    (hqs : ∀ p : I, QuasiSeparatedSpace (Dg.obj (op p)).obj) :
    SmallEtaleStagesFaithful B (ModuleCat.{u + 1} Λ) Dg c hX
      (fun Y => IsConstructibleModuleSheaf B Y Λ)

AlgebraicGeometry.smallEtaleStagesColimit_isConstructibleSetSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StageFullness.lean, line 1073. The attribute's comment: “clause (1)”.

Stacks 09YU, clause (1). Let X = lim X_i be the limit of a directed inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms inside a big étale site. The category of constructible sheaves of sets on X_étale is the colimit of the categories of constructible sheaves of sets on the (X_i)_étale, along étale inverse image: the comparison is faithful (AlgebraicGeometry.smallEtaleStagesFaithful_isConstructibleSetSheaf), full (AlgebraicGeometry.smallEtaleStagesFull_isConstructibleSetSheaf) and essentially surjective (AlgebraicGeometry.smallEtaleStagesEssSurj_isConstructibleSetSheaf), which over a directed index is the assertion that the category on the limit is the filtered colimit of the categories at the stages.

public theorem smallEtaleStagesColimit_isConstructibleSetSheaf (hc : IsLimit c)
    (haff : ∀ {p q : Iᵒᵖ} (e : p ⟶ q), IsAffineHom (B.inclusion.map (Dg.map e)))
    (hqc : ∀ p : I, CompactSpace (Dg.obj (op p)).obj)
    (hqs : ∀ p : I, QuasiSeparatedSpace (Dg.obj (op p)).obj) :
    SmallEtaleStagesColimit B (Type (u + 1)) Dg c hX (fun X => IsConstructibleSetSheaf B X)

AlgebraicGeometry.smallEtaleStagesColimit_isConstructibleAbelianSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StageFullnessAbelian.lean, line 1049. The attribute's comment: “clause (2)”.

Stacks 09YU, clause (2). Let X = lim X_i be the limit of a directed inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms inside a big étale site. The category of constructible abelian sheaves on X_étale is the colimit of the categories of constructible abelian sheaves on the (X_i)_étale, along étale inverse image: the comparison is faithful (AlgebraicGeometry.smallEtaleStagesFaithful_isConstructibleAbelianSheaf), full (AlgebraicGeometry.smallEtaleStagesFull_isConstructibleAbelianSheaf) and essentially surjective (AlgebraicGeometry.smallEtaleStagesEssSurj_isConstructibleAbelianSheaf), which over a directed index is the assertion that the category on the limit is the filtered colimit of the categories at the stages.

public theorem smallEtaleStagesColimit_isConstructibleAbelianSheaf [Nonempty I]
    [IsDirected I (· ≤ ·)] (hc : IsLimit c)
    (haff : ∀ {p q : Iᵒᵖ} (e : p ⟶ q), IsAffineHom (B.inclusion.map (Dg.map e)))
    (hqc : ∀ p : I, CompactSpace (Dg.obj (op p)).obj)
    (hqs : ∀ p : I, QuasiSeparatedSpace (Dg.obj (op p)).obj) :
    SmallEtaleStagesColimit B AddCommGrpCat.{u + 1} Dg c hX
      (fun Y => IsConstructibleAbelianSheaf B Y)

AlgebraicGeometry.exists_stage_isConstructibleSetSheaf_iso_sheafifiedYoneda, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StageRepresentableEssSurj.lean, line 152. The attribute's comment: “clause (1), the essential surjectivity assertion for the sheaves represented by a quasi-compact and quasi-separated object of the small etale site, which is the case the source's proof reduces that assertion to”.

Stacks 09YU, clause (1), the essential surjectivity assertion for a representable sheaf. Let X = lim X_i be the limit of a directed inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms inside a big étale site. For every quasi-compact and quasi-separated object U of X_étale there is a stage i and a constructible sheaf of sets on (X_i)_étale whose inverse image to X_étale is the sheaf h_U represented by U.

This is the case of the essential surjectivity assertion of clause (1) to which the source reduces it through Tag 09Y9. The object U is descended to the stage by AlgebraicGeometry.exists_stage_smallEtaleModel_of_qcqs; inverse image carries the representable sheaf of the descended object to the representable sheaf of its base change, because inverse image along a continuous functor commutes with the sheafified Yoneda embedding; and the representable sheaf of a quasi-compact and quasi-separated object is constructible by Tag 03S8 part (1).

public theorem exists_stage_isConstructibleSetSheaf_iso_sheafifiedYoneda (hc : IsLimit c)
    (haff : ∀ {p q : Iᵒᵖ} (e : p ⟶ q), IsAffineHom (B.inclusion.map (Dg.map e)))
    (hqc : ∀ p : I, CompactSpace (Dg.obj (op p)).obj)
    (hqs : ∀ p : I, QuasiSeparatedSpace (Dg.obj (op p)).obj)
    (U : SmallEtale B c.pt hX)
    (hUc : CompactSpace U.obj.left.obj) (hUq : QuasiSeparatedSpace U.obj.left.obj) :
    ∃ (i : I) (Fi : Sheaf (SmallEtale.topology B (Dg.obj (op i)).obj
        (Dg.obj (op i)).property) (Type (u + 1))),
      IsConstructibleSetSheaf B (Dg.obj (op i)) Fi ∧
        Nonempty ((smallEtaleStageProjection B (Type (u + 1)) Dg c hX i).obj Fi ≅
          (Sheaf.sheafifiedYoneda (SmallEtale.topology B c.pt hX)).obj U)

Tag 0GL2, a lemma

Tag 0GL2 in the Stacks Project.

AlgebraicGeometry.smallEtaleStagesColimit_isFiniteLocallyConstant_type, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/FiniteLocallyConstantLimitColimit.lean, line 68. The attribute's comment: “part (1)”.

Stacks Tag 0GL2, clause (1). Let X = lim X_i be the limit of a directed inverse system of quasi-compact, quasi-separated schemes with affine transition morphisms. The category of finite locally constant sheaves of sets on X_étale is the colimit of the categories of finite locally constant sheaves of sets on the (X_i)_étale: the comparison is faithful, full and essentially surjective.

public theorem smallEtaleStagesColimit_isFiniteLocallyConstant_type (hc : IsLimit c)
    (haff : ∀ {p q : Iᵒᵖ} (e : p ⟶ q), IsAffineHom (B.inclusion.map (Dg.map e)))
    (hqc : ∀ p : I, CompactSpace (Dg.obj (op p)).obj)
    (hqs : ∀ p : I, QuasiSeparatedSpace (Dg.obj (op p)).obj) :
    SmallEtaleStagesColimit B (Type (u + 1)) Dg c hX
      (isFiniteLocallyConstantSmallEtaleSheaf B (Type (u + 1)))

AlgebraicGeometry.smallEtaleStagesColimit_isFiniteLocallyConstant_addCommGrpCat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/FiniteLocallyConstantLimitColimit.lean, line 83. The attribute's comment: “part (2)”.

Stacks Tag 0GL2, clause (2). Let X = lim X_i be the limit of a directed inverse system of quasi-compact, quasi-separated schemes with affine transition morphisms. The category of finite locally constant abelian sheaves on X_étale is the colimit of the categories of finite locally constant abelian sheaves on the (X_i)_étale.

public theorem smallEtaleStagesColimit_isFiniteLocallyConstant_addCommGrpCat (hc : IsLimit c)
    (haff : ∀ {p q : Iᵒᵖ} (e : p ⟶ q), IsAffineHom (B.inclusion.map (Dg.map e)))
    (hqc : ∀ p : I, CompactSpace (Dg.obj (op p)).obj)
    (hqs : ∀ p : I, QuasiSeparatedSpace (Dg.obj (op p)).obj) :
    SmallEtaleStagesColimit B AddCommGrpCat.{u + 1} Dg c hX
      (isFiniteLocallyConstantSmallEtaleSheaf B AddCommGrpCat.{u + 1})

AlgebraicGeometry.smallEtaleStagesColimit_isFiniteTypeLocallyConstant_moduleCat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/FiniteLocallyConstantLimitColimit.lean, line 101. The attribute's comment: “part (3)”.

Stacks Tag 0GL2, clause (3). Let X = lim X_i be the limit of a directed inverse system of quasi-compact, quasi-separated schemes with affine transition morphisms and let Λ be a commutative ring (the source assumes Λ Noetherian; that is not needed). The category of finite type, locally constant sheaves of Λ-modules on X_étale is the colimit of the categories of finite type, locally constant sheaves of Λ-modules on the (X_i)_étale.

public theorem smallEtaleStagesColimit_isFiniteTypeLocallyConstant_moduleCat
    (Λ : Type (u + 1)) [CommRing Λ] (hc : IsLimit c)
    (haff : ∀ {p q : Iᵒᵖ} (e : p ⟶ q), IsAffineHom (B.inclusion.map (Dg.map e)))
    (hqc : ∀ p : I, CompactSpace (Dg.obj (op p)).obj)
    (hqs : ∀ p : I, QuasiSeparatedSpace (Dg.obj (op p)).obj) :
    SmallEtaleStagesColimit B (ModuleCat.{u + 1} Λ) Dg c hX
      (isFiniteTypeLocallyConstantSmallEtaleSheaf B Λ)

Tag 09BG, a lemma

Tag 09BG in the Stacks Project.

AlgebraicGeometry.constantSetSubsheaf_eq_of_genericStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstantSubsheafGenericStalk.lean, line 161. The attribute's comment: “part (1)”.

Stacks 09BG (1). A subsheaf of a constant sheaf of sets on an irreducible scheme which contains the constant subsheaf on its geometric generic stalk is that constant subsheaf.

public theorem constantSetSubsheaf_eq_of_genericStalk
    [HasWeakSheafify (SmallEtale.topology B X hX) (Type (u + 1))]
    {T' T : Type (u + 1)} (m : T' ⟶ T) [Mono m]
    (G : Sheaf (SmallEtale.topology B X hX) (Type (u + 1)))
    (i : (constantSheaf (SmallEtale.topology B X hX) (Type (u + 1))).obj T' ⟶ G)
    (j : G ⟶ (constantSheaf (SmallEtale.topology B X hX) (Type (u + 1))).obj T) [Mono j]
    (hij : i ≫ j = (constantSheaf (SmallEtale.topology B X hX) (Type (u + 1))).map m)
    (hstalk : IsIso (colimMap (Functor.whiskerLeft
      (CategoryOfElements.π (geometricPointFiber B X hX s)).op i.hom))) :
    IsIso i

AlgebraicGeometry.constantAbelianSubsheaf_eq_of_genericStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstantSubsheafGenericStalk.lean, line 180. The attribute's comment: “part (2)”.

Stacks 09BG (2). A subsheaf of a constant sheaf of abelian groups on an irreducible scheme which contains the constant subsheaf on its geometric generic stalk is that constant subsheaf.

public theorem constantAbelianSubsheaf_eq_of_genericStalk
    [HasWeakSheafify (SmallEtale.topology B X hX) AddCommGrpCat.{u + 1}]
    {A' A : AddCommGrpCat.{u + 1}} (m : A' ⟶ A) [Mono m]
    (G : Sheaf (SmallEtale.topology B X hX) AddCommGrpCat.{u + 1})
    (i : (constantSheaf (SmallEtale.topology B X hX) AddCommGrpCat.{u + 1}).obj A' ⟶ G)
    (j : G ⟶ (constantSheaf (SmallEtale.topology B X hX) AddCommGrpCat.{u + 1}).obj A) [Mono j]
    (hij : i ≫ j = (constantSheaf (SmallEtale.topology B X hX) AddCommGrpCat.{u + 1}).map m)
    (hstalk : IsIso (colimMap (Functor.whiskerLeft
      (CategoryOfElements.π (geometricPointFiber B X hX s)).op i.hom))) :
    IsIso i

AlgebraicGeometry.constantModuleSubsheaf_eq_of_genericStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstantSubsheafGenericStalk.lean, line 198. The attribute's comment: “part (3)”.

Stacks 09BG (3). A subsheaf of a constant sheaf of modules on an irreducible scheme which contains the constant subsheaf on its geometric generic stalk is that constant subsheaf.

public theorem constantModuleSubsheaf_eq_of_genericStalk (Λ : Type (u + 1)) [Ring Λ]
    [HasWeakSheafify (SmallEtale.topology B X hX) (ModuleCat.{u + 1} Λ)]
    {M' M : ModuleCat.{u + 1} Λ} (m : M' ⟶ M) [Mono m]
    (G : Sheaf (SmallEtale.topology B X hX) (ModuleCat.{u + 1} Λ))
    (i : (constantSheaf (SmallEtale.topology B X hX) (ModuleCat.{u + 1} Λ)).obj M' ⟶ G)
    (j : G ⟶ (constantSheaf (SmallEtale.topology B X hX) (ModuleCat.{u + 1} Λ)).obj M) [Mono j]
    (hij : i ≫ j = (constantSheaf (SmallEtale.topology B X hX) (ModuleCat.{u + 1} Λ)).map m)
    (hstalk : IsIso (colimMap (Functor.whiskerLeft
      (CategoryOfElements.π (geometricPointFiber B X hX s)).op i.hom))) :
    IsIso i

Tag 09Z5, a lemma

Tag 09Z5 in the Stacks Project.

Stacks.EtaleCohomology.isIso_constantSheafPushforwardComparison_genericPointInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstantSheafPushforwardNormal.lean, line 419. The attribute's comment: “part (1)”. References: SGA 4 IX (2.14.1), “special case”; SGA 7 VIII (5.1), “special case”.

On an integral normal scheme the direct image of a constant sheaf of sets along the inclusion of the generic point is the constant sheaf: the canonical comparison morphism is an isomorphism.

theorem isIso_constantSheafPushforwardComparison_genericPointInclusion (X : Scheme.{u})
    [AlgebraicGeometry.IsIntegral X] [IsNormal X] (E : Type (max (u + 1) v)) :
    IsIso (constantSheafPushforwardComparison.{u, v} (genericPointInclusion X) E)

Stacks.EtaleCohomology.constantSheafGenericPointPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstantSheafPushforwardNormal.lean, line 435. The attribute's comment: “part (1)”. References: SGA 4 IX (2.14.1), “special case”; SGA 7 VIII (5.1), “special case”.

The identification g_* E̲ = E̲ of the direct image of a constant sheaf of sets along the inclusion g : Spec K ⟶ X of the generic point of an integral normal scheme with the constant sheaf, given by the canonical comparison morphism.

def constantSheafGenericPointPushforwardIso (X : Scheme.{u})
    [AlgebraicGeometry.IsIntegral X] [IsNormal X] (E : Type (max (u + 1) v)) :
    (constantSheaf X.smallEtaleTopology (Type (max (u + 1) v))).obj E ≅
      (smallEtaleDirectImage.{u, v} (genericPointInclusion X)).obj
        ((constantSheaf (Spec X.functionField).smallEtaleTopology
          (Type (max (u + 1) v))).obj E)

Stacks.EtaleCohomology.isIso_constantSheafPushforwardComparison_opensIota, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstantSheafPushforwardNormal.lean, line 448. The attribute's comment: “part (2)”.

On an integral normal scheme the direct image of a constant sheaf of sets along the inclusion of a nonempty open subscheme is the constant sheaf: the canonical comparison morphism is an isomorphism.

theorem isIso_constantSheafPushforwardComparison_opensIota {X : Scheme.{u}}
    [AlgebraicGeometry.IsIntegral X] [IsNormal X] (U : X.Opens) (hU : (U : Set X).Nonempty)
    (E : Type (max (u + 1) v)) :
    IsIso (constantSheafPushforwardComparison.{u, v} U.ι E)

Stacks.EtaleCohomology.constantSheafOpensPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstantSheafPushforwardNormal.lean, line 463. The attribute's comment: “part (2)”.

The identification j_* E̲ = E̲ of the direct image of a constant sheaf of sets along the inclusion j : U ⟶ X of a nonempty open subscheme of an integral normal scheme with the constant sheaf, given by the canonical comparison morphism.

def constantSheafOpensPushforwardIso {X : Scheme.{u}} [AlgebraicGeometry.IsIntegral X]
    [IsNormal X] (U : X.Opens) (hU : (U : Set X).Nonempty) (E : Type (max (u + 1) v)) :
    (constantSheaf X.smallEtaleTopology (Type (max (u + 1) v))).obj E ≅
      (smallEtaleDirectImage.{u, v} U.ι).obj
        ((constantSheaf U.toScheme.smallEtaleTopology (Type (max (u + 1) v))).obj E)

Tag 0F0M, a lemma

Tag 0F0M in the Stacks Project.

AlgebraicGeometry.exists_isFilteredColimit_isConstructibleAbelianSheaf_support_notMem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ZeroStalkAtGenericPoint.lean, line 238. The attribute's comment: “part (1), abelian sheaves, with Stacks 03SA for torsion abelian sheaves (h03SA) and Stacks 095P after restriction to η (h095P) carried as hypotheses”.

Stacks 0F0M (1). Let X be a quasi-compact and quasi-separated scheme and let η be a generic point of an irreducible component of X. Let ℱ be an abelian sheaf on the small étale site of X whose stalk at a geometric point η̄ above η is zero. Then ℱ is a filtered colimit of constructible abelian sheaves, each of whose supports is contained in a closed subset of X — equivalently a closed subscheme of X — not containing η.

Two inputs of the source proof are carried as hypotheses, as described in the module documentation: h03SA is Stacks 03SA for torsion abelian sheaves, the presentation of ℱ as a filtered colimit of constructible abelian sheaves, which is also where the torsion hypothesis of the source statement is used and so does not appear here; and h095P is Stacks 095P in the form the proof uses it, after restriction to η. Everything else is proved: the construction of the index category and of the diagram, that it is filtered and that its colimit is ℱ again, constructibility of its terms by Stacks 03RZ, vanishing of their stalks at η̄, constructibility of their supports by Stacks 09YS (2), and that the closure of such a support avoids η.

public theorem exists_isFilteredColimit_isConstructibleAbelianSheaf_support_notMem
    (η : X.obj) (hη : η ∈ genericPoints X.obj)
    (p : GeometricPoint X.obj) (hp : GeometricPoint.LiesOver p η)
    (ℱ : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
    (hstalk : IsZero ((smallEtaleGeometricStalkFunctor B X p).obj ℱ))
    (h03SA : ∃ (I : Type (u + 1)) (_ : SmallCategory I) (_ : IsFiltered I)
      (D : I ⥤ Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
      (ι : D ⟶ (Functor.const I).obj ℱ),
      Nonempty (IsColimit (Cocone.mk ℱ ι)) ∧ ∀ i, IsConstructibleAbelianSheaf B X (D.obj i))
    (h095P : ∀ (I : Type (u + 1)) (_ : SmallCategory I) (_ : IsFiltered I)
      (D : I ⥤ Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
      (ι : D ⟶ (Functor.const I).obj ℱ), IsColimit (Cocone.mk ℱ ι) →
      (∀ i, IsConstructibleAbelianSheaf B X (D.obj i)) →
      IsZero ((smallEtaleGeometricStalkFunctor B X p).obj ℱ) →
      ∀ i : I, ∃ (j : I) (f : i ⟶ j),
        (smallEtaleGeometricStalkFunctor B X p).map (D.map f) = 0) :
    ∃ (J : Type (u + 1)) (_ : SmallCategory J) (_ : IsFiltered J)
      (G : J ⥤ Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
      (κ : G ⟶ (Functor.const J).obj ℱ),
      Nonempty (IsColimit (Cocone.mk ℱ κ)) ∧
        (∀ j, IsConstructibleAbelianSheaf B X (G.obj j)) ∧
          ∀ j, ∃ Z : Set X.obj, IsClosed Z ∧ η ∉ Z ∧
            supportSheaf.{u, u + 1} B X.obj X.property (G.obj j) ⊆ Z

AlgebraicGeometry.exists_isFilteredColimit_isConstructibleAbelianSheaf_support_notMem_of_torsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ZeroStalkAtGenericPointColimit.lean, line 190. The attribute's comment: “part (1), torsion abelian sheaves, torsion in the local sense of Stacks 0DD7”.

Stacks 0F0M (1). Let X be a quasi-compact and quasi-separated scheme and let η be a generic point of an irreducible component of X. Let ℱ be a torsion abelian sheaf on X_étale whose stalk at a geometric point η̄ above η is zero. Then ℱ is a filtered colimit of constructible abelian sheaves, each of whose supports is contained in a closed subset of X — equivalently a closed subscheme of X — not containing η.

Torsion is the local condition of Stacks 0DD7, Stacks.Torsion.torsionSheafProperty. This is AlgebraicGeometry.exists_isFilteredColimit_isConstructibleAbelianSheaf_support_notMem with its two inputs proved: Stacks 03SA (2) is AlgebraicGeometry.exists_isFilteredColimit_isConstructibleAbelianSheaf_of_qcqs, and Stacks 095P in the form the source uses is AlgebraicGeometry.exists_smallEtaleGeometricStalkFunctor_map_eq_zero.

public theorem exists_isFilteredColimit_isConstructibleAbelianSheaf_support_notMem_of_torsion
    [CompactSpace X.obj] [QuasiSeparatedSpace X.obj]
    (η : X.obj) (hη : η ∈ genericPoints X.obj)
    (p : GeometricPoint X.obj) (hp : GeometricPoint.LiesOver p η)
    (ℱ : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
    (hℱ : Stacks.Torsion.torsionSheafProperty (SmallEtale.topology B X.obj X.property) ℱ)
    (hstalk : IsZero ((smallEtaleGeometricStalkFunctor B X p).obj ℱ)) :
    ∃ (J : Type (u + 1)) (_ : SmallCategory J) (_ : IsFiltered J)
      (G : J ⥤ Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
      (κ : G ⟶ (Functor.const J).obj ℱ),
      Nonempty (IsColimit (Cocone.mk ℱ κ)) ∧
        (∀ j, IsConstructibleAbelianSheaf B X (G.obj j)) ∧
          ∀ j, ∃ Z : Set X.obj, IsClosed Z ∧ η ∉ Z ∧
            supportSheaf.{u, u + 1} B X.obj X.property (G.obj j) ⊆ Z

AlgebraicGeometry.exists_isFilteredColimit_isConstructibleModuleSheaf_support_notMem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ZeroStalkAtGenericPointColimit.lean, line 296. The attribute's comment: “part (2), sheaves of modules over a Noetherian ring”.

Stacks 0F0M (2). Let X be a quasi-compact and quasi-separated scheme, let η be a generic point of an irreducible component of X and let Λ be a Noetherian ring. Let ℱ be a sheaf of Λ-modules on X_étale whose stalk at a geometric point η̄ above η is zero. Then ℱ is a filtered colimit of constructible sheaves of Λ-modules, each of whose supports is contained in a closed subset of X — equivalently a closed subscheme of X — not containing η.

The proof is the source's proof of part (1), which it says carries over verbatim. Write ℱ = colim ℱᵢ with ℱᵢ constructible by Stacks 03SA (3); out of every i choose a transition map ℱᵢ ⟶ ℱ_{i'(i)} whose stalk at η̄ vanishes, by Stacks 095P in the stalkwise form AlgebraicGeometry.exists_smallEtaleGeometricStalkModuleFunctor_map_eq_zero; the images of these transition maps form a filtered system with colimit ℱ (CategoryTheory.Limits.isColimitArrowImageCocone), each image is constructible by Stacks 03RZ and has vanishing stalk at η̄, its support is constructible by Stacks 09YS (3), and the closure of a constructible set avoiding the generic point η avoids η.

public theorem exists_isFilteredColimit_isConstructibleModuleSheaf_support_notMem
    [CompactSpace X.obj] [QuasiSeparatedSpace X.obj]
    (η : X.obj) (hη : η ∈ genericPoints X.obj)
    (p : GeometricPoint X.obj) (hp : GeometricPoint.LiesOver p η)
    (ℱ : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} Λ))
    (hstalk : IsZero (etaleStalk B X.obj X.property p ℱ.obj)) :
    ∃ (J : Type (u + 1)) (_ : SmallCategory J) (_ : IsFiltered J)
      (G : J ⥤ Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} Λ))
      (κ : G ⟶ (Functor.const J).obj ℱ),
      Nonempty (IsColimit (Cocone.mk ℱ κ)) ∧
        (∀ j, IsConstructibleModuleSheaf B X Λ (G.obj j)) ∧
          ∀ j, ∃ Z : Set X.obj, IsClosed Z ∧ η ∉ Z ∧ supportModuleSheaf B X Λ (G.obj j) ⊆ Z

Sources

• Section 59.73, Tag 095M
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isConstructibleAbelianSheaf_abelianShriekConstant · AlgebraicGeometry.abelianShriekZModIsConstructible · AlgebraicGeometry.isConstructibleSetSheaf_sheafifiedYoneda · AlgebraicGeometry.isConstructible_sheafifiedYoneda_and_abelianShriekConstant_and_moduleShriek_of_qcqs · AlgebraicGeometry.isConstructibleModuleSheaf_moduleShriek · AlgebraicGeometry.isConstructibleSetSheaf_sheafifiedYoneda_of_qcqs · AlgebraicGeometry.isConstructibleModuleSheaf_moduleShriekConstant · AlgebraicGeometry.exists_isFilteredColimit_isConstructibleAbelianSheaf_of_torsionSheafProperty

Section59.74 Constructible sheaves on Noetherian schemes#

Section 59.74 of the Stacks Project, Tag 03RY. 5 tags here are carried by 29 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09BH, a proposition

Tag 09BH in the Stacks Project.

AlgebraicGeometry.isConstructibleSetSheaf_of_mono_of_epi_and_isSerreClass_abelian_and_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/SerreSubcategory.lean, line 80.

Stacks 09BH. Let X be a Noetherian scheme and let Λ be a Noetherian ring.

1. Any sub or quotient sheaf of a constructible sheaf of sets on the small étale site of X is constructible.
2. The constructible abelian sheaves on that site form a (strong) Serre subcategory of all abelian sheaves on it; in particular every subsheaf and quotient sheaf of a constructible abelian sheaf is constructible.
3. The constructible sheaves of Λ-modules on that site form a (strong) Serre subcategory of all sheaves of Λ-modules on it; in particular every submodule and quotient module of a constructible sheaf of Λ-modules is constructible.

CategoryTheory.ObjectProperty.IsSerreClass is containing zero and closure under subobjects, quotients and extensions, which is a Serre subcategory by Stacks 02MP.

public theorem isConstructibleSetSheaf_of_mono_of_epi_and_isSerreClass_abelian_and_module
    (B : BigEtaleSite.{u}) (X : B.Scheme) [IsNoetherian X.obj]
    (Λ : Type r) [CommRing Λ] [IsNoetherianRing Λ] [Small.{u + 1} Λ] :
    ((∀ (F G : Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1))) (i : G ⟶ F),
        Mono i → IsConstructibleSetSheaf B X F → IsConstructibleSetSheaf B X G) ∧
      (∀ (F Q : Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1))) (p : F ⟶ Q),
        Epi p → IsConstructibleSetSheaf B X F → IsConstructibleSetSheaf B X Q)) ∧
      ObjectProperty.IsSerreClass
        (fun F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1} =>
          IsConstructibleAbelianSheaf B X F) ∧
      ObjectProperty.IsSerreClass
        (fun F : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} Λ) =>
          IsConstructibleModuleSheaf B X Λ F)

AlgebraicGeometry.isConstructibleModuleSheaf_of_mono', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ShrinkCoefficients.lean, line 237. The attribute's comment: “part (3), subsheaf, for a Noetherian coefficient ring in any universe”.

Stacks 09BH, part (3), subsheaves, for a coefficient ring in any universe. A subsheaf of a constructible sheaf of R-modules on the small étale site of a Noetherian scheme is constructible.

AlgebraicGeometry.isConstructibleModuleSheaf_of_mono proves this for a ring in Type (u + 1). Here R need only be small in that universe: the statement is read at Shrink.{u + 1} R, a Noetherian ring in Type (u + 1), and transported back. The equivalence of sheaf categories preserves monomorphisms, so the subsheaf upstairs is one.

public theorem isConstructibleModuleSheaf_of_mono' [IsNoetherian X.obj] [IsNoetherianRing R]
    {G F : Sheaf (SmallEtale.topology B X.1 X.property) (ModuleCat.{u + 1} R)}
    (i : G ⟶ F) [Mono i] (hF : IsConstructibleModuleSheaf B X R F) :
    IsConstructibleModuleSheaf B X R G

AlgebraicGeometry.isConstructibleModuleSheaf_of_epi', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ShrinkCoefficients.lean, line 251. The attribute's comment: “part (3), quotient sheaf, for a Noetherian coefficient ring in any universe”.

Stacks 09BH, part (3), quotient sheaves, for a coefficient ring in any universe. A quotient of a constructible sheaf of R-modules on the small étale site of a Noetherian scheme is constructible. This is AlgebraicGeometry.isConstructibleModuleSheaf_of_epi transported along the same equivalence, which preserves epimorphisms.

public theorem isConstructibleModuleSheaf_of_epi' [IsNoetherian X.obj] [IsNoetherianRing R]
    {G Q : Sheaf (SmallEtale.topology B X.1 X.property) (ModuleCat.{u + 1} R)}
    (p : G ⟶ Q) [Epi p] (hG : IsConstructibleModuleSheaf B X R G) :
    IsConstructibleModuleSheaf B X R Q

AlgebraicGeometry.isConstructibleAbelianSheaf_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StrongSerreAbelian.lean, line 168. The attribute's comment: “part (2), subsheaf, with Stacks 00YT as hunderlying, Stacks 03S8 as hrep and the surjection half of Stacks 09Y9 as hcover”.

A subsheaf of a constructible sheaf of abelian groups on the small étale site of a Noetherian scheme is constructible. It assumes hunderlying : SmallEtaleUnderlyingSetCommutes B X, hrep : RepresentableIsConstructibleSetSheaf B X and hcover : HasFiniteRepresentableCover B X.

public theorem isConstructibleAbelianSheaf_of_mono [IsNoetherian X.obj]
    (hunderlying : SmallEtaleUnderlyingSetCommutes B X)
    (hrep : RepresentableIsConstructibleSetSheaf B X)
    (hcover : HasFiniteRepresentableCover B X)
    {F G : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1}}
    (i : G ⟶ F) [Mono i] (hF : IsConstructibleAbelianSheaf B X F) :
    IsConstructibleAbelianSheaf B X G

AlgebraicGeometry.isConstructibleAbelianSheaf_of_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StrongSerreAbelian.lean, line 217. The attribute's comment: “part (2), quotient sheaf, with Stacks 00YT as hunderlying, Stacks 03S8 as hrep and the surjection half of Stacks 09Y9 as hcover”.

A quotient of a constructible sheaf of abelian groups on the small étale site of a Noetherian scheme is constructible. It assumes hunderlying : SmallEtaleUnderlyingSetCommutes B X, hrep : RepresentableIsConstructibleSetSheaf B X and hcover : HasFiniteRepresentableCover B X.

public theorem isConstructibleAbelianSheaf_of_epi [IsNoetherian X.obj]
    (hunderlying : SmallEtaleUnderlyingSetCommutes B X)
    (hrep : RepresentableIsConstructibleSetSheaf B X)
    (hcover : HasFiniteRepresentableCover B X)
    {F Q : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1}}
    (p : F ⟶ Q) [Epi p] (hF : IsConstructibleAbelianSheaf B X F) :
    IsConstructibleAbelianSheaf B X Q

AlgebraicGeometry.isSerreClass_isConstructibleAbelianSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StrongSerreAbelian.lean, line 235. The attribute's comment: “part (2), the strong Serre property, with Stacks 00YT as hunderlying, Stacks 03S8 as hrep and the surjection half of Stacks 09Y9 as hcover”.

The constructible sheaves of abelian groups on the small étale site of a Noetherian scheme form a strong Serre subcategory of all abelian sheaves on that site: they contain zero and are closed under subobjects, quotients and extensions. It assumes hunderlying : SmallEtaleUnderlyingSetCommutes B X, hrep : RepresentableIsConstructibleSetSheaf B X and hcover : HasFiniteRepresentableCover B X.

public theorem isSerreClass_isConstructibleAbelianSheaf [IsNoetherian X.obj]
    (hunderlying : SmallEtaleUnderlyingSetCommutes B X)
    (hrep : RepresentableIsConstructibleSetSheaf B X)
    (hcover : HasFiniteRepresentableCover B X) :
    (isConstructibleAbelianSheafProperty B X :
      ObjectProperty (Sheaf (SmallEtale.topology B X.obj X.property)
        AddCommGrpCat.{u + 1})).IsSerreClass

AlgebraicGeometry.isConstructibleModuleSheaf_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StrongSerreModules.lean, line 167. The attribute's comment: “part (3), subsheaf; Stacks 095E, Stacks 09YR, Stacks 03RZ (3) and the geometric step of the source's proof are all discharged from the library”.

Stacks 09BH, part (3), subsheaves. A subsheaf of a constructible sheaf of Λ-modules on the small étale site of a Noetherian scheme is constructible.

By Stacks 095E the ambient sheaf is locally constant of finite type on the strata of a single stratification of X. Inverse image to a stratum is left exact, so the subsheaf restricts to a subsheaf there, and the geometric step of the source's proof, AlgebraicGeometry.finiteTypeLocallyConstantSubsheavesAreConstructible, makes that restriction constructible on the stratum. The strata are immersed with constructible images and they cover X, so Stacks 09YR carries constructibility back to X.

public theorem isConstructibleModuleSheaf_of_mono [IsNoetherian X.obj]
    {G F : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} Λ)}
    (i : G ⟶ F) [Mono i] (hF : IsConstructibleModuleSheaf B X Λ F) :
    IsConstructibleModuleSheaf B X Λ G

AlgebraicGeometry.isConstructibleModuleSheaf_of_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StrongSerreModules.lean, line 209. The attribute's comment: “part (3), quotient sheaf; Stacks 095E, Stacks 09YR, Stacks 03RZ (3) and the geometric step of the source's proof are all discharged from the library”.

Stacks 09BH, part (3), quotient sheaves. A quotient of a constructible sheaf of Λ-modules on the small étale site of a Noetherian scheme is constructible.

An epimorphism of sheaves of modules is the cokernel of its kernel; the kernel is a subobject, so it is constructible by AlgebraicGeometry.isConstructibleModuleSheaf_of_mono, and the weak Serre property of Stacks 03RZ (3) then puts the target in the class.

public theorem isConstructibleModuleSheaf_of_epi [IsNoetherian X.obj]
    {G Q : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} Λ)}
    (p : G ⟶ Q) [Epi p] (hG : IsConstructibleModuleSheaf B X Λ G) :
    IsConstructibleModuleSheaf B X Λ Q

AlgebraicGeometry.isSerreClass_isConstructibleModuleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StrongSerreModules.lean, line 246. The attribute's comment: “part (3), the strong Serre property; Stacks 095E, Stacks 09YR, Stacks 03RZ (3) and the geometric step of the source's proof are all discharged from the library”.

Stacks 09BH, part (3). The constructible sheaves of Λ-modules on the small étale site of a Noetherian scheme form a strong Serre subcategory of all sheaves of Λ-modules on that site: CategoryTheory.ObjectProperty.IsSerreClass is closure under subobjects, quotients and extensions together with containing zero, which is the characterisation of a Serre subcategory in Stacks 02MP.

Closure under extensions and the zero object are the weak Serre property of Stacks 03RZ (3), which is unconditional; closure under subobjects is AlgebraicGeometry.isConstructibleModuleSheaf_of_mono, and it implies closure under quotients because an epimorphism is the cokernel of its kernel.

public theorem isSerreClass_isConstructibleModuleSheaf [IsNoetherian X.obj] :
    ObjectProperty.IsSerreClass
      (fun F : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} Λ) =>
        IsConstructibleModuleSheaf B X Λ F)

AlgebraicGeometry.isConstructibleSetSheaf_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StrongSerreSets.lean, line 608. The attribute's comment: “part (1), subsheaf, with Stacks 03S8 as hrep and the surjection half of Stacks 09Y9 as hcover”.

Stacks 09BH, part (1), subsheaves. A subsheaf of a constructible sheaf of sets on the small étale site of a Noetherian scheme is constructible.

hrep is Stacks 03S8 and hcover is the surjection half of Stacks 09Y9; neither mentions subobjects. Given a surjection onto F from a finite coproduct of quasi-compact representables, sub-closure for the coproduct and for its square descends to F, and sub-closure for a quasi-compact representable is isConstructibleSetSheaf_of_mono_representable.

public theorem isConstructibleSetSheaf_of_mono (B : BigEtaleSite.{u})
    (X : B.Scheme) [IsNoetherian X.obj]
    (hrep : RepresentableIsConstructibleSetSheaf B X)
    (hcover : HasFiniteRepresentableCover B X)
    {F G : Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1))}
    (i : G ⟶ F) [Mono i] (hF : IsConstructibleSetSheaf B X F) :
    IsConstructibleSetSheaf B X G

AlgebraicGeometry.isConstructibleSetSheaf_of_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/StrongSerreSets.lean, line 641. The attribute's comment: “part (1), quotient sheaf, with Stacks 03S8 as hrep and the surjection half of Stacks 09Y9 as hcover”.

Stacks 09BH, part (1), quotient sheaves. A quotient sheaf of a constructible sheaf of sets on the small étale site of a Noetherian scheme is constructible.

This is the source's argument: the kernel pair ℱ ×_𝒬 ℱ is a subsheaf of ℱ × ℱ, hence constructible by the subsheaf case and Stacks 03RZ (1), and 𝒬 is the coequalizer of that kernel pair, hence constructible by Stacks 03RZ (1) again.

public theorem isConstructibleSetSheaf_of_epi (B : BigEtaleSite.{u})
    (X : B.Scheme) [IsNoetherian X.obj]
    (hrep : RepresentableIsConstructibleSetSheaf B X)
    (hcover : HasFiniteRepresentableCover B X)
    {F Q : Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1))}
    (p : F ⟶ Q) [Epi p] (hF : IsConstructibleSetSheaf B X F) :
    IsConstructibleSetSheaf B X Q

Stacks.EtaleCohomology.FiniteLevelSheaf.isConstructible_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/LevelConstructibility.lean, line 63. The attribute's comment: “part (3), subsheaf, at the coefficients Z/l^{n+1}Z of a finite level of an l-adic sheaf”.

A subsheaf of a constructible finite-level sheaf is constructible.

public theorem isConstructible_of_mono (n : ℕ)
    {G F : FiniteLevelSheaf.{u, u + 1} B X ℓ n} (i : G ⟶ F) [Mono i]
    (hF : IsConstructibleModuleSheaf B X (ZMod (ℓ ^ (n + 1))) F) :
    IsConstructibleModuleSheaf B X (ZMod (ℓ ^ (n + 1))) G

Stacks.EtaleCohomology.FiniteLevelSheaf.isConstructible_of_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/LevelConstructibility.lean, line 74. The attribute's comment: “part (3), quotient sheaf, at the coefficients Z/l^{n+1}Z of a finite level of an l-adic sheaf”.

A quotient of a constructible finite-level sheaf is constructible.

public theorem isConstructible_of_epi (n : ℕ)
    {G Q : FiniteLevelSheaf.{u, u + 1} B X ℓ n} (p : G ⟶ Q) [Epi p]
    (hG : IsConstructibleModuleSheaf B X (ZMod (ℓ ^ (n + 1))) G) :
    IsConstructibleModuleSheaf B X (ZMod (ℓ ^ (n + 1))) Q

Stacks.EtaleCohomology.LAdicSheaf.isConstructible_stableKernelLevel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/StableKernel.lean, line 225. The attribute's comment: “part (3), subsheaf, applied to the intersection of the images of the levelwise kernels inside a levelwise kernel”.

Each level of the kernel of a morphism of ℓ-adic sheaves is a constructible sheaf.

public theorem isConstructible_stableKernelLevel {F G : LAdicSheaf.{u, u + 1} B X ℓ} (f : F ⟶ G)
    (n : ℕ) :
    IsConstructibleModuleSheaf B X (ZMod (ℓ ^ (n + 1))) (stableKernelLevel f n)

Tag 09YV, a lemma

Tag 09YV in the Stacks Project.

AlgebraicGeometry.isNoetherianObject_of_isConstructibleSetSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ConstructibleAscendingChain.lean, line 80. The attribute's comment: “sheaves of sets, carrying Stacks 09BH (a subsheaf of a constructible sheaf of sets is constructible) as the explicit hypothesis hsub and Stacks 095P (a filtered system of constructible sheaves of sets whose colimit is constructible is essentially constant) as the explicit hypothesis hess”.

Stacks Project, Tag 09YV for sheaves of sets. On a Noetherian scheme every ascending chain of subsheaves of a constructible sheaf of sets stabilizes.

public theorem isNoetherianObject_of_isConstructibleSetSheaf
    (B : BigEtaleSite.{u}) (X : B.Scheme) [IsNoetherian X.obj]
    (hsub : ∀ {G H : Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1))}
      (i : G ⟶ H), Mono i → IsConstructibleSetSheaf B X H → IsConstructibleSetSheaf B X G)
    (hess : ∀ (M : ℕ ⥤ Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1)))
      (c : Cocone M), IsColimit c →
      (∀ n, IsConstructibleSetSheaf B X (M.obj n)) → IsConstructibleSetSheaf B X c.pt →
      ∃ (n : ℕ) (r : c.pt ⟶ M.obj n),
        EssentiallyConstantInd.IsEssentiallyConstantWith M c n r)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1)))
    (hF : IsConstructibleSetSheaf B X F) :
    IsNoetherianObject F

AlgebraicGeometry.isNoetherianObject_of_isConstructibleAbelianSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ConstructibleAscendingChain.lean, line 104. The attribute's comment: “sheaves of abelian groups, carrying Stacks 09BH (a subsheaf of a constructible sheaf of abelian groups is constructible) as the explicit hypothesis hsub and Stacks 095P (a filtered system of constructible sheaves of abelian groups whose colimit is constructible is essentially constant) as the explicit hypothesis hess”.

Stacks Project, Tag 09YV for sheaves of abelian groups. On a Noetherian scheme every ascending chain of subsheaves of a constructible sheaf of abelian groups stabilizes.

public theorem isNoetherianObject_of_isConstructibleAbelianSheaf
    (B : BigEtaleSite.{u}) (X : B.Scheme) [IsNoetherian X.obj]
    [∀ (S T : B.Scheme) (f : T ⟶ S),
      ((smallEtaleBaseChange B f).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
        (SmallEtale.topology B S.obj S.property)
        (SmallEtale.topology B T.obj T.property)).IsRightAdjoint]
    [∀ (T : B.Scheme) (V : SmallEtale B T.obj T.property),
      HasWeakSheafify ((SmallEtale.topology B T.obj T.property).over V) AddCommGrpCat.{u + 1}]
    (hsub : ∀ {G H : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1}}
      (i : G ⟶ H), Mono i →
      IsConstructibleAbelianSheaf B X H → IsConstructibleAbelianSheaf B X G)
    (hess : ∀ (M : ℕ ⥤ Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
      (c : Cocone M), IsColimit c →
      (∀ n, IsConstructibleAbelianSheaf B X (M.obj n)) →
      IsConstructibleAbelianSheaf B X c.pt →
      ∃ (n : ℕ) (r : c.pt ⟶ M.obj n),
        EssentiallyConstantInd.IsEssentiallyConstantWith M c n r)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
    (hF : IsConstructibleAbelianSheaf B X F) :
    IsNoetherianObject F

AlgebraicGeometry.isNoetherianObject_of_isConstructibleModuleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ConstructibleAscendingChain.lean, line 136. The attribute's comment: “sheaves of modules over a Noetherian ring, carrying Stacks 09BH (a subsheaf of a constructible sheaf of modules is constructible) as the explicit hypothesis hsub and Stacks 095P (a filtered system of constructible sheaves of modules whose colimit is constructible is essentially constant) as the explicit hypothesis hess”.

Stacks Project, Tag 09YV for sheaves of modules. On a Noetherian scheme, and over a Noetherian coefficient ring, every ascending chain of subsheaves of a constructible sheaf of modules stabilizes.

public theorem isNoetherianObject_of_isConstructibleModuleSheaf
    (B : BigEtaleSite.{u}) (X : B.Scheme) [IsNoetherian X.obj]
    (R : Type r) [CommRing R] [IsNoetherianRing R]
    [∀ (S T : B.Scheme) (f : T ⟶ S),
      ((smallEtaleBaseChange B f).sheafPushforwardContinuous (ModuleCat.{w} R)
        (SmallEtale.topology B S.obj S.property)
        (SmallEtale.topology B T.obj T.property)).IsRightAdjoint]
    [∀ (T : B.Scheme) (V : SmallEtale B T.obj T.property),
      HasWeakSheafify ((SmallEtale.topology B T.obj T.property).over V) (ModuleCat.{w} R)]
    [HasSheafify (SmallEtale.topology B X.obj X.property) (ModuleCat.{w} R)]
    (hsub : ∀ {G H : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{w} R)}
      (i : G ⟶ H), Mono i →
      IsConstructibleModuleSheaf B X R H → IsConstructibleModuleSheaf B X R G)
    (hess : ∀ (M : ℕ ⥤ Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{w} R))
      (c : Cocone M), IsColimit c →
      (∀ n, IsConstructibleModuleSheaf B X R (M.obj n)) →
      IsConstructibleModuleSheaf B X R c.pt →
      ∃ (n : ℕ) (r : c.pt ⟶ M.obj n),
        EssentiallyConstantInd.IsEssentiallyConstantWith M c n r)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{w} R))
    (hF : IsConstructibleModuleSheaf B X R F) :
    IsNoetherianObject F

AlgebraicGeometry.isNoetherianObject_of_isConstructibleSetSheaf', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ConstructibleAscendingChainSetsAbelian.lean, line 79. The attribute's comment: “sheaves of sets: on a Noetherian scheme a constructible sheaf of sets on the small etale site is a Noetherian object, so every ascending chain of subsheaves stabilizes”. References: SGA 4 IX (2.9), “(ii)”.

Stacks 09YV for sheaves of sets. On a Noetherian scheme every ascending chain of subsheaves of a constructible sheaf of sets on the small étale site stabilizes: the sheaf is a Noetherian object of the category of sheaves of sets.

Stacks 09BH (1) and Stacks 095P (1) are supplied to AlgebraicGeometry.isNoetherianObject_of_isConstructibleSetSheaf by AlgebraicGeometry.isConstructibleSetSheaf_of_mono and AlgebraicGeometry.exists_isEssentiallyConstantWith_of_isConstructibleSetSheaf_colimit.

public theorem isNoetherianObject_of_isConstructibleSetSheaf'
    (B : BigEtaleSite.{u}) (X : B.Scheme) [IsNoetherian X.obj]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (Type (u + 1)))
    (hF : IsConstructibleSetSheaf B X F) :
    IsNoetherianObject F

AlgebraicGeometry.isNoetherianObject_of_isConstructibleAbelianSheaf', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ConstructibleAscendingChainSetsAbelian.lean, line 103. The attribute's comment: “sheaves of abelian groups: on a Noetherian scheme a constructible abelian sheaf on the small etale site is a Noetherian object, so every ascending chain of subsheaves stabilizes”. References: SGA 4 IX (2.9), “(ii), special case”.

Stacks 09YV for sheaves of abelian groups. On a Noetherian scheme every ascending chain of subsheaves of a constructible sheaf of abelian groups on the small étale site stabilizes: the sheaf is a Noetherian object of the category of abelian sheaves.

Stacks 09BH (2) and Stacks 095P (2) are supplied to AlgebraicGeometry.isNoetherianObject_of_isConstructibleAbelianSheaf by AlgebraicGeometry.isConstructibleAbelianSheaf_of_mono and AlgebraicGeometry.exists_isEssentiallyConstantWith_of_isConstructibleAbelianSheaf_colimit.

public theorem isNoetherianObject_of_isConstructibleAbelianSheaf'
    (B : BigEtaleSite.{u}) (X : B.Scheme) [IsNoetherian X.obj]
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
    (hF : IsConstructibleAbelianSheaf B X F) :
    IsNoetherianObject F

AlgebraicGeometry.isNoetherianObject_of_isConstructibleModuleSheaf', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/ShrinkCoefficients.lean, line 328. The attribute's comment: “sheaves of modules over a Noetherian ring in any universe, with Stacks 09BH and Stacks 095P discharged”. References: SGA 4 IX (2.10).

Stacks 09YV for sheaves of modules, with nothing granted and the coefficient ring in any universe. On a Noetherian scheme, over a Noetherian ring, every ascending chain of subsheaves of a constructible sheaf of R-modules stabilizes.

AlgebraicGeometry.isNoetherianObject_of_isConstructibleModuleSheaf carries Stacks 09BH and Stacks 095P as the explicit hypotheses hsub and hess. Both are available above at a coefficient ring in any universe, so they are supplied here and nothing is granted. The quasi-compactness and quasi-separatedness that Stacks 095P asks of X follow from its being Noetherian.

public theorem isNoetherianObject_of_isConstructibleModuleSheaf' [IsNoetherian X.obj]
    [IsNoetherianRing R]
    [HasSheafify (SmallEtale.topology B X.1 X.property) (ModuleCat.{u + 1} R)]
    (F : Sheaf (SmallEtale.topology B X.1 X.property) (ModuleCat.{u + 1} R))
    (hF : IsConstructibleModuleSheaf B X R F) :
    IsNoetherianObject F

Stacks.EtaleCohomology.FiniteLevelSheaf.isNoetherianObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/LevelConstructibility.lean, line 95. The attribute's comment: “sheaves of modules, at the coefficients Z/l^{n+1}Z of a finite level of an l-adic sheaf”.

A constructible finite-level sheaf is a Noetherian object: every ascending chain of subsheaves of it stabilises.

public theorem isNoetherianObject (n : ℕ) (F : FiniteLevelSheaf.{u, u + 1} B X ℓ n)
    (hF : IsConstructibleModuleSheaf B X (ZMod (ℓ ^ (n + 1))) F) :
    IsNoetherianObject F

Tag 09Z6, a lemma

Tag 09Z6 in the Stacks Project.

Stacks.EtaleCohomology.exists_mono_biproduct_etaleModuleDirectImage_constantSheaf_and_nsmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleEmbedding/Main.lean, line 74. The attribute's comment: “(3)”.

Stacks 09Z6 (3), with the refinement of its last sentence. Let X be a Noetherian scheme, Λ a Noetherian ring and ℱ a constructible sheaf of Λ-modules on X_étale. There is an injective map of sheaves of modules ℱ ⟶ ⨁ᵢ fᵢ_* M̲ᵢ into a finite direct sum, with fᵢ : Yᵢ ⟶ X finite (and of finite presentation) and Mᵢ a finite Λ-module. Moreover each Yᵢ is irreducible and reduced and maps onto an irreducible and reduced closed subscheme Zᵢ of X such that Yᵢ ⟶ Zᵢ is finite étale over a nonempty open of Zᵢ (AlgebraicGeometry.IsGenericallyFiniteEtaleOntoImage). In addition, every integer killing ℱ kills the Mᵢ.

The ring Λ lives in Type (u + 1), the universe of the library's constructibility theory.

theorem exists_mono_biproduct_etaleModuleDirectImage_constantSheaf_and_nsmul
    {X : Scheme.{u}} [IsNoetherian X] (F : EtaleModules.{u, u + 1} Λ X)
    (hF : IsConstructibleEtaleModule Λ F) :
    ∃ (n : ℕ) (Y : Fin n → Scheme.{u}) (f : ∀ k, Y k ⟶ X) (_ : ∀ k, IsFinite (f k))
      (_ : ∀ k, FinitePresentation (f k)) (M : Fin n → ModuleCat.{u + 1} Λ)
      (_ : ∀ k, Module.Finite Λ (M k))
      (φ : F ⟶ ⨁ fun k => (etaleModuleDirectImage.{u, u + 1} Λ (f k)).obj
        ((constantSheaf (Y k).smallEtaleTopology (ModuleCat.{u + 1} Λ)).obj (M k))),
      Mono φ ∧ (∀ N : ℕ, N • 𝟙 F = 0 → ∀ k (m : M k), N • m = 0) ∧
        ∀ k, IsGenericallyFiniteEtaleOntoImage (f k)

Stacks.EtaleCohomology.exists_mono_biproduct_etaleAbelianDirectImage_constantSheaf_isGenericallyFiniteEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleEmbedding/Main.lean, line 122. The attribute's comment: “(2)”. References: SGA 4 XIV (1.11), “special case”; SGA 4½ Arcata (4.3.2), “(i) ⇒ (ii)”.

Stacks 09Z6 (2), with the refinement of its last sentence. Let X be a Noetherian scheme and ℱ a constructible abelian sheaf on X_étale. There is an injective map of abelian sheaves ℱ ⟶ ⨁ᵢ fᵢ_* M̲ᵢ into a finite direct sum, with fᵢ : Yᵢ ⟶ X finite (and of finite presentation) and Mᵢ a finite abelian group. Moreover each Yᵢ is irreducible and reduced and maps onto an irreducible and reduced closed subscheme Zᵢ of X such that Yᵢ ⟶ Zᵢ is finite étale over a nonempty open of Zᵢ (AlgebraicGeometry.IsGenericallyFiniteEtaleOntoImage).

The abelian sheaves take values in AddCommGrpCat.{u + 1} (constructibility in the universe v = 0 of _root_.Stacks.EtaleCohomology.IsConstructibleSmallEtaleAbelianSheaf), the universe of the library's constructibility theory; the proof views them as sheaves of ULift ℤ-modules.

theorem exists_mono_biproduct_etaleAbelianDirectImage_constantSheaf_isGenericallyFiniteEtale
    {X : Scheme.{u}}
    [IsNoetherian X] (F : Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1})
    (hF : _root_.Stacks.EtaleCohomology.IsConstructibleSmallEtaleAbelianSheaf.{u, 0} F) :
    ∃ (J : Type) (_ : Finite J) (Y : J → Scheme.{u}) (f : ∀ j, Y j ⟶ X)
      (_ : ∀ j, IsFinite (f j)) (_ : ∀ j, FinitePresentation (f j))
      (M : J → AddCommGrpCat.{u + 1}) (_ : ∀ j, Finite (M j))
      (m : F ⟶ ⨁ fun j => (etaleAbelianDirectImage.{u, 0} (f j)).obj
        ((constantSheaf (Y j).smallEtaleTopology AddCommGrpCat.{u + 1}).obj (M j))),
      Mono m ∧ ∀ j, IsGenericallyFiniteEtaleOntoImage (f j)

Stacks.EtaleCohomology.exists_mono_pi_smallEtalePushforward_constantSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleEmbedding/Sets.lean, line 176. The attribute's comment: “(1)”. References: SGA 4 IX (2.14), “(ii), special case”.

Stacks 09Z6 (1), with the refinement of its last sentence. Let X be a Noetherian scheme and ℱ a constructible sheaf of sets on X_étale. There is an injective map of sheaves ℱ ⟶ ∏ᵢ fᵢ_* E̲ᵢ into a finite product, with fᵢ : Yᵢ ⟶ X finite (and of finite presentation) and Eᵢ a finite set. Moreover each Yᵢ is irreducible and reduced and maps onto an irreducible and reduced closed subscheme Zᵢ of X such that Yᵢ ⟶ Zᵢ is finite étale over a nonempty open of Zᵢ (AlgebraicGeometry.IsGenericallyFiniteEtaleOntoImage).

The sheaves of sets take values in Type (u + 1), the universe of AlgebraicGeometry.IsConstructibleSetSheaf.

theorem exists_mono_pi_smallEtalePushforward_constantSheaf {X : Scheme.{u}} [IsNoetherian X]
    (F : Sheaf X.smallEtaleTopology (Type (u + 1))) (hF : IsConstructibleEtaleSetSheaf F) :
    ∃ (n : ℕ) (Y : Fin n → Scheme.{u}) (f : ∀ k, Y k ⟶ X) (_ : ∀ k, IsFinite (f k))
      (_ : ∀ k, FinitePresentation (f k)) (E : Fin n → Type (u + 1)) (_ : ∀ k, Finite (E k))
      (φ : F ⟶ ∏ᶜ fun k => (smallEtalePushforward (f k) (Type (u + 1))).obj
        ((constantSheaf (Y k).smallEtaleTopology (Type (u + 1))).obj (E k))),
      Mono φ ∧ ∀ k, IsGenericallyFiniteEtaleOntoImage (f k)

Tag 09Z7, a lemma

Tag 09Z7 in the Stacks Project.

Stacks.EtaleCohomology.exists_mono_biproduct_etaleAbelianDirectImage_constantSheaf_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/FinitePushforwardEmbedding.lean, line 117. The attribute's comment: “(2)”. References: SGA 4 IX (2.14), “(ii), special case”; SGA 4 XIV (1.11), “special case”; SGA 4½ Arcata (4.3.2), “(i) ⇒ (ii)”.

Stacks Project, Tag 09Z7, part (2). Let X be a quasi-compact and quasi-separated scheme and F a constructible abelian sheaf on X_étale. There is an injective map of abelian sheaves F ⟶ ⨁ⱼ fⱼ_* Mⱼ into a finite direct sum, where each fⱼ : Yⱼ ⟶ X is finite and of finite presentation and each Mⱼ is a finite abelian group.

The proof descends F to a Noetherian stage of an absolute Noetherian approximation of X (Stacks 01ZA, the essential-surjectivity assertion of Stacks 09YU), embeds it there (Stacks 09Z6 (2)), and pulls the embedding back, the inverse image of each finite pushforward being the finite pushforward along the base change (Stacks 0959).

theorem exists_mono_biproduct_etaleAbelianDirectImage_constantSheaf_of_qcqs (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X]
    (F : Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1})
    (hF : IsConstructibleSmallEtaleAbelianSheaf.{u, 0} F) :
    ∃ (J : Type) (_ : Finite J) (Y : J → Scheme.{u}) (f : ∀ j, Y j ⟶ X)
      (_ : ∀ j, IsFinite (f j)) (_ : ∀ j, FinitePresentation (f j))
      (M : J → AddCommGrpCat.{u + 1}) (_ : ∀ j, Finite (M j))
      (m : F ⟶ ⨁ fun j => (etaleAbelianDirectImage.{u, 0} (f j)).obj
        ((constantSheaf (Y j).smallEtaleTopology AddCommGrpCat.{u + 1}).obj (M j))),
      Mono m

Stacks.EtaleCohomology.exists_mono_biproduct_etaleModuleDirectImage_constantSheaf_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/FinitePushforwardEmbedding.lean, line 170. The attribute's comment: “(3)”. References: SGA 4 IX (2.14), “(ii), A-modules”.

Stacks Project, Tag 09Z7, part (3). Let X be a quasi-compact and quasi-separated scheme, Λ a Noetherian ring and F a constructible sheaf of Λ-modules on X_étale. There is an injective map of sheaves of modules F ⟶ ⨁ᵢ fᵢ_* M̲ᵢ into a finite direct sum, where each fᵢ : Yᵢ ⟶ X is finite and of finite presentation and each Mᵢ is a finite Λ-module.

The proof descends F to a Noetherian stage of an absolute Noetherian approximation of X (Stacks 01ZA, the essential-surjectivity assertion of Stacks 09YU), embeds it there (Stacks 09Z6 (3)), and pulls the embedding back, the inverse image of each finite pushforward being the finite pushforward along the base change (Stacks 0959). The ring Λ lives in Type (u + 1), the universe of Stacks 09Z6 (3).

theorem exists_mono_biproduct_etaleModuleDirectImage_constantSheaf_of_qcqs
    (Λ : Type (u + 1)) [CommRing Λ] [IsNoetherianRing Λ] (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X] (F : EtaleModules.{u, u + 1} Λ X)
    (hF : IsConstructibleEtaleModule Λ F) :
    ∃ (n : ℕ) (Y : Fin n → Scheme.{u}) (f : ∀ k, Y k ⟶ X) (_ : ∀ k, IsFinite (f k))
      (_ : ∀ k, FinitePresentation (f k)) (M : Fin n → ModuleCat.{u + 1} Λ)
      (_ : ∀ k, Module.Finite Λ (M k))
      (φ : F ⟶ ⨁ fun k => (etaleModuleDirectImage.{u, u + 1} Λ (f k)).obj
        ((constantSheaf (Y k).smallEtaleTopology (ModuleCat.{u + 1} Λ)).obj (M k))),
      Mono φ

Stacks.EtaleCohomology.exists_mono_pi_smallEtalePushforward_constantSheaf_of_qcqs, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/FinitePushforwardEmbedding.lean, line 230. The attribute's comment: “(1)”. References: SGA 4 IX (2.14), “(ii), sheaves of sets”.

Stacks Project, Tag 09Z7, part (1). Let X be a quasi-compact and quasi-separated scheme and F a constructible sheaf of sets on X_étale. There is an injective map of sheaves F ⟶ ∏ᵢ fᵢ_* E̲ᵢ into a finite product, where each fᵢ : Yᵢ ⟶ X is finite and of finite presentation and each Eᵢ is a finite set.

As for Stacks 09Z6 (1), the proof goes through part (3) over the finite ring Λ = ULift (ZMod 2): F embeds in the free sheaf of Λ-modules Λ[F] (CategoryTheory.Sheaf.mono_adjunction_free_unit), which is constructible (Stacks.EtaleCohomology.isConstructibleEtaleModule_composeAndSheafify_free); part (3) embeds Λ[F] in ⨁ᵢ fᵢ_* M̲ᵢ, and forgetting the module structure carries this to ∏ᵢ fᵢ_* M̲ᵢ with the Mᵢ finite sets. The sheaves of sets take values in Type (u + 1), the universe of AlgebraicGeometry.IsConstructibleSetSheaf.

theorem exists_mono_pi_smallEtalePushforward_constantSheaf_of_qcqs (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X]
    (F : Sheaf X.smallEtaleTopology (Type (u + 1))) (hF : IsConstructibleEtaleSetSheaf F) :
    ∃ (n : ℕ) (Y : Fin n → Scheme.{u}) (f : ∀ k, Y k ⟶ X) (_ : ∀ k, IsFinite (f k))
      (_ : ∀ k, FinitePresentation (f k)) (E : Fin n → Type (u + 1)) (_ : ∀ k, Finite (E k))
      (φ : F ⟶ ∏ᶜ fun k => (smallEtalePushforward (f k) (Type (u + 1))).obj
        ((constantSheaf (Y k).smallEtaleTopology (Type (u + 1))).obj (E k))),
      Mono φ

Tag 0F0N, a lemma

Tag 0F0N in the Stacks Project.

AlgebraicGeometry.exists_isFilteredColimit_isConstructibleModuleSheaf_isClosed_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/SpecializationClosedSupportColimit.lean, line 461. The attribute's comment: “part (2); Stacks 03SA (3), Stacks 093C, Stacks 03S8 for sheaves of modules, Stacks 09BH (3), Stacks 09YS (3), Stacks 0903, Stacks 095E, Stacks 09YR and Stacks 03RZ (3) are all discharged from the library”.

Stacks 0F0N, part (2). Let X be a Noetherian scheme, let Λ be a Noetherian ring and let E ⊆ X be stable under specialization. A sheaf of Λ-modules F on the small étale site of X whose support is contained in E is a filtered colimit of constructible sheaves of Λ-modules, each of whose supports is contained in a closed subset of E.

The source says of this part only that it is "exactly the same" as part (1), and so it is: write F as a filtered colimit of constructible sheaves of Λ-modules by Stacks 03SA (3) — which is in the library — replace each term by the image of its map to F, and run the same three steps, with Stacks 09BH (3) in place of Stacks 09BH (2) and Stacks 09YS (3) in place of Stacks 09YS (2).

Stacks 03SA (3) enters as the unconditional AlgebraicGeometry.exists_isFilteredColimit_isConstructibleModuleSheaf_of_qcqs, so neither Stacks 093C in the shriek spelling nor the sheaves-of-modules case of Stacks 03S8 has to be supplied here. Stacks 09BH (3) enters through AlgebraicGeometry.isConstructibleModuleSheaf_forall_epi, whose own geometric step is AlgebraicGeometry.finiteTypeLocallyConstantSubsheavesAreConstructible. So this statement assumes nothing.

public theorem exists_isFilteredColimit_isConstructibleModuleSheaf_isClosed_support
    [IsNoetherian X.obj]
    (E : Set X.obj) (hE : StableUnderSpecialization E)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} Λ))
    (hsupp : supportModuleSheaf B X Λ F ⊆ E) :
    ∃ (I : Type (u + 1)) (_ : SmallCategory I) (_ : IsFiltered I)
      (D : I ⥤ Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} Λ))
      (ι : D ⟶ (Functor.const I).obj F), Nonempty (IsColimit (Cocone.mk F ι)) ∧
        ∀ i, IsConstructibleModuleSheaf B X Λ (D.obj i) ∧
          ∃ Z : Set X.obj, IsClosed Z ∧ Z ⊆ E ∧ supportModuleSheaf B X Λ (D.obj i) ⊆ Z

AlgebraicGeometry.exists_isFilteredColimit_isConstructibleAbelianSheaf_isClosed_support_of_torsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Constructible/SpecializationClosedSupportTorsionColimit.lean, line 48. The attribute's comment: “part (1), torsion abelian sheaves, torsion in the local sense of Stacks 0DD7”. References: SGA 4½ Arcata (4.3.3), “more general”.

Let X be a Noetherian scheme and let E ⊆ X be stable under specialization. A torsion abelian sheaf F on the small étale site of X whose support is contained in E is a filtered colimit of constructible abelian sheaves, each of whose supports is contained in a closed subset of E. Here torsion is the local condition Stacks.Torsion.torsionSheafProperty.

public theorem exists_isFilteredColimit_isConstructibleAbelianSheaf_isClosed_support_of_torsion
    (B : BigEtaleSite.{u}) (X : B.Scheme) [IsNoetherian X.obj]
    (E : Set X.obj) (hE : StableUnderSpecialization E)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
    (hF : Stacks.Torsion.torsionSheafProperty (SmallEtale.topology B X.obj X.property) F)
    (hsupp : supportSheaf B X.obj X.property F ⊆ E) :
    ∃ (I : Type (u + 1)) (_ : SmallCategory I) (_ : IsFiltered I)
      (D : I ⥤ Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
      (ι : D ⟶ (Functor.const I).obj F), Nonempty (IsColimit (Cocone.mk F ι)) ∧
        ∀ i, IsConstructibleAbelianSheaf B X (D.obj i) ∧
          ∃ Z : Set X.obj, IsClosed Z ∧ Z ⊆ E ∧
            supportSheaf B X.obj X.property (D.obj i) ⊆ Z

Sources

• Section 59.74, Tag 03RY
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isConstructibleSetSheaf_of_mono_of_epi_and_isSerreClass_abelian_and_module · AlgebraicGeometry.isConstructibleModuleSheaf_of_mono' · AlgebraicGeometry.isConstructibleModuleSheaf_of_epi' · AlgebraicGeometry.isConstructibleAbelianSheaf_of_mono · AlgebraicGeometry.isConstructibleAbelianSheaf_of_epi · AlgebraicGeometry.isSerreClass_isConstructibleAbelianSheaf · AlgebraicGeometry.isConstructibleModuleSheaf_of_mono · AlgebraicGeometry.isConstructibleModuleSheaf_of_epi

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.