61.19 Comparison with the étale… to 61.31 Change of partial universe

Section61.19 Comparison with the étale site#

Section 61.19 of the Stacks Project, Tag 099R. 12 tags here are carried by 25 declarations of the repository (all in StacksFrontier) and 13 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0GLZ, a lemma

Tag 0GLZ in the Stacks Project.

AlgebraicGeometry.Scheme.etaleSectionsPresheaf_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProetaleEtaleSheafPullback.lean, line 920. The attribute's comment: “the formula is a sheaf”.

For a sheaf ℱ on the small étale site of S, the rule (f : Y → S) ↦ Γ(Y_étale, f_étale⁻¹ℱ) is a sheaf on the small pro-étale site of S.

public theorem Scheme.etaleSectionsPresheaf_isSheaf (S : Scheme.{u})
    (F : Sheaf S.smallEtaleTopology (Type (max (u + 1) v))) :
    Presheaf.IsSheaf (Scheme.ProEt.topology S)
      ((Scheme.etaleSectionsPresheaf.{u, v} S).obj F)

AlgebraicGeometry.Scheme.proetaleInverseImageIsoEtaleSectionsSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProetaleEtaleSheafPullback.lean, line 965. The attribute's comment: “the identification with ε⁻¹”.

The sheaf defined by the rule is the inverse image ε⁻¹ℱ of the morphism of sites ε : S_proétale → S_étale, through the canonical comparison of two left adjoints of ε_*.

public def Scheme.proetaleInverseImageIsoEtaleSectionsSheaf :
    Functor.sheafPullbackConstruction.sheafPullback S.etaleToProetale
        (Type (max (u + 1) v)) S.smallEtaleTopology (Scheme.ProEt.topology S) ≅
      Scheme.etaleSectionsSheaf.{u, v} S

AlgebraicGeometry.Scheme.etaleSectionsFormulaIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProetaleEtaleSheafPullback.lean, line 1029. The attribute's comment: “the formula for sections”.

At a pro-étale object f : Y → S, the sheaf defined by the rule has as its sections the global sections on the small étale site of Y of the inverse image f_étale⁻¹ℱ, naturally in the étale sheaf ℱ.

public def Scheme.etaleSectionsFormulaIso (S : Scheme.{u}) (Y : S.ProEt) :
    Scheme.etaleSectionsSheaf.{u, v} S ⋙
        (sheafSections (Scheme.ProEt.topology S)
          (Type (max (u + 1) v))).obj (Opposite.op Y) ≅
      Stacks.EtaleCohomology.smallEtaleInverseImage.{u, v} Y.hom ⋙
        Sheaf.Γ Y.left.smallEtaleTopology (Type (max (u + 1) v))

AlgebraicGeometry.Scheme.proetaleInverseImageSectionsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProetaleEtaleSheafPullback.lean, line 1040. The attribute's comment: “the formula for sections”.

The sections of ε⁻¹ℱ at a pro-étale object f : Y → S are the global sections on the small étale site of Y of f_étale⁻¹ℱ.

public def Scheme.proetaleInverseImageSectionsIso (S : Scheme.{u}) (Y : S.ProEt) :
    Functor.sheafPullbackConstruction.sheafPullback S.etaleToProetale
          (Type (max (u + 1) v)) S.smallEtaleTopology (Scheme.ProEt.topology S) ⋙
        (sheafSections (Scheme.ProEt.topology S)
          (Type (max (u + 1) v))).obj (Opposite.op Y) ≅
      Stacks.EtaleCohomology.smallEtaleInverseImage.{u, v} Y.hom ⋙
        Sheaf.Γ Y.left.smallEtaleTopology (Type (max (u + 1) v))
Tag 099T, a lemma

Tag 099T in the Stacks Project.

AlgebraicGeometry.Scheme.isIso_unit_of_etaleToProetale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProetaleEtaleSheafPullbackUnit.lean, line 86. The attribute's comment: “the adjunction map ℱ ⟶ ε_ε⁻¹ℱ is an isomorphism, for an arbitrary left adjoint ε⁻¹ of ε_”.

For every sheaf ℱ on the small étale site of a scheme S, the adjunction map ℱ ⟶ ε_*ε⁻¹ℱ is an isomorphism, where ε : S_proétale → S_étale is the morphism of sites given by the inclusion of the small étale category into the small pro-étale category and ε⁻¹ is an arbitrary left adjoint of ε_*.

public theorem Scheme.isIso_unit_of_etaleToProetale
    {L : Sheaf S.smallEtaleTopology (Type (max (u + 1) v)) ⥤
      Sheaf (Scheme.ProEt.topology S) (Type (max (u + 1) v))}
    (adj : L ⊣ S.etaleToProetale.sheafPushforwardContinuous (Type (max (u + 1) v))
      S.smallEtaleTopology (Scheme.ProEt.topology S)) :
    IsIso adj.unit

AlgebraicGeometry.Scheme.isIso_proetaleInverseImageAdjunction_unit, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProetaleEtaleSheafPullbackUnit.lean, line 102. The attribute's comment: “the unit of the adjunction ε⁻¹ ⊣ ε_* is an isomorphism”.

The unit ℱ ⟶ ε_*ε⁻¹ℱ of the adjunction between the sheafified left Kan extension along the inclusion of the small étale category and restriction along it is an isomorphism.

public instance Scheme.isIso_proetaleInverseImageAdjunction_unit :
    IsIso (Functor.sheafPullbackConstruction.sheafAdjunctionContinuous S.etaleToProetale
      (Type (max (u + 1) v)) S.smallEtaleTopology (Scheme.ProEt.topology S)).unit

AlgebraicGeometry.Scheme.proetaleInverseImageEtaleSectionsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProetaleEtaleSheafPullbackUnit.lean, line 110. The attribute's comment: “the sections form: ε⁻¹ℱ(U) = ℱ(U) for U in S_étale”.

At an étale object U of S the sections of ε⁻¹ℱ are the sections of ℱ, naturally in ℱ.

public def Scheme.proetaleInverseImageEtaleSectionsIso (U : S.Etale) :
    Functor.sheafPullbackConstruction.sheafPullback S.etaleToProetale
          (Type (max (u + 1) v)) S.smallEtaleTopology (Scheme.ProEt.topology S) ⋙
        (sheafSections (Scheme.ProEt.topology S) (Type (max (u + 1) v))).obj
          (op (S.etaleToProetale.obj U)) ≅
      (sheafSections S.smallEtaleTopology (Type (max (u + 1) v))).obj (op U)

AlgebraicGeometry.Scheme.proetaleInverseImageFullyFaithful, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProetaleEtaleSheafPullbackUnit.lean, line 123. The attribute's comment: “equivalently, ε⁻¹ is fully faithful”.

The inverse image ε⁻¹ along the inclusion of the small étale site of S into its small pro-étale site is fully faithful.

public def Scheme.proetaleInverseImageFullyFaithful :
    (Functor.sheafPullbackConstruction.sheafPullback S.etaleToProetale
      (Type (max (u + 1) v)) S.smallEtaleTopology (Scheme.ProEt.topology S)).FullyFaithful
Tag 099S, a lemma

Tag 099S in the Stacks Project.

AlgebraicGeometry.Scheme.proetaleInverseImage_exists_map_eq_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProetaleEtaleSheafPullbackLimit.lean, line 113. The attribute's comment: “the injectivity half of ε⁻¹ℱ(Y) = colim ε⁻¹ℱ(Y_i), proved: two sections over a stage that agree over the limit agree over a later stage. The surjectivity half, hence the formula itself, is not proved here. Y = lim Y_i is the scheme-theoretic limit, as in the source; the index category is small in the universe of the schemes”.

Stacks 099S, the injectivity half. Let Y = lim Y_i be the limit of an inverse system of quasi-compact objects of X_proétale with affine transition morphisms, and let ℱ be a sheaf on X_étale. Two sections of ε⁻¹ℱ over a stage Y_i with the same restriction to Y already have the same restriction to some later stage Y_j; equivalently, the canonical map colim ε⁻¹ℱ(Y_i) → ε⁻¹ℱ(Y) is injective.

The sections are computed by the formula of Stacks 0GLZ through AlgebraicGeometry.Scheme.proetaleInverseImageIsoEtaleSectionsSheaf, which turns this into AlgebraicGeometry.Scheme.etaleSectionsSheaf_exists_map_eq_of_isLimit.

public theorem Scheme.proetaleInverseImage_exists_map_eq_of_isLimit
    {I : Type u} [SmallCategory I] [IsCofiltered I] (X : Scheme.{u}) (Y : I ⥤ X.ProEt)
    (c : Cone Y) (hc : IsLimit ((Scheme.ProEt.forget X ⋙ Over.forget X).mapCone c))
    (haffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Y.map f).left)
    (hqc : ∀ i : I, CompactSpace (Y.obj i).left)
    (F : Sheaf X.smallEtaleTopology (Type (max (u + 1) v))) (i : I)
    (s t : ((Functor.sheafPullbackConstruction.sheafPullback X.etaleToProetale
      (Type (max (u + 1) v)) X.smallEtaleTopology
      (Scheme.ProEt.topology X)).obj F).obj.obj (op (Y.obj i)))
    (hst : ((Functor.sheafPullbackConstruction.sheafPullback X.etaleToProetale
        (Type (max (u + 1) v)) X.smallEtaleTopology
        (Scheme.ProEt.topology X)).obj F).obj.map (c.π.app i).op s =
      ((Functor.sheafPullbackConstruction.sheafPullback X.etaleToProetale
        (Type (max (u + 1) v)) X.smallEtaleTopology
        (Scheme.ProEt.topology X)).obj F).obj.map (c.π.app i).op t) :
    ∃ (j : I) (f : j ⟶ i),
      ((Functor.sheafPullbackConstruction.sheafPullback X.etaleToProetale
          (Type (max (u + 1) v)) X.smallEtaleTopology
          (Scheme.ProEt.topology X)).obj F).obj.map (Y.map f).op s =
        ((Functor.sheafPullbackConstruction.sheafPullback X.etaleToProetale
          (Type (max (u + 1) v)) X.smallEtaleTopology
          (Scheme.ProEt.topology X)).obj F).obj.map (Y.map f).op t

AlgebraicGeometry.Scheme.injective_desc_proetaleInverseImage_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProetaleEtaleSheafPullbackLimit.lean, line 155. The attribute's comment: “proved: the comparison map colim ε⁻¹ℱ(Y_i) → ε⁻¹ℱ(Y) of the displayed formula is INJECTIVE, for every colimit cocone of the sections at the stages. Its surjectivity is not proved, so the formula itself is not”.

Stacks 099S, the injectivity half, for the comparison map out of the colimit. The canonical map colim ε⁻¹ℱ(Y_i) → ε⁻¹ℱ(Y) induced by the limit cone is injective, for any cocone exhibiting the colimit of the sections at the stages.

Elements of a filtered colimit come from a stage and the comparison map restricts on a stage to restriction along the cone leg, so this is AlgebraicGeometry.Scheme.proetaleInverseImage_exists_map_eq_of_isLimit at a stage below both.

public theorem Scheme.injective_desc_proetaleInverseImage_of_isLimit
    {I : Type u} [SmallCategory I] [IsCofiltered I] (X : Scheme.{u}) (Y : I ⥤ X.ProEt)
    (c : Cone Y) (hc : IsLimit ((Scheme.ProEt.forget X ⋙ Over.forget X).mapCone c))
    (haffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Y.map f).left)
    (hqc : ∀ i : I, CompactSpace (Y.obj i).left)
    (F : Sheaf X.smallEtaleTopology (Type (max (u + 1) v)))
    (E : Cocone (Y.op ⋙ ((Functor.sheafPullbackConstruction.sheafPullback X.etaleToProetale
      (Type (max (u + 1) v)) X.smallEtaleTopology (Scheme.ProEt.topology X)).obj F).obj))
    (hE : IsColimit E) :
    Function.Injective (hE.desc (((Functor.sheafPullbackConstruction.sheafPullback
      X.etaleToProetale (Type (max (u + 1) v)) X.smallEtaleTopology
      (Scheme.ProEt.topology X)).obj F).obj.mapCocone c.op))

AlgebraicGeometry.Scheme.etaleSections_exists_map_eq_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProetaleEtaleSheafPullbackLimit.lean, line 201. The attribute's comment: “the final statement ε⁻¹ℱ(Y) = colim ℱ(Y_i) for étale stages, injectivity half proved: two sections of ℱ over a stage with the same image in ε⁻¹ℱ(Y) agree over a later stage. Surjectivity is not proved, so the formula itself is not”.

Stacks 099S for étale stages, the injectivity half. If the stages Y_i are objects of X_étale, two sections of ℱ over a stage whose images in ε⁻¹ℱ(Y) under the unit ℱ ⟶ ε_*ε⁻¹ℱ agree already agree over some later stage; equivalently, the canonical map colim ℱ(Y_i) → ε⁻¹ℱ(Y) is injective.

The unit is an isomorphism by Stacks 099T, naturally in the étale object, which reduces this to AlgebraicGeometry.Scheme.proetaleInverseImage_exists_map_eq_of_isLimit.

public theorem Scheme.etaleSections_exists_map_eq_of_isLimit
    {I : Type u} [SmallCategory I] [IsCofiltered I] (X : Scheme.{u}) (Y : I ⥤ X.Etale)
    (c : Cone (Y ⋙ X.etaleToProetale))
    (hc : IsLimit ((Scheme.ProEt.forget X ⋙ Over.forget X).mapCone c))
    (haffine : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Y.map f).left)
    (hqc : ∀ i : I, CompactSpace (Y.obj i).left)
    (F : Sheaf X.smallEtaleTopology (Type (max (u + 1) v))) (i : I)
    (s t : F.obj.obj (op (Y.obj i)))
    (hst : ((Functor.sheafPullbackConstruction.sheafPullback X.etaleToProetale
          (Type (max (u + 1) v)) X.smallEtaleTopology
          (Scheme.ProEt.topology X)).obj F).obj.map (c.π.app i).op
        (((Functor.sheafPullbackConstruction.sheafAdjunctionContinuous X.etaleToProetale
          (Type (max (u + 1) v)) X.smallEtaleTopology
          (Scheme.ProEt.topology X)).unit.app F).hom.app (op (Y.obj i)) s) =
      ((Functor.sheafPullbackConstruction.sheafPullback X.etaleToProetale
          (Type (max (u + 1) v)) X.smallEtaleTopology
          (Scheme.ProEt.topology X)).obj F).obj.map (c.π.app i).op
        (((Functor.sheafPullbackConstruction.sheafAdjunctionContinuous X.etaleToProetale
          (Type (max (u + 1) v)) X.smallEtaleTopology
          (Scheme.ProEt.topology X)).unit.app F).hom.app (op (Y.obj i)) t)) :
    ∃ (j : I) (f : j ⟶ i), F.obj.map (Y.map f).op s = F.obj.map (Y.map f).op t

Declarations registered for the tag:

Tag 099U, a lemma

Tag 099U in the Stacks Project.

Declarations registered for the tag:

Tag 099V, a lemma

Tag 099V in the Stacks Project.

Declarations registered for the tag:

Tag 099W, a lemma

Tag 099W in the Stacks Project.

Declarations registered for the tag:

Tag 099X, a lemma

Tag 099X in the Stacks Project.

Declarations registered for the tag:

Tag 09B1, a lemma

Tag 09B1 in the Stacks Project.

Declarations registered for the tag:

Tag 099Y, a lemma

Tag 099Y in the Stacks Project.

Declarations registered for the tag:

Tag 099Z, a lemma

Tag 099Z in the Stacks Project.

Declarations registered for the tag:

Tag 09B2, a lemma

Tag 09B2 in the Stacks Project.

AlgebraicGeometry.ProEtale.essImage_mapDerivedCategory_and_hasTorAmplitude_derivedExtendScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Cohomology/AdicReductionComparison.lean, line 277.

Stacks 09B2. Let X be a scheme, Λ a Noetherian ring, I ⊆ Λ an ideal and K an object of D(X_proétale, Λ). Set Kₙ = K ⊗_Λ^L Λ/Iⁿ, the derived extension of scalars of K along Λ → Λ/Iⁿ. If K₁ is in the essential image of ε⁻¹ : D(X\_étale, Λ/I) ⥤ D(X\_proétale, Λ/I) and has Tor amplitude in [a, ∞), then, for every n, Kₙ is in the essential image of ε⁻¹ : D(X_étale, Λ/Iⁿ) ⥤ D(X_proétale, Λ/Iⁿ) and has Tor amplitude in [a, ∞).

Here ε⁻¹ on derived categories is ε⁻¹ applied termwise, and Tor amplitude in [a, ∞) is Stacks.ModuleSheaf.HasTorAmplitude for Set.Ici a: Hⁱ(L ⊗^L F) = 0 for i < a and every sheaf of modules F.

theorem essImage_mapDerivedCategory_and_hasTorAmplitude_derivedExtendScalars
    [IsNoetherianRing Λ]
    (K : DerivedCategory (Sheaf (Scheme.ProEt.topology X) (ModuleCat.{max (u + 1) w} Λ)))
    (a : ℤ)
    (h₁ : (Scheme.etaleInverseImage.{u, w} X (Λ ⧸ I)).mapDerivedCategory.essImage
      ((derivedExtendScalars _ (Ideal.Quotient.mk I)).obj K))
    (h₂ : HasTorAmplitude (J := Scheme.ProEt.topology X)
      ((derivedExtendScalars _ (Ideal.Quotient.mk I)).obj K) (Set.Ici a))
    (n : ℕ) :
    (Scheme.etaleInverseImage.{u, w} X (Λ ⧸ I ^ n)).mapDerivedCategory.essImage
        ((derivedExtendScalars _ (Ideal.Quotient.mk (I ^ n))).obj K) ∧
      HasTorAmplitude (J := Scheme.ProEt.topology X)
        ((derivedExtendScalars _ (Ideal.Quotient.mk (I ^ n))).obj K)
        (Set.Ici a)
Tag 0F6D, an example

Tag 0F6D in the Stacks Project.

AlgebraicGeometry.ProEtale.pointFunctions_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/PointFunctions.lean, line 235. The attribute's comment: “fun(-, A) is a sheaf on the pro-étale site”.

The point functions form a sheaf. The rule U ↦ (|U| → A) is a sheaf for the pro-étale topology: it is the sheaf of continuous maps to A with the indiscrete topology, which is an fpqc sheaf.

theorem pointFunctions_isSheaf (X : Scheme.{u}) (A : Type v) [AddCommGroup A] :
    Presheaf.IsSheaf (Scheme.ProEt.topology X) (pointFunctions.{u, v} X A)

AlgebraicGeometry.ProEtale.mono_constantToPointFunctions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/PointFunctions.lean, line 289. The attribute's comment: “exactness on the left of 0 → A → fun(-, A) → F → 0”.

The constant sheaf is a subsheaf of fun(-, A): the map A ⟶ fun(-, A) is a monomorphism, which is exactness on the left of 0 → A → fun(-, A) → F → 0.

theorem mono_constantToPointFunctions (X : Scheme.{u}) (A : Type v) [AddCommGroup A] :
    Mono (constantToPointFunctions.{u, v} X A)

AlgebraicGeometry.ProEtale.pointFunctionsShortComplex_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/PointFunctions.lean, line 333. The attribute's comment: “the sequence 0 → A → fun(-, A) → F → 0 is exact”.

The sequence 0 → A → fun(-, A) → F → 0 is short exact.

theorem pointFunctionsShortComplex_shortExact (X : Scheme.{u}) (A : Type v) [AddCommGroup A] :
    (pointFunctionsShortComplex X A).ShortExact

AlgebraicGeometry.ProEtale.ker_pointFunctionsQuotientProjApp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/PointFunctions.lean, line 352. The attribute's comment: “the kernel of fun(U, A) → F(U) is A(U)”.

The kernel of fun(U, A) ⟶ F(U) is A(U), for every object U of the small pro-étale site: sections are left exact.

theorem ker_pointFunctionsQuotientProjApp (X : Scheme.{u}) (A : Type v) [AddCommGroup A]
    (U : X.ProEt) :
    (pointFunctionsQuotientProjApp X A U).ker = (constantToPointFunctionsApp X A U).range

AlgebraicGeometry.ProEtale.constantSheafCompEpsilonInverseImageIsoConstantSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/PointFunctions.lean, line 374. The attribute's comment: “A = ε⁻¹A: the constant sheaf is pulled back from the étale site”.

The constant sheaf is pulled back from the étale site: A = ε⁻¹A. Both the constant sheaf functor of the small pro-étale site and the constant sheaf functor of the small étale site followed by ε⁻¹ are left adjoint to taking sections over the final object X ⟶ X, that is, both are the pullback from the final topos; the isomorphism is the comparison of these two left adjoints, natural in the coefficient group.

def constantSheafCompEpsilonInverseImageIsoConstantSheaf (X : Scheme.{u}) :
    constantSheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v} ⋙
        epsilonInverseImage.{u, v} X ≅
      constantSheaf (Scheme.ProEt.topology X) AddCommGrpCat.{max (u + 1) v}

AlgebraicGeometry.ProEtale.not_etalePullback_pointFunctionsSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/PointFunctions.lean, line 603. The attribute's comment: “if A has more than one element, fun(-, A) is not pulled back from the étale site (for X nonempty)”.

fun(-, A) is not pulled back from the étale site. If X is nonempty and A has more than one element, fun(-, A) is not in the essential image of ε⁻¹.

A pulled back sheaf restricted to the fibre over a point x only sees continuous functions on the fibres of its sections' domains with the discrete topology on A, since the fibres of étale X-schemes over x are discrete; but there is a weakly étale X-scheme whose fibre over x contains a Cantor set, on which not every function is continuous.

theorem not_etalePullback_pointFunctionsSheaf (X : Scheme.{u}) (A : Type v)
    [AddCommGroup A] (hX : Nonempty X) (hA : Nontrivial A) :
    ¬ (epsilonInverseImage.{u, v} X).essImage (pointFunctionsSheaf X A)

AlgebraicGeometry.ProEtale.isClosed_singleton_of_proetale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/PointFunctions.lean, line 632. The attribute's comment: “if all points of X are closed, then all points of U are closed”.

Closed points pass to weakly étale X-schemes. If all points of X are closed, then all points of every object U of the small pro-étale site of X are closed: over an affine open of X, whose spectrum is then profinite, an affine open of U has profinite spectrum too.

theorem isClosed_singleton_of_proetale (X : Scheme.{u})
    (hclosed : ∀ x : X, IsClosed ({x} : Set X))
    (U : X.ProEt) (y : U.left) : IsClosed ({y} : Set U.left)

AlgebraicGeometry.ProEtale.isSepClosed_residueField_of_proetale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/PointFunctions.lean, line 698. The attribute's comment: “if all residue fields of X are separably closed, then so are those of U”.

Separably closed residue fields pass to weakly étale X-schemes. If all residue fields of X are separably closed, then so are all residue fields of every object U of the small pro-étale site of X: the residue field extensions of a weakly étale morphism are separable algebraic.

theorem isSepClosed_residueField_of_proetale (X : Scheme.{u})
    (hsep : ∀ x : X, IsSepClosed (X.residueField x))
    (U : X.ProEt) (y : U.left) : IsSepClosed (U.left.residueField y)

AlgebraicGeometry.ProEtale.subsingleton_etaleH_one_constantSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/PointFunctions.lean, line 717. The attribute's comment: “H¹_étale(U, A) = 0 for affine U, when all points of X are closed with separably closed residue fields”.

H¹_étale(U, A) = 0 for an affine object U of the small pro-étale site of a scheme X all of whose points are closed with separably closed residue fields: the points of U are then closed with separably closed residue fields, and étale cohomology in positive degrees vanishes on such an affine scheme.

theorem subsingleton_etaleH_one_constantSheaf (X : Scheme.{u}) (A : Type v) [AddCommGroup A]
    (hclosed : ∀ x : X, IsClosed ({x} : Set X))
    (hsep : ∀ x : X, IsSepClosed (X.residueField x))
    (U : X.ProEt) [IsAffine U.left]
    [HasExt.{w} (Sheaf U.left.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})] :
    Subsingleton (Sheaf.H.{w}
      ((constantSheaf U.left.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}).obj
        (pointFunctionsCoeff.{u} A)) 1)

AlgebraicGeometry.ProEtale.subsingleton_proetaleH_one_constantSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/PointFunctions.lean, line 740. The attribute's comment: “H¹_proétale(U, A) = 0 for affine U, when all points of X are closed with separably closed residue fields”.

H¹_proétale(U, A) = 0 for an affine object U of the small pro-étale site of a scheme X all of whose points are closed with separably closed residue fields: by the comparison H^i(U_étale, ℱ) = H^i(U_proétale, ε⁻¹ℱ) of étale and pro-étale cohomology on U (Stacks 099W (1), AlgebraicGeometry.ProEtale.epsilonInverseImageCompFunctorHIso) and A = ε⁻¹A, it reduces to H¹_étale(U, A) = 0.

theorem subsingleton_proetaleH_one_constantSheaf (X : Scheme.{u})
    (A : Type v) [AddCommGroup A]
    (hclosed : ∀ x : X, IsClosed ({x} : Set X))
    (hsep : ∀ x : X, IsSepClosed (X.residueField x))
    (U : X.ProEt) [IsAffine U.left]
    [HasExt.{w} (Sheaf (Scheme.ProEt.topology U.left) AddCommGrpCat.{max (u + 1) v})] :
    Subsingleton (Sheaf.H.{w}
      ((constantSheaf (Scheme.ProEt.topology U.left) AddCommGrpCat.{max (u + 1) v}).obj
        (pointFunctionsCoeff.{u} A)) 1)

AlgebraicGeometry.ProEtale.surjective_pointFunctionsQuotientProjApp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/PointFunctions.lean, line 812. The attribute's comment: “F(U) = fun(U, A)/A(U) for affine U: every section of F over U lifts to fun(U, A)”.

fun(U, A) ⟶ F(U) is surjective for an affine object U of the small pro-étale site of a scheme X all of whose points are closed with separably closed residue fields: the obstruction lies in H¹_proétale(U, A), which vanishes.

theorem surjective_pointFunctionsQuotientProjApp (X : Scheme.{u})
    (A : Type v) [AddCommGroup A]
    (hclosed : ∀ x : X, IsClosed ({x} : Set X))
    (hsep : ∀ x : X, IsSepClosed (X.residueField x))
    (U : X.ProEt) [IsAffine U.left] :
    Function.Surjective (pointFunctionsQuotientProjApp.{u, v} X A U)

AlgebraicGeometry.ProEtale.pointFunctionsQuotientAppEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/PointFunctions.lean, line 874. The attribute's comment: “F(U) = fun(U, A)/A(U) for affine U, when all points of X are closed with separably closed residue fields”.

F(U) = fun(U, A)/A(U) for an affine object U of the small pro-étale site of a scheme X all of whose points are closed with separably closed residue fields: the projection fun(U, A) ⟶ F(U) is surjective with kernel the constant sections A(U).

def pointFunctionsQuotientAppEquiv (X : Scheme.{u})
    (A : Type v) [AddCommGroup A]
    (hclosed : ∀ x : X, IsClosed ({x} : Set X))
    (hsep : ∀ x : X, IsSepClosed (X.residueField x))
    (U : X.ProEt) [IsAffine U.left] :
    (U.left → ULift.{max (u + 1) v} A) ⧸ (constantToPointFunctionsApp.{u, v} X A U).range ≃+
      (pointFunctionsQuotient.{u, v} X A).obj.obj (op U)

AlgebraicGeometry.ProEtale.not_etalePullback_pointFunctionsQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/PointFunctions.lean, line 892. The attribute's comment: “if A has more than one element, the quotient F is not pulled back from the étale site (for X nonempty)”.

F is not pulled back from the étale site. If X is nonempty and A has more than one element, the quotient F = fun(-, A)/A is not in the essential image of ε⁻¹: since Rε_*ε⁻¹ℱ = ℱ for abelian sheaves ℱ on X_étale (Stacks 099V (1), AlgebraicGeometry.ProEtale.isIso_unit_app_and_isZero_rightDerived_epsilonDirectImage), the essential image of ε⁻¹ is closed under extensions, A = ε⁻¹A, and fun(-, A) is not in it.

theorem not_etalePullback_pointFunctionsQuotient (X : Scheme.{u}) (A : Type v)
    [AddCommGroup A] (hX : Nonempty X) (hA : Nontrivial A) :
    ¬ (epsilonInverseImage.{u, v} X).essImage (pointFunctionsQuotient X A)
Sources
LeanAlgebraicGeometry.Scheme.etaleSectionsPresheaf_isSheaf · AlgebraicGeometry.Scheme.proetaleInverseImageIsoEtaleSectionsSheaf · AlgebraicGeometry.Scheme.etaleSectionsFormulaIso · AlgebraicGeometry.Scheme.proetaleInverseImageSectionsIso · AlgebraicGeometry.Scheme.isIso_unit_of_etaleToProetale · AlgebraicGeometry.Scheme.isIso_proetaleInverseImageAdjunction_unit · AlgebraicGeometry.Scheme.proetaleInverseImageEtaleSectionsIso · AlgebraicGeometry.Scheme.proetaleInverseImageFullyFaithful

Section61.20 Derived completion in the constant Noetherian case#

Section 61.20 of the Stacks Project, Tag 099L. 2 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 099M, a lemma

Tag 099M in the Stacks Project.

AlgebraicGeometry.RingedSite.derivedCompletion_eq_rlim_constantAdicTower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/ConstantNoetherianCompletion.lean, line 466.

Let 𝒞 be a site, let Λ be a Noetherian ring and let I ⊂ Λ be an ideal. The left adjoint K ↦ K^∧ of the inclusion of the objects of D(𝒞, Λ) derived complete along IΛ̲ ([Stacks, Tag 099F]) sends K to R lim (K ⊗^𝐋_Λ (Λ/Iⁿ)̲); and K is derived complete exactly when K = R lim (K ⊗^𝐋_Λ (Λ/Iⁿ)̲).

theorem derivedCompletion_eq_rlim_constantAdicTower
    (K : DerivedCategory (SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (constant J Λ).O))) :
    IsDerivedLimit (constantAdicTower J Λ I K)
        ((derivedCompletion (constant J Λ) (constantIdealSheaf J Λ I)).obj K) ∧
      (IsDerivedComplete.{u, u, u, u} (constant J Λ) (constantIdealSheaf J Λ I) K ↔
        IsDerivedLimit (constantAdicTower J Λ I K) K)

Stacks.ModuleSheaf.exists_leftAdjoint_isDerivedLimitWithProjections_derivedReductionTower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/DerivedTensorModuleSheaf/DerivedCompletion.lean, line 84. The attribute's comment: “the left adjoint is K ↦ R lim (K ⊗^L Λ/Iⁿ)”.

The derived completion functor in the constant Noetherian case. The inclusion of the derived complete objects of D(C, Λ) has a left adjoint K ↦ K^∧, where K^∧ is a derived limit R lim (K ⊗_Λ^L \underline{Λ/Iⁿ}) with projections natural in K, whose composites with the unit K → K^∧ are the reductions K → K ⊗_Λ^L \underline{Λ/Iⁿ}.

theorem exists_leftAdjoint_isDerivedLimitWithProjections_derivedReductionTower :
    let P : ObjectProperty (DerivedCategory (Sheaf J (ModuleCat.{w} Λ))) :=
      fun K ↦ IsDerivedComplete I K
    ∃ (Lf : DerivedCategory (Sheaf J (ModuleCat.{w} Λ)) ⥤ P.FullSubcategory) (adj : Lf ⊣ P.ι)
      (π : ∀ n : ℕ, Lf ⋙ P.ι ⟶
        derivedReductionTowerFunctor J Λ I ⋙ (evaluation ℕᵒᵖ _).obj ⟨n⟩),
      (∀ K, IsDerivedLimitWithProjections (derivedReductionTower J Λ I K) ((Lf ⋙ P.ι).obj K)
        fun n ↦ (π n).app K) ∧
      ∀ K (n : ℕ), adj.unit.app K ≫ (π n).app K = (derivedReductionMap J Λ I K).app ⟨n⟩

Stacks.ModuleSheaf.isDerivedComplete_iff_isDerivedLimitWithProjections_derivedReductionTower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/DerivedTensorModuleSheaf/DerivedCompletion.lean, line 101. The attribute's comment: “in particular: K is complete iff K = R lim (K ⊗^L Λ/Iⁿ)”.

K is derived complete if and only if K = R lim (K ⊗_Λ^L \underline{Λ/Iⁿ}), i.e. K, with the reductions K → K ⊗_Λ^L \underline{Λ/Iⁿ}, is a derived limit of the reductions.

theorem isDerivedComplete_iff_isDerivedLimitWithProjections_derivedReductionTower
    (K : DerivedCategory (Sheaf J (ModuleCat.{w} Λ))) :
    IsDerivedComplete I K ↔ IsDerivedLimitWithProjections (derivedReductionTower J Λ I K) K
      fun n ↦ (derivedReductionMap J Λ I K).app ⟨n⟩
Tag 099N, a lemma

Tag 099N in the Stacks Project.

MorphismOfTopoi.isDerivedComplete_constantDerivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/ConstantPushforwardCompletion.lean, line 350. The attribute's comment: “(1)”.

Rf_* preserves derived completeness. Let Λ be a Noetherian ring, I ⊂ Λ an ideal and f : Sh(𝒟) ⟶ Sh(𝒞) a morphism of topoi. If E in D(𝒟, Λ) is derived complete along IΛ̲, so is Rf_*E in D(𝒞, Λ).

theorem isDerivedComplete_constantDerivedPushforward
    (E : DerivedCategory (SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (RingedTopos.constant K Λ).O)))
    (hE : RingedSite.IsDerivedComplete.{u, u, u, u} (RingedSite.constant K Λ)
      (RingedSite.constantIdealSheaf K Λ I) E) :
    RingedSite.IsDerivedComplete.{u, u, u, u} (RingedSite.constant J Λ)
      (RingedSite.constantIdealSheaf J Λ I) ((constantDerivedPushforward Λ f).obj E)

MorphismOfTopoi.constantDerivedCompletePullbackPushforwardAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/ConstantToposCompletion.lean, line 126. The attribute's comment: “(2)”.

[Stacks, Tag 099N], part (2). Let Λ be a Noetherian ring, I ⊂ Λ an ideal and f : Sh(𝒟) ⟶ Sh(𝒞) a morphism of topoi. The functor Rf_* : D_comp(𝒟, Λ) ⥤ D_comp(𝒞, Λ) has a left adjoint Lf^*_comp : D_comp(𝒞, Λ) ⥤ D_comp(𝒟, Λ), which is Lf^* followed by derived completion (MorphismOfTopoi.constantDerivedCompletePullback_comp_ι).

def constantDerivedCompletePullbackPushforwardAdjunction :
    constantDerivedCompletePullback Λ I f ⊣ constantDerivedCompletePushforward Λ I f

MorphismOfTopoi.isIso_derivedCompletionComparison_constantDerivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/ConstantToposCompletion.lean, line 134. The attribute's comment: “(3)”.

[Stacks, Tag 099N], part (3). Let Λ be a Noetherian ring, I ⊂ Λ an ideal and f : Sh(𝒟) ⟶ Sh(𝒞) a morphism of topoi. Rf_* commutes with derived completion: the canonical comparison (Rf_*K)^∧ ⟶ Rf_*(K^∧), natural in K in D(𝒟, Λ), is an isomorphism.

theorem isIso_derivedCompletionComparison_constantDerivedPushforward :
    IsIso (RingedSite.derivedCompletionComparison (RingedSite.constantIdealSheaf K Λ I)
      (RingedSite.constantIdealSheaf J Λ I) (constantDerivedPushforward Λ f)
      (fun E hE => isDerivedComplete_constantDerivedPushforward Λ f I E hE))

MorphismOfTopoi.isDerivedLimit_constantAdicTower_constantDerivedPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/ConstantToposCompletion.lean, line 146. The attribute's comment: “(4)”.

[Stacks, Tag 099N], part (4). Let Λ be a Noetherian ring, I ⊂ Λ an ideal and f : Sh(𝒟) ⟶ Sh(𝒞) a morphism of topoi. For K in D_comp(𝒟, Λ), Rf_*K = R lim Rf_*(K ⊗^𝐋_Λ (Λ/Iⁿ)̲): Rf_*K is a derived limit of the tower n ↦ Rf_*(K ⊗^𝐋_Λ (Λ/Iⁿ)̲).

theorem isDerivedLimit_constantAdicTower_constantDerivedPushforward
    (E : DerivedCategory (SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (RingedTopos.constant K Λ).O)))
    (hE : RingedSite.IsDerivedComplete.{u, u, u, u} (RingedSite.constant K Λ)
      (RingedSite.constantIdealSheaf K Λ I) E) :
    IsDerivedLimit (RingedSite.constantAdicTower K Λ I E ⋙ constantDerivedPushforward Λ f)
      ((constantDerivedPushforward Λ f).obj E)

MorphismOfTopoi.isDerivedLimit_constantAdicTower_constantDerivedCompletePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/ConstantToposCompletion.lean, line 178. The attribute's comment: “(5)”.

[Stacks, Tag 099N], part (5). Let Λ be a Noetherian ring, I ⊂ Λ an ideal and f : Sh(𝒟) ⟶ Sh(𝒞) a morphism of topoi. For M in D_comp(𝒞, Λ), Lf^*_comp M = R lim Lf^*(M ⊗^𝐋_Λ (Λ/Iⁿ)̲): Lf^*_comp M is a derived limit of the tower n ↦ Lf^*(M ⊗^𝐋_Λ (Λ/Iⁿ)̲).

theorem isDerivedLimit_constantAdicTower_constantDerivedCompletePullback
    (M : ObjectProperty.FullSubcategory (RingedSite.IsDerivedComplete.{u, u, u, u}
      (RingedTopos.constant J Λ).toRingedSite (RingedSite.constantIdealSheaf J Λ I))) :
    IsDerivedLimit (RingedSite.constantAdicTower J Λ I M.1 ⋙ constantDerivedPullback Λ f)
      ((constantDerivedCompletePullback Λ I f).obj M).1

AlgebraicGeometry.RingedSite.isDerivedLimit_derivedPushforward_adicReductionTower_of_proIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardAdicLimit.lean, line 167. The attribute's comment: “part (4), for an arbitrary ringed site and ℐ' the ideal sheaf generated by finitely many global sections, in place of the source's constant Noetherian coefficients (𝒞, Λ), and with the tower of adic quotients taken on the source site. ASSUMED: the pro-isomorphism a in D(𝒪') of the dual Koszul tower with the tower n ↦ 𝒪'/ℐ'ⁿ⁺¹, which is the one hypothesis of this library's form of [Stacks, Tag 099M] and which the source derives from [Stacks, Tag 0921] over a Noetherian coefficient ring; and, carried from [Stacks, Tag 0A0E], the instance HasCoproduct for the Koszul system, which is automatic in the source”.

Part (4) of [Stacks, Tag 099N], granted the pro-isomorphism of towers of [Stacks, Tag 099M]. Let f : (Sh(𝒟), 𝒪') ⟶ (Sh(𝒞), 𝒪) be a morphism of ringed sites, let g_1, …, g_r be global sections of 𝒪' and let ℐ' = (g_1, …, g_r). Suppose the tower n ↦ Kₙ^∨ of duals of the Koszul complexes on the powers of the g_i is isomorphic, as a pro-object of D(𝒪'), to the tower n ↦ 𝒪'/ℐ'ⁿ⁺¹. Then for every K in D(𝒪') derived complete along ℐ',

Rf_*K = R lim Rf_*(K ⊗^𝐋_{𝒪'} 𝒪'/ℐ'ⁿ⁺¹).

This is the source's proof: Tag 099M in criterion form, isDerivedComplete_iff_isDerivedLimit_adicReductionTower_of_proIso, exhibits K itself as a derived limit of the tower of its adic reductions, and [Stacks, Tag 0A07], Stacks.Cohomology.DerivedPushforwardOnRingedTopoi.isDerivedLimit_map_derivedPushforward, carries a derived limit along Rf_*.

theorem isDerivedLimit_derivedPushforward_adicReductionTower_of_proIso
    (K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    [HasCoproduct ((koszulPowerSystem X g ⋙ DerivedCategory.Q).obj)]
    (hK : IsDerivedComplete.{u, u, u, u} X (idealOfGlobalSections X g) K)
    (a : InverseSequence.ProIso (koszulPowerDualSystem X g)
      (adicQuotientDerivedTower X (idealOfGlobalSections X g))) :
    IsDerivedLimit (adicReductionTower X (idealOfGlobalSections X g) K ⋙
        derivedPushforward.{u} f.toRingedToposSiteHom)
      ((derivedPushforward.{u} f.toRingedToposSiteHom).obj K)

AlgebraicGeometry.RingedSite.isDerivedLimit_adicReductionTower_derivedCompletePullback_of_proIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardAdicLimit.lean, line 207. The attribute's comment: “part (5), at the generality of part (4) — an arbitrary ringed site, ℐ' generated by finitely many global sections, and the tower of adic quotients formed on the source site, where the source's n ↦ Lf^*(M ⊗^𝐋 Λ/Iⁿ) becomes n ↦ Lf^*M ⊗^𝐋_{𝒪'} 𝒪'/ℐ'ⁿ⁺¹. ASSUMED: exactly what part (4) assumes — the pro-isomorphism a and the HasCoproduct instance — and nothing else”.

Part (5) of [Stacks, Tag 099N], granted the pro-isomorphism of towers of [Stacks, Tag 099M]. In the situation of isDerivedLimit_derivedPushforward_adicReductionTower_of_proIso, and for an arbitrary sheaf of ideals ℐ ⊂ 𝒪 on the base, the completed pullback Lf^*_comp M of AlgebraicGeometry.RingedSite.derivedCompletePullback — that is Lf^* followed by derived completion along ℐ' — of an object M of D_comp(𝒪, ℐ) satisfies

Lf^*_comp M = R lim (Lf^*M ⊗^𝐋_{𝒪'} 𝒪'/ℐ'ⁿ⁺¹).

The source writes the tower as n ↦ Lf^*(M ⊗^𝐋 Λ/Iⁿ), which with its constant coefficients is the same system: Lf^* commutes with ⊗^𝐋 by [Stacks, Tag 07A4] and fixes the constant sheaf Λ/Iⁿ. Here the reductions are formed on the source site to begin with, so what is proved is Tag 099M in formula form, isDerivedLimit_adicReductionTower_completionFunctor_of_proIso, at the object Lf^*M, whose completion is Lf^*_comp M by definition. The completion there is named by the Čech functor of [Stacks, Tag 099B] and here by the reflector of [Stacks, Tag 099F]; the two are identified by AlgebraicGeometry.RingedSite.exists_iso_derivedCompletion_completionFunctor, and the derived limit crosses that isomorphism by CategoryTheory.Pretriangulated.IsDerivedLimit.of_objIso.

theorem isDerivedLimit_adicReductionTower_derivedCompletePullback_of_proIso
    (I : SheafOfModules.Submodule (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)))
    [HasCoproduct ((koszulPowerSystem X g ⋙ DerivedCategory.Q).obj)]
    (M : ObjectProperty.FullSubcategory (IsDerivedComplete.{u, u, u, u} Y I))
    (a : InverseSequence.ProIso (koszulPowerDualSystem X g)
      (adicQuotientDerivedTower X (idealOfGlobalSections X g))) :
    letI := isRightAdjoint_ι_isDerivedComplete_idealOfGlobalSections X g
    IsDerivedLimit
      (adicReductionTower X (idealOfGlobalSections X g)
        ((derivedPullback.{u} f.toRingedToposSiteHom).obj M.1))
      ((derivedCompletePullback f I (idealOfGlobalSections X g)).obj M).1

AlgebraicGeometry.RingedSite.derivedCompletePushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletion.lean, line 301. The attribute's comment: “part (1), for an arbitrary ringed site in place of the source's constant Noetherian coefficients (𝒞, Λ)”.

The first statement of [Stacks, Tag 099K], for a morphism of ringed sites. Rf_* as a functor D_comp(𝒪', ℐ') ⥤ D_comp(𝒪, ℐ): the derived direct image of a derived-complete object is derived complete, by [Stacks, Tag 099J]. The tag is registered for a morphism of ringed topoi, on AlgebraicGeometry.RingedToposHom.isDerivedComplete_derivedPushforward.

This is also part (1) of [Stacks, Tag 099N], stated for an arbitrary ringed site rather than for the constant Noetherian coefficients (𝒞, Λ) of that tag. The identification of D(𝒞, Λ) with D(𝒪) for the constant sheaf of rings Λ is not formalized in this library, so what is proved is the statement at a generality containing the source's, not a composite with that identification.

def derivedCompletePushforward :
    ObjectProperty.FullSubcategory (IsDerivedComplete.{u, u, u, u} X I') ⥤
      ObjectProperty.FullSubcategory (IsDerivedComplete.{u, u, u, u} Y I)

AlgebraicGeometry.RingedSite.derivedCompletePullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletion.lean, line 323. The attribute's comment: “part (2), the functor Lf^*_comp, for an arbitrary ringed site in place of the source's constant Noetherian coefficients, and for every ℐ' whose derived-complete objects are reflective in D(𝒪') — which [Stacks, Tag 099F] gives for an ideal sheaf of finite type”.

The left adjoint of [Stacks, Tag 099K], for a reflective D_comp(𝒪', ℐ'). Lf^*_comp, that is Lf^* followed by derived completion, as a functor D_comp(𝒪, ℐ) ⥤ D_comp(𝒪', ℐ').

The source reaches the derived completion functor from "ℐ' of finite type" through [Stacks, Tag 099F]. What this construction consumes is that conclusion alone — that the inclusion of the derived-complete objects has a left adjoint — so that is what the statement asks for; for an ℐ' of finite type the instance of [Stacks, Tag 099F], AlgebraicGeometry.RingedSite.isRightAdjoint_ι_isDerivedComplete, supplies it. This is also part (2) of [Stacks, Tag 099N], at the generality of part (1).

def derivedCompletePullback :
    ObjectProperty.FullSubcategory (IsDerivedComplete.{u, u, u, u} Y I) ⥤
      ObjectProperty.FullSubcategory (IsDerivedComplete.{u, u, u, u} X I')

AlgebraicGeometry.RingedSite.derivedCompletePullbackPushforwardAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletion.lean, line 350. The attribute's comment: “part (2), the adjunction, at the generality named on derivedCompletePullback; parts (4) and (5) are in PushforwardAdicLimit.lean”.

The adjunction of [Stacks, Tag 099K], for a reflective D_comp(𝒪', ℐ'). On the derived-complete objects, Lf^* followed by derived completion is left adjoint to Rf_*. This is the source's chain Hom(K, Rf_*M) = Hom(Lf^*K, M) = Hom(Lf^*_comp K, M): the composite of the adjunction Lf^* ⊣ Rf_* of [Stacks, Tag 07A6] with the reflector adjunction of [Stacks, Tag 099F], restricted along the fully faithful inclusion of D_comp(𝒪, ℐ) into D(𝒪).

The @[stacks 099K] registration of this second statement is on the statement for a morphism of ringed topoi, AlgebraicGeometry.RingedToposHom.derivedCompletePullbackPushforwardAdjunction of PushforwardCompletionTopos.lean.

This is also part (2) of [Stacks, Tag 099N]. Parts (4) and (5) of that tag, the formulas Rf_*K = R lim Rf_*(K ⊗^L Λ/Iⁿ) and Lf^*_comp M = R lim Lf^*(M ⊗^L Λ/Iⁿ), are proved in PushforwardAdicLimit.lean of this directory, as AlgebraicGeometry.RingedSite.isDerivedLimit_derivedPushforward_adicReductionTower_of_proIso and AlgebraicGeometry.RingedSite.isDerivedLimit_adicReductionTower_derivedCompletePullback_of_proIso; each carries the single hypothesis of this library's form of [Stacks, Tag 099M], a pro-isomorphism of the dual Koszul tower with the tower of adic quotients.

def derivedCompletePullbackPushforwardAdjunction :
    derivedCompletePullback f I I' ⊣ derivedCompletePushforward f I I' hI

AlgebraicGeometry.RingedSite.isIso_derivedCompletionPushforwardComparison_of_isDerivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/DerivedCompletionRinged/PushforwardCommutesCompletion.lean, line 500. The attribute's comment: “part (3), for a derived-complete object and an arbitrary ringed site”.

[Stacks, Tag 0A0G] at a derived-complete object. For K in D_comp(𝒪', ℐ') the canonical map (Rf_*K)^∧ ⟶ Rf_*(K^∧) is invertible, so Rf_*(K^∧) = Rf_*K = (Rf_*K)^∧: the unit K ⟶ K^∧ is invertible on a derived-complete K.

The general case of Tag 0A0G is not proved; see isIso_derivedCompletionPushforwardComparison_of_isIso_map_unit for the criterion that is, and the module documentation for the state of the four inputs of the source's proof. Three of them ([Stacks, Tags 0A0F, 0A0E, 0A07]) are now available; what is missing is the base case K = 𝒪[n] of the projection formula [Stacks, Tag 0944] on a ringed topos — the dévissage from it to a strictly perfect complex is available, and takes that case as a hypothesis — together with the identification of Lf^* of a Koszul complex with a Koszul complex. That is also why part (3) of [Stacks, Tag 099N] is registered here only for a derived-complete object.

This statement also carries [Stacks, Tag 0A0I], Equation 52.7.0.1 Rf_*(ℱ^∧) = (Rf_*ℱ)^∧, which the source justifies by citing Tag 0A0G: what is proved is that ringed-site statement, at a derived-complete object. The display's own setting — a proper morphism of schemes and a coherent module, Section 52.7 — is not formalized here. It also carries part (3) of [Stacks, Tag 099N], with the restrictions named on derivedCompletePushforward.

theorem isIso_derivedCompletionPushforwardComparison_of_isDerivedComplete
    {K : DerivedCategory (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))}
    (hK : IsDerivedComplete.{u, u, u, u} X I' K) :
    IsIso ((derivedCompletionPushforwardComparison f I I' hI).app K)
Sources
LeanAlgebraicGeometry.RingedSite.derivedCompletion_eq_rlim_constantAdicTower · Stacks.ModuleSheaf.exists_leftAdjoint_isDerivedLimitWithProjections_derivedReductionTower · Stacks.ModuleSheaf.isDerivedComplete_iff_isDerivedLimitWithProjections_derivedReductionTower · MorphismOfTopoi.isDerivedComplete_constantDerivedPushforward · MorphismOfTopoi.constantDerivedCompletePullbackPushforwardAdjunction · MorphismOfTopoi.isIso_derivedCompletionComparison_constantDerivedPushforward · MorphismOfTopoi.isDerivedLimit_constantAdicTower_constantDerivedPushforward · MorphismOfTopoi.isDerivedLimit_constantAdicTower_constantDerivedCompletePullback

Section61.21 Derived completion and weakly contractible objects#

Section 61.21 of the Stacks Project, Tag 099P. 1 tag here is carried by 20 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 099Q, a proposition

Tag 099Q in the Stacks Project.

AlgebraicGeometry.RingedSite.isLimit_adicQuotientSystem_iff_of_slicedObjectsSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/AdicCompletionCriterion.lean, line 1059. The attribute's comment: “completion_criterion”.

Ordinary completeness is derived completeness plus separatedness.

theorem isLimit_adicQuotientSystem_iff_of_slicedObjectsSituation
    (X : RingedSite.{u, v, max u v})
    [HasSheafify X.J AddCommGrpCat.{max u v}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{max u v}]
    (hX : Stacks.WeaklyContractible.SlicedObjectsSituation.{w, v, u, max u v} X.C X.J)
    (I : SheafOfModules.Submodule
      (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hI : ∀ U : X.C, hX.B U →
      (I.toSubmodule.obj (op U)).FG)
    (F : SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) :
    Nonempty (IsLimit (Cone.mk F (adicQuotientSystem X I F).quotientMap)) ↔
      AlgebraicGeometry.RingedSite.IsDerivedComplete X I
        ((DerivedCategory.singleFunctor
          (SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj F) ∧
        (⨅ n : ℕ, idealPowerProduct X I F n) = ⊥

AlgebraicGeometry.RingedSite.isLimit_adicQuotientSystem_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/AdicCompletionCriterion.lean, line 1398. The attribute's comment: “completion_criterion”.

Ordinary completeness is derived completeness plus separatedness.

theorem isLimit_adicQuotientSystem_iff
    (X : RingedSite.{u, v, max u v})
    [Small.{v} X.C] [HasSheafify X.J (Type v)]
    [HasSheafify X.J AddCommGrpCat.{max u v}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{max u v}]
    (hX : X.J.HasEnoughWeaklyContractibleObjects)
    (I : SheafOfModules.Submodule
      (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hI : ∀ U : X.C, X.J.IsWeaklyContractible U →
      (I.toSubmodule.obj (op U)).FG)
    (F : SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) :
    Nonempty (IsLimit (Cone.mk F (adicQuotientSystem X I F).quotientMap)) ↔
      AlgebraicGeometry.RingedSite.IsDerivedComplete X I
        ((DerivedCategory.singleFunctor
          (SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj F) ∧
        (⨅ n : ℕ, idealPowerProduct X I F n) = ⊥

AlgebraicGeometry.RingedSite.isLimit_adicQuotientSystem_iff_of_sliceTestingFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/AdicCompletionCriterionSliceTesting.lean, line 741. The attribute's comment: “completion_criterion”.

Ordinary completeness is derived completeness plus separatedness.

theorem isLimit_adicQuotientSystem_iff_of_sliceTestingFamily
    (X : RingedSite.{u, v, max u v w})
    [HasSheafify X.J AddCommGrpCat.{max u v w}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{max u v w}]
    (B : Stacks.WeaklyContractible.SliceTestingFamily.{max u v w} X.C X.J)
    (I : SheafOfModules.Submodule
      (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hI : ∀ U : X.C, B.B U →
      (I.toSubmodule.obj (op U)).FG)
    (F : SheafOfModules.{max u v w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) :
    Nonempty (IsLimit (Cone.mk F (adicQuotientSystemOfSize X I F).quotientMap)) ↔
      AlgebraicGeometry.RingedSite.IsDerivedComplete.{u, v, max u v w, max u v w} X I
        ((DerivedCategory.singleFunctor
          (SheafOfModules.{max u v w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj F) ∧
        (⨅ n : ℕ, idealPowerProductOfSize X I F n) = ⊥

AlgebraicGeometry.RingedSite.isDerivedComplete_iff_homology_of_slicedObjectsSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteCohomology.lean, line 125. The attribute's comment: “cohomology_criterion”.

A complex is derived complete precisely when each cohomology sheaf is.

theorem isDerivedComplete_iff_homology_of_slicedObjectsSituation
    (X : RingedSite.{u, v, max u v})
    [HasSheafify X.J AddCommGrpCat.{max u v}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{max u v}]
    (I : SheafOfModules.Submodule
      (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hJ : Stacks.WeaklyContractible.SlicedObjectsSituation.{w, v, u, max u v} X.C X.J)
    (K : DerivedCategory (SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    AlgebraicGeometry.RingedSite.IsDerivedComplete X I K ↔
      ∀ p : ℤ, AlgebraicGeometry.RingedSite.IsDerivedComplete X I
        ((DerivedCategory.singleFunctor
          (SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj
          ((DerivedCategory.homologyFunctor
            (SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) p).obj K))

AlgebraicGeometry.RingedSite.isDerivedComplete_iff_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteCohomology.lean, line 160. The attribute's comment: “cohomology_criterion”.

A complex is derived complete precisely when each cohomology sheaf is.

theorem isDerivedComplete_iff_homology
    (X : RingedSite.{u, v, max u v})
    [Small.{v} X.C] [HasSheafify X.J (Type v)]
    (I : SheafOfModules.Submodule
      (SheafOfModules.unit ((Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
    (hJ : X.J.HasEnoughWeaklyContractibleObjects)
    (K : DerivedCategory
      (SheafOfModules.{max u v} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O)))) :
    AlgebraicGeometry.RingedSite.IsDerivedComplete X I K ↔
      ∀ p : ℤ, AlgebraicGeometry.RingedSite.IsDerivedComplete X I
        ((DerivedCategory.singleFunctor
          (SheafOfModules.{max u v} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O))) 0).obj
          ((DerivedCategory.homologyFunctor
            (SheafOfModules.{max u v} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O))) p).obj K))

AlgebraicGeometry.RingedSite.isDerivedComplete_iff_homology_of_sliceTestingFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteCohomologySliceTesting.lean, line 52. The attribute's comment: “cohomology_criterion”.

A complex is derived complete precisely when each cohomology sheaf is.

theorem isDerivedComplete_iff_homology_of_sliceTestingFamily
    (X : RingedSite.{u, v, max u v w})
    (I : SheafOfModules.Submodule
      (SheafOfModules.unit ((Stacks.SheafOfModules.Tensor.ringSheaf X.O))))
    (h : Stacks.WeaklyContractible.SliceTestingFamily.{max u v w} X.C X.J)
    (K : DerivedCategory
      (SheafOfModules.{max u v w} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O)))) :
    AlgebraicGeometry.RingedSite.IsDerivedComplete.{u, v, max u v w, max u v w} X I K ↔
      ∀ p : ℤ, AlgebraicGeometry.RingedSite.IsDerivedComplete.{u, v, max u v w, max u v w} X I
        ((DerivedCategory.singleFunctor
          (SheafOfModules.{max u v w} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O))) 0).obj
          ((DerivedCategory.homologyFunctor
            (SheafOfModules.{max u v w} ((Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
            p).obj K))

AlgebraicGeometry.RingedSite.isDerivedComplete_limit_adicQuotientTower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteCompletedStructureSheaf.lean, line 76. The attribute's comment: “completed_structure_sheaf”.

The completion limₙ 𝒪/ℐⁿ of the structure sheaf is derived complete along ℐ. Every term of the tower of adic quotients is derived complete, and an inverse limit of derived-complete sheaves of modules is derived complete.

theorem isDerivedComplete_limit_adicQuotientTower
    (X : RingedSite.{u, u, u}) [Small.{u} X.C] [HasSheafify X.J (Type u)]
    (hX : X.J.HasEnoughWeaklyContractibleObjects)
    (I : SheafOfModules.Submodule
      (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    AlgebraicGeometry.RingedSite.IsDerivedComplete X I
      ((DerivedCategory.singleFunctor
        (SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj
        (limit (adicQuotientTower X I)))

AlgebraicGeometry.RingedSite.isWeakSerreClass_isDerivedComplete_constant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteConstantNoetherian.lean, line 190. The attribute's comment: “(1)”.

[Stacks, Tag 099Q] (1). On a site with enough weakly contractible objects, the derived complete sheaves of Λ-modules form a weak Serre subcategory of Mod(𝒞, Λ).

theorem isWeakSerreClass_isDerivedComplete_constant (hJ : J.HasEnoughWeaklyContractibleObjects)
    (I : Ideal Λ) :
    ObjectProperty.IsWeakSerreClass
      (fun F : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (constant J Λ).O) =>
        IsDerivedComplete (constant J Λ) (constantIdealSheaf J Λ I)
          ((DerivedCategory.singleFunctor _ 0).obj F))

AlgebraicGeometry.RingedSite.isDerivedComplete_limit_constant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteConstantNoetherian.lean, line 202. The attribute's comment: “(4)”.

[Stacks, Tag 099Q] (4). On a site with enough weakly contractible objects, the limit of an inverse system … → ℱ₃ → ℱ₂ → ℱ₁ of derived complete sheaves of Λ-modules is derived complete.

theorem isDerivedComplete_limit_constant (hJ : J.HasEnoughWeaklyContractibleObjects)
    (I : Ideal Λ)
    (F : ℕᵒᵖ ⥤ SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (constant J Λ).O))
    (hF : ∀ n : ℕ, IsDerivedComplete (constant J Λ) (constantIdealSheaf J Λ I)
      ((DerivedCategory.singleFunctor _ 0).obj (F.obj (op n)))) :
    IsDerivedComplete (constant J Λ) (constantIdealSheaf J Λ I)
      ((DerivedCategory.singleFunctor _ 0).obj (limit F))

AlgebraicGeometry.RingedSite.isDerivedComplete_iff_homology_constant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteConstantNoetherian.lean, line 215. The attribute's comment: “(5)”.

[Stacks, Tag 099Q] (5). On a site with enough weakly contractible objects, an object K of D(𝒞, Λ) is derived complete if and only if each cohomology sheaf Hᵖ(K) is derived complete.

theorem isDerivedComplete_iff_homology_constant (hJ : J.HasEnoughWeaklyContractibleObjects)
    (I : Ideal Λ)
    (K : DerivedCategory (SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (constant J Λ).O))) :
    IsDerivedComplete (constant J Λ) (constantIdealSheaf J Λ I) K ↔
      ∀ p : ℤ, IsDerivedComplete (constant J Λ) (constantIdealSheaf J Λ I)
        ((DerivedCategory.singleFunctor _ 0).obj ((DerivedCategory.homologyFunctor _ p).obj K))

AlgebraicGeometry.RingedSite.isLimit_adicQuotientSystem_iff_constant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteConstantNoetherian.lean, line 229. The attribute's comment: “(2)”.

[Stacks, Tag 099Q] (2). On a site with enough weakly contractible objects, a sheaf ℱ of Λ-modules satisfies ℱ = lim ℱ/Iⁿℱ — the maps ℱ ⟶ ℱ/Iⁿℱ form a limit cone — if and only if ℱ is derived complete and ⋂ Iⁿℱ = 0. Only the finite generation of I is used of the Noetherian hypothesis.

theorem isLimit_adicQuotientSystem_iff_constant (hJ : J.HasEnoughWeaklyContractibleObjects)
    {I : Ideal Λ} (hI : I.FG)
    (F : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf (constant J Λ).O)) :
    Nonempty (IsLimit (Cone.mk F
      (adicQuotientSystem (constant J Λ) (constantIdealSheaf J Λ I) F).quotientMap)) ↔
      IsDerivedComplete (constant J Λ) (constantIdealSheaf J Λ I)
        ((DerivedCategory.singleFunctor _ 0).obj F) ∧
        (⨅ n : ℕ, idealPowerProduct (constant J Λ) (constantIdealSheaf J Λ I) F n) = ⊥

AlgebraicGeometry.RingedSite.isDerivedComplete_constantCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteConstantNoetherian.lean, line 244. The attribute's comment: “(3)”.

[Stacks, Tag 099Q] (3). On a site with enough weakly contractible objects, the sheaf Λ̲^∧ = lim (Λ/Iⁿ)̲ is derived complete. Only the finite generation of I is used of the Noetherian hypothesis.

theorem isDerivedComplete_constantCompletion (hJ : J.HasEnoughWeaklyContractibleObjects)
    {I : Ideal Λ} (hI : I.FG) :
    IsDerivedComplete (constant J Λ) (constantIdealSheaf J Λ I)
      ((DerivedCategory.singleFunctor _ 0).obj
        (limit (Stacks.ConstantSheaf.adicQuotientSystem I ⋙ constantModuleFunctor J Λ)))

AlgebraicGeometry.RingedSite.isBoundedAbove_iff_constant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteConstantNoetherian.lean, line 316. The attribute's comment: “(6)”.

[Stacks, Tag 099Q] (6). On a site with enough weakly contractible objects, a derived complete object K of D(𝒞, Λ) is bounded above if and only if K ⊗^𝐋_Λ (Λ/I)̲ is bounded above.

theorem isBoundedAbove_iff_constant [IsNoetherianRing Λ]
    (hJ : J.HasEnoughWeaklyContractibleObjects) (I : Ideal Λ)
    (K : DerivedCategory (SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (constant J Λ).O)))
    (hK : IsDerivedComplete (constant J Λ) (constantIdealSheaf J Λ I) K) :
    Stacks.DerivedCategory.IsBoundedAbove K ↔
      Stacks.DerivedCategory.IsBoundedAbove
        (((Stacks.SheafOfModules.derivedTensorProductFunctor (constant J Λ)).obj K).obj
          ((DerivedCategory.singleFunctor _ 0).obj
            ((constantModuleFunctor J Λ).obj (ModuleCat.of Λ (Λ ⧸ I)))))

AlgebraicGeometry.RingedSite.isBounded_of_hasFiniteTorDimension_constant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteConstantNoetherian.lean, line 364. The attribute's comment: “(7)”.

[Stacks, Tag 099Q] (7). On a site with enough weakly contractible objects, a derived complete object K of D(𝒞, Λ) is bounded if K ⊗^𝐋_Λ Λ/I, as an object of D(𝒞, Λ/I), has finite Tor dimension, for any derived tensor product T₁ on D(𝒞, Λ/I) against which Tor dimension is measured.

theorem isBounded_of_hasFiniteTorDimension_constant [IsNoetherianRing Λ]
    (hJ : J.HasEnoughWeaklyContractibleObjects) (I : Ideal Λ)
    (K : DerivedCategory (SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (constant J Λ).O)))
    (hK : IsDerivedComplete (constant J Λ) (constantIdealSheaf J Λ I) K)
    (T₁ : Stacks.SheafOfModules.DerivedTensorProduct.{u, u, u, u + 1}
      (Stacks.Sites.adicQuotientRingedSite (constant J Λ) (constantIdealSheaf J Λ I) 1))
    (h : HasFiniteTorDimension.{u, u, u, u + 1} T₁
      ((Stacks.Cohomology.derivedCoefficientChange
        (Stacks.Sites.toAdicQuotient (constantIdealSheaf J Λ I) 1)).obj K)) :
    ∃ a b : ℤ, K.IsGE a ∧ K.IsLE b

AlgebraicGeometry.RingedSite.isDerivedComplete_limit_of_slicedObjectsSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteInverseLimit.lean, line 193. The attribute's comment: “inverse_limits, at a sliced situation of testing objects”.

The inverse limit of a countable system of derived-complete sheaves of modules is derived complete, on a ringed site equipped with a covering collection of objects which test surjectivity of sheaves of sets valued in the module universe, on the site and on each of its slices.

The weakly contractible objects enter only through that collection, so the statement reaches a site whose objects outnumber its morphisms — the small pro-étale site of a scheme among them — where weak contractibility cannot be tested at the morphism universe at all.

public theorem isDerivedComplete_limit_of_slicedObjectsSituation
    (X : RingedSite.{u, v, max u v})
    [HasSheafify X.J AddCommGrpCat.{max u v}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{max u v}]
    (hX : Stacks.WeaklyContractible.SlicedObjectsSituation.{w, v, u, max u v}
      X.C X.J)
    (I : SheafOfModules.Submodule
      (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (F : ℕᵒᵖ ⥤ SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    (hF : ∀ n : ℕ, AlgebraicGeometry.RingedSite.IsDerivedComplete X I
      ((DerivedCategory.singleFunctor
        (SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj
        (F.obj ⟨n⟩))) :
    AlgebraicGeometry.RingedSite.IsDerivedComplete X I
      ((DerivedCategory.singleFunctor
        (SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj
        (limit F))

AlgebraicGeometry.RingedSite.isDerivedComplete_limit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteInverseLimit.lean, line 264. The attribute's comment: “inverse_limits”.

The inverse limit of a countable system of derived-complete sheaves is derived complete.

public theorem isDerivedComplete_limit
    (X : RingedSite.{u, v, max u v})
    [Small.{v} X.C] [HasSheafify X.J (Type v)]
    (hX : X.J.HasEnoughWeaklyContractibleObjects)
    (I : SheafOfModules.Submodule
      (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (F : ℕᵒᵖ ⥤ SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    (hF : ∀ n : ℕ, AlgebraicGeometry.RingedSite.IsDerivedComplete X I
      ((DerivedCategory.singleFunctor
        (SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj
        (F.obj ⟨n⟩))) :
    AlgebraicGeometry.RingedSite.IsDerivedComplete X I
      ((DerivedCategory.singleFunctor
        (SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj
        (limit F))

AlgebraicGeometry.RingedSite.isDerivedComplete_limit_of_sliceTestingFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteInverseLimitSliceTesting.lean, line 64. The attribute's comment: “inverse_limits”.

The inverse limit of a countable system of derived-complete sheaves is derived complete, on a ringed site with a slice testing family of weakly contractible objects at the universe of the module sections.

public theorem isDerivedComplete_limit_of_sliceTestingFamily
    (X : RingedSite.{u, v, max u v w})
    (B : Stacks.WeaklyContractible.SliceTestingFamily.{max u v w} X.C X.J)
    (I : SheafOfModules.Submodule
      (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (F : ℕᵒᵖ ⥤ SheafOfModules.{max u v w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    (hF : ∀ n : ℕ, AlgebraicGeometry.RingedSite.IsDerivedComplete.{u, v, max u v w, max u v w} X I
      ((DerivedCategory.singleFunctor
        (SheafOfModules.{max u v w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj
        (F.obj ⟨n⟩))) :
    AlgebraicGeometry.RingedSite.IsDerivedComplete.{u, v, max u v w, max u v w} X I
      ((DerivedCategory.singleFunctor
        (SheafOfModules.{max u v w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj
        (limit F))

AlgebraicGeometry.RingedSite.derivedCompleteSheaves_isWeakSerreClass_of_slicedObjectsSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteWeakSerre.lean, line 56. The attribute's comment: “weak_serre”.

Derived-complete sheaves of modules form a weak Serre subcategory on a site with enough weakly contractible objects.

theorem derivedCompleteSheaves_isWeakSerreClass_of_slicedObjectsSituation
    (X : RingedSite.{u, v, max u v})
    [HasSheafify X.J AddCommGrpCat.{max u v}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{max u v}]
    (hX : Stacks.WeaklyContractible.SlicedObjectsSituation.{w, v, u, max u v} X.C X.J)
    (I : SheafOfModules.Submodule
      (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    ObjectProperty.IsWeakSerreClass
      (fun F : SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O) =>
        AlgebraicGeometry.RingedSite.IsDerivedComplete X I
          ((DerivedCategory.singleFunctor
            (SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj F))

AlgebraicGeometry.RingedSite.derivedCompleteSheaves_isWeakSerreClass, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteWeakSerre.lean, line 215. The attribute's comment: “weak_serre”.

Derived-complete sheaves of modules form a weak Serre subcategory on a site with enough weakly contractible objects.

theorem derivedCompleteSheaves_isWeakSerreClass
    (X : RingedSite.{u, v, max u v})
    [Small.{v} X.C]
    [HasSheafify X.J (Type v)]
    [HasSheafify X.J AddCommGrpCat.{max u v}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{max u v}]
    (hX : X.J.HasEnoughWeaklyContractibleObjects)
    (I : SheafOfModules.Submodule
      (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    ObjectProperty.IsWeakSerreClass
      (fun F : SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O) =>
        AlgebraicGeometry.RingedSite.IsDerivedComplete X I
          ((DerivedCategory.singleFunctor
            (SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
            0).obj F))

AlgebraicGeometry.RingedSite.derivedCompleteSheaves_isWeakSerreClass_of_sliceTestingFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteWeakSerreSliceTesting.lean, line 69. The attribute's comment: “weak_serre”.

Derived-complete sheaves of modules form a weak Serre subcategory on a site with enough weakly contractible objects.

theorem derivedCompleteSheaves_isWeakSerreClass_of_sliceTestingFamily
    (X : RingedSite.{u, v, max u v w})
    [HasSheafify X.J AddCommGrpCat.{max u v w}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{max u v w}]
    (B : Stacks.WeaklyContractible.SliceTestingFamily.{max u v w} X.C X.J)
    (I : SheafOfModules.Submodule
      (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf X.O))) :
    ObjectProperty.IsWeakSerreClass
      (fun F : SheafOfModules.{max u v w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O) =>
        AlgebraicGeometry.RingedSite.IsDerivedComplete.{u, v, max u v w, max u v w} X I
          ((DerivedCategory.singleFunctor
            (SheafOfModules.{max u v w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj
              F))
Sources
LeanAlgebraicGeometry.RingedSite.isLimit_adicQuotientSystem_iff_of_slicedObjectsSituation · AlgebraicGeometry.RingedSite.isLimit_adicQuotientSystem_iff · AlgebraicGeometry.RingedSite.isLimit_adicQuotientSystem_iff_of_sliceTestingFamily · AlgebraicGeometry.RingedSite.isDerivedComplete_iff_homology_of_slicedObjectsSituation · AlgebraicGeometry.RingedSite.isDerivedComplete_iff_homology · AlgebraicGeometry.RingedSite.isDerivedComplete_iff_homology_of_sliceTestingFamily · AlgebraicGeometry.RingedSite.isDerivedComplete_limit_adicQuotientTower · AlgebraicGeometry.RingedSite.isWeakSerreClass_isDerivedComplete_constant

Section61.22 Cohomology of a point#

Section 61.22 of the Stacks Project, Tag 09B3. 1 tag here is carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09B4, a lemma

Tag 09B4 in the Stacks Project.

AlgebraicGeometry.GaloisSheaf.profiniteSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/CompletedGaloisSheaf.lean, line 207. The attribute's comment: “case (1): the canonical sheaf of a profinite abelian group”.

The canonical pro-étale sheaf M^∧ attached to a profinite abelian group M with continuous action of the absolute Galois group of a field: the inverse limit of the pro-étale pullbacks of the locally constant étale sheaves of the discrete quotients M/N by the open Galois-stable subgroups N.

def profiniteSheaf (K : Type u) [Field K] (M : Type w) [AddCommGroup M] [TopologicalSpace M]
    [IsTopologicalAddGroup M] [CompactSpace M] [T2Space M] [TotallyDisconnectedSpace M]
    (ρ : Representation ℤ (galoisGroup K) M)
    (_hρ : Continuous fun p : galoisGroup K × M ↦ ρ p.1 p.2) :
    Sheaf (Scheme.ProEt.topology (base K)) (ModuleCat.{max (u + 1) w} ℤ)

AlgebraicGeometry.GaloisSheaf.adicSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/CompletedGaloisSheaf.lean, line 237. The attribute's comment: “case (2): the canonical sheaf of an adically complete module”.

The canonical pro-étale sheaf M^∧ attached to an I-adically complete module M over a Noetherian ring, with continuous action of the absolute Galois group of a field for the I-adic topology: the inverse limit of the pro-étale pullbacks of the locally constant étale sheaves of the discrete quotients M/IⁿM.

def adicSheaf (K : Type u) [Field K] [IsNoetherianRing Λ] (I : Ideal Λ) (M : Type w)
    [AddCommGroup M] [Module Λ M] [IsAdicComplete I M]
    (ρ : Representation Λ (galoisGroup K) M)
    (_hρ : letI : TopologicalSpace M := I.adicModuleTopology M
      Continuous fun p : galoisGroup K × M ↦ ρ p.1 p.2) :
    Sheaf (Scheme.ProEt.topology (base K)) (ModuleCat.{max (u + 1) r w} Λ)

AlgebraicGeometry.GaloisSheaf.rightDerivedAdicSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ContinuousGaloisCohomology.lean, line 317. The attribute's comment: “case (2), the cohomology comparison”.

Let K be a field with absolute Galois group G, let Λ be a Noetherian ring with an ideal I, and let M be an I-adically complete Λ-module with a continuous action of G for the I-adic topology. Then the pro-étale cohomology of Spec K with coefficients in the completed sheaf M^∧ = limₙ ε⁻¹(M/IⁿM) is the continuous cohomology of G with coefficients in M:

Hⁱ(Spec(K)_proét, M^∧) ≅ Hⁱ_cont(G, M).

Here Λ and M carry their I-adic topologies, pro-étale cohomology is the i-th right derived functor of global sections of the underlying abelian sheaf, and the identification is of abelian groups, the right hand side being lifted to the coefficient universe of the site.

def rightDerivedAdicSheafIso
    (ρ : Representation Λ (galoisGroup K) M)
    (hρ : letI := I.adicModuleTopology M
      Continuous fun p : galoisGroup K × M ↦ ρ p.1 p.2) (i : ℕ) :
    letI : TopologicalSpace Λ := I.adicTopology
    letI := I.adicModuleTopology M
    letI := hasSheafify_galois.{u, r, w} K
    letI := enoughInjectives_galois.{u, r, w} K
    letI := Stacks.Cohomology.GlobalSections.additive_Γ.{max r w, u, u + 1}
      (Scheme.ProEt.topology (base K))
    ((Sheaf.Γ (Scheme.ProEt.topology (base K)) AddCommGrpCat.{max (u + 1) r w}).rightDerived i).obj
      ((sheafCompose _ (forget₂ (ModuleCat.{max (u + 1) r w} Λ) AddCommGrpCat)).obj
        (adicSheaf Λ K I M ρ hρ)) ≅
      (underlyingAb.{u, r, w} Λ).obj (continuousCohomology i (uliftRep.{u} ρ hρ))

AlgebraicGeometry.GaloisSheaf.rightDerivedProfiniteSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ContinuousGaloisCohomology.lean, line 432. The attribute's comment: “case (1), the cohomology comparison”.

Let K be a field with absolute Galois group G and let M be a profinite abelian group with a continuous action of G. Then the pro-étale cohomology of Spec K with coefficients in the completed sheaf M^∧ = lim_N ε⁻¹(M/N), the limit over the open G-stable subgroups N, is the continuous cohomology of G with coefficients in M:

Hⁱ(Spec(K)_proét, M^∧) ≅ Hⁱ_cont(G, M).

Pro-étale cohomology is the i-th right derived functor of global sections of the underlying abelian sheaf, and the identification is of abelian groups, the right hand side being lifted to the coefficient universe of the site.

def rightDerivedProfiniteSheafIso (i : ℕ) :
    letI := hasSheafify_galois.{u, 0, w} K
    letI := enoughInjectives_galois.{u, 0, w} K
    letI := Stacks.Cohomology.GlobalSections.additive_Γ.{max 0 w, u, u + 1}
      (Scheme.ProEt.topology (base K))
    ((Sheaf.Γ (Scheme.ProEt.topology (base K)) AddCommGrpCat.{max (u + 1) w}).rightDerived i).obj
      ((sheafCompose _ (forget₂ (ModuleCat.{max (u + 1) w} ℤ) AddCommGrpCat)).obj
        (profiniteSheaf K M ρ hρ)) ≅
      (underlyingAb.{u, 0, w} ℤ).obj (continuousCohomology i (uliftRep.{u} ρ hρ))

AlgebraicGeometry.GaloisSheaf.rightDerivedAdicSheafLinearEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ContinuousGaloisCohomologyLinear.lean, line 371. The attribute's comment: “case (2), as Λ-modules”.

Stacks Project, Tag 09B4, case (2), as Λ-modules. In the situation of rightDerivedAdicSheafIso, the pro-étale cohomology Hⁱ(Spec(K)_proét, M^∧), a Λ-module through the action of Λ on M^∧, is isomorphic as a Λ-module to the continuous cohomology Hⁱ_cont(G, M), by the identification rightDerivedAdicSheafIso.

def rightDerivedAdicSheafLinearEquiv
    (ρ : Representation Λ (galoisGroup K) M)
    (hρ : letI := I.adicModuleTopology M
      Continuous fun p : galoisGroup K × M ↦ ρ p.1 p.2) (i : ℕ) :
    letI : TopologicalSpace Λ := I.adicTopology
    letI := I.adicModuleTopology M
    rightDerivedAdicSheafModule K Λ I M ρ hρ i ≃ₗ[Λ]
      ULift.{max (u + 1) r} (continuousCohomology i (uliftRep.{u} ρ hρ))
Sources
LeanAlgebraicGeometry.GaloisSheaf.profiniteSheaf · AlgebraicGeometry.GaloisSheaf.adicSheaf · AlgebraicGeometry.GaloisSheaf.rightDerivedAdicSheafIso · AlgebraicGeometry.GaloisSheaf.rightDerivedProfiniteSheafIso · AlgebraicGeometry.GaloisSheaf.rightDerivedAdicSheafLinearEquiv

Section61.23 Functoriality of the pro-étale site#

Section 61.23 of the Stacks Project, Tag 09A5. 1 tag here is carried by 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09A6, a lemma

Tag 09A6 in the Stacks Project.

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.Scheme.proetaleDirectImageEtaleInverseImageIso · AlgebraicGeometry.ProEtale.proetaleDirectImageRightDerivedEpsilonInverseImageIso

Section61.24 Finite morphisms and pro-étale sites#

Section 61.24 of the Stacks Project, Tag 09A7. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09A8, a lemma

Tag 09A8 in the Stacks Project.

AlgebraicGeometry.ProEtale.exact_smallProetalePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/SiteFunctoriality/FinitePushforwardExact.lean, line 90.

Stacks 09A8. For a finite morphism of schemes which is locally of finite presentation, direct image of abelian sheaves along the induced morphism of small pro-étale sites is exact.

theorem exact_smallProetalePushforward
    [IsFinite (B.inclusion.map f)] [LocallyOfFinitePresentation (B.inclusion.map f)] :
    exactFunctor
      (Sheaf (SmallProetale.topology B Z.obj Z.property) AddCommGrpCat.{u + 1})
      (Sheaf (SmallProetale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
      ((smallProetaleBaseChange B Z X f).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
        (SmallProetale.topology B X.obj X.property)
        (SmallProetale.topology B Z.obj Z.property))
Sources
LeanAlgebraicGeometry.ProEtale.exact_smallProetalePushforward

Section61.25 Closed immersions and pro-étale sites#

Section 61.25 of the Stacks Project, Tag 09A9. 6 tags here are carried by 55 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09BK, a lemma

Tag 09BK in the Stacks Project.

AlgebraicGeometry.ProEtale.appBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/AppProetaleSite.lean, line 223. The attribute's comment: “the base-change functor”.

The functor u: pro-étale base change along a morphism of affine schemes i : Z ⟶ X, as a functor X_app ⥤ Z_app between the affine ind-étale sites. On underlying schemes it is U ↦ U ×_X Z.

public noncomputable def appBaseChange {Z X : Scheme.{u}} [IsAffine X] [IsAffine Z]
    (i : Z ⟶ X) : AppProetale X ⥤ AppProetale Z

AlgebraicGeometry.ProEtale.appProetaleBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/AppSiteClosedImmersion.lean, line 428. The attribute's comment: “the base change functor”.

The base change functor. For a morphism i : Z ⟶ X of affine schemes, pulling back along i carries an affine object of the small pro-étale site of X with ind-étale ring of global sections to one over Z, giving a functor X_app ⥤ Z_app, U ↦ U ×_X Z.

public noncomputable def appProetaleBaseChange : AppSmallProetale X ⥤ AppSmallProetale Z

AlgebraicGeometry.ProEtale.isClosedImmersion_pullback_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/AppSiteClosedImmersion.lean, line 489. The attribute's comment: “the closed immersion V → v(V)”.

The closed immersion V → v(V). The first projection of the fibre product U ×_X Z is a closed immersion, being the base change of i; combined with the identification of V with v(V) ×_X Z this exhibits V → v(V) as a closed immersion.

public theorem isClosedImmersion_pullback_fst (U : AppSmallProetale X) :
    IsClosedImmersion (pullback.fst U.obj.hom i)

AlgebraicGeometry.ProEtale.appProetaleLift, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/AppSiteClosedImmersion.lean, line 506. The attribute's comment: “the left adjoint”.

The left adjoint v of base change. For a closed immersion i : Z ⟶ X of affine schemes, the lift of an object of Z_app to X_app: it is the right-adjoint lift of Stacks 097P on ind-étale algebras, read through the identification of each site with the opposite of a category of ind-étale algebras.

public noncomputable def appProetaleLift : AppSmallProetale Z ⥤ AppSmallProetale X

AlgebraicGeometry.ProEtale.appProetaleBaseChange_hasLeftAdjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/AppSiteClosedImmersion.lean, line 514. The attribute's comment: “the adjunction”.

The adjunction. The base change functor U ↦ U ×_X Z along a closed immersion of affine schemes has a left adjoint.

public theorem appProetaleBaseChange_hasLeftAdjoint :
    Nonempty (appProetaleLift i ⊣ appProetaleBaseChange i)

AlgebraicGeometry.ProEtale.appProetaleLift_fullyFaithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/AppSiteClosedImmersion.lean, line 523. The attribute's comment: “full faithfulness of the left adjoint”.

Full faithfulness of the left adjoint.

public theorem appProetaleLift_fullyFaithful :
    Nonempty (appProetaleLift i).FullyFaithful

AlgebraicGeometry.ProEtale.appProetaleLift_baseChangeIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/AppSiteClosedImmersion.lean, line 533. The attribute's comment: “the identification of V with u(v(V))”.

The identification of V with u(v(V)). For V in Z_app the unit of the adjunction identifies V with the fibre product v(V) ×_X Z.

public theorem appProetaleLift_baseChangeIso :
    Nonempty (𝟭 (AppSmallProetale Z) ≅ appProetaleLift i ⋙ appProetaleBaseChange i)

AlgebraicGeometry.ProEtale.appProetaleBaseChange_isCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/AppSiteContinuous.lean, line 73. The attribute's comment: “the base change functor is continuous”.

Stacks 09BK, continuity of the base change functor: coverings. For a morphism i : Z ⟶ X of affine schemes, the base change functor U ↦ U ×_X Z from X_app to Z_app carries a standard pro-étale covering family to a standard pro-étale covering family.

public theorem appProetaleBaseChange_isCovering {X Z : Scheme.{u}} [IsAffine X] [IsAffine Z]
    (i : Z ⟶ X) {U : AppSmallProetale X} (E : PreZeroHypercover.{u + 1} U)
    (hE : AppSmallProetale.IsCovering X ⟨U, E⟩) :
    AppSmallProetale.IsCovering Z
      ⟨(appProetaleBaseChange i).obj U, E.map (appProetaleBaseChange i)⟩

AlgebraicGeometry.ProEtale.appProetaleLift_isCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/AppSiteContinuous.lean, line 103. The attribute's comment: “the functor v is cocontinuous”.

Stacks 09BK, cocontinuity of the left adjoint. For a closed immersion i : Z ⟶ X of affine schemes the left adjoint v : Z_app ⥤ X_app of the base change functor is cocontinuous: it pulls covering sieves back to covering sieves.

public theorem appProetaleLift_isCocontinuous {X Z : Scheme.{u}} (i : Z ⟶ X)
    [IsClosedImmersion i] [IsAffine X] [IsAffine Z] :
    (appProetaleLift i).IsCocontinuous (AppSmallProetale.topology Z)
      (AppSmallProetale.topology X)

AlgebraicGeometry.ProEtale.appProetaleBaseChange_preservesPullbacks, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/AppSitePullback.lean, line 190. The attribute's comment: “the base change functor is continuous”.

Stacks 09BK, continuity of the base change functor: fibre products. For a morphism i : Z ⟶ X of affine schemes the functor U ↦ U ×_X Z from X_app to Z_app preserves fibre products, which is the second half of continuity in the sense of the Stacks Project.

public noncomputable instance appProetaleBaseChange_preservesPullbacks {X Z : Scheme.{u}}
    [IsAffine X] [IsAffine Z] (i : Z ⟶ X) :
    PreservesLimitsOfShape WalkingCospan (appProetaleBaseChange i)

AlgebraicGeometry.ProEtale.indEtaleQuotientLift_exists_specializes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/AppSiteSpecialization.lean, line 72. The attribute's comment: “every point of v(V) specialises to a point of V”.

Stacks 09BK, specialization to a point of V. Let A be a ring, I ⊆ A an ideal and V an ind-étale A ⧸ I-algebra. Writing C for the lift of V to an ind-étale A-algebra, so that v(V) = Spec C and V = Spec (C ⧸ I C) is the closed subscheme of v(V) cut out by the ideal generated by the image of I, every point of v(V) specializes to a point of V.

public theorem indEtaleQuotientLift_exists_specializes (A : Type u) [CommRing A] (I : Ideal A)
    (V : IndEtaleAlgebra (A ⧸ I))
    (p : PrimeSpectrum ((indEtaleQuotientLift A I).obj V).obj.right) :
    ∃ q : PrimeSpectrum ((indEtaleQuotientLift A I).obj V).obj.right, p ⤳ q ∧
      I.map ((indEtaleQuotientLift A I).obj V).obj.hom.hom ≤ q.asIdeal

AlgebraicGeometry.ProEtale.affineIndEtaleBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/SiteFunctoriality/AffineIndEtaleLift.lean, line 517. The attribute's comment: “the base-change functor”.

Pullback along a morphism of the base, on affine ind-étale pro-étale sites.

public noncomputable def affineIndEtaleBaseChange (i : Z ⟶ X)
    [IsAffine X.obj] [IsAffine Z.obj] :
    AffineIndEtaleProetale B X ⥤ AffineIndEtaleProetale B Z

AlgebraicGeometry.ProEtale.affineIndEtaleBaseChange_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/SiteFunctoriality/AffineIndEtaleLift.lean, line 614.

Base change on the affine ind-étale sites is continuous.

public instance affineIndEtaleBaseChange_isContinuous (i : Z ⟶ X)
    [IsAffine X.obj] [IsAffine Z.obj] :
    (affineIndEtaleBaseChange B i).IsContinuous (AffineIndEtaleProetale.topology B X)
      (AffineIndEtaleProetale.topology B Z)

AlgebraicGeometry.ProEtale.affineIndEtaleBaseChange_comp_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/SiteFunctoriality/AffineIndEtaleLift.lean, line 963. The attribute's comment: “the base-change comparison”.

On underlying schemes, affine ind-étale base change is ordinary fibre product.

public theorem affineIndEtaleBaseChange_comp_forget :
    Nonempty ((affineIndEtaleBaseChange B i ⋙ AffineIndEtaleProetale.inclusion B Z ⋙
      SmallProetale.inclusion B Z.obj Z.property) ≅
      (AffineIndEtaleProetale.inclusion B X ⋙ SmallProetale.inclusion B X.obj X.property ⋙
        Over.pullback i))

AlgebraicGeometry.ProEtale.affineIndEtaleLift_adj_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/SiteFunctoriality/AffineIndEtaleLift.lean, line 1697.

The lift is left adjoint to base change.

public theorem affineIndEtaleLift_adj_baseChange :
    Nonempty (affineIndEtaleLift B i ⊣ affineIndEtaleBaseChange B i)

AlgebraicGeometry.ProEtale.closedFiberInclusion_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/SiteFunctoriality/AffineIndEtaleLift.lean, line 1806.

The natural inclusion identifies an object with the closed fibre of its lift.

public theorem closedFiberInclusion_isPullback
    (V : AffineIndEtaleProetale B Z) :
    IsPullback ((closedFiberInclusion B i).app V) (B.inclusion.map V.obj.obj.hom)
      (B.inclusion.map ((affineIndEtaleLift B i).obj V).obj.obj.hom) (B.inclusion.map i)

AlgebraicGeometry.ProEtale.affineIndEtaleLift_baseChangeIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/SiteFunctoriality/AffineIndEtaleLift.lean, line 1936.

Base change of the lift is canonically the original object, naturally in that object.

public theorem affineIndEtaleLift_baseChangeIso :
    Nonempty (affineIndEtaleLift B i ⋙ affineIndEtaleBaseChange B i ≅
      𝟭 (AffineIndEtaleProetale B Z))

AlgebraicGeometry.ProEtale.affineIndEtaleLift_fullyFaithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/SiteFunctoriality/AffineIndEtaleLift.lean, line 2048.

The left-adjoint lift is fully faithful.

public theorem affineIndEtaleLift_fullyFaithful :
    Nonempty (affineIndEtaleLift B i).FullyFaithful

AlgebraicGeometry.ProEtale.closedFiberInclusion_isClosedImmersion, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/SiteFunctoriality/AffineIndEtaleLift.lean, line 2058.

The natural map from an object to its lift is a closed immersion.

public instance closedFiberInclusion_isClosedImmersion
    (V : AffineIndEtaleProetale B Z) :
    IsClosedImmersion ((closedFiberInclusion B i).app V)

AlgebraicGeometry.ProEtale.exists_specialization_closedFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/SiteFunctoriality/AffineIndEtaleLift.lean, line 2083.

Every point of the lift specializes to a point of its closed fibre.

public theorem exists_specialization_closedFiber
    (V : AffineIndEtaleProetale B Z)
    (x : ((affineIndEtaleLift B i).obj V).obj.obj.left.obj) :
    ∃ z : V.obj.obj.left.obj,
      x ⤳ ((closedFiberInclusion B i).app V).base z

AlgebraicGeometry.ProEtale.affineIndEtaleLift_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/SiteFunctoriality/AffineIndEtaleLift.lean, line 2124.

The lift is cocontinuous for the affine ind-étale topologies.

public instance affineIndEtaleLift_isCocontinuous :
    (affineIndEtaleLift B i).IsCocontinuous (AffineIndEtaleProetale.topology B Z)
      (AffineIndEtaleProetale.topology B X)

AlgebraicGeometry.ProEtale.affineIndEtaleLift_isCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/SiteFunctoriality/AffineIndEtaleLift.lean, line 2133.

The lift takes finite standard pro-étale coverings to such coverings.

public theorem affineIndEtaleLift_isCovering
    (E : Covering (AffineIndEtaleProetale B Z))
    (hE : AffineIndEtaleProetale.IsCovering B Z E) :
    AffineIndEtaleProetale.IsCovering B X
      ⟨(affineIndEtaleLift B i).obj E.1, E.2.map (affineIndEtaleLift B i)⟩
Tag 09BL, a lemma

Tag 09BL in the Stacks Project.

AlgebraicGeometry.ProEtale.abelianSmallProetalePushforward_fullyFaithful, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/AbelianLowerShriek.lean, line 262. The attribute's comment: “(6), full faithfulness of the direct image i_* on abelian sheaves, for the small pro-etale sites of a closed immersion of affine objects of a chosen big pro-etale site”.

Stacks 09BL (6) for the direct image on abelian sheaves. For a closed immersion of affine schemes the direct image i_* on abelian sheaves on the small pro-étale sites is fully faithful.

def abelianSmallProetalePushforward_fullyFaithful :
    ((smallProetaleBaseChange B Z X i).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
      (SmallProetale.topology B X.obj X.property)
      (SmallProetale.topology B Z.obj Z.property)).FullyFaithful

AlgebraicGeometry.ProEtale.abelianSmallProetale_isIso_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/AbelianLowerShriek.lean, line 290. The attribute's comment: “(5), the map i^{-1} i_* -> id is an isomorphism on abelian sheaves, for the small pro-etale sites of a closed immersion of affine objects of a chosen big pro-etale site”.

Stacks 09BL (5) for the direct image on abelian sheaves. For a closed immersion of affine schemes the counit i^{-1} i_* ⟶ id on abelian sheaves on the small pro-étale sites is an isomorphism, its right adjoint i_* being fully faithful.

theorem abelianSmallProetale_isIso_counit :
    IsIso (Functor.sheafPullbackConstruction.sheafAdjunctionContinuous
      (smallProetaleBaseChange B Z X i) AddCommGrpCat.{u + 1}
      (SmallProetale.topology B X.obj X.property)
      (SmallProetale.topology B Z.obj Z.property)).counit

AlgebraicGeometry.ProEtale.isRightAdjoint_abelianSmallProetaleSheafPullback, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/AbelianLowerShriek.lean, line 332. The attribute's comment: “(4), the inverse image i^{-1} : Ab(X_proetale) -> Ab(Z_proetale) of a closed immersion of affine objects of a chosen big pro-etale site has a left adjoint i_!”.

Stacks 09BL (4). The inverse image i^{-1} on abelian sheaves on the small pro-étale sites of a closed immersion of affine schemes has a left adjoint i_!.

instance isRightAdjoint_abelianSmallProetaleSheafPullback :
    (Functor.sheafPullbackConstruction.sheafPullback (smallProetaleBaseChange B Z X i)
      AddCommGrpCat.{u + 1} (SmallProetale.topology B X.obj X.property)
      (SmallProetale.topology B Z.obj Z.property)).IsRightAdjoint

AlgebraicGeometry.ProEtale.abelianSmallProetaleLowerShriek_unit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/AbelianLowerShriek.lean, line 380. The attribute's comment: “(5), the map id -> i^{-1} i_! is an isomorphism, for abelian sheaves on the small pro-etale sites of a closed immersion of affine objects of a chosen big pro-etale site”.

Stacks 09BL (5), the unit of lower shriek on abelian sheaves. For a closed immersion of affine schemes the unit id ⟶ i^{-1} i_! of the adjunction i_! ⊣ i^{-1} on abelian sheaves on the small pro-étale sites is an isomorphism.

In the adjoint triple i_! ⊣ i^{-1} ⊣ i_* the unit of the left adjunction is invertible exactly when the counit of the right one is, and the latter is abelianSmallProetale_isIso_counit.

theorem abelianSmallProetaleLowerShriek_unit_isIso :
    IsIso (abelianSmallProetaleLowerShriekAdjunction B i).unit

AlgebraicGeometry.ProEtale.abelianSmallProetaleLowerShriek_fullyFaithful, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/AbelianLowerShriek.lean, line 390. The attribute's comment: “(6), full faithfulness of i_!, for abelian sheaves on the small pro-etale sites of a closed immersion of affine objects of a chosen big pro-etale site”.

Stacks 09BL (6) for lower shriek on abelian sheaves. For a closed immersion of affine schemes the left adjoint i_! of the inverse image on abelian sheaves on the small pro-étale sites is fully faithful.

def abelianSmallProetaleLowerShriek_fullyFaithful :
    (abelianSmallProetaleLowerShriek B i).FullyFaithful

AlgebraicGeometry.ProEtale.affineIndEtalePushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/ClosedImmersion.lean, line 69. The attribute's comment: “topos_identification”.

Stacks 09BL. The direct image of the small pro-étale morphism of a closed immersion of affine schemes, read through the restriction equivalences to the affine ind-étale sites, is the direct image attached to the cocontinuous lift.

def affineIndEtalePushforwardIso :
    (smallProetaleMorphism B Z X i).pushforward ⋙
      (AffineIndEtaleProetale.inclusion B X).sheafPushforwardContinuous (Type (u + 1))
        (AffineIndEtaleProetale.topology B X) (SmallProetale.topology B X.obj X.property) ≅
    (AffineIndEtaleProetale.inclusion B Z).sheafPushforwardContinuous (Type (u + 1))
        (AffineIndEtaleProetale.topology B Z) (SmallProetale.topology B Z.obj Z.property) ⋙
      (affineIndEtaleLift B i).sheafPushforwardCocontinuous (Type (u + 1))
        (AffineIndEtaleProetale.topology B Z) (AffineIndEtaleProetale.topology B X)

AlgebraicGeometry.ProEtale.smallProetaleMorphism_counit_isIso_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/ClosedImmersion.lean, line 158. The attribute's comment: “pushforward_counit”.

Stacks 09BL. For a closed immersion of affine schemes, the counit i^{-1} i_* → id of the small pro-étale adjunction is an isomorphism.

theorem smallProetaleMorphism_counit_isIso_of_isAffine :
    IsIso (smallProetaleMorphism B Z X i).adj.counit

AlgebraicGeometry.ProEtale.proetaleInverseImage_sheafify_affineIndEtaleLift, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/ClosedImmersion.lean, line 170. The attribute's comment: “inverse_image_formula”.

Stacks 09BL. For a closed immersion of affine schemes, the inverse image of a small pro-étale sheaf, restricted to the affine ind-étale site of Z, is the sheafification of the presheaf of its values on the lift, naturally in the sheaf.

def proetaleInverseImage_sheafify_affineIndEtaleLift :
    (smallProetaleMorphism B Z X i).inverseImage ⋙
        (AffineIndEtaleProetale.inclusion B Z).sheafPushforwardContinuous (Type (u + 1))
          (AffineIndEtaleProetale.topology B Z) (SmallProetale.topology B Z.obj Z.property) ≅
      sheafToPresheaf (SmallProetale.topology B X.obj X.property) (Type (u + 1)) ⋙
        (Functor.whiskeringLeft (AffineIndEtaleProetale B Z)ᵒᵖ
          (SmallProetale B X.obj X.property)ᵒᵖ (Type (u + 1))).obj
            (affineIndEtaleLift B i ⋙ AffineIndEtaleProetale.inclusion B X).op ⋙
        presheafToSheaf (AffineIndEtaleProetale.topology B Z) (Type (u + 1))

AlgebraicGeometry.ProEtale.isRightAdjoint_smallProetaleMorphism_inverseImage, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/LowerShriek.lean, line 220. The attribute's comment: “(3), the inverse image i^{-1} : Sh(X_proetale) -> Sh(Z_proetale) of a closed immersion of affine objects of a chosen big pro-etale site has a left adjoint i^{Sh}_!”.

Stacks 09BL (3). The inverse image i^{-1} on small pro-étale sheaves of sets of a closed immersion of affine schemes has a left adjoint i^{Sh}_!.

instance isRightAdjoint_smallProetaleMorphism_inverseImage :
    (smallProetaleMorphism B Z X i).inverseImage.IsRightAdjoint

AlgebraicGeometry.ProEtale.smallProetaleLowerShriek_unit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/LowerShriek.lean, line 270. The attribute's comment: “(5), the map id -> i^{-1} i^{Sh}_! is an isomorphism, for sheaves of sets on the small pro-etale sites of a closed immersion of affine objects of a chosen big pro-etale site”.

Stacks 09BL (5), the unit of lower shriek. For a closed immersion of affine schemes the unit id ⟶ i^{-1} i^{Sh}_! of the adjunction i^{Sh}_! ⊣ i^{-1} on small pro-étale sheaves of sets is an isomorphism.

In an adjoint triple i^{Sh}_! ⊣ i^{-1} ⊣ i_* the unit of the left adjunction is invertible exactly when the counit of the right one is, and the latter is Stacks 09BL (5) for i^{-1}i_*.

theorem smallProetaleLowerShriek_unit_isIso :
    IsIso (smallProetaleLowerShriekAdjunction B i).unit

AlgebraicGeometry.ProEtale.smallProetaleLowerShriek_fullyFaithful, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/LowerShriek.lean, line 279. The attribute's comment: “(6), full faithfulness of i^{Sh}_!, for sheaves of sets on the small pro-etale sites of a closed immersion of affine objects of a chosen big pro-etale site”.

Stacks 09BL (6) for lower shriek. For a closed immersion of affine schemes the left adjoint i^{Sh}_! of the inverse image on small pro-étale sheaves of sets is fully faithful.

def smallProetaleLowerShriek_fullyFaithful :
    (smallProetaleLowerShriek B i).FullyFaithful

AlgebraicGeometry.ProEtale.proetaleInverseImage_sections_iso_affineIndEtaleLift, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/WeaklyContractible.lean, line 575. The attribute's comment: “weakly_contractible_evaluation”.

At a weakly contractible affine ind-étale object of the closed fibre, inverse image is evaluation at its lift, naturally in the sheaf.

def proetaleInverseImage_sections_iso_affineIndEtaleLift (V : AffineIndEtaleProetale B Z)
    (hV : (AffineIndEtaleProetale.topology B Z).IsWeaklyContractible V) :
    Functor.sheafPullbackConstruction.sheafPullback (smallProetaleBaseChange B Z X i)
        (Type (max (u + 1) v)) (SmallProetale.topology B X.obj X.property)
        (SmallProetale.topology B Z.obj Z.property) ⋙
      sheafToPresheaf (SmallProetale.topology B Z.obj Z.property)
        (Type (max (u + 1) v)) ⋙
      (evaluation _ _).obj (Opposite.op ((AffineIndEtaleProetale.inclusion B Z).obj V)) ≅
    sheafToPresheaf (SmallProetale.topology B X.obj X.property)
        (Type (max (u + 1) v)) ⋙
      (evaluation _ _).obj
        (Opposite.op ((AffineIndEtaleProetale.inclusion B X).obj
          ((affineIndEtaleLift B i).obj V)))

AlgebraicGeometry.ProEtale.proetaleInverseImage_sections_iso_affineIndEtaleLiftAddCommGrp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/WeaklyContractibleAbelian.lean, line 182. The attribute's comment: “(2) for abelian sheaves: at a weakly contractible object V of Z_app the inverse image of an abelian sheaf is F(v(V)), for the morphism of topoi of a closed immersion of affine objects of a chosen big pro-etale site”.

Stacks 09BL (2) for abelian sheaves. At a weakly contractible affine ind-étale object of the closed fibre, the inverse image of an abelian pro-étale sheaf is evaluation at the lift of that object, naturally in the sheaf.

def proetaleInverseImage_sections_iso_affineIndEtaleLiftAddCommGrp
    (V : AffineIndEtaleProetale B Z)
    (hV : (AffineIndEtaleProetale.topology B Z).IsWeaklyContractible V) :
    Functor.sheafPullbackConstruction.sheafPullback (smallProetaleBaseChange B Z X i)
        AddCommGrpCat.{u + 1} (SmallProetale.topology B X.obj X.property)
        (SmallProetale.topology B Z.obj Z.property) ⋙
      sheafToPresheaf (SmallProetale.topology B Z.obj Z.property) AddCommGrpCat.{u + 1} ⋙
      (evaluation _ _).obj (Opposite.op ((AffineIndEtaleProetale.inclusion B Z).obj V)) ≅
    sheafToPresheaf (SmallProetale.topology B X.obj X.property) AddCommGrpCat.{u + 1} ⋙
      (evaluation _ _).obj
        (Opposite.op ((AffineIndEtaleProetale.inclusion B X).obj
          ((affineIndEtaleLift B i).obj V)))

AlgebraicGeometry.ProEtale.appProetaleInverseImage_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/AppSiteClosedImmersionTopos.lean, line 135. The attribute's comment: “(1), the inverse image is the sheafification of the presheaf V -> F(v(V)), for the morphism of topoi induced by the fully faithful cocontinuous functor v of Tag 09BK”.

Stacks 09BL (1), the formula. The inverse image of the morphism of topoi induced by v is the sheafification of the presheaf V ↦ F(v(V)) on Z_app: it is restriction along v.op sandwiched between the inclusion of sheaves into presheaves and sheafification.

public theorem appProetaleInverseImage_eq :
    appProetaleInverseImage i =
      sheafToPresheaf (AppSmallProetale.topology X) (Type (u + 1)) ⋙
        (Functor.whiskeringLeft (AppSmallProetale Z)ᵒᵖ (AppSmallProetale X)ᵒᵖ
            (Type (u + 1))).obj (appProetaleLift i).op ⋙
          presheafToSheaf (AppSmallProetale.topology Z) (Type (u + 1))

AlgebraicGeometry.ProEtale.appProetaleInverseImageAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/AppSiteClosedImmersionTopos.lean, line 148. The attribute's comment: “(1), the sheafification of V -> F(v(V)) is the inverse image, being left adjoint to the direct image of the morphism of topoi induced by the cocontinuous functor v of Tag 09BK”.

Stacks 09BL (1), that this is the inverse image. The sheafification of V ↦ F(v(V)) is left adjoint to the direct image, so it is the inverse image of the morphism of topoi induced by v.

public noncomputable def appProetaleInverseImageAdjunction :
    appProetaleInverseImage i ⊣ appProetalePushforward i

AlgebraicGeometry.ProEtale.appProetalePushforwardFullyFaithful, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/AppSiteClosedImmersionTopos.lean, line 176. The attribute's comment: “(6), full faithfulness of the direct image i_*, for the morphism of topoi induced by the fully faithful cocontinuous functor v of Tag 09BK”.

Stacks 09BL (6) for the direct image. The direct image i_* of the morphism of topoi induced by v is fully faithful.

On underlying presheaves i_* is restriction along the base change functor u, whose left adjoint is restriction along v; the composite of the two is restriction along v ⋙ u, which is the identity because v is fully faithful.

public noncomputable def appProetalePushforwardFullyFaithful :
    (appProetalePushforward i).FullyFaithful

AlgebraicGeometry.ProEtale.appProetale_isIso_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/AppSiteClosedImmersionTopos.lean, line 193. The attribute's comment: “(5), the map i^{-1} i_* -> id is an isomorphism, for the morphism of topoi induced by the fully faithful cocontinuous functor v of Tag 09BK”.

Stacks 09BL (5) for the direct image. The counit i^{-1}i_* ⟶ id of the morphism of topoi induced by v is an isomorphism, because its right adjoint i_* is fully faithful.

public theorem appProetale_isIso_counit :
    IsIso (appProetaleInverseImageAdjunction i).counit
Tag 09AA, a lemma

Tag 09AA in the Stacks Project.

AlgebraicGeometry.ProEtale.smallProetaleMorphism_counit_isIso_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/ClosedImmersionEmbedding.lean, line 174. The attribute's comment: “(3), the counit i^{-1} i_* -> id of the morphism of topoi of a closed immersion of objects of a chosen big pro-etale site is an isomorphism”.

Stacks 09AA (3). For a closed immersion i : Z ⟶ X of objects of a chosen big pro-étale site, the counit i⁻¹ i_* ⟶ id of the direct-image adjunction on small pro-étale sheaves of sets is an isomorphism.

The assertion is Zariski local on X by AlgebraicGeometry.ProEtale.smallProetaleMorphism_counit_isIso_of_affineCounit, which reduces it to the affine objects of the small pro-étale site of X; over such an object the base change of i is a closed immersion of affine objects, where the assertion is Stacks 09BL.

theorem smallProetaleMorphism_counit_isIso_of_isClosedImmersion
    [IsClosedImmersion (B.inclusion.map i)] :
    IsIso (smallProetaleMorphism B Z X i).adj.counit

AlgebraicGeometry.ProEtale.smallProetaleMorphism_pushforward_fullyFaithful_of_isClosedImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/ClosedImmersionEmbedding.lean, line 189. The attribute's comment: “(2), the direct image i_* of the morphism of topoi of a closed immersion of objects of a chosen big pro-etale site is fully faithful”.

Stacks 09AA (2). For a closed immersion i : Z ⟶ X of objects of a chosen big pro-étale site, the direct image i_* on small pro-étale sheaves of sets is fully faithful.

This is assertion (3) together with the equivalence of Sites 04D6: the right adjoint of an adjunction whose counit is invertible is fully faithful.

def smallProetaleMorphism_pushforward_fullyFaithful_of_isClosedImmersion :
    (smallProetaleMorphism B Z X i).pushforward.FullyFaithful

AlgebraicGeometry.ProEtale.smallProetaleMorphism_inverseImage_preservesLimits_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/ClosedImmersionEmbedding.lean, line 207. The attribute's comment: “(1), the inverse image i^{-1} of the morphism of topoi of a closed immersion of objects of a chosen big pro-etale site commutes with limits”.

Stacks 09AA (1). For a closed immersion i : Z ⟶ X of objects of a chosen big pro-étale site, the inverse image i⁻¹ on small pro-étale sheaves of sets commutes with limits.

The base changes along i of the affine objects of the small pro-étale site of X cover the final object of the small pro-étale site of Z, so the canonical comparison map from i⁻¹ of a limit to the limit of i⁻¹ is invertible as soon as it is bijective on the sections over the objects lying over one of them, and that is invertibility of its restriction to such a member. Restriction commutes with limits, being a right adjoint, and exchanges with i⁻¹ across the base-change square by Beck–Chevalley, so the restricted comparison map is the comparison map for the base-changed closed immersion of affine objects, whose inverse image commutes with limits by Stacks 09BL (3).

theorem smallProetaleMorphism_inverseImage_preservesLimits_of_isClosedImmersion :
    PreservesLimits (smallProetaleMorphism B Z X i).inverseImage

AlgebraicGeometry.ProEtale.smallProetaleMorphismPushforwardFullyFaithfulOfAdjoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/SiteFunctoriality/SmallBaseChangeAdjoint.lean, line 77. The attribute's comment: “(2), the direct image is fully faithful, given that pro-etale base change admits a fully faithful left adjoint -- the adjoint that Tag 09BK supplies for a closed immersion”.

Stacks 09AA (2) given the adjoint of Stacks 09BK. If small pro-étale base change along f admits a fully faithful left adjoint, the direct image f_* on small pro-étale sheaves of sets is fully faithful.

The direct image is restriction along base change, which is fully faithful on presheaves because restriction along the left adjoint is a left adjoint of it with invertible counit.

public noncomputable def smallProetaleMorphismPushforwardFullyFaithfulOfAdjoint
    [v.Full] [v.Faithful] :
    (smallProetaleMorphism B T S f).pushforward.FullyFaithful

AlgebraicGeometry.ProEtale.smallProetaleMorphism_isIso_counit_of_adjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/SiteFunctoriality/SmallBaseChangeAdjoint.lean, line 92. The attribute's comment: “(3), the counit of the morphism of topoi is an isomorphism, given that pro-etale base change admits a fully faithful left adjoint”.

Stacks 09AA (3) given the adjoint of Stacks 09BK. If small pro-étale base change along f admits a fully faithful left adjoint, the counit f⁻¹f_*F ⟶ F of the morphism of topoi is an isomorphism, so f⁻¹f_* is the identity on small pro-étale sheaves of sets.

public theorem smallProetaleMorphism_isIso_counit_of_adjoint [v.Full] [v.Faithful] :
    IsIso (smallProetaleMorphism B T S f).adj.counit

AlgebraicGeometry.ProEtale.smallProetaleMorphism_inverseImage_preservesLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/SiteFunctoriality/SmallBaseChangeAdjoint.lean, line 103. The attribute's comment: “(1), the inverse image commutes with limits, given that it admits a left adjoint -- which is clause (3) of Tag 09BL”.

Stacks 09AA (1) given the left adjoint of Stacks 09BL (3). If the inverse image f⁻¹ on small pro-étale sheaves of sets admits a left adjoint, it commutes with limits.

public theorem smallProetaleMorphism_inverseImage_preservesLimits
    [(smallProetaleMorphism B T S f).inverseImage.IsRightAdjoint] :
    PreservesLimits (smallProetaleMorphism B T S f).inverseImage
Tag 09AB, a lemma

Tag 09AB in the Stacks Project.

AlgebraicGeometry.ProEtale.smallProetalePushforward_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/TopologicalInvariance.lean, line 1641. The attribute's comment: “direct image, assuming essential surjectivity of etale pullback (the content of Stacks 04DZ) and Stacks 09YZ over a qcqs base”.

Topological invariance of the small pro-étale topos, direct image. For an integral, universally injective and surjective morphism f : T ⟶ S in a chosen big pro-étale site, the direct image of the induced morphism of small pro-étale topoi is an equivalence.

This is the direct-image half of Stacks Project, Tag 09AB, with the two inputs that this library does not have carried as explicit hypotheses: essential surjectivity of base change on small étale sites, which is the remaining content of Stacks Project, Tag 04DZ, and AlgebraicGeometry.IntegralHasFinitePresentationLimit, which is Stacks Project, Tag 09YZ over a quasi-compact quasi-separated base and is what Stacks Project, Tag 05YU still needs.

theorem smallProetalePushforward_isEquivalence
    (hIntegral : IsIntegralHom (B.inclusion.map f))
    (hInjective : UniversallyInjective (B.inclusion.map f))
    (hSurjective : Surjective (B.inclusion.map f)) :
    (smallProetaleMorphism B T S f).pushforward.IsEquivalence

AlgebraicGeometry.ProEtale.smallProetaleInverseImage_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/TopologicalInvariance.lean, line 1687. The attribute's comment: “inverse image, assuming essential surjectivity of etale pullback (the content of Stacks 04DZ) and Stacks 09YZ over a qcqs base”.

Topological invariance of the small pro-étale topos, inverse image. For an integral, universally injective and surjective morphism f : T ⟶ S in a chosen big pro-étale site, the inverse image of the induced morphism of small pro-étale topoi is an equivalence.

Together with AlgebraicGeometry.ProEtale.smallProetalePushforward_isEquivalence and CategoryTheory.Adjunction.toEquivalence of the adjunction f⁻¹ ⊣ f_*, this is Stacks Project, Tag 09AB; its two hypotheses are those of the direct-image half.

theorem smallProetaleInverseImage_isEquivalence
    (hIntegral : IsIntegralHom (B.inclusion.map f))
    (hInjective : UniversallyInjective (B.inclusion.map f))
    (hSurjective : Surjective (B.inclusion.map f)) :
    (smallProetaleMorphism B T S f).inverseImage.IsEquivalence

AlgebraicGeometry.ProEtale.smallProetaleMorphism_isIso_unit_and_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/TopologicalInvariance/QuasiInverse.lean, line 89. The attribute's comment: “unit and counit of f^{-1} -| f_* are isomorphisms; unconditional: only f integral, universally injective, surjective; 04DZ and 09YZ are proved and supplied, not assumed”.

Topological invariance of the small pro-étale topos. Let f : T ⟶ S be an integral, universally injective and surjective morphism of schemes. Then the direct image f_* and the inverse image f⁻¹ of the induced morphism of small pro-étale topoi are quasi-inverse equivalences: the unit and the counit of the adjunction f⁻¹ ⊣ f_* are isomorphisms.

The only hypotheses are f and the three conditions on it. The proof supplies Stacks 04DZ, by Stacks.Etale.etalePullback_isEquivalence, and Stacks 09YZ, by Stacks.AlgebraicGeometry.Tag0817PartTwo.nonempty_integralLimitPresentation, to the base's conditional AlgebraicGeometry.ProEtale.smallProetalePushforward_isEquivalence, so it has no further hypotheses.

theorem smallProetaleMorphism_isIso_unit_and_counit
    (hIntegral : IsIntegralHom (B.inclusion.map f))
    (hInjective : UniversallyInjective (B.inclusion.map f))
    (hSurjective : Surjective (B.inclusion.map f)) :
    IsIso (smallProetaleMorphism B T S f).adj.unit ∧
      IsIso (smallProetaleMorphism B T S f).adj.counit

AlgebraicGeometry.ProEtale.smallProetalePushforward_isEquivalence_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/TopologicalInvariance/QuasiInverse.lean, line 120. The attribute's comment: “direct image f_* is an equivalence; unconditional: only f integral, universally injective, surjective; 04DZ and 09YZ are proved and supplied, not assumed”.

Topological invariance of the small pro-étale topos, direct image, unconditionally. Let f : T ⟶ S be an integral, universally injective and surjective morphism of schemes. Then the direct image f_* of the induced morphism of small pro-étale topoi is an equivalence.

The only hypotheses are f and the three conditions integral, universally injective and surjective. The base's AlgebraicGeometry.ProEtale.smallProetalePushforward_isEquivalence is the same statement taking in addition topological invariance of the étale site (Stacks 04DZ) and integral morphisms as limits of finite ones (Stacks 09YZ) as section hypotheses; this theorem is that one with both supplied, by Stacks.Etale.etalePullback_isEquivalence and Stacks.AlgebraicGeometry.Tag0817PartTwo.nonempty_integralLimitPresentation, so it has no further hypotheses.

theorem smallProetalePushforward_isEquivalence_of_isIntegralHom
    [IsIntegralHom (B.inclusion.map f)] [UniversallyInjective (B.inclusion.map f)]
    [Surjective (B.inclusion.map f)] :
    (smallProetaleMorphism B T S f).pushforward.IsEquivalence

AlgebraicGeometry.ProEtale.smallProetaleInverseImage_isEquivalence_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/TopologicalInvariance/QuasiInverse.lean, line 140. The attribute's comment: “inverse image f^{-1} is an equivalence; unconditional: only f integral, universally injective, surjective; 04DZ and 09YZ are proved and supplied, not assumed”.

Topological invariance of the small pro-étale topos, inverse image, unconditionally. Let f : T ⟶ S be an integral, universally injective and surjective morphism of schemes. Then the inverse image f⁻¹ of the induced morphism of small pro-étale topoi is an equivalence.

The only hypotheses are f and the three conditions integral, universally injective and surjective. The base's AlgebraicGeometry.ProEtale.smallProetaleInverseImage_isEquivalence is the same statement taking in addition Stacks 04DZ and Stacks 09YZ as section hypotheses; this theorem is that one with both supplied, by Stacks.Etale.etalePullback_isEquivalence and Stacks.AlgebraicGeometry.Tag0817PartTwo.nonempty_integralLimitPresentation, so it has no further hypotheses.

theorem smallProetaleInverseImage_isEquivalence_of_isIntegralHom
    [IsIntegralHom (B.inclusion.map f)] [UniversallyInjective (B.inclusion.map f)]
    [Surjective (B.inclusion.map f)] :
    (smallProetaleMorphism B T S f).inverseImage.IsEquivalence

AlgebraicGeometry.ProEtale.smallProetaleEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/TopologicalInvariance/QuasiInverse.lean, line 159. The attribute's comment: “f^{-1} and f_* as quasi-inverse equivalences of the small pro-etale topoi; unconditional: only f integral, universally injective, surjective”.

The small pro-étale topoi along an integral universal homeomorphism are equivalent. For f : T ⟶ S integral, universally injective and surjective, the equivalence between the small pro-étale topos of S and that of T whose functor is the inverse image f⁻¹ and whose inverse is the direct image f_*, with unit and counit those of the adjunction f⁻¹ ⊣ f_*: these two functors are quasi-inverse equivalences.

The only hypotheses are f and the three conditions on it; Stacks 04DZ and Stacks 09YZ, which the base's conditional statements take as section hypotheses, are supplied by Stacks.Etale.etalePullback_isEquivalence and Stacks.AlgebraicGeometry.Tag0817PartTwo.nonempty_integralLimitPresentation.

noncomputable def smallProetaleEquivalence
    (hIntegral : IsIntegralHom (B.inclusion.map f))
    (hInjective : UniversallyInjective (B.inclusion.map f))
    (hSurjective : Surjective (B.inclusion.map f)) :
    Sheaf (SmallProetale.topology B S.obj S.property) (Type (u + 1)) ≌
      Sheaf (SmallProetale.topology B T.obj T.property) (Type (u + 1))
Tag 09AC, a lemma

Tag 09AC in the Stacks Project.

AlgebraicGeometry.ProEtale.abelianProetaleInverseImage_sections_iso_closedFibre, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/ClosedFibreInverseImage.lean, line 193. The attribute's comment: “i^{-1}F(U x_X Z) = F(U) for every abelian sheaf F on X_proetale, naturally in F, for an ARBITRARY closed immersion i : Z -> X and U affine and weakly contractible (in the chosen big pro-etale site, Tag 098H) all of whose points specialize into U x_X Z”.

Stacks 09AC. Let i : Z ⟶ X be a closed immersion of objects of a chosen big pro-étale site and let U be an object of the small pro-étale site of X such that

  1. U is affine and weakly contractible, and
  2. every point of U specializes to a point of U ×_X Z.

Then i^{-1}F(U ×_X Z) = F(U) for every abelian sheaf F on the small pro-étale site of X, naturally in F.

Weak contractibility of U is taken in the chosen big pro-étale site; for an affine object it is equivalent to w-contractibility of its ring of global sections by Stacks 098H, and it implies weak contractibility of U as an object of the small pro-étale site of X.

def abelianProetaleInverseImage_sections_iso_closedFibre [IsAffine U.obj.left.obj]
    (hU : B.topology.IsWeaklyContractible U.obj.left)
    (hspec : ∀ x : U.obj.left.obj, ∃ w : (pullback U.obj.hom i).obj,
      x ⤳ (B.inclusion.map (pullback.fst U.obj.hom i)).base w) :
    Functor.sheafPullbackConstruction.sheafPullback (smallProetaleBaseChange B Z X i)
        AddCommGrpCat.{u + 1} (SmallProetale.topology B X.obj X.property)
        (SmallProetale.topology B Z.obj Z.property) ⋙
      sheafToPresheaf (SmallProetale.topology B Z.obj Z.property) AddCommGrpCat.{u + 1} ⋙
      (evaluation _ _).obj (op ((smallProetaleBaseChange B Z X i).obj U)) ≅
    sheafToPresheaf (SmallProetale.topology B X.obj X.property) AddCommGrpCat.{u + 1} ⋙
      (evaluation _ _).obj (op U)

AlgebraicGeometry.ProEtale.existsUnique_algHom_comp_quotientMk_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/IndEtale/JacobsonQuotientRetraction.lean, line 231. The attribute's comment: “the ring-theoretic statement the lemma reduces to: for A w-contractible and I in the Jacobson radical, a factorization A -> B -> A/I with A -> B ind-etale has a unique retraction B -> A compatible with the maps to A/I; the source's B/IB = A/I x R splitting is not used, see the module docstring”.

The ring-theoretic content of Stacks 09AC. Let A be a w-contractible ring and I ⊆ A an ideal contained in the Jacobson radical of A. Every A-algebra map from an ind-étale A-algebra B to A ⧸ I factors through the quotient map A → A ⧸ I by a unique A-algebra map B → A.

theorem existsUnique_algHom_comp_quotientMk_eq (A : Type u) [CommRing A]
    (hA : ProetaleWContractible.IsWContractible.{u, u} A) (I : Ideal A)
    (hI : I ≤ Ring.jacobson A) (B : Type u) [CommRing B] [Algebra A B]
    (hB : StacksDraft.IndEtale A B) (φ : B →ₐ[A] A ⧸ I) :
    ∃! σ : B →ₐ[A] A, (Ideal.Quotient.mkₐ A I).comp σ = φ

AlgebraicGeometry.ProEtale.appProetaleLiftBaseChangeObjIsoOfIsWContractible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/AppSiteLiftOfClosedFibre.lean, line 157. The attribute's comment: “the identification v(U x_X Z) = U, to which Stacks 09BL (1) reduces the lemma; hypothesis (1) is w-contractibility of Gamma(U, O_U) and hypothesis (2) is containment of the ideal of the closed fibre in its Jacobson radical”.

Stacks 09AC. Let i : Z ⟶ X be a closed immersion of affine schemes and let U be an object of X_app which is affine and weakly contractible and every point of which specializes to a point of U ×_X Z. Then U is the lift of its closed fibre: v(U ×_X Z) ≅ U.

public noncomputable def appProetaleLiftBaseChangeObjIsoOfIsWContractible (U : AppSmallProetale X)
    (hU : ProetaleWContractible.IsWContractible.{u, u} (appAlg U).obj.right)
    (hjac : (appTopKer i).map (appAlg U).obj.hom.hom ≤ Ring.jacobson (appAlg U).obj.right) :
    (appProetaleLift i).obj ((appProetaleBaseChange i).obj U) ≅ U
Tag 09BM, a lemma

Tag 09BM in the Stacks Project.

AlgebraicGeometry.ProEtale.exact_smallProetalePushforward_of_isRetrocompact_compl_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/SiteFunctoriality/ClosedImmersionPushforwardExact.lean, line 156.

Stacks 09BM. Let i : Z → X be a closed immersion of schemes whose open complement is retrocompact. Then direct image of abelian sheaves along the induced morphism of small pro-étale sites is exact.

theorem exact_smallProetalePushforward_of_isRetrocompact_compl_range
    (B : BigProetaleSite.{u}) {Z X : B.Scheme} (i : Z ⟶ X)
    [IsClosedImmersion (B.inclusion.map i)]
    (hi : IsRetrocompact ((Set.range (B.inclusion.map i).base)ᶜ)) :
    exactFunctor
      (Sheaf (SmallProetale.topology B Z.obj Z.property) AddCommGrpCat.{u + 1})
      (Sheaf (SmallProetale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
      ((smallProetaleBaseChange B Z X i).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
        (SmallProetale.topology B X.obj X.property)
        (SmallProetale.topology B Z.obj Z.property))
Sources
LeanAlgebraicGeometry.ProEtale.appBaseChange · AlgebraicGeometry.ProEtale.appProetaleBaseChange · AlgebraicGeometry.ProEtale.isClosedImmersion_pullback_fst · AlgebraicGeometry.ProEtale.appProetaleLift · AlgebraicGeometry.ProEtale.appProetaleBaseChange_hasLeftAdjoint · AlgebraicGeometry.ProEtale.appProetaleLift_fullyFaithful · AlgebraicGeometry.ProEtale.appProetaleLift_baseChangeIso · AlgebraicGeometry.ProEtale.appProetaleBaseChange_isCovering

Section61.26 Extension by zero#

Section 61.26 of the Stacks Project, Tag 09AD. 6 tags here are carried by 30 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09AE, a definition

Tag 09AE in the Stacks Project.

AlgebraicGeometry.ProEtale.Abelian.exists_extensionByZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/Abelian.lean, line 75. The attribute's comment: “extension_by_zero_abelian”. References: SGA 4 IV (11.3.1), “pro-étale site, Ab”.

Restriction of abelian pro-étale sheaves has a left adjoint.

theorem exists_extensionByZero {U X : Scheme.{u}} (j : U ⟶ X) [WeaklyEtale j] :
    Nonempty (Σ F : Sheaf (Scheme.ProEt.topology U) AddCommGrpCat.{max (u + 1) v} ⥤
      Sheaf (Scheme.ProEt.topology X) AddCommGrpCat.{max (u + 1) v},
        F ⊣ proetaleRestriction j)

AlgebraicGeometry.ProEtale.Abelian.sheafifiedExtensionByZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/Abelian.lean, line 109. The attribute's comment: “(2), the functor j_! : Ab(U_proetale) -> Ab(X_proetale) called extension by zero, as explicit data: the sheafification of the left Kan extension along the opposite of postcomposition by j”.

Extension by zero of abelian sheaves on the small pro-étale site, as an explicit functor: the composite of the inclusion of sheaves into presheaves, left Kan extension along the opposite of postcomposition by j, and sheafification.

def sheafifiedExtensionByZero {U X : Scheme.{u}} (j : U ⟶ X) [WeaklyEtale j] :
    Sheaf (Scheme.ProEt.topology U) AddCommGrpCat.{max (u + 1) v} ⥤
      Sheaf (Scheme.ProEt.topology X) AddCommGrpCat.{max (u + 1) v}

AlgebraicGeometry.ProEtale.Abelian.sheafifiedExtensionByZeroAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/Abelian.lean, line 121. The attribute's comment: “(2), the adjunction j_! ⊣ j^{-1} on abelian sheaves, witnessing that restriction along a weakly étale morphism has extension by zero as a left adjoint”.

The explicit extension-by-zero functor is left adjoint to restriction.

def sheafifiedExtensionByZeroAdjunction {U X : Scheme.{u}} (j : U ⟶ X) [WeaklyEtale j] :
    sheafifiedExtensionByZero.{u, v} j ⊣ proetaleRestriction.{u, v} j

AlgebraicGeometry.ProEtale.Modules.exists_extensionByZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/Modules.lean, line 154. The attribute's comment: “extension_by_zero_modules”. References: SGA 4 IV (11.3.1), “pro-étale, Λ-modules”.

Restriction of pro-étale module sheaves has a left adjoint.

theorem exists_extensionByZero {U X : Scheme.{u}} (j : U ⟶ X) [WeaklyEtale j]
    (Λ : Type v) [Ring Λ] :
    Nonempty (Σ F : Sheaf (Scheme.ProEt.topology U) (ModuleCat.{max (u + 1) w} Λ) ⥤
      Sheaf (Scheme.ProEt.topology X) (ModuleCat.{max (u + 1) w} Λ),
        F ⊣ proetaleRestriction j Λ)

AlgebraicGeometry.ProEtale.Modules.sheafifiedExtensionByZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/Modules.lean, line 195. The attribute's comment: “(3), the functor j_! : Mod(U_proetale, Λ) -> Mod(X_proetale, Λ) called extension by zero, as explicit data: the sheafification of the left Kan extension along the opposite of postcomposition by j”.

Extension by zero of pro-étale sheaves of Λ-modules, as an explicit functor: the composite of the inclusion of sheaves into presheaves, left Kan extension along the opposite of postcomposition by j, and sheafification.

def sheafifiedExtensionByZero {U X : Scheme.{u}} (j : U ⟶ X) [WeaklyEtale j]
    (Λ : Type v) [Ring Λ] :
    Sheaf (Scheme.ProEt.topology U) (ModuleCat.{max (u + 1) w} Λ) ⥤
      Sheaf (Scheme.ProEt.topology X) (ModuleCat.{max (u + 1) w} Λ)

AlgebraicGeometry.ProEtale.Modules.sheafifiedExtensionByZeroAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/Modules.lean, line 208. The attribute's comment: “(3), the adjunction j_! ⊣ j^{-1} on sheaves of Λ-modules, witnessing that restriction along a weakly étale morphism has extension by zero as a left adjoint”.

The explicit extension-by-zero functor is left adjoint to restriction.

def sheafifiedExtensionByZeroAdjunction {U X : Scheme.{u}} (j : U ⟶ X) [WeaklyEtale j]
    (Λ : Type v) [Ring Λ] :
    sheafifiedExtensionByZero.{u, v, w} j Λ ⊣ proetaleRestriction.{u, v, w} j Λ

AlgebraicGeometry.ProEtale.Sets.extensionByZero, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/Sets.lean, line 56. The attribute's comment: “extension_by_zero_sets”.

Extension by zero of sheaves of sets along a weakly étale morphism.

def extensionByZero {U X : Scheme.{u}} (j : U ⟶ X) [WeaklyEtale j] :
    Sheaf (Scheme.ProEt.topology U) (Type (max (u + 1) v)) ⥤
      Sheaf (Scheme.ProEt.topology X) (Type (max (u + 1) v))

AlgebraicGeometry.ProEtale.Sets.extensionByZeroAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/Sets.lean, line 66. The attribute's comment: “extension_by_zero_sets”.

Extension by zero is left adjoint to restriction.

def extensionByZeroAdjunction {U X : Scheme.{u}} (j : U ⟶ X) [WeaklyEtale j] :
    extensionByZero.{u, v} j ⊣ proetaleRestriction.{u, v} j
Tag 09AF, a lemma

Tag 09AF in the Stacks Project.

AlgebraicGeometry.ProEtale.epsilonInverseImageExtensionByZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/EtaleComparison.lean, line 133. The attribute's comment: “the natural isomorphism eps^{-1} j_! = j_! eps^{-1}”.

Stacks Tag 09AF. For an étale morphism j : U ⟶ X, pulling back along the comparison morphism ε of the small pro-étale and small étale sites commutes with extension by zero: ε^{-1} j_! ≅ j_! ε^{-1} on abelian sheaves. Both sides are left adjoint to ε_* j^{-1} = j^{-1} ε_*.

def epsilonInverseImageExtensionByZeroIso :
    Stacks.EtaleCohomology.extensionByZero.{u, v} j ⋙ epsilonInverseImage.{u, v} X ≅
      epsilonInverseImage.{u, v} U ⋙ Abelian.extensionByZero.{u, v} j

AlgebraicGeometry.ProEtale.epsilonInverseImageExtensionByZeroObjIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/EtaleComparison.lean, line 145. The attribute's comment: “at an abelian sheaf G on U_etale: eps^{-1} j_! G = j_! eps^{-1} G”.

Stacks Tag 09AF, evaluated at an abelian sheaf G on U_étale: ε^{-1} j_! G = j_! ε^{-1} G as abelian sheaves on X_proétale. This is the form in which the source states the lemma.

def epsilonInverseImageExtensionByZeroObjIso
    (G : Sheaf U.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}) :
    (epsilonInverseImage.{u, v} X).obj
        ((Stacks.EtaleCohomology.extensionByZero.{u, v} j).obj G) ≅
      (Abelian.extensionByZero.{u, v} j).obj ((epsilonInverseImage.{u, v} U).obj G)
Tag 09AG, a lemma

Tag 09AG in the Stacks Project.

AlgebraicGeometry.ProEtale.isZero_extensionByZero_sections_of_specializes_to_closed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/ClosedFibreVanishing.lean, line 620.

Extension by zero vanishes on an affine pro-étale object whose points specialize to a closed fibre disjoint from the weakly étale source.

theorem isZero_extensionByZero_sections_of_specializes_to_closed
    {U X Z : Scheme.{u}} (j : U ⟶ X) [WeaklyEtale j]
    (i : Z ⟶ X) [IsClosedImmersion i]
    (hdisjoint : IsEmpty (pullback j i : Scheme.{u}))
    (V : X.ProEt) [IsAffine V.left]
    (hV : ∀ x : V.left, ∃ z : (pullback V.hom i : Scheme.{u}),
      Specializes x ((pullback.fst V.hom i).base z))
    (F : Sheaf (Scheme.ProEt.topology U) AddCommGrpCat.{max (u + 1) v}) :
    IsZero (((Abelian.extensionByZero j).obj F).obj.obj (op V))
Tag 09BN, a lemma

Tag 09BN in the Stacks Project.

AlgebraicGeometry.ProEtale.extensionByZero_unit_isIso_sets, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/OpenImmersion.lean, line 133. The attribute's comment: “sets: extension-by-zero unit”.

The extension-by-zero unit for sheaves of sets along an open immersion is a natural isomorphism.

theorem extensionByZero_unit_isIso_sets {U X : Scheme.{u}}
    (j : U ⟶ X) [IsOpenImmersion j] :
    IsIso (Sets.extensionByZeroAdjunction.{u, v} j).unit

AlgebraicGeometry.ProEtale.extensionByZero_fullyFaithful_sets, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/OpenImmersion.lean, line 141. The attribute's comment: “sets: extension by zero fully faithful”.

Extension by zero of pro-étale sheaves of sets is fully faithful.

theorem extensionByZero_fullyFaithful_sets {U X : Scheme.{u}}
    (j : U ⟶ X) [IsOpenImmersion j] :
    Nonempty (Sets.extensionByZero.{u, v} j).FullyFaithful

AlgebraicGeometry.ProEtale.directImage_counit_isIso_sets, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/OpenImmersion.lean, line 316. The attribute's comment: “sets: direct-image counit”. References: SGA 4 I (5.7), “u_* half, sheaves of”.

The direct-image counit for sheaves of sets along an open immersion is a natural isomorphism.

theorem directImage_counit_isIso_sets
    (B : BigProetaleSite.{u}) {T S : B.Scheme} (j : T ⟶ S)
    [IsOpenImmersion (B.inclusion.map j)] :
    IsIso (smallProetaleMorphism B T S j).adj.counit

AlgebraicGeometry.ProEtale.directImage_fullyFaithful_sets, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/OpenImmersion.lean, line 362. The attribute's comment: “sets: direct image fully faithful”.

Direct image of pro-étale sheaves of sets is fully faithful.

theorem directImage_fullyFaithful_sets
    (B : BigProetaleSite.{u}) {T S : B.Scheme} (j : T ⟶ S)
    [IsOpenImmersion (B.inclusion.map j)] :
    Nonempty (smallProetaleMorphism B T S j).pushforward.FullyFaithful

AlgebraicGeometry.ProEtale.extensionByZero_unit_isIso_abelian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/OpenImmersion.lean, line 373. The attribute's comment: “abelian: extension-by-zero unit”.

The extension-by-zero unit for abelian pro-étale sheaves along an open immersion is a natural isomorphism.

theorem extensionByZero_unit_isIso_abelian {U X : Scheme.{u}}
    (j : U ⟶ X) [IsOpenImmersion j] :
    IsIso (Abelian.extensionByZero_adjunction.{u, v} j).unit

AlgebraicGeometry.ProEtale.extensionByZero_fullyFaithful_abelian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/OpenImmersion.lean, line 382. The attribute's comment: “abelian: extension by zero fully faithful”.

Extension by zero of abelian pro-étale sheaves is fully faithful.

theorem extensionByZero_fullyFaithful_abelian {U X : Scheme.{u}}
    (j : U ⟶ X) [IsOpenImmersion j] :
    Nonempty (Abelian.extensionByZero.{u, v} j).FullyFaithful

AlgebraicGeometry.ProEtale.exists_directImage_abelian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/OpenImmersion.lean, line 391. The attribute's comment: “abelian: direct-image functor”.

Restriction of abelian pro-étale sheaves has a right adjoint.

theorem exists_directImage_abelian {U X : Scheme.{u}}
    (j : U ⟶ X) [IsOpenImmersion j] :
    Nonempty (Σ R : Sheaf (Scheme.ProEt.topology U) AddCommGrpCat.{max (u + 1) v} ⥤
      Sheaf (Scheme.ProEt.topology X) AddCommGrpCat.{max (u + 1) v},
      Abelian.proetaleRestriction j ⊣ R)

AlgebraicGeometry.ProEtale.directImage_counit_isIso_abelian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/OpenImmersion.lean, line 401. The attribute's comment: “abelian: direct-image counit”. References: SGA 4 I (5.7), “u_* half, pro-étale”.

The counit of restriction and any of its right adjoints is invertible.

theorem directImage_counit_isIso_abelian {U X : Scheme.{u}}
    (j : U ⟶ X) [IsOpenImmersion j]
    (R : Sheaf (Scheme.ProEt.topology U) AddCommGrpCat.{max (u + 1) v} ⥤
      Sheaf (Scheme.ProEt.topology X) AddCommGrpCat.{max (u + 1) v})
    (adj : Abelian.proetaleRestriction j ⊣ R) :
    IsIso adj.counit

AlgebraicGeometry.ProEtale.directImage_fullyFaithful_abelian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/OpenImmersion.lean, line 413. The attribute's comment: “abelian: direct image fully faithful”.

Direct image of abelian pro-étale sheaves is fully faithful.

theorem directImage_fullyFaithful_abelian {U X : Scheme.{u}}
    (j : U ⟶ X) [IsOpenImmersion j]
    (R : Sheaf (Scheme.ProEt.topology U) AddCommGrpCat.{max (u + 1) v} ⥤
      Sheaf (Scheme.ProEt.topology X) AddCommGrpCat.{max (u + 1) v})
    (adj : Abelian.proetaleRestriction j ⊣ R) :
    Nonempty R.FullyFaithful

AlgebraicGeometry.ProEtale.extensionByZero_unit_isIso_modules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/OpenImmersion.lean, line 425. The attribute's comment: “modules: extension-by-zero unit”.

The extension-by-zero unit for module pro-étale sheaves along an open immersion is a natural isomorphism.

theorem extensionByZero_unit_isIso_modules {U X : Scheme.{u}}
    (j : U ⟶ X) [IsOpenImmersion j] (Λ : Type v) [Ring Λ] :
    IsIso (Modules.extensionByZero_adjunction.{u, v, w} j Λ).unit

AlgebraicGeometry.ProEtale.extensionByZero_fullyFaithful_modules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/OpenImmersion.lean, line 434. The attribute's comment: “modules: extension by zero fully faithful”.

Extension by zero of module pro-étale sheaves is fully faithful.

theorem extensionByZero_fullyFaithful_modules {U X : Scheme.{u}}
    (j : U ⟶ X) [IsOpenImmersion j] (Λ : Type v) [Ring Λ] :
    Nonempty (Modules.extensionByZero.{u, v, w} j Λ).FullyFaithful

AlgebraicGeometry.ProEtale.exists_directImage_modules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/OpenImmersion.lean, line 443. The attribute's comment: “modules: direct-image functor”.

Restriction of module pro-étale sheaves has a right adjoint.

theorem exists_directImage_modules {U X : Scheme.{u}}
    (j : U ⟶ X) [IsOpenImmersion j] (Λ : Type v) [Ring Λ] :
    Nonempty (Σ R : Sheaf (Scheme.ProEt.topology U) (ModuleCat.{max (u + 1) w} Λ) ⥤
      Sheaf (Scheme.ProEt.topology X) (ModuleCat.{max (u + 1) w} Λ),
      Modules.proetaleRestriction j Λ ⊣ R)

AlgebraicGeometry.ProEtale.directImage_counit_isIso_modules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/OpenImmersion.lean, line 453. The attribute's comment: “modules: direct-image counit”. References: SGA 4 I (5.7), “u_* half, Λ-modules”.

The counit of restriction and any of its right adjoints is invertible.

theorem directImage_counit_isIso_modules {U X : Scheme.{u}}
    (j : U ⟶ X) [IsOpenImmersion j] (Λ : Type v) [Ring Λ]
    (R : Sheaf (Scheme.ProEt.topology U) (ModuleCat.{max (u + 1) w} Λ) ⥤
      Sheaf (Scheme.ProEt.topology X) (ModuleCat.{max (u + 1) w} Λ))
    (adj : Modules.proetaleRestriction j Λ ⊣ R) :
    IsIso adj.counit

AlgebraicGeometry.ProEtale.directImage_fullyFaithful_modules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/OpenImmersion.lean, line 465. The attribute's comment: “modules: direct image fully faithful”.

Direct image of module pro-étale sheaves is fully faithful.

theorem directImage_fullyFaithful_modules {U X : Scheme.{u}}
    (j : U ⟶ X) [IsOpenImmersion j] (Λ : Type v) [Ring Λ]
    (R : Sheaf (Scheme.ProEt.topology U) (ModuleCat.{max (u + 1) w} Λ) ⥤
      Sheaf (Scheme.ProEt.topology X) (ModuleCat.{max (u + 1) w} Λ))
    (adj : Modules.proetaleRestriction j Λ ⊣ R) :
    Nonempty R.FullyFaithful
Tag 09AH, a lemma

Tag 09AH in the Stacks Project.

AlgebraicGeometry.ProEtale.hasEnoughObjects_openPart_or_closedFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/OpenClosedSequence.lean, line 761. The attribute's comment: “the geometric reduction of the source's proof: quasi-compactness of j splits every affine weakly contractible object of X_proetale into a part lying over U and the ind-Zariski localization along its closed fibre”.

Stacks 09AH, the geometric reduction. For a closed immersion i and its complementary quasi-compact open immersion j, every object of X_proétale is covered by objects which are either pulled back from U_proétale, or affine, weakly contractible and with all their points specializing into the closed fibre.

Quasi-compactness of j is what makes the closed fibre of an affine object cut out by finitely many equations, and hence what produces the ind-Zariski localization of Stacks 096V along it.

theorem hasEnoughObjects_openPart_or_closedFibre {Z U X : Scheme.{u}} (i : Z ⟶ X)
    [IsClosedImmersion i] (j : U ⟶ X) [IsOpenImmersion j] [QuasiCompact j]
    (hij : Set.range j.base = (Set.range i.base)ᶜ) :
    (Scheme.ProEt.topology X).HasEnoughObjects (fun V : X.ProEt ↦
      (∃ W : U.ProEt, Nonempty (V ≅ (proetalePostcompose j).obj W)) ∨
      (IsAffine V.left ∧ (Scheme.ProEt.topology X).IsWeaklyContractible V ∧
        ∀ x : V.left, ∃ z : (pullback V.hom i : Scheme.{u}),
          Specializes x ((pullback.fst V.hom i).base z)))

AlgebraicGeometry.ProEtale.openClosedShortComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/OpenClosedSequence.lean, line 884. The attribute's comment: “the two canonical maps j_! j^{-1} F -> F -> i_* i^{-1} F and the fact that they compose to zero, i.e. the short complex of the tag; its short exactness is NOT proved here, see shortExact_openClosedShortComplex_of_isIso_unit_app”.

Stacks 09AH. The canonical short complex j_! j^{-1} F ⟶ F ⟶ i_* i^{-1} F on the small pro-étale site of X, for a closed subscheme i : Z ⟶ X and the inclusion j : U ⟶ X of its complement. Its two maps are the counit of j_! ⊣ j^{-1} and the unit of i^{-1} ⊣ i_*.

The tag states in addition that this short complex is short exact when j is quasi-compact. That is not proved here: shortExact_openClosedShortComplex_of_isIso_unit_app below reduces it to the single input described in the header of this file.

def openClosedShortComplex
    (F : Sheaf (Scheme.ProEt.topology X) AddCommGrpCat.{max (u + 1) v}) :
    ShortComplex (Sheaf (Scheme.ProEt.topology X) AddCommGrpCat.{max (u + 1) v})

AlgebraicGeometry.ProEtale.shortExact_map_proetaleRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/OpenClosedSequence.lean, line 915. The attribute's comment: “exactness over the open part only: the restriction to U of the canonical short complex is short exact, unconditionally. Short exactness of the sequence on X_proetale itself is NOT proved in this file: shortExact_openClosedShortComplex_of_isIso_unit_app proves it at the source's hypotheses but assumes Tag 09AC for the site of AlgebraicGeometry.Scheme.ProEt, namely that the unit F -> i_* i^{-1} F is invertible on sections over every affine weakly contractible object all of whose points specialize into its closed fibre”.

Stacks 09AH, over the open part. Restricted to U, the short complex of the tag is short exact, and indeed split: its third term vanishes over U and its first map becomes invertible there.

theorem shortExact_map_proetaleRestriction [IsOpenImmersion j]
    (F : Sheaf (Scheme.ProEt.topology X) AddCommGrpCat.{max (u + 1) v}) :
    ((openClosedShortComplex.{u, v} i j hij F).map
      (Abelian.proetaleRestriction.{u, v} j)).ShortExact

AlgebraicGeometry.ProEtale.shortExact_openClosedShortComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/OpenClosedSequenceShortExact.lean, line 76.

Stacks 09AH. Let i : Z ⟶ X be a closed immersion and let j : U ⟶ X be an open immersion onto the complement of its image, and assume j quasi-compact. For every abelian sheaf F on the small pro-étale site of X the canonical sequence 0 → j_! j^{-1} F → F → i_* i^{-1} F → 0, whose maps are the counit of j_! ⊣ j^{-1} and the unit of i^{-1} ⊣ i_*, is short exact.

theorem shortExact_openClosedShortComplex {Z U X : Scheme.{u}} (i : Z ⟶ X) (j : U ⟶ X)
    [IsClosedImmersion i] [IsOpenImmersion j] [QuasiCompact j]
    (hij : Set.range j.base = (Set.range i.base)ᶜ)
    (F : Sheaf (Scheme.ProEt.topology X) AddCommGrpCat.{max (u + 1) v}) :
    (openClosedShortComplex.{u, v} i j hij F).ShortExact
Tag 09BP, a lemma

Tag 09BP in the Stacks Project.

AlgebraicGeometry.ProEtale.preservesLimits_extensionByZero_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/PreservesLimits.lean, line 390.

Stacks 09BP. For a quasi-compact open immersion j : U ⟶ X of schemes, extension by zero j_! : Ab(U_proétale) ⥤ Ab(X_proétale) of abelian sheaves on the small pro-étale sites commutes with limits.

Nothing is assumed: j_! j^{-1} commutes with limits by preservesLimits_proetaleRestriction_comp_extensionByZero_of_quasiCompact, whose proof computes the sections of j_! j^{-1} on the covering family that quasi-compactness of j produces; and j_! is isomorphic to j_! j^{-1} j_* because the counit of j^{-1} ⊣ j_* is invertible for an open immersion.

theorem preservesLimits_extensionByZero_unconditional [IsOpenImmersion j] [QuasiCompact j] :
    PreservesLimits (Abelian.extensionByZero.{u, v} j)
Sources
LeanAlgebraicGeometry.ProEtale.Abelian.exists_extensionByZero · AlgebraicGeometry.ProEtale.Abelian.sheafifiedExtensionByZero · AlgebraicGeometry.ProEtale.Abelian.sheafifiedExtensionByZeroAdjunction · AlgebraicGeometry.ProEtale.Modules.exists_extensionByZero · AlgebraicGeometry.ProEtale.Modules.sheafifiedExtensionByZero · AlgebraicGeometry.ProEtale.Modules.sheafifiedExtensionByZeroAdjunction · AlgebraicGeometry.ProEtale.Sets.extensionByZero · AlgebraicGeometry.ProEtale.Sets.extensionByZeroAdjunction

Section61.27 Constructible sheaves on the pro-étale site#

Section 61.27 of the Stacks Project, Tag 09AI. 6 tags here are carried by 5 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09AJ, a definition

Tag 09AJ in the Stacks Project.

AlgebraicGeometry.ProEtale.IsConstructibleModuleSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Constructible/Defs.lean, line 79.

Stacks 09AJ. A sheaf of Λ-modules on the small pro-étale site of X, with Λ Noetherian, is constructible if every affine open of X has a finite partition into constructible locally closed subschemes on each of which the inverse image of the sheaf is locally constant of finite type.

abbrev IsConstructibleModuleSheaf (X : Scheme.{u}) (Λ : Type v) [CommRing Λ]
    [IsNoetherianRing Λ]
    [∀ Y : Scheme.{u}, HasWeakSheafify (Scheme.ProEt.topology Y) (ModuleCat.{w} Λ)]
    [∀ (Y : Scheme.{u}) (V : Y.ProEt),
      HasWeakSheafify ((Scheme.ProEt.topology Y).over V) (ModuleCat.{w} Λ)]
    [∀ {Z Y : Scheme.{u}} (f : Z ⟶ Y),
      ((Scheme.proetaleBaseChange f).sheafPushforwardContinuous
        (ModuleCat.{w} Λ) (Scheme.ProEt.topology Y)
        (Scheme.ProEt.topology Z)).IsRightAdjoint]
    (F : Sheaf (Scheme.ProEt.topology X) (ModuleCat.{w} Λ)) : Prop

AlgebraicGeometry.ProEtale.IsConstructibleModuleSheaf', an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ConstructibleSheaves.lean, line 85.

Stacks 09AJ. A sheaf of Λ-modules on the small pro-étale site of X is constructible when every affine open U of X admits a finite decomposition into constructible locally closed subschemes on each of which the inverse image of the sheaf is locally constant of finite type.

This is reducible, so a client can use the witnesses of the stratification directly.

The primed name records the weaker hypotheses: pinning the sections universe to max (u + 1) v w makes sheafification and the left Kan extensions exist unconditionally, so this form needs none of the HasWeakSheafify and IsRightAdjoint assumptions that AlgebraicGeometry.ProEtale.IsConstructibleModuleSheaf of StacksFrontier.AlgebraicGeometry.ProEtale.Constructible.Defs carries, at the cost of leaving that universe no longer free. The two are stated with different local-constancy predicates — Stacks.ConstantSheaf.IsFiniteTypeLocallyConstantModuleSheaf here against Stacks.ConstantSheaf.IsFiniteTypeLocallyConstant there — and identifying them is not done.

public abbrev IsConstructibleModuleSheaf' (X : Scheme.{u}) (Λ : Type v) [CommRing Λ]
    [IsNoetherianRing Λ]
    (F : Sheaf (Scheme.ProEt.topology X) (ModuleCat.{max (u + 1) v w} Λ)) : Prop
Tag 09AK, a lemma

Tag 09AK in the Stacks Project.

Declarations registered for the tag:

Tag 09B5, a lemma

Tag 09B5 in the Stacks Project.

AlgebraicGeometry.ProEtale.isWeakSerreClass_isConstructibleModuleSheaf', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Constructible/WeakSerre.lean, line 113.

Stacks 09B5. For Λ a Noetherian ring, the constructible sheaves of Λ-modules on the small pro-étale site of a scheme X form a weak Serre subcategory of all sheaves of Λ-modules on that site. There is no hypothesis on X.

public theorem isWeakSerreClass_isConstructibleModuleSheaf' :
    ObjectProperty.IsWeakSerreClass
      (fun F : Sheaf (Scheme.ProEt.topology X) (ModuleCat.{max (u + 1) v w} Λ) =>
        IsConstructibleModuleSheaf'.{u, v, w} X Λ F)
Tag 09AL, a lemma

Tag 09AL in the Stacks Project.

Declarations registered for the tag:

Tag 09BQ, a lemma

Tag 09BQ in the Stacks Project.

AlgebraicGeometry.ProEtale.minus_tensor_and_isConstructibleModuleSheaf'_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Constructible/DerivedTensor.lean, line 158.

Stacks 09BQ. Let X be a scheme and Λ a Noetherian ring. If K and L are bounded above objects of D(X_proét, Λ) whose cohomology sheaves are constructible, then their derived tensor product K ⊗_Λ^L L is bounded above and has constructible cohomology sheaves: it lies in D_c^-(X_proét, Λ).

theorem minus_tensor_and_isConstructibleModuleSheaf'_homology
    (K L : DerivedCategory (Sheaf (Scheme.ProEt.topology X) (ModuleCat.{max (u + 1) w} Λ)))
    (hK : DerivedCategory.TStructure.t.minus K) (hL : DerivedCategory.TStructure.t.minus L)
    (hKc : ∀ i, IsConstructibleModuleSheaf'.{u, max (u + 1) w, w} X Λ
      ((DerivedCategory.homologyFunctor _ i).obj K))
    (hLc : ∀ i, IsConstructibleModuleSheaf'.{u, max (u + 1) w, w} X Λ
      ((DerivedCategory.homologyFunctor _ i).obj L)) :
    DerivedCategory.TStructure.t.minus (K ⊗ L) ∧
      ∀ i, IsConstructibleModuleSheaf'.{u, max (u + 1) w, w} X Λ
        ((DerivedCategory.homologyFunctor _ i).obj (K ⊗ L))
Tag 09BR, a lemma

Tag 09BR in the Stacks Project.

AlgebraicGeometry.ProEtale.minus_and_isConstructibleModuleSheaf'_homology_derivedExtendScalars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Constructible/DerivedReduction.lean, line 265.

Stacks 09BR. Let X be a scheme, Λ a Noetherian ring, I ⊆ Λ an ideal and K an object of D(X_proét, Λ). Set Kₙ = K ⊗_Λ^L Λ/Iⁿ, the derived extension of scalars of K along Λ → Λ/Iⁿ. If K₁ lies in D_c^-(X_proét, Λ/I), that is, it is bounded above and its cohomology sheaves are constructible, then Kₙ lies in D_c^-(X_proét, Λ/Iⁿ) for all n.

theorem minus_and_isConstructibleModuleSheaf'_homology_derivedExtendScalars
    (K : DerivedCategory (Sheaf (Scheme.ProEt.topology X) (ModuleCat.{max (u + 1) w} Λ)))
    (hK : DerivedCategory.TStructure.t.minus
        ((derivedExtendScalars _ (Ideal.Quotient.mk I)).obj K) ∧
      ∀ i, IsConstructibleModuleSheaf'.{u, max (u + 1) w, w} X (Λ ⧸ I)
        ((DerivedCategory.homologyFunctor _ i).obj
          ((derivedExtendScalars _ (Ideal.Quotient.mk I)).obj K)))
    (n : ℕ) :
    DerivedCategory.TStructure.t.minus
        ((derivedExtendScalars _ (Ideal.Quotient.mk (I ^ n))).obj K) ∧
      ∀ i, IsConstructibleModuleSheaf'.{u, max (u + 1) w, w} X (Λ ⧸ I ^ n)
        ((DerivedCategory.homologyFunctor _ i).obj
          ((derivedExtendScalars _ (Ideal.Quotient.mk (I ^ n))).obj K))
Sources
LeanAlgebraicGeometry.ProEtale.IsConstructibleModuleSheaf · AlgebraicGeometry.ProEtale.IsConstructibleModuleSheaf' · AlgebraicGeometry.ProEtale.isEquivalence_etaleInverseImageConstructible · AlgebraicGeometry.ProEtale.isWeakSerreClass_isConstructibleModuleSheaf' · AlgebraicGeometry.ProEtale.isEquivalence_etaleInverseImageDerivedConstructible · AlgebraicGeometry.ProEtale.minus_tensor_and_isConstructibleModuleSheaf'_homology · AlgebraicGeometry.ProEtale.minus_and_isConstructibleModuleSheaf'_homology_derivedExtendScalars

Section61.28 Constructible adic sheaves#

Section 61.28 of the Stacks Project, Tag 09BS. 7 tags here are carried by 19 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09BT, a definition

Tag 09BT in the Stacks Project.

AlgebraicGeometry.ProEtale.IsConstructibleAdicSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Constructible/Adic.lean, line 84. The attribute's comment: “part (1): constructible Λ-sheaves”.

A sheaf of Λ-modules on the small pro-étale site is a constructible Λ-sheaf if it is the limit of its quotients by the powers of I and each of those quotients is, as a sheaf of Λ ⧸ Iⁿ-modules, constructible.

abbrev IsConstructibleAdicSheaf (X : Scheme.{u}) (Λ : Type v) [CommRing Λ] [IsNoetherianRing Λ]
    [UnivLE.{u + 1, w}] (I : Ideal Λ)
    [∀ (n : ℕ) (Y : Scheme.{u}),
      HasWeakSheafify (Scheme.ProEt.topology Y) (ModuleCat.{w} (Λ ⧸ I ^ n))]
    [∀ (n : ℕ) (Y : Scheme.{u}) (V : Y.ProEt),
      HasWeakSheafify ((Scheme.ProEt.topology Y).over V) (ModuleCat.{w} (Λ ⧸ I ^ n))]
    [∀ (n : ℕ) {Z Y : Scheme.{u}} (f : Z ⟶ Y),
      ((Scheme.proetaleBaseChange f).sheafPushforwardContinuous
        (ModuleCat.{w} (Λ ⧸ I ^ n)) (Scheme.ProEt.topology Y)
        (Scheme.ProEt.topology Z)).IsRightAdjoint]
    (F : Sheaf (Scheme.ProEt.topology X) (ModuleCat.{w} Λ)) : Prop

AlgebraicGeometry.ProEtale.IsLisse, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Constructible/Adic.lean, line 106. The attribute's comment: “part (2): lisse”.

A constructible Λ-sheaf is lisse if each of its quotients by a power of I is a locally constant sheaf of Λ ⧸ Iⁿ-modules.

abbrev IsLisse (X : Scheme.{u}) (Λ : Type v) [CommRing Λ] [IsNoetherianRing Λ]
    [UnivLE.{u + 1, w}] (I : Ideal Λ)
    [∀ (n : ℕ) (Y : Scheme.{u}),
      HasWeakSheafify (Scheme.ProEt.topology Y) (ModuleCat.{w} (Λ ⧸ I ^ n))]
    [∀ (n : ℕ) (Y : Scheme.{u}) (V : Y.ProEt),
      HasWeakSheafify ((Scheme.ProEt.topology Y).over V) (ModuleCat.{w} (Λ ⧸ I ^ n))]
    [∀ (n : ℕ) {Z Y : Scheme.{u}} (f : Z ⟶ Y),
      ((Scheme.proetaleBaseChange f).sheafPushforwardContinuous
        (ModuleCat.{w} (Λ ⧸ I ^ n)) (Scheme.ProEt.topology Y)
        (Scheme.ProEt.topology Z)).IsRightAdjoint]
    (F : Sheaf (Scheme.ProEt.topology X) (ModuleCat.{w} Λ)) : Prop

AlgebraicGeometry.ProEtale.IsAdicConstructible, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Constructible/Adic.lean, line 128. The attribute's comment: “part (4): adic constructible”.

A sheaf of Λ-modules on the small pro-étale site of X is adic constructible if every affine open of X decomposes into constructible locally closed subschemes on each of which the inverse image of the sheaf is adic lisse.

abbrev IsAdicConstructible (X : Scheme.{u}) (Λ : Type v) [CommRing Λ] (I : Ideal Λ)
    [∀ Y : Scheme.{u}, HasWeakSheafify (Scheme.ProEt.topology Y) (ModuleCat.{w} Λ)]
    [∀ (Y : Scheme.{u}) (V : Y.ProEt),
      HasWeakSheafify ((Scheme.ProEt.topology Y).over V) (ModuleCat.{w} Λ)]
    [∀ {Z Y : Scheme.{u}} (f : Z ⟶ Y),
      ((Scheme.proetaleBaseChange f).sheafPushforwardContinuous
        (ModuleCat.{w} Λ) (Scheme.ProEt.topology Y)
        (Scheme.ProEt.topology Z)).IsRightAdjoint]
    (F : Sheaf (Scheme.ProEt.topology X) (ModuleCat.{w} Λ)) : Prop

AlgebraicGeometry.ProEtale.IsConstructibleAdicModuleSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Constructible/AdicModuleSheaf.lean, line 95. The attribute's comment: “part (1): constructible Λ-sheaves”.

Stacks 09BT (1). A sheaf of Λ-modules on the small pro-étale site is a constructible Λ-sheaf if it is the limit of its quotients by the powers of I and each of those quotients is, as a sheaf of Λ ⧸ Iⁿ-modules, constructible.

def IsConstructibleAdicModuleSheaf [IsNoetherianRing Λ]
    (F : Sheaf (Scheme.ProEt.topology X) (ModuleCat.{max (u + 1) v w} Λ)) : Prop

AlgebraicGeometry.ProEtale.IsLisseAdicModuleSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Constructible/AdicModuleSheaf.lean, line 111. The attribute's comment: “part (2): lisse”.

Stacks 09BT (2). A constructible Λ-sheaf is lisse if each of its quotients by a power of I is a locally constant sheaf of Λ ⧸ Iⁿ-modules.

def IsLisseAdicModuleSheaf [IsNoetherianRing Λ]
    (F : Sheaf (Scheme.ProEt.topology X) (ModuleCat.{max (u + 1) v w} Λ)) : Prop

AlgebraicGeometry.ProEtale.IsAdicConstructibleModuleSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Constructible/AdicModuleSheaf.lean, line 137. The attribute's comment: “part (4): adic constructible”.

Stacks 09BT (4). A sheaf of Λ-modules on the small pro-étale site of X is adic constructible if every affine open of X decomposes into constructible locally closed subschemes on each of which the inverse image of the sheaf is adic lisse.

def IsAdicConstructibleModuleSheaf
    (F : Sheaf (Scheme.ProEt.topology X) (ModuleCat.{max (u + 1) v w} Λ)) : Prop

AlgebraicGeometry.ProEtale.IsAdicLisse, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ExtensionByZero/AdicSheaves.lean, line 77. The attribute's comment: “adic_lisse_sheaf”.

A sheaf which is pro-étale locally the completed constant sheaf of a fixed I-adically complete module with finite quotient modulo I.

abbrev IsAdicLisse (X : Scheme.{u}) (Λ : Type v) [CommRing Λ] (I : Ideal Λ)
    [HasWeakSheafify (Scheme.ProEt.topology X) (ModuleCat.{w} Λ)]
    (F : Sheaf (Scheme.ProEt.topology X) (ModuleCat.{w} Λ)) : Prop
Tag 09BU, a lemma

Tag 09BU in the Stacks Project.

AlgebraicGeometry.ProEtale.exists_isLisseAdicModuleSheaf_stratification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Constructible/LisseStratification.lean, line 541. References: SGA 4½ Rapport (2.5), “more general”.

Stacks 09BU. Let X be a Noetherian scheme, Λ a Noetherian ring and I ⊆ Λ an ideal. A constructible Λ-sheaf on X_proet is lisse on the strata of a finite partition of X into constructible locally closed subschemes.

theorem exists_isLisseAdicModuleSheaf_stratification [IsNoetherianRing Λ] {X : Scheme.{u}}
    [IsNoetherian X]
    (I : Ideal Λ) {F : Sheaf (Scheme.ProEt.topology X) (ModuleCat.{max (u + 1) v w} Λ)}
    (hF : IsConstructibleAdicModuleSheaf.{w} X Λ I F) :
    ∃ s : Scheme.ConstructibleStratification X ⊤, ∀ i, IsLisseAdicModuleSheaf.{w} (s.piece i) Λ I
      ((proetaleModuleInverseImage.{u, v, w} (s.inclusion i) Λ).obj F)
Tag 09BV, a lemma

Tag 09BV in the Stacks Project.

AlgebraicGeometry.ProEtale.exists_iso_completedConstantSheaf_of_isConstant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Constructible/ConstantAdicCompletedIso.lean, line 169. The attribute's comment: “the sheaf is the completed constant sheaf of a finite complete module”.

Let X be a scheme whose pro-étale topos is not empty, let Λ be a Noetherian ring and I ⊆ Λ an ideal, and let F be a sheaf of Λ-modules on the small pro-étale site of X such that

  1. F is the limit of its adic reductions F / IⁿF,
  2. every F / IⁿF is a constant sheaf, and
  3. F / IF is the constant sheaf of a finite module.

Then F ≅ M̲^∧ for an I-adically complete Λ-module M which is finite over Λ^∧.

theorem exists_iso_completedConstantSheaf_of_isConstant
    (hne : ∃ U : X.ProEt, (⊥ : Sieve U) ∉ Scheme.ProEt.topology X U)
    (F : Sheaf (Scheme.ProEt.topology X) (ModuleCat.{max (u + 1) w} Λ))
    (Q : ℕᵒᵖ ⥤ Sheaf (Scheme.ProEt.topology X) (ModuleCat.{max (u + 1) w} Λ))
    (q : (Functor.const ℕᵒᵖ).obj F ⟶ Q)
    (hq : ∀ n : ℕ, IsQuotientBy X Λ (I ^ n) F (Q.obj (op n)) (q.app (op n)))
    (hlim : IsLimit (Limits.Cone.mk F q))
    (hconst : ∀ n : ℕ, ∃ N : ModuleCat.{max (u + 1) w} Λ,
      Nonempty ((constantSheaf (Scheme.ProEt.topology X)
        (ModuleCat.{max (u + 1) w} Λ)).obj N ≅ Q.obj (op n)))
    (hfin : ∃ N : ModuleCat.{max (u + 1) w} Λ,
      Module.Finite Λ (N : Type (max (u + 1) w)) ∧
      Nonempty ((constantSheaf (Scheme.ProEt.topology X)
        (ModuleCat.{max (u + 1) w} Λ)).obj N ≅ Q.obj (op 1))) :
    ∃ M : ModuleCat.{max (u + 1) w} Λ,
      IsAdicComplete I (M : Type (max (u + 1) w)) ∧
      Module.Finite (AdicCompletion I Λ) (AdicCompletion I (M : Type (max (u + 1) w))) ∧
      Nonempty (F ≅ completedConstantSheaf X Λ I M)

Stacks.ModuleSheaf.exists_finite_isAdicComplete_constantSheaf_iso_of_isConstant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Constructible/ConstantAdicQuotientTower.lean, line 355. The attribute's comment: “the coefficient module, on any site with a terminal object”.

Stacks 09BV, the coefficient module, on a site with a terminal object. Let Λ be Noetherian, I ⊆ Λ an ideal and F a sheaf of Λ-modules on a site with a terminal object whose topos is not empty, whose reductions F / IⁿF are constant sheaves and whose first reduction is the constant sheaf of a finite module. Then there is an I-adically complete Λ-module M, finite over Λ^∧ and with every reduction M / IⁿM finite over Λ, whose tower of constant reductions is termwise isomorphic to the adic quotient tower of F.

theorem exists_finite_isAdicComplete_constantSheaf_iso_of_isConstant (I : Ideal Λ)
    (hne : ∃ U : C, (⊥ : Sieve U) ∉ J U)
    (F : Sheaf J (ModuleCat.{w} Λ))
    (Q : ℕᵒᵖ ⥤ Sheaf J (ModuleCat.{w} Λ))
    (q : (Functor.const ℕᵒᵖ).obj F ⟶ Q)
    (hq : ∀ n : ℕ, IsQuotientBy J Λ (I ^ n) F (Q.obj (op n)) (q.app (op n)))
    (hconst : ∀ n : ℕ, ∃ N : ModuleCat.{w} Λ,
      Nonempty ((constantSheaf J (ModuleCat.{w} Λ)).obj N ≅
        Q.obj (op n)))
    (hfin : ∃ N : ModuleCat.{w} Λ, Module.Finite Λ (N : Type w) ∧
      Nonempty ((constantSheaf J (ModuleCat.{w} Λ)).obj N ≅
        Q.obj (op 1))) :
    ∃ M : ModuleCat.{w} Λ, IsAdicComplete I (M : Type w) ∧
      Module.Finite Λ ((M : Type w) ⧸ (I • ⊤ : Submodule Λ (M : Type w))) ∧
      Module.Finite (AdicCompletion I Λ) (AdicCompletion I (M : Type w)) ∧
      (∀ n : ℕ, Module.Finite Λ ((M : Type w) ⧸ (I ^ n • ⊤ : Submodule Λ (M : Type w)))) ∧
      ∀ n : ℕ, Nonempty ((adicQuotientModuleSystem Λ I M ⋙
        constantSheaf J (ModuleCat.{w} Λ)).obj (op n) ≅
          Q.obj (op n))

AlgebraicGeometry.ProEtale.exists_finite_isAdicComplete_constantSheaf_iso_of_isConstant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Constructible/ConstantAdicReductions.lean, line 475. The attribute's comment: “the finite complete coefficient module and its termwise constant reductions”.

Stacks 09BV, the coefficient module. Let Λ be Noetherian, I ⊆ Λ an ideal and F a sheaf of Λ-modules on the small pro-étale site whose reductions F / IⁿF are constant sheaves and whose first reduction is of finite type. Then there is an I-adically complete Λ-module M, finite over Λ^∧ and with every reduction M / IⁿM finite over Λ, whose tower of constant reductions is termwise isomorphic to the adic quotient tower of F.

theorem exists_finite_isAdicComplete_constantSheaf_iso_of_isConstant (I : Ideal Λ)
    (hne : ∃ U : X.ProEt, (⊥ : Sieve U) ∉ Scheme.ProEt.topology X U)
    (F : Sheaf (Scheme.ProEt.topology X) (ModuleCat.{w} Λ))
    (Q : ℕᵒᵖ ⥤ Sheaf (Scheme.ProEt.topology X) (ModuleCat.{w} Λ))
    (q : (Functor.const ℕᵒᵖ).obj F ⟶ Q)
    (hq : ∀ n : ℕ, IsQuotientBy X Λ (I ^ n) F (Q.obj (op n)) (q.app (op n)))
    (hconst : ∀ n : ℕ, ∃ N : ModuleCat.{w} Λ,
      Nonempty ((constantSheaf (Scheme.ProEt.topology X) (ModuleCat.{w} Λ)).obj N ≅
        Q.obj (op n)))
    (hfin : ∃ N : ModuleCat.{w} Λ, Module.Finite Λ (N : Type w) ∧
      Nonempty ((constantSheaf (Scheme.ProEt.topology X) (ModuleCat.{w} Λ)).obj N ≅
        Q.obj (op 1))) :
    ∃ M : ModuleCat.{w} Λ, IsAdicComplete I (M : Type w) ∧
      Module.Finite Λ ((M : Type w) ⧸ (I • ⊤ : Submodule Λ (M : Type w))) ∧
      Module.Finite (AdicCompletion I Λ) (AdicCompletion I (M : Type w)) ∧
      (∀ n : ℕ, Module.Finite Λ ((M : Type w) ⧸ (I ^ n • ⊤ : Submodule Λ (M : Type w)))) ∧
      ∀ n : ℕ, Nonempty ((adicQuotientModuleSystem Λ I M ⋙
        constantSheaf (Scheme.ProEt.topology X) (ModuleCat.{w} Λ)).obj (op n) ≅
          Q.obj (op n))
Tag 09BW, a lemma

Tag 09BW in the Stacks Project.

AlgebraicGeometry.ProEtale.isAdicLisse_of_isLisseAdicModuleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Constructible/AdicLisse.lean, line 62.

Stacks 09BW. Let X be a connected scheme, Λ a Noetherian ring and I ⊆ Λ an ideal. A lisse constructible Λ-sheaf on the small pro-étale site of X is adic lisse.

theorem isAdicLisse_of_isLisseAdicModuleSheaf [ConnectedSpace X] [IsNoetherianRing Λ]
    {F : Sheaf (Scheme.ProEt.topology X) (ModuleCat.{max (u + 1) v w} Λ)}
    (hF : IsLisseAdicModuleSheaf.{w} X Λ I F) : IsAdicLisse X Λ I F
Tag 09BX, a lemma

Tag 09BX in the Stacks Project.

AlgebraicGeometry.ProEtale.isAdicConstructibleModuleSheaf_of_isConstructibleAdicModuleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Constructible/AdicConstructible.lean, line 84.

Stacks 09BX. Let X be a Noetherian scheme, Λ a Noetherian ring and I ⊆ Λ an ideal. A constructible Λ-sheaf on the small pro-étale site of X is adic constructible: it is lisse on the strata of a finite partition of X (Stacks 09BU).

theorem isAdicConstructibleModuleSheaf_of_isConstructibleAdicModuleSheaf [IsNoetherianRing Λ]
    {X : Scheme.{u}} [IsNoetherian X]
    {F : Sheaf (Scheme.ProEt.topology X) (ModuleCat.{max (u + 1) v w} Λ)}
    (hF : IsConstructibleAdicModuleSheaf.{w} X Λ I F) :
    IsAdicConstructibleModuleSheaf.{w} X Λ I F
Tag 09BY, a lemma

Tag 09BY in the Stacks Project.

AlgebraicGeometry.RingedSite.isZero_of_isDerivedComplete_of_idealProduct_eq_top_of_slicedObjectsSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/AdicCompletionCriterion.lean, line 1152. The attribute's comment: “generalized to a ringed site with a covering collection of objects testing surjectivity of sheaves of sets in the module universe, on the site and on its slices, and to an arbitrary sheaf of ideals; the Small and HasSheafify hypotheses that used to exclude the pro-etale site are gone, but the sliced bundle is not yet constructed for that site, so the pro-etale site is still NOT an instance of this statement”.

Stacks 09BY. A sheaf of modules on a ringed site with enough weakly contractible objects which is derived complete along a sheaf of ideals and satisfies IF = F, that is whose adic quotient F/IF vanishes, is zero. The sheaf of ideals is assumed finitely generated on sections over the weakly contractible objects.

This generalizes the content of the tag, whose site is X_proétale and whose coefficients are a constant ring Λ with a finitely generated ideal I: the site here is any ringed site with enough weakly contractible objects, I is any sheaf of ideals, and the finite-generation requirement is weaker than the source's, being asked only on sections over weakly contractible objects.

The weakly contractible objects enter only through the bundle hX, whose members test surjectivity of sheaves of sets valued in the module universe max u v, on the site and on each of its slice sites. That is what makes the statement readable at a site whose objects outnumber its morphisms. The small pro-étale site of a scheme is such a site: it is a RingedSite.{u + 1, u, _} — for instance AlgebraicGeometry.ProEtale.constantCoefficientRingedSite, which is X_proétale ringed by the constant sheaf Λ̲ — and its weak contractibility cannot be tested at the morphism universe u at all, since Small.{u} X.ProEt is false: the objects of X.ProEt lie in Type (u + 1) and the site is small, and essentially small, only at u + 1.

theorem isZero_of_isDerivedComplete_of_idealProduct_eq_top_of_slicedObjectsSituation
    (X : RingedSite.{u, v, max u v})
    [HasSheafify X.J AddCommGrpCat.{max u v}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{max u v}]
    (hX : Stacks.WeaklyContractible.SlicedObjectsSituation.{w, v, u, max u v} X.C X.J)
    (I : SheafOfModules.Submodule
      (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hI : ∀ U : X.C, hX.B U →
      (I.toSubmodule.obj (op U)).FG)
    (F : SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    (hF : AlgebraicGeometry.RingedSite.IsDerivedComplete X I
      ((DerivedCategory.singleFunctor
        (SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj F))
    (hIF : idealPowerProduct X I F 1 = ⊤) :
    IsZero F

AlgebraicGeometry.RingedSite.isZero_of_isDerivedComplete_of_idealProduct_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/AdicCompletionCriterion.lean, line 1424.

Stacks 09BY. A sheaf of modules on a ringed site with enough weakly contractible objects which is derived complete along a sheaf of ideals and satisfies IF = F, that is whose adic quotient F/IF vanishes, is zero. The sheaf of ideals is assumed finitely generated on sections over the weakly contractible objects.

theorem isZero_of_isDerivedComplete_of_idealProduct_eq_top
    (X : RingedSite.{u, v, max u v}) [Small.{v} X.C]
    [HasSheafify X.J (Type v)]
    [HasSheafify X.J AddCommGrpCat.{max u v}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{max u v}]
    (hX : X.J.HasEnoughWeaklyContractibleObjects)
    (I : SheafOfModules.Submodule
      (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hI : ∀ U : X.C, X.J.IsWeaklyContractible U →
      (I.toSubmodule.obj (op U)).FG)
    (F : SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    (hF : AlgebraicGeometry.RingedSite.IsDerivedComplete X I
      ((DerivedCategory.singleFunctor
        (SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj F))
    (hIF : idealPowerProduct X I F 1 = ⊤) :
    IsZero F

AlgebraicGeometry.RingedSite.isZero_of_isDerivedComplete_of_idealProduct_eq_top_of_sliceTestingFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/AdicCompletionCriterionSliceTesting.lean, line 796.

Stacks 09BY. A sheaf of modules on a ringed site with enough weakly contractible objects which is derived complete along a sheaf of ideals and satisfies IF = F, that is whose adic quotient F/IF vanishes, is zero. The sheaf of ideals is assumed finitely generated on sections over the weakly contractible objects.

theorem isZero_of_isDerivedComplete_of_idealProduct_eq_top_of_sliceTestingFamily
    (X : RingedSite.{u, v, max u v w})
    [HasSheafify X.J AddCommGrpCat.{max u v w}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{max u v w}]
    (B : Stacks.WeaklyContractible.SliceTestingFamily.{max u v w} X.C X.J)
    (I : SheafOfModules.Submodule
      (SheafOfModules.unit (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (hI : ∀ U : X.C, B.B U →
      (I.toSubmodule.obj (op U)).FG)
    (F : SheafOfModules.{max u v w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    (hF : AlgebraicGeometry.RingedSite.IsDerivedComplete.{u, v, max u v w, max u v w} X I
      ((DerivedCategory.singleFunctor
        (SheafOfModules.{max u v w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) 0).obj F))
    (hIF : idealPowerProductOfSize X I F 1 = ⊤) :
    IsZero F

AlgebraicGeometry.ProEtale.isZero_of_isDerivedComplete_constantCoefficients, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteConstantCoefficients.lean, line 249.

[Stacks, Tag 09BY]. Let X be a scheme, let Λ be a ring with a finitely generated ideal I ⊂ Λ, and let ℱ be a sheaf of Λ-modules on X_proétale — a sheaf of modules over the constant coefficient ring sheaf Λ̲. If ℱ is derived complete along the ideal sheaf IΛ̲ cut out by I, and ℱ/Iℱ = 0, then ℱ = 0.

This is the tag's own statement at the tag's own objects. It is AlgebraicGeometry.ProEtale.isZero_of_isDerivedComplete_proetale — the chapter's lemma at the small pro-étale site for an arbitrary sheaf of rings and an arbitrary sheaf of ideals — read at 𝒪 = Λ̲ and ℐ = AlgebraicGeometry.ProEtale.constantCoefficientIdealSheaf, with that statement's finite-generation hypothesis discharged by AlgebraicGeometry.ProEtale.fg_constantCoefficientIdealSheaf_obj. The two ringed sites agree on the nose, so no transport is needed at this step.

Λ is an arbitrary commutative ring: I.FG is the only hypothesis on the coefficients, as in the source. The hypothesis hIF says the first ideal power product is everything, which is the vanishing of the adic quotient ℱ/Iℱ.

theorem isZero_of_isDerivedComplete_constantCoefficients (X : Scheme.{u}) (Λ : Type u)
    [CommRing Λ] (I : Ideal Λ) (hI : I.FG)
    (F : SheafOfModules.{u + 1}
      (Stacks.SheafOfModules.Tensor.ringSheaf (constantCoefficientRingedSite.{u, u, u} X Λ).O))
    (hF : RingedSite.IsDerivedComplete.{u + 1, u, u + 1, u + 1}
      (constantCoefficientRingedSite.{u, u, u} X Λ)
      (constantCoefficientIdealSheaf.{u, u, u} X Λ I)
      ((DerivedCategory.singleFunctor
        (SheafOfModules.{u + 1}
          (Stacks.SheafOfModules.Tensor.ringSheaf
            (constantCoefficientRingedSite.{u, u, u} X Λ).O)) 0).obj F))
    (hIF : RingedSite.idealPowerProduct (constantCoefficientRingedSite.{u, u, u} X Λ)
      (constantCoefficientIdealSheaf.{u, u, u} X Λ I) F 1 = ⊤) :
    IsZero F
Tag 09BZ, a lemma

Tag 09BZ in the Stacks Project.

AlgebraicGeometry.ProEtale.exists_epi_biproduct_completedConstantCoefficientSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/CompletedConstantSheafMaps.lean, line 737. The attribute's comment: “F/IF is only assumed of finite type, which a locally constant sheaf of finite type is”.

Derived complete sheaves are quotients of finite sums of \underline{Λ}^∧. Let X be a weakly contractible affine scheme, Λ a Noetherian ring and I ⊆ Λ an ideal. Let F be a derived complete sheaf of Λ-modules on X_proét with F/IF of finite type, for instance locally constant of finite type. Then there are an integer t and a surjection (\underline{Λ}^∧)^{⊕ t} → F.

theorem exists_epi_biproduct_completedConstantCoefficientSheaf [IsAffine X]
    (hX : IsWeaklyContractibleObj X)
    (F : RingedSite.Modules.{u + 1, u, max (u + 1) w}
      (constantCoefficientRingedSite.{u, max (u + 1) w, w} X Λ))
    (hF : RingedSite.IsDerivedComplete.{u + 1, u, max (u + 1) w, w}
      (constantCoefficientRingedSite.{u, max (u + 1) w, w} X Λ)
      (constantCoefficientIdealSheaf.{u, max (u + 1) w, w} X Λ I)
      ((DerivedCategory.singleFunctor _ 0).obj F))
    (hFI : (cokernel (RingedSite.idealPowerProductOfSize.{u + 1, u, w} _
      (constantCoefficientIdealSheaf.{u, max (u + 1) w, w} X Λ I) F 1).ι).IsFiniteType) :
    ∃ (t : ℕ) (α : (⨁ fun _ : Fin t =>
        (completedConstantCoefficientSheafFunctor.{u, max (u + 1) w, w} X Λ I).obj
          (Functor.unitModule Λ)) ⟶ F), Epi α

AlgebraicGeometry.ProEtale.exists_epi_sigma_completedConstantSheaf_of_isDerivedComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/DerivedCompleteFiniteGeneration.lean, line 682.

[Stacks, Tag 09BZ]. Let X be a weakly contractible affine scheme, let Λ be a Noetherian ring and let I ⊂ Λ be an ideal. Let ℱ be a sheaf of Λ-modules on X_proétale which is derived complete, and such that ℱ/Iℱ is a locally constant sheaf of Λ/I-modules of finite type. Then there is an integer t and a surjection (Λ̲^∧)^{⊕t} ⟶ ℱ.

theorem exists_epi_sigma_completedConstantSheaf_of_isDerivedComplete
    [IsAffine X] (hX : ProetaleWContractible.IsWeaklyContractibleObj X)
    (F : RingedSite.Modules.{u + 1, u, u + 1} (constantCoefficientRingedSite.{u, u + 1, u} X Λ))
    (hF : RingedSite.IsDerivedComplete.{u + 1, u, u + 1, u + 1}
      (constantCoefficientRingedSite.{u, u + 1, u} X Λ)
      (constantCoefficientIdealSheaf.{u, u + 1, u} X Λ I)
      ((DerivedCategory.singleFunctor _ 0).obj F))
    (hFI : ∃ G : Sheaf (Scheme.ProEt.topology X) (ModuleCat.{u + 1} (Λ ⧸ I)),
      Stacks.ConstantSheaf.IsFiniteTypeLocallyConstant (Λ ⧸ I) (Scheme.ProEt.topology X) G ∧
      Nonempty ((toCoefficientModuleSheaf.{u, u + 1, u} X Λ).obj
          (cokernel (RingedSite.idealPowerProduct (constantCoefficientRingedSite.{u, u + 1, u} X Λ)
            (constantCoefficientIdealSheaf.{u, u + 1, u} X Λ I) F 1).ι) ≅
        (restrictQuotientScalars.{u + 1, u + 1, u} X Λ I).obj G)) :
    ∃ t : ℕ, ∃ α : (∐ fun _ : Fin t =>
        (moduleSheafOverConstantCoefficientsFunctor.{u, u + 1, u} X Λ).obj
          (Stacks.ConstantSheaf.completedConstantSheaf (Scheme.ProEt.topology X) I)) ⟶ F,
      Epi α
Sources
LeanAlgebraicGeometry.ProEtale.IsConstructibleAdicSheaf · AlgebraicGeometry.ProEtale.IsLisse · AlgebraicGeometry.ProEtale.IsAdicConstructible · AlgebraicGeometry.ProEtale.IsConstructibleAdicModuleSheaf · AlgebraicGeometry.ProEtale.IsLisseAdicModuleSheaf · AlgebraicGeometry.ProEtale.IsAdicConstructibleModuleSheaf · AlgebraicGeometry.ProEtale.IsAdicLisse · AlgebraicGeometry.ProEtale.exists_isLisseAdicModuleSheaf_stratification

Section61.29 A suitable derived category#

Section 61.29 of the Stacks Project, Tag 09C0. 7 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09C1, a definition

Tag 09C1 in the Stacks Project.

AlgebraicGeometry.ProEtale.IsConstructibleDerivedSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ConstructibleComplexes.lean, line 254. The attribute's comment: “constructible objects”.

Stacks 09C1. An object K of D(X_proét, Λ) is constructible with respect to the ideal I of the Noetherian coefficient ring Λ when it is derived complete along the ideal sheaf cut out by I, and its derived reduction K ⊗_Λ^L Λ/I, formed with the derived base change T, has constructible cohomology sheaves and locally has finite Tor dimension measured against the derived tensor products D on the slices.

abbrev IsConstructibleDerivedSheaf
    (T : DerivedReduction.{u, r, w} X Λ I)
    (D : ∀ U : (constantCoefficientRingedSite.{u, r, w} X (Λ ⧸ I)).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, max (u + 1) r w,
          max (u + 1) r w + 1}
        ((constantCoefficientRingedSite.{u, r, w} X (Λ ⧸ I)).over U))
    (K : DerivedSheaves.{u, r, w} X Λ) : Prop

AlgebraicGeometry.ProEtale.constructibleDerivedSheaves, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ConstructibleComplexes.lean, line 271. The attribute's comment: “the full subcategory”.

Stacks 09C1. The full subcategory D_cons(X, Λ) of D(X_proét, Λ) on the constructible objects.

abbrev constructibleDerivedSheaves
    (T : DerivedReduction.{u, r, w} X Λ I)
    (D : ∀ U : (constantCoefficientRingedSite.{u, r, w} X (Λ ⧸ I)).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, max (u + 1) r w,
          max (u + 1) r w + 1}
        ((constantCoefficientRingedSite.{u, r, w} X (Λ ⧸ I)).over U))

AlgebraicGeometry.ProEtale.IsConstructibleViaDerivedReduction, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ConstructibleDerivedSheaves.lean, line 131. The attribute's comment: “constructible objects”.

Stacks 09C1. An object K of D(X_proét, Λ) is constructible with respect to the ideal I of the Noetherian coefficient ring Λ when it is derived complete along the ideal sheaf cut out by I, and its derived reduction K ⊗_Λ^L \underline{Λ/I} has constructible cohomology sheaves and locally has finite Tor dimension.

abbrev IsConstructibleViaDerivedReduction (K : DerivedSheaves.{u, max (u + 1) w, w} X Λ) : Prop

AlgebraicGeometry.ProEtale.constructibleDerivedSheavesViaDerivedReduction, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ConstructibleDerivedSheaves.lean, line 142. The attribute's comment: “the full subcategory”.

Stacks 09C1. The full subcategory D_cons(X, Λ) of D(X_proét, Λ) on the constructible objects.

abbrev constructibleDerivedSheavesViaDerivedReduction
Tag 09C2, a lemma

Tag 09C2 in the Stacks Project.

AlgebraicGeometry.ProEtale.hasConstructibleCohomology_derivedReduction_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ConstructibleReductions.lean, line 106. The attribute's comment: “part (3)”.

The reductions of a constructible complex have constructible cohomology sheaves. If X is quasi-compact and K lies in D_cons(X, Λ), every reduction Kₙ = K ⊗_Λ^L Λ/Iⁿ has constructible cohomology sheaves.

theorem hasConstructibleCohomology_derivedReduction_pow [CompactSpace X]
    {K : DerivedSheaves.{u, max (u + 1) w, w} X Λ}
    (hK : IsConstructibleViaDerivedReduction.{u, w} X Λ I K)
    (n : ℕ) :
    HasConstructibleModuleSheafCohomology.{u, w} X (Λ ⧸ I ^ n)
      ((derivedReduction.{u, w} X Λ (I ^ n)).obj K)

AlgebraicGeometry.ProEtale.exists_isDerivedLimit_derivedReductionTower_and_hasTorAmplitude, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ConstructibleReductions.lean, line 217. The attribute's comment: “parts (1) and (2)”.

Let X be quasi-compact and K an object of D_cons(X, Λ), and set Kₙ = K ⊗_Λ^L \underline{Λ/Iⁿ}. There are integers a and b such that

  1. K = R lim Kₙ, with the reduction maps K ⟶ Kₙ as projections, and Hⁱ(K) = 0 for i ∉ [a, b];
  2. every Kₙ has Tor amplitude in [a, b].

In (1) the tower Kₙ is read in the derived category of sheaves of Λ-modules, as the derived tensor product of K with the constant sheaves \underline{Λ/Iⁿ}; in (2) Kₙ is the derived reduction of K, an object of D(X_proét, Λ/Iⁿ).

theorem exists_isDerivedLimit_derivedReductionTower_and_hasTorAmplitude [CompactSpace X]
    {K : DerivedSheaves.{u, max (u + 1) w, w} X Λ}
    (hK : IsConstructibleViaDerivedReduction.{u, w} X Λ I K) :
    ∃ a b : ℤ,
      (NoetherianAdicCompletion.IsDerivedLimitWithProjections
          (derivedReductionTower.{u, w} X Λ I
            ((derivedModuleEquiv.{u, max (u + 1) w, w} X Λ).inverse.obj K))
          ((derivedModuleEquiv.{u, max (u + 1) w, w} X Λ).inverse.obj K)
          (fun n ↦ (Stacks.ModuleSheaf.derivedReductionMap (Scheme.ProEt.topology X) Λ I
            ((derivedModuleEquiv.{u, max (u + 1) w, w} X Λ).inverse.obj K)).app ⟨n⟩) ∧
        ∀ i : ℤ, i ∉ Set.Icc a b →
          IsZero ((DerivedCategory.homologyFunctor _ i).obj K)) ∧
      ∀ n : ℕ, Stacks.ModuleSheaf.HasTorAmplitude (J := Scheme.ProEt.topology X)
        ((derivedReduction.{u, w} X Λ (I ^ n)).obj K) (Set.Icc a b)

AlgebraicGeometry.ProEtale.exists_etaleInverseImage_iso_derivedReduction_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ConstructibleReductions.lean, line 294. The attribute's comment: “part (4)”.

The reductions of a constructible complex come from the étale site. If X is quasi-compact and K lies in D_cons(X, Λ), every reduction Kₙ = K ⊗_Λ^L Λ/Iⁿ is ε⁻¹ Lₙ for an object Lₙ of D(X_étale, Λ/Iⁿ) with constructible cohomology sheaves and finite Tor dimension.

Here ε⁻¹ on derived categories is ε⁻¹ applied termwise.

theorem exists_etaleInverseImage_iso_derivedReduction_pow [CompactSpace X]
    {K : DerivedSheaves.{u, max (u + 1) w, w} X Λ}
    (hK : IsConstructibleViaDerivedReduction.{u, w} X Λ I K)
    (n : ℕ) :
    ∃ L : DerivedCategory (Sheaf X.smallEtaleTopology (ModuleCat.{max (u + 1) w} (Λ ⧸ I ^ n))),
      (∀ i : ℤ, Scheme.IsConstructibleEtaleModuleSheaf.{u, max (u + 1) w, w} X (Λ ⧸ I ^ n)
        ((DerivedCategory.homologyFunctor _ i).obj L)) ∧
      Stacks.ModuleSheaf.HasFiniteTorDimension (J := X.smallEtaleTopology) L ∧
      Nonempty ((Scheme.etaleInverseImage.{u, w} X (Λ ⧸ I ^ n)).mapDerivedCategory.obj L ≅
        (derivedReduction.{u, w} X Λ (I ^ n)).obj K)
Tag 09C3, a lemma

Tag 09C3 in the Stacks Project.

AlgebraicGeometry.ProEtale.hasFiniteDisjointCompletedConstantModel_of_isLocallyConstant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/LocallyConstantCompletedModel.lean, line 85.

Stacks 09C3. Let X be a weakly contractible affine scheme, Λ a Noetherian ring, I ⊆ Λ an ideal and K an object of D_cons(X, Λ) such that the cohomology sheaves of K ⊗_Λ^L \underline{Λ/I} are locally constant. Then there are a finite disjoint open covering X = ∐ U_i and, for each i, finite projective Λ^∧-modules M^a, …, M^b such that K|_{U_i} is represented in D(U_{i, proét}, Λ) by a complex (\underline{M^a})^∧ → ⋯ → (\underline{M^b})^∧ for some maps of sheaves of Λ-modules between consecutive terms.

The covering, the restrictions and the models are those of AlgebraicGeometry.ProEtale.HasFiniteDisjointCompletedConstantModel; weak contractibility of X is that of Stacks 090L.

theorem hasFiniteDisjointCompletedConstantModel_of_isLocallyConstant [IsAffine X]
    (hX : ProetaleWContractible.IsWeaklyContractibleObj X)
    (K : DerivedSheaves.{u, max (u + 1) w, w} X Λ)
    (hK : IsConstructibleViaDerivedReduction.{u, w} X Λ I K)
    (hloc : ∀ i : ℤ, Stacks.ConstantSheaf.IsLocallyConstant (Scheme.ProEt.topology X)
      ((DerivedCategory.homologyFunctor _ i).obj ((derivedReduction.{u, w} X Λ I).obj K))) :
    HasFiniteDisjointCompletedConstantModel.{u, max (u + 1) w, w} X Λ I K
Tag 09C4, a definition

Tag 09C4 in the Stacks Project.

AlgebraicGeometry.ProEtale.IsAdicConstructibleViaDerivedInverseImage, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/AdicConstructibleComplexes.lean, line 82. The attribute's comment: “part (2): adic constructible”.

Stacks 09C4, part (2). An object K of D(X_proét, Λ) is adic constructible if every affine open U of X admits a decomposition U = ∐ U_i into constructible locally closed subschemes such that every restriction K|_{U_i} is adic lisse.

abbrev IsAdicConstructibleViaDerivedInverseImage (K : DerivedSheaves.{u, r, w} X Λ) : Prop

AlgebraicGeometry.ProEtale.IsAdicLisseDerivedSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ConstructibleComplexes.lean, line 454. The attribute's comment: “part (1): adic lisse”.

Stacks 09C4, part (1). An object K of D(X_proét, Λ) is adic lisse if there is a finite complex M^• of finite projective Λ^∧-modules such that K is pro-étale locally isomorphic to the complex \underline{M^a}^∧ → ⋯ → \underline{M^b}^∧ of completed constant sheaves, whose differentials are those induced by the differentials of M^•.

abbrev IsAdicLisseDerivedSheaf (K : DerivedSheaves.{u, r, w} X Λ) : Prop

AlgebraicGeometry.ProEtale.IsAdicConstructibleDerivedSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ConstructibleComplexes.lean, line 535. The attribute's comment: “part (2): adic constructible”.

Stacks 09C4, part (2). An object K of D(X_proét, Λ) is adic constructible if every affine open of X admits a decomposition into constructible locally closed subschemes on which the restriction of K is adic lisse.

abbrev IsAdicConstructibleDerivedSheaf (K : DerivedSheaves.{u, r, w} X Λ) : Prop
Tag 09C5, a lemma

Tag 09C5 in the Stacks Project.

AlgebraicGeometry.ProEtale.isMittagLefflerCategorical_derivedReductionSectionsSystem_of_isConstructibleViaDerivedReduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/AdicModelReductionSections.lean, line 272. The attribute's comment: “the Mittag-Leffler condition for the inverse system n ↦ H^0(X, K ⊗_Λ^L Λ/I^n) of sections modules, with its canonical transition maps; the hypothesis that each reduction is a complex of constant sheaves is read, as in the source's proof, as K ⊗_Λ^L Λ/I^n ≅ \underline{E_n} for an object E_n of D(Λ/I^n)”.

Stacks 09C5. Let X be a weakly contractible affine scheme, Λ a Noetherian ring, I ⊆ Λ an ideal and K an object of D_cons(X, Λ) such that every reduction K ⊗_Λ^L Λ/Iⁿ is isomorphic, in D(X_proét, Λ/Iⁿ), to a complex of constant sheaves of Λ/Iⁿ-modules. Then the inverse system n ↦ H⁰(X, K ⊗_Λ^L Λ/Iⁿ) of Λ-modules satisfies the Mittag-Leffler condition.

The conclusion is the Mittag-Leffler condition of Stacks Tag 02N0 for the system derivedReductionSectionsSystem X Λ I K', K' being K read in the derived category of sheaves of Λ-modules; its terms are the sections modules H⁰(X, K ⊗_Λ^L Λ/Iⁿ) and its transition maps are induced by the reductions Λ/Iⁿ⁺¹ → Λ/Iⁿ. Constructibility is AlgebraicGeometry.ProEtale.IsConstructibleViaDerivedReduction, and the reductions are AlgebraicGeometry.ProEtale.derivedReduction.

The proof: for a K-flat representative P of K, AlgebraicGeometry.ProEtale.exists_isBoundedAboveFiniteFree_reduction_iso gives a bounded above complex F of finite free Λ^∧-modules whose constant complex has, levelwise, the reductions of P; the sections system of the reductions of \underline{F} is j ↦ Γ(X, \underline{H⁰(F/IʲF)}), which is Mittag-Leffler by the Artin–Rees lemma (AlgebraicGeometry.ProEtale.isMittagLefflerCategorical_constantComplexReductionSections), and Stacks.ModuleSheaf.isMittagLefflerCategorical_reductionSections_of_adicModel transports the condition. Over the empty scheme every term of the system vanishes.

theorem
    isMittagLefflerCategorical_derivedReductionSectionsSystem_of_isConstructibleViaDerivedReduction
    [IsAffine X] (hX : ProetaleWContractible.IsWeaklyContractibleObj X)
    (K : DerivedSheaves.{u, max (u + 1) w, w} X Λ)
    (hK : IsConstructibleViaDerivedReduction.{u, w} X Λ I K)
    (hconstant : ∀ n : ℕ, ∃ E : DerivedCategory (ModuleCat.{max (u + 1) w} (Λ ⧸ I ^ n)),
      Nonempty ((derivedReduction.{u, w} X Λ (I ^ n)).obj K ≅
        (constantSheaf (Scheme.ProEt.topology X)
          (ModuleCat.{max (u + 1) w} (Λ ⧸ I ^ n))).mapDerivedCategory.obj E)) :
    IsMittagLefflerCategorical (derivedReductionSectionsSystem X Λ I
      ((derivedModuleEquiv.{u, max (u + 1) w, w} X Λ).inverse.obj K))

AlgebraicGeometry.ProEtale.isMittagLefflerCategorical_derivedReductionSectionsSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/ConstructibleReductionSections.lean, line 336.

Stacks 09C5. Let X be a weakly contractible affine scheme, Λ a Noetherian ring, I ⊆ Λ an ideal and K an object of D_cons(X, Λ) such that for every n ≥ 1 the reduction K ⊗_Λ^L \underline{Λ/Iⁿ} is isomorphic in D(X_proét, Λ/Iⁿ) to a complex of constant sheaves of Λ/Iⁿ-modules. Then the inverse system n ↦ H⁰(X, K ⊗_Λ^L Λ/Iⁿ) of Λ-modules satisfies the Mittag-Leffler condition.

The reductions in the hypothesis are taken with derived base changes Tn n along Λ → Λ/Iⁿ (any two of which are canonically isomorphic), and a complex of constant sheaves is the constant sheaf functor applied to a complex E of Λ/Iⁿ-modules. The inverse system of the conclusion is AlgebraicGeometry.ProEtale.derivedReductionSectionsSystem: degree-zero cohomology and sections over X of the derived tensor products of K with the constant sheaves \underline{Λ/Iⁿ}, whose transition maps are induced by the reductions Λ/Iⁿ⁺¹ → Λ/Iⁿ; here K is read in the derived category of sheaves of Λ-modules, where the derived tensor product is constructed, through the constant coefficients equivalence.

theorem isMittagLefflerCategorical_derivedReductionSectionsSystem [IsAffine X]
    (hX : ProetaleWContractible.IsWeaklyContractibleObj X)
    (T : DerivedReduction.{u, max (u + 1) w, w} X Λ I)
    (D : ∀ U : (constantCoefficientRingedSite.{u, max (u + 1) w, w} X (Λ ⧸ I)).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, max (u + 1) w,
          max (u + 1) w + 1}
        ((constantCoefficientRingedSite.{u, max (u + 1) w, w} X (Λ ⧸ I)).over U))
    (K : DerivedSheaves.{u, max (u + 1) w, w} X Λ)
    (hK : IsConstructibleDerivedSheaf.{u, max (u + 1) w, w} X Λ I T D K)
    (Tn : ∀ n : ℕ, DerivedReduction.{u, max (u + 1) w, w} X Λ (I ^ n))
    (hconstant : ∀ n : ℕ, 1 ≤ n →
      ∃ E : CochainComplex (ModuleCat.{max (u + 1) w} (Λ ⧸ I ^ n)) ℤ,
        Nonempty ((Tn n).baseChange.obj K ≅ DerivedCategory.Q.obj
          (((constantSheafOverCoefficients.{u, max (u + 1) w, w} X (Λ ⧸ I ^ n)).mapHomologicalComplex
            (ComplexShape.up ℤ)).obj E))) :
    IsMittagLefflerCategorical (derivedReductionSectionsSystem X Λ I
      ((derivedCoefficientModuleSheafEquivalence.{u, max (u + 1) w, w} X Λ).functor.obj K))

AlgebraicGeometry.ProEtale.isMittagLefflerCategorical_reductionSectionsSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/LocallyConstantAdicModel.lean, line 367. The attribute's comment: “the Mittag-Leffler conclusion for the INVERSE SYSTEM over n, stated about the concrete system of sections modules H^0(X, K ⊗_Λ^L Λ/I^n) and proved from the pro-domination of that system by the adic quotient system n ↦ N/I^nN of a Λ-module N. Two things are assumed rather than proved. First, the transition maps of the system are taken as a datum t: the source's are those induced by Λ/I^(n+1) → Λ/I^n, and the comparison of the derived base changes along Λ → Λ/I^(n+1) → Λ/I^n and along Λ → Λ/I^n is not constructed in the library, so the statement is proved for every family t. Second, the pro-domination itself is the output of the source's steps (1)-(6): steps (1)-(5) rest on 09C3 (the local adic model, also not formalized), 0658 (perfectness of the reduction E_1), 09BE (local constancy of a map of complexes of constant sheaves) and 09AW (the complex M^• of finite projective Λ^∧-modules with M^•/I^nM^• ≅ E_n), and step (6) on the Tor spectral sequence together with 0911 (strict pro-vanishing of Tor); that chain is not assembled. What is proved outright is the Mittag-Leffler condition for the sections system from that data, including the surjectivity of the transition maps of the adic quotient system. The source's weak contractibility of X and constructibility of K are not needed for this implication and are carried unused”.

Stacks 09C5, for the inverse system over n, from the pro-domination data that the source's steps (1)–(6) supply.

Let X be a weakly contractible affine scheme, Λ a Noetherian ring, I ⊆ Λ an ideal and K a constructible object of D(X_proét, Λ) such that every reduction K ⊗_Λ^L Λ/Iⁿ is isomorphic, in D(X_proét, Λ/Iⁿ), to a complex of constant sheaves of Λ/Iⁿ-modules. Then the inverse system n ↦ H⁰(X, K ⊗_Λ^L Λ/Iⁿ) of Λ-modules satisfies the Mittag-Leffler condition.

The conclusion is the Mittag-Leffler condition of Stacks Tag 02N0 for the system indexed by n, not a statement about any single n, and it is stated about the concrete system reductionSectionsSystem X Λ I Tn K t whose terms are the sections modules H⁰(X, K ⊗_Λ^L Λ/Iⁿ) themselves.

The setting hypotheses _hX, _hK and _hconstant are not used in the proof: pro-domination of the sections system by an adic quotient system already forces the Mittag-Leffler condition, without weak contractibility of X and without constructibility of K. They are retained, underscore-prefixed, so that the statement reads as the source's; the result is therefore more general than the source, which this charter permits.

theorem isMittagLefflerCategorical_reductionSectionsSystem [IsAffine X]
    (_hX : ProetaleWContractible.IsWeaklyContractibleObj X)
    (T : DerivedReduction.{u, r, w} X Λ I)
    (D : ∀ U : (constantCoefficientRingedSite.{u, r, w} X (Λ ⧸ I)).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, max (u + 1) r w,
          max (u + 1) r w + 1}
        ((constantCoefficientRingedSite.{u, r, w} X (Λ ⧸ I)).over U))
    (K : DerivedSheaves.{u, r, w} X Λ)
    (_hK : IsConstructibleDerivedSheaf.{u, r, w} X Λ I T D K)
    (Tn : ∀ n : ℕ, DerivedReduction.{u, r, w} X Λ (I ^ n))
    (_hconstant : ∀ n : ℕ, IsConstantSheafComplexModel.{u, r, w} X (Λ ⧸ I ^ n)
      ((Tn n).baseChange.obj K))
    (t : ∀ n : ℕ, reductionSectionsObj.{u, r, w} X Λ I Tn K (n + 1) ⟶
      reductionSectionsObj.{u, r, w} X Λ I Tn K n)
    (N : ModuleCat.{max (u + 1) r w} Λ) (c : ℕ)
    (β : ∀ n : ℕ, (adicQuotientModuleSystem Λ I N).obj (op (n + c)) ⟶
      (reductionSectionsSystem.{u, r, w} X Λ I Tn K t).obj (op n))
    (hβ : ∀ (i j : ℕ) (h : i ≤ j),
      (adicQuotientModuleSystem Λ I N).map (homOfLE (Nat.add_le_add_right h c)).op ≫ β i =
        β j ≫ (reductionSectionsSystem.{u, r, w} X Λ I Tn K t).map (homOfLE h).op)
    (α : ∀ n : ℕ, (reductionSectionsSystem.{u, r, w} X Λ I Tn K t).obj (op (n + c)) ⟶
      (adicQuotientModuleSystem Λ I N).obj (op n))
    (hαβ : ∀ n : ℕ, α (n + c) ≫ β n =
      (reductionSectionsSystem.{u, r, w} X Λ I Tn K t).map
        (homOfLE (show n ≤ n + c + c by omega)).op) :
    IsMittagLefflerCategorical (reductionSectionsSystem.{u, r, w} X Λ I Tn K t)
Tag 09C6, a lemma

Tag 09C6 in the Stacks Project.

AlgebraicGeometry.ProEtale.isAdicLisseDerivedSheaf_of_isLocallyConstant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/AdicLisseOfLocallyConstant.lean, line 719. The attribute's comment: “a constructible complex over a connected scheme whose reduction modulo I has locally constant cohomology sheaves is adic lisse”.

Let X be a connected scheme, Λ a Noetherian ring and I ⊆ Λ an ideal. If K is in D_cons(X, Λ) and K ⊗_Λ^L \underline{Λ/I} has locally constant cohomology sheaves, then K is adic lisse.

theorem isAdicLisseDerivedSheaf_of_isLocallyConstant [ConnectedSpace X] [IsNoetherianRing Λ]
    {K : DerivedSheaves.{u, max (u + 1) w, w} X Λ}
    (hK : IsConstructibleViaDerivedReduction.{u, w} X Λ I K)
    (hloc : ∀ i : ℤ, Stacks.ConstantSheaf.IsLocallyConstant (Scheme.ProEt.topology X)
      ((DerivedCategory.homologyFunctor _ i).obj ((derivedReduction.{u, w} X Λ I).obj K))) :
    IsAdicLisseDerivedSheaf.{u, max (u + 1) w, w} X Λ I K
Tag 09C7, a proposition

Tag 09C7 in the Stacks Project.

AlgebraicGeometry.ProEtale.isAdicConstructibleDerivedSheaf_of_isConstructibleDerivedSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/AdicConstructibleOfConstructible.lean, line 46.

Stacks 09C7. Let X be a Noetherian scheme, Λ a Noetherian ring and I ⊆ Λ an ideal. Every object K of D_cons(X, Λ) is adic constructible.

theorem isAdicConstructibleDerivedSheaf_of_isConstructibleDerivedSheaf {X : Scheme.{u}}
    [IsNoetherian X] {Λ : Type (max (u + 1) w)} [CommRing Λ] [IsNoetherianRing Λ] {I : Ideal Λ}
    {K : DerivedSheaves.{u, max (u + 1) w, w} X Λ}
    (hK : IsConstructibleViaDerivedReduction.{u, w} X Λ I K) :
    IsAdicConstructibleViaDerivedInverseImage.{u, max (u + 1) w, w} X Λ I K
Sources
LeanAlgebraicGeometry.ProEtale.IsConstructibleDerivedSheaf · AlgebraicGeometry.ProEtale.constructibleDerivedSheaves · AlgebraicGeometry.ProEtale.IsConstructibleViaDerivedReduction · AlgebraicGeometry.ProEtale.constructibleDerivedSheavesViaDerivedReduction · AlgebraicGeometry.ProEtale.hasConstructibleCohomology_derivedReduction_pow · AlgebraicGeometry.ProEtale.exists_isDerivedLimit_derivedReductionTower_and_hasTorAmplitude · AlgebraicGeometry.ProEtale.exists_etaleInverseImage_iso_derivedReduction_pow · AlgebraicGeometry.ProEtale.hasFiniteDisjointCompletedConstantModel_of_isLocallyConstant

Section61.30 Proper base change#

Section 61.30 of the Stacks Project, Tag 09C8. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09C9, a theorem

Tag 09C9 in the Stacks Project.

AlgebraicGeometry.ProEtale.isIso_proetaleCompletedBaseChangeMap_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Cohomology/CompletedProperBaseChangeTheorem.lean, line 100.

Stacks 09C9 (proper base change for derived complete complexes). Let f : X ⟶ Y be a proper morphism of schemes and g : Y' ⟶ Y a morphism, with base change square sq : IsPullback g' f' f g. Let Λ be a Noetherian ring and I ⊆ Λ an ideal such that Λ/I is torsion. Let K be an object of D(X_proétale, Λ) such that 1. K is derived complete, 2. K ⊗^L_Λ Λ/Iⁿ is bounded below with cohomology sheaves coming from X_étale, and 3. Λ/Iⁿ is a perfect Λ-module, for every n ≥ 1. Then the base change map Lg^*_comp Rf_* K ⟶ Rf'_* L(g')^*_comp K is an isomorphism.

theorem isIso_proetaleCompletedBaseChangeMap_of_isProper [IsNoetherianRing Λ] (I : Ideal Λ)
    (hI : AddMonoid.IsTorsion (Λ ⧸ I))
    {X Y X' Y' : Scheme.{u}} (f : X ⟶ Y) [IsProper f] (g : Y' ⟶ Y) (g' : X' ⟶ X) (f' : X' ⟶ Y')
    (sq : IsPullback g' f' f g)
    (K : ProetaleDerivedCategory Λ X) (hK : IsDerivedComplete I K)
    (hbdd : ∀ n : ℕ, 1 ≤ n → ∃ a : ℤ, ((proetaleDerivedReduction Λ I X n).obj K).IsGE a)
    (het : ∀ n : ℕ, 1 ≤ n → ∀ q : ℤ, (Scheme.etaleInverseImage.{u, 0, u + 1} X Λ).essImage
      ((DerivedCategory.homologyFunctor _ q).obj ((proetaleDerivedReduction Λ I X n).obj K)))
    (hperf : ∀ n : ℕ, 1 ≤ n → StacksDraft.Perfect.IsPerfectModule (R := Λ) (Λ ⧸ I ^ n)) :
    IsIso (proetaleCompletedBaseChangeMap Λ I f g f' g' sq.w.symm K)
Sources
LeanAlgebraicGeometry.ProEtale.isIso_proetaleCompletedBaseChangeMap_of_isProper

Section61.31 Change of partial universe#

Section 61.31 of the Stacks Project, Tag 0F4R. 4 tags here are carried by 23 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 098J, a lemma

Tag 098J in the Stacks Project.

AlgebraicGeometry.ProEtale.exists_covering_refining_proetaleCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/PartialUniverseChange.lean, line 114.

Stacks 098J. Let B be a chosen big pro-étale site and T one of its objects. Let {Z i → T}_{i ∈ I} be an arbitrary pro-étale covering of the underlying scheme of T: the index type I is unrestricted and the members Z i are arbitrary schemes, so neither the family nor its sources need belong to the chosen site. Then there is a covering family E of T in the site — one of the chosen bounded pro-étale families — which refines {Z i → T}: every member of E factors through some member of the given covering.

The family E is built by covering T inside the site by affine objects with w-contractible global sections (Stacks 098I), refining the pullback of the given covering over each of them by a finite disjoint clopen decomposition (Stacks 098F), and taking a chosen representative of the composite.

theorem exists_covering_refining_proetaleCovering (B : BigProetaleSite.{u}) (T : B.Scheme)
    {I : Type w} (Z : I → Scheme.{u}) (g : (i : I) → Z i ⟶ T.obj)
    (hcov : Presieve.ofArrows Z g ∈ Scheme.proetalePrecoverage.coverings T.obj) :
    ∃ E : PreZeroHypercover.{u + 1} T, B.covering ⟨T, E⟩ ∧
      ∀ j : E.I₀, ∃ (i : I) (h : (E.X j).obj ⟶ Z i),
        h ≫ g i = B.inclusion.map (E.f j)
Tag 098Y, a lemma

Tag 098Y in the Stacks Project.

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.fullyFaithfulSmallFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/SmallEnlargement.lean, line 116. The attribute's comment: “hypothesis (c) of 00XU for the inclusion of the small sites: full faithfulness”.

Stacks 098Y, hypothesis (c) of Stacks 00XU: the inclusion of the two small pro-étale sites of S is fully faithful.

Both small sites are full subcategories of nested big pro-étale categories over S, and the inclusion of those is fully faithful.

def fullyFaithfulSmallFunctor : (h.smallFunctor S hS).FullyFaithful

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.smallFunctor_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/SmallEnlargement.lean, line 142. The attribute's comment: “hypotheses (d) and (e) of 00XU for the inclusion of the small sites: preservation of fibre products and of the final object”.

Stacks 098Y, hypotheses (d) and (e) of Stacks 00XU: fibre products exist in the smaller small pro-étale site and are preserved by the inclusion, which also carries the final object S/S to the final object S/S.

Both small sites have fibre products and the final object 𝟙 S (Stacks 098M), both computed in the ambient big pro-étale category over S; the inclusion therefore preserves all finite limits.

theorem smallFunctor_preservesFiniteLimits : PreservesFiniteLimits (h.smallFunctor S hS)

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.smallFunctor_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/SmallEnlargement.lean, line 182. The attribute's comment: “hypothesis (a) of 00XU for the inclusion of the small sites: cocontinuity”.

Stacks 098Y, hypothesis (a) of Stacks 00XU: the inclusion of the two small pro-étale sites of S is cocontinuous.

A covering sieve of the larger small site at an object X of the smaller one contains a covering family of the larger small site, whose image in the larger big pro-étale category is a chosen covering family there, hence an arbitrary pro-étale covering of the scheme underlying X. By Stacks 098J that covering is refined by a chosen covering family of the smaller big site. The members of the refining family are weakly étale over X, being members of a pro-étale covering, hence weakly étale over S, so the family is a covering family of the smaller small site; and each of its members factors through a member of the given family, over S because the factorization is compatible with the maps to X.

instance smallFunctor_isCocontinuous :
    (h.smallFunctor S hS).IsCocontinuous (SmallProetale.topology B S hS)
      (SmallProetale.topology B' S (h.contains hS))

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.smallFunctor_isMorphismOfSites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/SmallEnlargement.lean, line 263. The attribute's comment: “hypothesis (b) of 00XU for the inclusion of the small sites: continuity, in the form of being a morphism of sites”.

Stacks 098Y, hypothesis (b) of Stacks 00XU: the inclusion of the two small pro-étale sites of S is continuous, and in fact defines a morphism of sites.

Continuity follows from cover-preservation because the inclusion is representably flat, being left exact; the left adjoint of the pushforward on sheaves of sets is the sheafified left Kan extension, which is left exact for the same reason.

theorem smallFunctor_isMorphismOfSites :
    _root_.IsMorphismOfSites.{u + 1} (h.smallFunctor S hS)
      (SmallProetale.topology B S hS) (SmallProetale.topology B' S (h.contains hS))

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.smallToposRetraction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/SmallEnlargement.lean, line 303. The attribute's comment: “the two morphisms of topoi of the small sites, with f ∘ g isomorphic to the identity and f_* = g^{-1}”.

Stacks 098Y, the conclusion of Stacks 00XU for the two small pro-étale sites of S: the morphisms of topoi g : Sh(S_proetale) → Sh(S'_proetale) and f : Sh(S'\_proetale) → Sh(S\_proetale) induced by the inclusion, whose composite is isomorphic to the identity and which satisfy f_* = g^{-1}.

The direct image of g is the cocontinuous pushforward and the direct image of f is the continuous pushforward, which is also the inverse image of g; that is the identification f_* = g^{-1}. The retraction is the counit of the adjunction g^{-1} ⊣ g_*, invertible because the inclusion is fully faithful and cocontinuous.

noncomputable def smallToposRetraction :
    letI : (h.smallFunctor S hS).IsCocontinuous (SmallProetale.topology B S hS)
        (SmallProetale.topology B' S (h.contains hS)) := h.smallFunctor_isCocontinuous S hS
    letI : (h.smallFunctor S hS).IsContinuous (SmallProetale.topology B S hS)
        (SmallProetale.topology B' S (h.contains hS)) :=
      (h.smallFunctor_isMorphismOfSites S hS).toIsContinuous
    ToposRetraction (SmallProetale B S hS) (SmallProetale B' S (h.contains hS))
      (SmallProetale.topology B S hS) (SmallProetale.topology B' S (h.contains hS))
      (h.smallFunctor S hS)

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.smallCohomologyRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/SmallEnlargement.lean, line 424. The attribute's comment: “part (1): H^p(S'_proetale, F') = H^p(S_proetale, g^{-1} F')”.

Stacks 098Y, part (1). For an abelian sheaf F' on the larger small pro-étale site of S and every degree p,

H^p(S'_proetale, F') = H^p(S_proetale, g^{-1} F'),

naturally in F'.

This is Stacks 03YU applied to the inclusion: restriction along it is exact and carries injective abelian sheaves to injective abelian sheaves, because its left adjoint g_! is exact (Stacks 04BH), and it matches the two final objects S/S.

noncomputable def smallCohomologyRestrictionIso (p : ℕ) :
    (h.smallFunctor S hS).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
          (SmallProetale.topology B S hS) (SmallProetale.topology B' S (h.contains hS)) ⋙
        Sheaf.functorH.{u + 1, u + 1, u, u + 1} (SmallProetale.topology B S hS) p ≅
      Sheaf.functorH.{u + 1, u + 1, u, u + 1}
        (SmallProetale.topology B' S (h.contains hS)) p

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.smallCohomologyPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/SmallEnlargement.lean, line 443. The attribute's comment: “part (2), first equality: H^p(S_proetale, F) = H^p(S'_proetale, g_* F)”.

Stacks 098Y, part (2), first equality. For an abelian sheaf F on the smaller small pro-étale site of S and every degree p,

H^p(S_proetale, F) = H^p(S'_proetale, g_* F),

naturally in F. This follows from part (1) because g^{-1} g_* F = F, the counit of g^{-1} ⊣ g_* being invertible for a fully faithful cocontinuous functor.

noncomputable def smallCohomologyPushforwardIso (p : ℕ) :
    Sheaf.functorH.{u + 1, u + 1, u, u + 1} (SmallProetale.topology B S hS) p ≅
      (h.smallFunctor S hS).sheafPushforwardCocontinuous AddCommGrpCat.{u + 1}
          (SmallProetale.topology B S hS) (SmallProetale.topology B' S (h.contains hS)) ⋙
        Sheaf.functorH.{u + 1, u + 1, u, u + 1}
          (SmallProetale.topology B' S (h.contains hS)) p

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.smallCohomologyLowerShriekIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/SmallEnlargement.lean, line 469. The attribute's comment: “part (2), second equality: H^p(S_proetale, F) = H^p(S'_proetale, f^{-1} F)”.

Stacks 098Y, part (2), second equality. For an abelian sheaf F on the smaller small pro-étale site of S and every degree p,

H^p(S_proetale, F) = H^p(S'_proetale, f^{-1} F),

naturally in F. This follows from part (1) because g^{-1} f^{-1} F = F: the inverse image f^{-1} = g_! is fully faithful (Stacks 00XU), so the unit of g_! ⊣ g^{-1} is invertible.

noncomputable def smallCohomologyLowerShriekIso (p : ℕ) :
    Sheaf.functorH.{u + 1, u + 1, u, u + 1} (SmallProetale.topology B S hS) p ≅
      (h.smallFunctor S hS).sheafPullback AddCommGrpCat.{u + 1}
          (SmallProetale.topology B S hS) (SmallProetale.topology B' S (h.contains hS)) ⋙
        Sheaf.functorH.{u + 1, u + 1, u, u + 1}
          (SmallProetale.topology B' S (h.contains hS)) p
Tag 0F4S, a lemma

Tag 0F4S in the Stacks Project.

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.fullyFaithfulFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/Enlargement.lean, line 94. The attribute's comment: “hypothesis (c) of 00XU for the inclusion of the big sites: full faithfulness”.

Hypothesis (c) of Stacks 00XU for the big sites: the inclusion functor is fully faithful.

def fullyFaithfulFunctor : h.functor.FullyFaithful

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.functor_isCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/Enlargement.lean, line 99. The attribute's comment: “hypothesis (a) of 00XU for the inclusion of the big sites: cocontinuity”.

Hypothesis (a) of Stacks 00XU for the big sites: the inclusion functor is cocontinuous.

theorem functor_isCocontinuous : h.functor.IsCocontinuous B.topology B'.topology

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.functor_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/Enlargement.lean, line 125. The attribute's comment: “hypotheses (d) and (e) of 00XU for the inclusion of the big sites: preservation of fibre products and of the final object”.

Hypotheses (d) and (e) of Stacks 00XU for the big sites: fibre products exist in the smaller category and are preserved by the inclusion, which also carries the final object Spec ℤ to the final object Spec ℤ; that is, the inclusion preserves finite limits.

theorem functor_preservesFiniteLimits : PreservesFiniteLimits h.functor

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.functor_isMorphismOfSites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/Enlargement.lean, line 174. The attribute's comment: “hypothesis (b) of 00XU for the inclusion of the big sites: continuity, in the form of being a morphism of sites”.

Hypothesis (b) of Stacks 00XU for the big sites: the inclusion functor is continuous, and in fact defines a morphism of sites.

theorem functor_isMorphismOfSites :
    _root_.IsMorphismOfSites.{u + 1} h.functor B.topology B'.topology

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.toposRetraction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/Enlargement.lean, line 190. The attribute's comment: “the two morphisms of topoi of the big sites, with f ∘ g isomorphic to the identity and f_* = g^{-1}”.

The conclusion of Stacks 00XU for the big sites: the two morphisms of topoi g : Sh(Sch_proetale) → Sh(Sch'_proetale) and f : Sh(Sch'_proetale) → Sh(Sch_proetale) induced by the inclusion, together with the isomorphism f ∘ g ≅ id.

The direct image of g is the cocontinuous pushforward and the direct image of f is the continuous pushforward, which is also the inverse image of g; this is the identification f_* = g^{-1}. The retraction is the counit of the adjunction g^{-1} ⊣ g_*.

noncomputable def toposRetraction :
    let : h.functor.IsCocontinuous B.topology B'.topology := h.functor_isCocontinuous
    let : h.functor.IsContinuous B.topology B'.topology :=
      h.functor_isMorphismOfSites.toIsContinuous
    ToposRetraction B.Scheme B'.Scheme B.topology B'.topology h.functor

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.fullyFaithfulFunctorOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/Enlargement.lean, line 236. The attribute's comment: “hypothesis (c) of 00XU for the inclusion of the slices: full faithfulness”.

Hypothesis (c) of Stacks 00XU for the slices: the inclusion functor of the slices over S is fully faithful.

def fullyFaithfulFunctorOver : (h.functorOver S hS).FullyFaithful

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.functorOver_isCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/Enlargement.lean, line 242. The attribute's comment: “hypothesis (a) of 00XU for the inclusion of the slices: cocontinuity”.

Hypothesis (a) of Stacks 00XU for the slices: the inclusion functor of the slices over S is cocontinuous.

theorem functorOver_isCocontinuous :
    (h.functorOver S hS).IsCocontinuous (BigProetaleOver.topology B S hS)
      (BigProetaleOver.topology B' S (h.contains hS))

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.functorOver_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/Enlargement.lean, line 255. The attribute's comment: “hypotheses (d) and (e) of 00XU for the inclusion of the slices: preservation of fibre products and of the final object”.

Hypotheses (d) and (e) of Stacks 00XU for the slices: the inclusion functor of the slices over S preserves finite limits.

theorem functorOver_preservesFiniteLimits : PreservesFiniteLimits (h.functorOver S hS)

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.functorOver_isMorphismOfSites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/Enlargement.lean, line 264. The attribute's comment: “hypothesis (b) of 00XU for the inclusion of the slices: continuity, in the form of being a morphism of sites”.

Hypothesis (b) of Stacks 00XU for the slices: the inclusion functor of the slices over S is continuous, and in fact defines a morphism of sites.

theorem functorOver_isMorphismOfSites :
    _root_.IsMorphismOfSites.{u + 1} (h.functorOver S hS)
      (BigProetaleOver.topology B S hS) (BigProetaleOver.topology B' S (h.contains hS))

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.toposRetractionOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/Enlargement.lean, line 280. The attribute's comment: “the two morphisms of topoi of the slices, with f ∘ g isomorphic to the identity and f_* = g^{-1}”.

The conclusion of Stacks 00XU for the slices: the two morphisms of topoi g : Sh((Sch/S)_proetale) → Sh((Sch'/S)_proetale) and f in the other direction induced by the inclusion of the slices over S, together with the isomorphism f ∘ g ≅ id.

noncomputable def toposRetractionOver :
    let : (h.functorOver S hS).IsCocontinuous (BigProetaleOver.topology B S hS)
        (BigProetaleOver.topology B' S (h.contains hS)) := h.functorOver_isCocontinuous S hS
    let : (h.functorOver S hS).IsContinuous (BigProetaleOver.topology B S hS)
        (BigProetaleOver.topology B' S (h.contains hS)) :=
      (h.functorOver_isMorphismOfSites S hS).toIsContinuous
    ToposRetraction (BigProetaleOver B S hS) (BigProetaleOver B' S (h.contains hS))
      (BigProetaleOver.topology B S hS) (BigProetaleOver.topology B' S (h.contains hS))
      (h.functorOver S hS)
Tag 0F4T, a lemma

Tag 0F4T in the Stacks Project.

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.cohomologyRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/ChangeOfPartialUniverse.lean, line 139. The attribute's comment: “part (1), the cohomology over an object of the smaller big pro-étale site of the restriction of an abelian sheaf agrees with its cohomology over the image of that object”.

Let S be a scheme and let (Sch/S)_proétale and (Sch'/S)_proétale be two big pro-étale sites of S as in Definition 098K, the first contained in the second. For any object U of (Sch/S)_proétale and any degree p,

H^p(U, ℱ'|_{(Sch/S)_proétale}) = H^p(U, ℱ')

naturally in the abelian sheaf ℱ' on (Sch'/S)_proétale, where cohomology over an object is Mathlib's Ext-based CategoryTheory.Sheaf.cohomologyPresheafFunctor.

By Stacks 0F4S the localized inclusion is continuous, cocontinuous and preserves finite limits, and both localized sites are essentially small, so this is Stacks 03YU, Stacks.Cohomology.BiggerSite.cohomologyPresheafFunctorIso.

noncomputable def cohomologyRestrictionIso
    [HasSheafify (BigProetaleOver.topology B S hS) Ab.{u}]
    [HasSheafify (BigProetaleOver.topology B' S (h.contains hS)) Ab.{u}]
    [HasExt.{w} (Sheaf (BigProetaleOver.topology B S hS) Ab.{u})]
    [HasExt.{w} (Sheaf (BigProetaleOver.topology B' S (h.contains hS)) Ab.{u})]
    (U : BigProetaleOver B S hS) (p : ℕ) :
    (h.functorOver S hS).sheafPushforwardContinuous Ab.{u}
          (BigProetaleOver.topology B S hS)
          (BigProetaleOver.topology B' S (h.contains hS)) ⋙
        Sheaf.cohomologyPresheafFunctor (BigProetaleOver.topology B S hS) p ⋙
          (evaluation (BigProetaleOver B S hS)ᵒᵖ Ab.{w}).obj (op U) ≅
      Sheaf.cohomologyPresheafFunctor (BigProetaleOver.topology B' S (h.contains hS)) p ⋙
        (evaluation (BigProetaleOver B' S (h.contains hS))ᵒᵖ Ab.{w}).obj
          (op ((h.functorOver S hS).obj U))

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.exists_extension_abelianSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/ChangeOfPartialUniverse.lean, line 223. The attribute's comment: “part (2), every abelian sheaf on the smaller big pro-étale site is the restriction of an abelian sheaf on the bigger site”.

Let S be a scheme and let (Sch/S)_proétale and (Sch'/S)_proétale be two big pro-étale sites of S as in Definition 098K, the first contained in the second. For any abelian sheaf ℱ on (Sch/S)_proétale there is an abelian sheaf ℱ' on (Sch'/S)_proétale whose restriction to (Sch/S)_proétale is isomorphic to ℱ.

The witness is the sheaf pullback along the inclusion, and the isomorphism is the inverse unit of the adjunction, invertible by Stacks 00XU.

theorem exists_extension_abelianSheaf
    (F : Sheaf (BigProetaleOver.topology B S hS) Ab.{u}) :
    ∃ F' : Sheaf (BigProetaleOver.topology B' S (h.contains hS)) Ab.{u},
      Nonempty ((h.abelianRestrictionOver S hS).obj F' ≅ F)

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.cohomologyPresheafRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/ChangeOfPartialUniverseUnconditional.lean, line 105. The attribute's comment: “part (1), the cohomology over an object of the smaller big pro-étale site of the restriction of an abelian sheaf on the bigger site agrees with the cohomology of that sheaf over the same object in the bigger site, naturally in the sheaf, for every degree”.

Stacks 0F4T (1). Let S be a scheme and let (Sch/S)_proétale and (Sch'/S)_proétale be two big pro-étale sites of S as in Definition 098K, the first contained in the second. For any object U of (Sch/S)_proétale and any degree p,

H^p(U, ℱ'|_{(Sch/S)_proétale}) = H^p(U, ℱ')

naturally in the abelian sheaf ℱ' on (Sch'/S)_proétale, where cohomology over an object is Mathlib's Ext-based CategoryTheory.Sheaf.cohomologyPresheafFunctor with values in any universe w where the Ext-groups of the two sheaf categories are small (for instance w = u, by AlgebraicGeometry.ProEtale.hasExt_sheaf_bigProetaleOver).

Sheafification on both sites is AlgebraicGeometry.ProEtale.hasSheafify_bigProetaleOver_abelian, and the comparison is AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.cohomologyRestrictionIso.

noncomputable def cohomologyPresheafRestrictionIso
    [HasExt.{w} (Sheaf (BigProetaleOver.topology B S hS) Ab.{u})]
    [HasExt.{w} (Sheaf (BigProetaleOver.topology B' S (h.contains hS)) Ab.{u})]
    (U : BigProetaleOver B S hS) (p : ℕ) :
    (h.functorOver S hS).sheafPushforwardContinuous Ab.{u}
          (BigProetaleOver.topology B S hS)
          (BigProetaleOver.topology B' S (h.contains hS)) ⋙
        Sheaf.cohomologyPresheafFunctor (BigProetaleOver.topology B S hS) p ⋙
          (evaluation (BigProetaleOver B S hS)ᵒᵖ Ab.{w}).obj (op U) ≅
      Sheaf.cohomologyPresheafFunctor (BigProetaleOver.topology B' S (h.contains hS)) p ⋙
        (evaluation (BigProetaleOver B' S (h.contains hS))ᵒᵖ Ab.{w}).obj
          (op ((h.functorOver S hS).obj U))

AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.essSurj_abelianRestrictionOver, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProEtale/Site/ChangeOfPartialUniverseUnconditional.lean, line 131. The attribute's comment: “part (2), restriction of abelian sheaves from the bigger big pro-étale site to the smaller one is essentially surjective: every abelian sheaf on the smaller site is isomorphic to the restriction of an abelian sheaf on the bigger site”.

Stacks 0F4T (2). Let S be a scheme and let (Sch/S)_proétale and (Sch'/S)_proétale be two big pro-étale sites of S as in Definition 098K, the first contained in the second. Restriction of abelian sheaves from (Sch'/S)_proétale to (Sch/S)_proétale is essentially surjective: for any abelian sheaf ℱ on (Sch/S)_proétale there is an abelian sheaf ℱ' on (Sch'/S)_proétale whose restriction to (Sch/S)_proétale is isomorphic to ℱ.

The witness is the sheaf pullback along the inclusion, which exists by AlgebraicGeometry.ProEtale.hasSheafify_bigProetaleOver_abelian; this is AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.exists_extension_abelianSheaf.

instance essSurj_abelianRestrictionOver : (h.abelianRestrictionOver S hS).EssSurj
Sources
LeanAlgebraicGeometry.ProEtale.exists_covering_refining_proetaleCovering · AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.fullyFaithfulSmallFunctor · AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.smallFunctor_preservesFiniteLimits · AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.smallFunctor_isCocontinuous · AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.smallFunctor_isMorphismOfSites · AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.smallToposRetraction · AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.smallCohomologyRestrictionIso · AlgebraicGeometry.ProEtale.BigProetaleSite.IsContainedIn.smallCohomologyPushforwardIso

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.