59.75 Specializations and étale… to 59.85 First cohomology of…

Section59.75 Specializations and étale sheaves#

Section 59.75 of the Stacks Project, Tag 0GJ2. 8 tags here are carried by 21 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0GJ3, a remark

Tag 0GJ3 in the Stacks Project.

AlgebraicGeometry.etaleStalkToSectionsAb_eq_smallEtaleSpecializationStalkAb, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/SpecializationStalk.lean, line 253. The attribute's comment: “the specialization map is pullback by the geometric point of the strict henselization, after the identification of the stalk at the specialized point with sections on that point. The factorization of the left-hand side through sections over the strict henselization itself is not proved here; see the module docstring.”.

The specialization map is pullback by t. Composed with the comparison F_{t ≫ p} ⟶ Γ(t, (t ≫ p)⁻¹F) of Stacks 03Q1, the specialization map on stalks is the canonical map F_s ⟶ Γ(t, (t ≫ p)⁻¹F) of Stacks 0GJN, which restricts the germ at s of a section over an étale neighbourhood W along the composite t ⟶ Spec(𝒪^{sh}_{S,s}) ⟶ W.

theorem etaleStalkToSectionsAb_eq_smallEtaleSpecializationStalkAb :
    etaleStalkToSectionsAb B S hS s t.hom =
      smallEtaleSpecializationStalkAb B S hS s t ≫
        geometricStalkToPullbackSectionsAb (t.hom ≫ strictHenselizationToBase B S hS s)

AlgebraicGeometry.smallEtaleSpecializationStalkAb_eq_sectionsRestrictionAb, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SpecializationStalkIdentifications.lean, line 354. The attribute's comment: “the specialization map is pullback of sections along t, read through the two identifications F_s = Γ(Spec 𝒪^sh_{S,s}, p⁻¹F) (03Q9 at the identity) and F_{t ≫ p} = Γ(t, t⁻¹p⁻¹F) (03Q1), both isomorphisms”.

Let S be a scheme, s a geometric point of S, p : Spec(𝒪^{sh}_{S,s}) ⟶ S the structure morphism of the strict henselization at s, and t a geometric point of Spec(𝒪^{sh}_{S,s}), so that the image of t ≫ p is a specialization of the image of s. Use the two identifications

F_s = Γ(Spec(𝒪^{sh}_{S,s}), p⁻¹F) and F_{t ≫ p} = Γ(t, t⁻¹p⁻¹F),

the first of which is Theorem 03Q9 applied to id_S : S ⟶ S and the second Lemma 03Q1. Then the specialization map sp : F_s ⟶ F_{t ≫ p} of Stacks 0GJ2 is the map induced between them by pullback of sections along t, that is, it is the composite of the first identification, the restriction of sections along t, and the inverse of the second.

Here the first identification is AlgebraicGeometry.etaleStalkSectionsAbIso, the second is AlgebraicGeometry.geometricStalkPullbackSectionsAbIso, and restriction of sections along t is Stacks.EtaleCohomology.smallEtaleSectionsRestrictionAb.

theorem smallEtaleSpecializationStalkAb_eq_sectionsRestrictionAb :
    smallEtaleSpecializationStalkAb B S hS s t =
      (etaleStalkSectionsAbIso B S hS s).hom ≫
        smallEtaleSectionsRestrictionAb
            (𝟙 (strictHenselization B S hS s) ≫ strictHenselizationToBase B S hS s) t.hom
            (t.hom ≫ strictHenselizationToBase B S hS s)
            ((Category.assoc t.hom (𝟙 (strictHenselization B S hS s))
                (strictHenselizationToBase B S hS s)).symm.trans
              (congrArg (fun y : t.source ⟶ strictHenselization B S hS s =>
                y ≫ strictHenselizationToBase B S hS s) (Category.comp_id t.hom))) ≫
          (geometricStalkPullbackSectionsAbIso
            (t.hom ≫ strictHenselizationToBase B S hS s)).inv

AlgebraicGeometry.etaleStalkToSectionsAb_id_comp_sectionsRestrictionAb, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/StalkSectionsTransitivity.lean, line 506. The attribute's comment: “the displayed composite: the identification of the stalk at s with sections over the strict henselization, followed by pullback by t, is the specialization map followed by the identification of the stalk at the specialized point with sections on that point. The two identifications are the canonical maps; this statement compares them and does not assert that either is invertible. Invertibility is Stacks 03Q1 and Stacks 03Q9. Of these the library carries 03Q1 for Type-valued sheaves, as AlgebraicGeometry.smallEtalePullbackStalkIso, and 03Q9 only conditionally on the base being the spectrum of a strictly henselian local ring; neither is in the abelian form and at the generality used here, so neither is applied.”.

Stacks 0GJ3, the displayed composite. Let S be a scheme, s a geometric point of S, p : Spec(𝒪^{sh}_{S,s}) ⟶ S the structure morphism of the strict henselization at s, and t a geometric point of Spec(𝒪^{sh}_{S,s}). Then the identification F_s = Γ(Spec(𝒪^{sh}_{S,s}), p⁻¹F) of Stacks 03Q9, followed by pullback of sections by t, is the specialization map sp : F_s ⟶ F_{t ≫ p} followed by the identification F_{t ≫ p} = Γ(t, (t ≫ p)⁻¹F) of Stacks 03Q1.

This is the source's displayed description of sp as pullback by t. The two identifications are AlgebraicGeometry.etaleStalkToSectionsAb at the identity of the strict henselization and AlgebraicGeometry.geometricStalkToPullbackSectionsAb; they are the canonical maps, which Stacks 03Q9 and 03Q1 assert are isomorphisms.

theorem etaleStalkToSectionsAb_id_comp_sectionsRestrictionAb :
    etaleStalkToSectionsAb B S hS s (𝟙 (strictHenselization B S hS s)) ≫
        smallEtaleSectionsRestrictionAb
          (𝟙 (strictHenselization B S hS s) ≫ strictHenselizationToBase B S hS s) t.hom
          (t.hom ≫ strictHenselizationToBase B S hS s)
          ((Category.assoc t.hom (𝟙 (strictHenselization B S hS s))
              (strictHenselizationToBase B S hS s)).symm.trans
            (congrArg (fun y : t.source ⟶ strictHenselization B S hS s =>
              y ≫ strictHenselizationToBase B S hS s) (Category.comp_id t.hom))) =
      smallEtaleSpecializationStalkAb B S hS s t ≫
        geometricStalkToPullbackSectionsAb (t.hom ≫ strictHenselizationToBase B S hS s)
Tag 0GJ4, a remark

Tag 0GJ4 in the Stacks Project.

AlgebraicGeometry.existsUnique_specializationMorphism_and_specialization_eq_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/SpecializationIsPullbackByMorphism.lean, line 408. The attribute's comment: “the whole remark: (1) the unique existence of c; (2) global sections over the two strictly henselian schemes are exact and are stalks at their closed geometric points; (3) on abelian sheaves, the identifications of the stalks at s and at t ≫ p with the sections over the two strict henselizations are isomorphisms, and sp is pullback by c; (4) the same on the unbounded derived category, with RΓ. The big etale site B with hS is a size device, not a source hypothesis.”.

Stacks 0GJ4. Let S be a scheme, s a geometric point of S, and t a geometric point of the strict henselization Spec(𝒪^{sh}_{S,s}), with structure morphism p : Spec(𝒪^{sh}_{S,s}) ⟶ S.

  1. There is exactly one morphism c : Spec(𝒪^{sh}_{S,t ≫ p}) ⟶ Spec(𝒪^{sh}_{S,s}) over S compatible with the given morphism t to Spec(𝒪^{sh}_{S,s}) and the canonical geometric point of Spec(𝒪^{sh}_{S,t ≫ p}).
  2. Taking global sections of abelian sheaves over the strictly henselian schemes Spec(𝒪^{sh}_{S,s}) and Spec(𝒪^{sh}_{S,t ≫ p}) is exact, and is the same as taking stalks at their canonical geometric points (lying over s and over t ≫ p). This is the source's reason that the equality signs below are valid.
  3. For abelian sheaves F on the small étale site of S, the identifications F_s = Γ(Spec(𝒪^{sh}_{S,s}), p⁻¹F) and F_{t ≫ p} = Γ(Spec(𝒪^{sh}_{S,t ≫ p}), p⁻¹F) are isomorphisms, and the specialization map sp : F_s ⟶ F_{t ≫ p} is pullback by c: the first identification followed by restriction of sections along c is sp followed by the second identification.
  4. The same holds for objects K of the unbounded derived category D(S_étale), with RΓ in place of Γ and the specialization map on derived stalks in place of sp: both identifications K_s = RΓ(Spec(𝒪^{sh}_{S,s}), K) and K_{t ≫ p} = RΓ(Spec(𝒪^{sh}_{S,t ≫ p}), K) are isomorphisms, and sp is pullback by c.

Part (1) is AlgebraicGeometry.existsUnique_specializationMorphism; part (2) is AlgebraicGeometry.preservesFiniteColimits_smallEtaleGlobalSections_strictHenselization and AlgebraicGeometry.isIso_strictHenselizationSectionsToStalkAb; the invertibility in (3) and (4) is AlgebraicGeometry.isIso_etaleStalkToSectionsAb_id and AlgebraicGeometry.isIso_vanishingCyclesMap_id, the source's reason that global sections over a strictly henselian scheme are exact and are the stalk at the closed point; the equations are AlgebraicGeometry.etaleStalkToSectionsAb_id_comp_sectionsRestrictionAb_specializationMorphism and AlgebraicGeometry.vanishingCyclesMap_id_comp_derivedSectionsRestriction_specializationMorphism. The derivability instances that unbounded derived global sections on the two strict henselizations are formed with are bound inside part (4); they hold for every scheme (Stacks.EtaleCohomology.smallEtaleGlobalSectionsAb_hasRightDerivedFunctor), and part (4) is proved for every choice of them.

public theorem existsUnique_specializationMorphism_and_specialization_eq_pullback
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) (s : GeometricPoint S)
    (t : GeometricPoint (strictHenselization B S hS s)) :
    (∃! c : strictHenselization B S hS (t.map (strictHenselizationToBase B S hS s)) ⟶
        strictHenselization B S hS s,
        c ≫ strictHenselizationToBase B S hS s =
            strictHenselizationToBase B S hS
              (t.map (strictHenselizationToBase B S hS s)) ∧
          geometricPointToStrictHenselization B S hS
              (t.map (strictHenselizationToBase B S hS s)) ≫ c = t.hom) ∧
      (PreservesFiniteColimits
          (Sheaf.Γ (smallEtaleTopology (strictHenselization B S hS s)) Ab.{u + 1}) ∧
        PreservesFiniteColimits (Sheaf.Γ (smallEtaleTopology (strictHenselization B S hS
          (t.map (strictHenselizationToBase B S hS s)))) Ab.{u + 1}) ∧
        IsIso (strictHenselizationSectionsToStalkAb B S hS s) ∧
        IsIso (strictHenselizationSectionsToStalkAb B S hS
          (t.map (strictHenselizationToBase B S hS s)))) ∧
      (IsIso (etaleStalkToSectionsAb B S hS s (𝟙 (strictHenselization B S hS s))) ∧
        IsIso (etaleStalkToSectionsAb B S hS (t.map (strictHenselizationToBase B S hS s))
          (𝟙 (strictHenselization B S hS (t.map (strictHenselizationToBase B S hS s))))) ∧
        etaleStalkToSectionsAb B S hS s (𝟙 (strictHenselization B S hS s)) ≫
            smallEtaleSectionsRestrictionAb
              (𝟙 (strictHenselization B S hS s) ≫ strictHenselizationToBase B S hS s)
              (specializationMorphism B S hS s t)
              (𝟙 (strictHenselization B S hS
                  (t.map (strictHenselizationToBase B S hS s))) ≫
                strictHenselizationToBase B S hS
                  (t.map (strictHenselizationToBase B S hS s)))
              (specializationMorphism_id_comp B S hS s t) =
          smallEtaleSpecializationStalkAb B S hS s t ≫
            etaleStalkToSectionsAb B S hS (t.map (strictHenselizationToBase B S hS s))
              (𝟙 (strictHenselization B S hS
                (t.map (strictHenselizationToBase B S hS s))))) ∧
        ∀ [((Sheaf.Γ (smallEtaleTopology (strictHenselization B S hS s))
                Ab.{u + 1}).mapHomotopyCategory (.up ℤ) ⋙
              DerivedCategory.Qh).HasRightDerivedFunctor
              (HomotopyCategory.quasiIso
                (Sheaf (smallEtaleTopology (strictHenselization B S hS s))
                  Ab.{u + 1}) (.up ℤ))]
            [((Sheaf.Γ (smallEtaleTopology (strictHenselization B S hS
                    (t.map (strictHenselizationToBase B S hS s))))
                  Ab.{u + 1}).mapHomotopyCategory (.up ℤ) ⋙
                DerivedCategory.Qh).HasRightDerivedFunctor
                (HomotopyCategory.quasiIso
                  (Sheaf (smallEtaleTopology (strictHenselization B S hS
                    (t.map (strictHenselizationToBase B S hS s)))) Ab.{u + 1}) (.up ℤ))],
          IsIso (vanishingCyclesMap B S hS s (𝟙 (strictHenselization B S hS s))) ∧
          IsIso (vanishingCyclesMap B S hS (t.map (strictHenselizationToBase B S hS s))
            (𝟙 (strictHenselization B S hS (t.map (strictHenselizationToBase B S hS s))))) ∧
          vanishingCyclesMap B S hS s (𝟙 (strictHenselization B S hS s)) ≫
              Functor.whiskerLeft
                  (smallEtaleDerivedPullbackAb
                    (𝟙 (strictHenselization B S hS s) ≫
                      strictHenselizationToBase B S hS s))
                  (smallEtaleDerivedGlobalSectionsRestriction
                    (specializationMorphism B S hS s t)) ≫
                (Functor.associator
                    (smallEtaleDerivedPullbackAb
                      (𝟙 (strictHenselization B S hS s) ≫
                        strictHenselizationToBase B S hS s))
                    (smallEtaleDerivedPullbackAb (specializationMorphism B S hS s t))
                    (smallEtaleDerivedGlobalSections (strictHenselization B S hS
                      (t.map (strictHenselizationToBase B S hS s))))).inv ≫
                  Functor.whiskerRight (Functor.mapDerivedCategoryCompIsoOfCompIso
                      (smallEtalePullbackAbCompIso (specializationMorphism B S hS s t)
                          (𝟙 (strictHenselization B S hS s) ≫
                            strictHenselizationToBase B S hS s) ≪≫
                        eqToIso (congrArg
                          (fun m : strictHenselization B S hS
                              (t.map (strictHenselizationToBase B S hS s)) ⟶ S =>
                            smallEtalePullbackAb m)
                          (specializationMorphism_id_comp B S hS s t)))).hom
                    (smallEtaleDerivedGlobalSections (strictHenselization B S hS
                      (t.map (strictHenselizationToBase B S hS s)))) =
            smallEtaleDerivedSpecializationStalkAb B S hS s t ≫
              vanishingCyclesMap B S hS (t.map (strictHenselizationToBase B S hS s))
                (𝟙 (strictHenselization B S hS
                  (t.map (strictHenselizationToBase B S hS s))))

AlgebraicGeometry.existsUnique_specializationMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/SpecializationMorphism.lean, line 195. The attribute's comment: “specialization_morphism_of_strict_henselizations”.

The specialization morphism of strict henselizations exists and is unique: a geometric point t of the strict henselization at s determines exactly one morphism from the strict henselization at the image of t in S to the strict henselization at s which lies over S and carries the canonical geometric point of its source to t.

public theorem existsUnique_specializationMorphism (s : GeometricPoint S)
    (t : GeometricPoint (strictHenselization B S hS s)) :
    let T := strictHenselization B S hS s
    let p := strictHenselizationToBase B S hS s
    let tS := t.map p
    ∃! c : strictHenselization B S hS tS ⟶ T,
      (c ≫ p = strictHenselizationToBase B S hS tS) ∧
      (geometricPointToStrictHenselization B S hS tS ≫ c = t.hom)

AlgebraicGeometry.specializationMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/SpecializationMorphism.lean, line 398. The attribute's comment: “specialization_morphism_of_strict_henselizations”.

The specialization morphism of strict henselizations attached to a geometric point of the strict henselization at s: the unique morphism over S from the strict henselization at the image of that point in S to the strict henselization at s which carries the canonical geometric point of its source to the given one.

public def specializationMorphism (s : GeometricPoint S)
    (t : GeometricPoint (strictHenselization B S hS s)) :
    strictHenselization B S hS (t.map (strictHenselizationToBase B S hS s)) ⟶
      strictHenselization B S hS s

AlgebraicGeometry.specializationMapOnSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/SpecializationOnSections.lean, line 161. The attribute's comment: “specialization_map_on_sections”.

Specialization of a section along the canonical morphism of strict henselizations determined by a geometric point t of the strict henselization at s: the pullback of global sections along the specialization morphism.

public def specializationMapOnSections
    (t : GeometricPoint (strictHenselization B S hS s))
    (hT : B.Contains (strictHenselization B S hS s))
    (hU : B.Contains (strictHenselization B S hS
      (t.map (strictHenselizationToBase B S hS s))))
    (F : Sheaf (SmallEtale.topology B S hS) (Type (u + 1))) :
    let p : (⟨strictHenselization B S hS s, hT⟩ : B.Scheme) ⟶ (⟨S, hS⟩ : B.Scheme) :=
      ⟨strictHenselizationToBase B S hS s⟩
    haveI := smallEtaleBaseChange_isContinuous B p
    let c : (⟨strictHenselization B S hS
      (t.map (strictHenselizationToBase B S hS s)), hU⟩ : B.Scheme) ⟶
      (⟨strictHenselization B S hS s, hT⟩ : B.Scheme) :=
      ⟨specializationMorphism B S hS s t⟩
    haveI := smallEtaleBaseChange_isContinuous B c
    let G := ((smallEtaleBaseChange B p).sheafPullback (Type (u + 1))
      (SmallEtale.topology B S hS)
      (SmallEtale.topology B _ hT)).obj F
    (Sheaf.Γ (SmallEtale.topology B _ hT) (Type (u + 1))).obj G ⟶
      (Sheaf.Γ (SmallEtale.topology B _ hU) (Type (u + 1))).obj
        (((smallEtaleBaseChange B c).sheafPullback (Type (u + 1))
          (SmallEtale.topology B _ hT)
          (SmallEtale.topology B _ hU)).obj G)

AlgebraicGeometry.abelianSpecializationMapOnSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/SpecializationOnSections.lean, line 199. The attribute's comment: “specialization_map_on_sections”.

Specialization along the canonical morphism of strict henselizations, as a natural transformation of functors on abelian sheaves.

public def abelianSpecializationMapOnSections
    (t : GeometricPoint (strictHenselization B S hS s))
    (hT : B.Contains (strictHenselization B S hS s))
    (hU : B.Contains (strictHenselization B S hS
      (t.map (strictHenselizationToBase B S hS s)))) :
    let p : (⟨strictHenselization B S hS s, hT⟩ : B.Scheme) ⟶ (⟨S, hS⟩ : B.Scheme) :=
      ⟨strictHenselizationToBase B S hS s⟩
    haveI := smallEtaleBaseChange_isContinuous B p
    let c : (⟨strictHenselization B S hS
      (t.map (strictHenselizationToBase B S hS s)), hU⟩ : B.Scheme) ⟶
      (⟨strictHenselization B S hS s, hT⟩ : B.Scheme) :=
      ⟨specializationMorphism B S hS s t⟩
    haveI := smallEtaleBaseChange_isContinuous B c
    ((smallEtaleBaseChange B p).sheafPullback Ab.{u + 1}
      (SmallEtale.topology B S hS) (SmallEtale.topology B _ hT) ⋙
      Sheaf.Γ (SmallEtale.topology B _ hT) Ab.{u + 1}) ⟶
    ((smallEtaleBaseChange B p).sheafPullback Ab.{u + 1}
      (SmallEtale.topology B S hS) (SmallEtale.topology B _ hT) ⋙
      ((smallEtaleBaseChange B c).sheafPullback Ab.{u + 1}
        (SmallEtale.topology B _ hT) (SmallEtale.topology B _ hU) ⋙
        Sheaf.Γ (SmallEtale.topology B _ hU) Ab.{u + 1}))

AlgebraicGeometry.specializationMapOnSections_germ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/SpecializationOnSections.lean, line 236. The attribute's comment: “specialization_map_on_sections”.

The geometric germ of a specialized global section is the pullback of its germ on the first strict henselization.

public theorem specializationMapOnSections_germ
    (t : GeometricPoint (strictHenselization B S hS s))
    (hT : B.Contains (strictHenselization B S hS s))
    (hU : B.Contains (strictHenselization B S hS
      (t.map (strictHenselizationToBase B S hS s))))
    (x : GeometricPoint (strictHenselization B S hS
      (t.map (strictHenselizationToBase B S hS s))))
    (F : Sheaf (SmallEtale.topology B S hS) (Type (u + 1))) :
    let p : (⟨strictHenselization B S hS s, hT⟩ : B.Scheme) ⟶ (⟨S, hS⟩ : B.Scheme) :=
      ⟨strictHenselizationToBase B S hS s⟩
    haveI := smallEtaleBaseChange_isContinuous B p
    let c : (⟨strictHenselization B S hS
      (t.map (strictHenselizationToBase B S hS s)), hU⟩ : B.Scheme) ⟶
      (⟨strictHenselization B S hS s, hT⟩ : B.Scheme) :=
      ⟨specializationMorphism B S hS s t⟩
    haveI := smallEtaleBaseChange_isContinuous B c
    let G := ((smallEtaleBaseChange B p).sheafPullback (Type (u + 1))
      (SmallEtale.topology B S hS)
      (SmallEtale.topology B _ hT)).obj F
    let H := ((smallEtaleBaseChange B c).sheafPullback (Type (u + 1))
      (SmallEtale.topology B _ hT)
      (SmallEtale.topology B _ hU)).obj G
    ∀ σ : (Sheaf.Γ (SmallEtale.topology B _ hT) (Type (u + 1))).obj G,
      ((smallEtalePullbackStalkIso B c x).hom.app G)
        ((globalSectionsToEtaleStalk B
          ↥(etaleLocalRing B S hS (t.map (strictHenselizationToBase B S hS s))) hU x H)
          (specializationMapOnSections B S hS s t hT hU F σ)) =
      (globalSectionsToEtaleStalk B ↥(etaleLocalRing B S hS s) hT
          (x.map (B.inclusion.map c)) G) σ
Tag 0GJ5, a remark

Tag 0GJ5 in the Stacks Project.

AlgebraicGeometry.isSeparable_residueField_strictHenselizationToBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/SpecializationLifting.lean, line 101. The attribute's comment: “the residue-field extension”.

The residue field at a point of the strict henselization at a geometric point is separable over the residue field at the image of that point in the scheme.

public theorem isSeparable_residueField_strictHenselizationToBase (sbar : GeometricPoint S)
    (x : strictHenselization B S hS sbar) :
    let f := strictHenselizationToBase B S hS sbar
    letI := (f.residueFieldMap x).hom.toAlgebra
    Algebra.IsSeparable (S.residueField (f x))
      ((strictHenselization B S hS sbar).residueField x)

AlgebraicGeometry.exists_lift_toStrictHenselization_of_specializes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HenselianRings/SpecializationLifting.lean, line 149. The attribute's comment: “lifting the generic geometric point”.

A geometric point over a generization lifts to the strict henselization at a geometric point over the specialization, and the lifted point specializes to the canonical point of the strict henselization.

public theorem exists_lift_toStrictHenselization_of_specializes
    (t s : S) (hts : t ⤳ s) (tbar sbar : GeometricPoint S)
    (ht : tbar.LiesOver t) (hs : sbar.LiesOver s) :
    ∃ lift : tbar.source ⟶ strictHenselization B S hS sbar,
      (lift ≫ strictHenselizationToBase B S hS sbar = tbar.hom) ∧
      (lift default ⤳ (geometricPointToStrictHenselization B S hS sbar) default)

Declarations registered for the tag:

Tag 0GJ6, a lemma

Tag 0GJ6 in the Stacks Project.

AlgebraicGeometry.specializationMapOnStalks_smallEtalePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/Specialization.lean, line 303.

Stacks Project, Tag 0GJ6. Let g : S' ⟶ S be a morphism of schemes, let s' be a geometric point of S' and let σ be a geometric specialization of s', and let h be the canonical morphism of strict henselizations, characterized by lying over g and carrying the canonical geometric point of its source to the canonical geometric point of its target. For a sheaf F on the small étale site of S the specialization map of the inverse image g⁻¹F from s' to σ is the specialization map of F from the image of s' to the image of σ, under the identification of the stalks of an inverse image with the stalks of F.

public theorem specializationMapOnStalks_smallEtalePullback (B : BigEtaleSite.{u})
    (S S' : B.Scheme) (g : S' ⟶ S) (s' : GeometricPoint S'.1)
    (σ : GeometricSpecialization B S'.1 S'.property s')
    (h : strictHenselization B S'.1 S'.property s' ⟶
      strictHenselization B S.1 S.property (s'.map (B.inclusion.map g)))
    (hbase : h ≫ strictHenselizationToBase B S.1 S.property (s'.map (B.inclusion.map g)) =
      strictHenselizationToBase B S'.1 S'.property s' ≫ B.inclusion.map g)
    (hpoint : geometricPointToStrictHenselization B S'.1 S'.property s' ≫ h =
      geometricPointToStrictHenselization B S.1 S.property (s'.map (B.inclusion.map g)))
    (F : Sheaf (SmallEtale.topology B S.1 S.property) (Type (u + 1))) :
    specializationMapOnStalks σ
          (((smallEtaleBaseChange B g).sheafPullback (Type (u + 1))
            (SmallEtale.topology B S.1 S.property)
            (SmallEtale.topology B S'.1 S'.property)).obj F).obj ≫
        (smallEtalePullbackStalkIso B g σ.target).hom.app F =
      (smallEtalePullbackStalkIso B g s').hom.app F ≫
        specializationMapOnStalks (σ.map g h hbase) F.obj
Tag 0GJ7, a lemma

Tag 0GJ7 in the Stacks Project.

AlgebraicGeometry.isFiniteLocallyConstant_iff_finite_etaleStalk_and_bijective_specializationMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SpecializationFiniteLocallyConstant.lean, line 236. References: SGA 4 IX (2.13), “(i), special case”.

Let S be a scheme every quasi-compact open of which has finitely many irreducible components and let F be a sheaf of sets on the small étale site of S. Then F is finite locally constant if and only if all its stalks at geometric points are finite and all specialization maps between those stalks are bijective.

public theorem isFiniteLocallyConstant_iff_finite_etaleStalk_and_bijective_specializationMap
    (hScomp : ∀ V : S.Opens, IsCompact (V : Set S) → (irreducibleComponents V).Finite)
    (F : Sheaf (SmallEtale.topology B S hS) (Type (u + 1))) :
    Stacks.ConstantSheaf.IsFiniteLocallyConstant (SmallEtale.topology B S hS) F ↔
      (∀ s : GeometricPoint S, Finite (etaleStalk B S hS s F.obj)) ∧
        ∀ (s : GeometricPoint S) (σ : GeometricSpecialization B S hS s),
          Function.Bijective (specializationMapOnStalks σ F.obj)
Tag 0GKC, a lemma

Tag 0GKC in the Stacks Project.

AlgebraicGeometry.isFG_etaleStalk_of_isFiniteTypeLocallyConstantModuleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SpecializationFiniteTypeLocallyConstantModule.lean, line 263. The attribute's comment: “(1) ⟹ (2), the stalks are finite modules”.

Stacks Project, Tag 0GKC, the implication (1) ⟹ (2), first half. The stalk at a geometric point of a finite type locally constant sheaf of Λ-modules on the small étale site of a scheme is a finitely generated Λ-module.

public theorem isFG_etaleStalk_of_isFiniteTypeLocallyConstantModuleSheaf
    (F : Sheaf (SmallEtale.topology B S hS) (ModuleCat.{max (u + 1) r} Λ))
    (hF : IsFiniteTypeLocallyConstantModuleSheaf.{u, u + 1, r}
      (SmallEtale.topology B S hS) Λ F)
    (s : GeometricPoint S) :
    ModuleCat.isFG Λ (etaleStalk B S hS s F.obj)

AlgebraicGeometry.bijective_specializationMapOnStalks_of_isFiniteTypeLocallyConstantModuleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SpecializationFiniteTypeLocallyConstantModule.lean, line 278. The attribute's comment: “(1) ⟹ (2), the specialization maps are bijective”. References: SGA 4 IX (2.13), “(i)”.

Stacks Project, Tag 0GKC, the implication (1) ⟹ (2), second half. Every specialization map between stalks of a finite type locally constant sheaf of Λ-modules on the small étale site of a scheme is bijective.

public theorem bijective_specializationMapOnStalks_of_isFiniteTypeLocallyConstantModuleSheaf
    (F : Sheaf (SmallEtale.topology B S hS) (ModuleCat.{max (u + 1) r} Λ))
    (hF : IsFiniteTypeLocallyConstantModuleSheaf.{u, u + 1, r}
      (SmallEtale.topology B S hS) Λ F)
    (s : GeometricPoint S) (σ : GeometricSpecialization B S hS s) :
    Function.Bijective (specializationMapOnStalks σ F.obj)

AlgebraicGeometry.isFiniteTypeLocallyConstantModuleSheaf_iff_stalks_and_specialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SpecializationFiniteTypeLocallyConstantModule.lean, line 302. The attribute's comment: “the equivalence, with (2) ⟹ (1) carried as the hypothesis hconverse”.

Stacks Project, Tag 0GKC. Let S be a scheme such that every quasi-compact open of S has a finite number of irreducible components, let Λ be a Noetherian ring and let F be a sheaf of Λ-modules on the small étale site of S. Then F is a finite type locally constant sheaf of Λ-modules if and only if all its stalks at geometric points are finite, i.e. finitely generated, Λ-modules and all specialization maps between stalks are bijective.

The implication (1) ⟹ (2) is proved here, using neither hqc nor the Noetherian hypothesis on Λ. The converse implication (2) ⟹ (1) is not proved: it is carried as the explicit hypothesis hconverse, which is the only use made of hqc and of IsNoetherianRing Λ. See the implementation notes of this file for what its proof needs.

public theorem isFiniteTypeLocallyConstantModuleSheaf_iff_stalks_and_specialization
    [IsNoetherianRing Λ]
    (hqc : ∀ V : S.Opens, IsCompact (V : Set S) → (irreducibleComponents V).Finite)
    (F : Sheaf (SmallEtale.topology B S hS) (ModuleCat.{max (u + 1) r} Λ))
    (hconverse : (∀ V : S.Opens, IsCompact (V : Set S) → (irreducibleComponents V).Finite) →
      (∀ s : GeometricPoint S, ModuleCat.isFG Λ (etaleStalk B S hS s F.obj)) →
      (∀ (s : GeometricPoint S) (σ : GeometricSpecialization B S hS s),
        Function.Bijective (specializationMapOnStalks σ F.obj)) →
      IsFiniteTypeLocallyConstantModuleSheaf.{u, u + 1, r}
        (SmallEtale.topology B S hS) Λ F) :
    IsFiniteTypeLocallyConstantModuleSheaf.{u, u + 1, r} (SmallEtale.topology B S hS) Λ F ↔
      (∀ s : GeometricPoint S, ModuleCat.isFG Λ (etaleStalk B S hS s F.obj)) ∧
        ∀ (s : GeometricPoint S) (σ : GeometricSpecialization B S hS s),
          Function.Bijective (specializationMapOnStalks σ F.obj)

AlgebraicGeometry.isFiniteTypeLocallyConstantModuleSheaf_iff_isFG_etaleStalk_and_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SpecializationFiniteTypeLocallyConstantModuleConverse.lean, line 217. References: SGA 4 IX (2.13), “(i), special case”.

Stacks Project, Tag 0GKC. Let S be a scheme such that every quasi-compact open of S has a finite number of irreducible components, let Λ be a Noetherian ring and let F be a sheaf of Λ-modules on the small étale site of S. Then F is a finite type locally constant sheaf of Λ-modules if and only if all its stalks at geometric points are finite, i.e. finitely generated, Λ-modules and all specialization maps between stalks are bijective.

public theorem isFiniteTypeLocallyConstantModuleSheaf_iff_isFG_etaleStalk_and_bijective
    [IsNoetherianRing Λ]
    (hqc : ∀ V : S.Opens, IsCompact (V : Set S) → (irreducibleComponents V).Finite)
    (F : Sheaf (SmallEtale.topology B S hS) (ModuleCat.{max (u + 1) r} Λ)) :
    IsFiniteTypeLocallyConstantModuleSheaf.{u, u + 1, r} (SmallEtale.topology B S hS) Λ F ↔
      (∀ s : GeometricPoint S, ModuleCat.isFG Λ (etaleStalk B S hS s F.obj)) ∧
        ∀ (s : GeometricPoint S) (σ : GeometricSpecialization B S hS s),
          Function.Bijective (specializationMapOnStalks σ F.obj)
Tag 0GJ8, a lemma

Tag 0GJ8 in the Stacks Project.

AlgebraicGeometry.pushforwardStalkToStrictHenselizationSectionsAb_comp_sectionsRestrictionAb, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/DerivedPushforwardStalkSpecialization.lean, line 589. The attribute's comment: “the square for an abelian sheaf F, in place of an object K of D⁺(X_étale): the vertical identifications are those of Stacks 0GIX rather than their derived counterparts”.

The square on abelian sheaves. The map (f_*F)_s ⟶ Γ(X ×_S Spec(𝒪^{sh}_{S,s}), p⁻¹F) of Stacks 0GIX at s, followed by restriction of sections along id_X × c, is the specialization map sp : (f_*F)_s ⟶ (f_*F)_{t ≫ p} followed by the same map at t ≫ p.

Both sides are maps out of the stalk at s of the direct image, so it suffices to compare them on the germ of a section over an étale neighbourhood (V, w) of s; there both are restriction along X ×_S Spec(𝒪^{sh}_{S,t ≫ p}) ⟶ X ×_S V of the corresponding section of F over X ×_S V, the two morphisms agreeing because c carries the canonical morphism from the strict henselization into V to the one for the specialized neighbourhood.

theorem pushforwardStalkToStrictHenselizationSectionsAb_comp_sectionsRestrictionAb :
    pushforwardStalkToStrictHenselizationSectionsAb B hS f s ≫
        smallEtaleSectionsRestrictionAb (strictHenselizationBaseChangeToSource B hS f s)
          (strictHenselizationBaseChangeSpecializationMap B hS f s t)
          (strictHenselizationBaseChangeToSource B hS f
            (t.map (strictHenselizationToBase B S hS s)))
          (strictHenselizationBaseChangeSpecializationMap_comp_toSource B hS f s t) =
      Functor.whiskerLeft (smallEtalePushforwardAb f)
          (smallEtaleSpecializationStalkAb B S hS s t) ≫
        pushforwardStalkToStrictHenselizationSectionsAb B hS f
          (t.map (strictHenselizationToBase B S hS s))

AlgebraicGeometry.specializationStalk_comp_derivedPushforwardStalkToStrictHenselizationSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SpecializationMapAndFibres.lean, line 939. The attribute's comment: “the square, with sp on top and the maps of Stacks 0GIX as its verticals, proved for an arbitrary morphism of schemes and an arbitrary object of D(X_etale)”.

For K in D(X_etale), the square whose top arrow is the specialization map sp on the stalk of Rf_*K and whose verticals are the maps of Stacks 0GIX from those stalks to the global sections over the base changes to the strict henselizations commutes, its bottom arrow being pullback along id_X × c. The verticals are the identifications of Theorem 03Q9 when f is quasi-compact and quasi-separated and K is bounded below; the square commutes for an arbitrary morphism of schemes and an arbitrary object of D(X_etale). It is the square of derivedPushforwardStalkToStrictHenselizationSections_comp_sectionsSpecialization read with sp on top.

theorem specializationStalk_comp_derivedPushforwardStalkToStrictHenselizationSections :
    Functor.whiskerLeft (smallEtaleDerivedPushforwardAb f)
          (smallEtaleDerivedSpecializationStalkAbAt B S hS s t) ≫
        derivedPushforwardStalkToStrictHenselizationSections B hS f
          (specializedGeometricPoint B S hS s t) =
      derivedPushforwardStalkToStrictHenselizationSections B hS f s ≫
        strictHenselizationSectionsSpecializationAt B hS f s t
Tag 0GJ9, a remark

Tag 0GJ9 in the Stacks Project.

AlgebraicGeometry.derivedPushforwardStalkToStrictHenselizationSections_comp_sectionsSpecialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SpecializationMapAndFibres.lean, line 896. The attribute's comment: “the left square, whose verticals are the specialization map sp and pullback along id_X × c; the source states that in general no vertical map exists between the cohomologies of K on the two fibres, so the right-hand column carries no square”.

Stacks 0GJ9. For K in D(X_etale) the specialization map on the stalk of Rf_*K at a geometric point s of S, and pullback along id_X × c on global sections over the base change to the strict henselization, form a commutative square with the two maps of Stacks 0GIX from those stalks.

Read with sp vertical this is the left square of the diagram of Stacks 0GJ9; read with sp horizontal it is the square of Stacks 0GJ8, which is AlgebraicGeometry.specializationStalk_comp_derivedPushforwardStalkToStrictHenselizationSections. It is proved here for an arbitrary morphism of schemes and an arbitrary object of D(X_etale), which is the generality Stacks 0GJ9 asserts it in.

theorem derivedPushforwardStalkToStrictHenselizationSections_comp_sectionsSpecialization :
    derivedPushforwardStalkToStrictHenselizationSections B hS f s ≫
        strictHenselizationSectionsSpecializationAt B hS f s t =
      Functor.whiskerLeft (smallEtaleDerivedPushforwardAb f)
          (smallEtaleDerivedSpecializationStalkAbAt B S hS s t) ≫
        derivedPushforwardStalkToStrictHenselizationSections B hS f
          (specializedGeometricPoint B S hS s t)

AlgebraicGeometry.derivedPushforwardStalkToStrictHenselizationSections_comp_sectionsSpecialization_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SpecializationMapAndFibresUnconditional.lean, line 64. The attribute's comment: “the left square for an arbitrary morphism of schemes and an arbitrary object of the unbounded D(X_etale): its verticals are sp and pullback along id_X × c, its horizontals the maps of Stacks 0GIX, and the unbounded Rf_* and RΓ are built from K-injective resolutions; the source states that no vertical map exists in general between the cohomologies of K on the two fibres, so the right-hand column carries no square”.

Let f : X ⟶ S be a morphism of schemes, s a geometric point of S and t a geometric point of the strict henselization of S at s. For K in the unbounded derived category D(X_étale), the maps of Stacks 0GIX from the stalks of Rf_*K at s and at the specialized point t ≫ p to the derived global sections over the base changes of X to the two strict henselizations form a commutative square with the specialization map sp on the left and pullback along id_X × c on the right.

theorem derivedPushforwardStalkToStrictHenselizationSections_comp_sectionsSpecialization_unconditional
    (B : BigEtaleSite.{u}) {X S : Scheme.{u}} (hS : B.Contains S) (f : X ⟶ S)
    (s : GeometricPoint S) (t : GeometricPoint (strictHenselization B S hS s)) :
    derivedPushforwardStalkToStrictHenselizationSections B hS f s ≫
        strictHenselizationSectionsSpecializationAt B hS f s t =
      Functor.whiskerLeft (smallEtaleDerivedPushforwardAb f)
          (smallEtaleDerivedSpecializationStalkAbAt B S hS s t) ≫
        derivedPushforwardStalkToStrictHenselizationSections B hS f
          (specializedGeometricPoint B S hS s t)
Sources
LeanAlgebraicGeometry.etaleStalkToSectionsAb_eq_smallEtaleSpecializationStalkAb · AlgebraicGeometry.smallEtaleSpecializationStalkAb_eq_sectionsRestrictionAb · AlgebraicGeometry.etaleStalkToSectionsAb_id_comp_sectionsRestrictionAb · AlgebraicGeometry.existsUnique_specializationMorphism_and_specialization_eq_pullback · AlgebraicGeometry.existsUnique_specializationMorphism · AlgebraicGeometry.specializationMorphism · AlgebraicGeometry.specializationMapOnSections · AlgebraicGeometry.abelianSpecializationMapOnSections

Section59.76 Complexes with constructible cohomology#

Section 59.76 of the Stacks Project, Tag 095V. 6 tags here are carried by 17 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 095W, a definition

Tag 095W in the Stacks Project.

Stacks.EtaleCohomology.ConstructibleDerivedCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/Basic.lean, line 67. References: SGA 5 I (App.1.1), “constant Λ coefficients”; SGA 5 IIIB (6.1), “D_c(-)”.

The full subcategory of the unbounded derived category of small-étale Λ-module sheaves with constructible cohomology sheaves.

public abbrev ConstructibleDerivedCategory (B : BigEtaleSite.{u}) (X : B.Scheme)
    (Λ : Type r) [Ring Λ]
    [HasSheafify (SmallEtale.topology B X.1 X.property) (ModuleCat.{w} Λ)]
    [∀ (S T : B.Scheme) (f : T ⟶ S),
      ((smallEtaleBaseChange B f).sheafPushforwardContinuous (ModuleCat.{w} Λ)
        (SmallEtale.topology B S.1 S.property)
        (SmallEtale.topology B T.1 T.property)).IsRightAdjoint]
    [∀ (T : B.Scheme) (V : SmallEtale B T.1 T.property),
      HasWeakSheafify ((SmallEtale.topology B T.1 T.property).over V) (ModuleCat.{w} Λ)]

Stacks.EtaleCohomology.ConstructibleEtaleDerivedCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/ConstructibleEtaleDerivedCategory.lean, line 48. The attribute's comment: “the full subcategory of D(X_ét, Λ) of complexes whose cohomology sheaves are constructible, for module sections in any universe containing that of the schemes”. References: SGA 5 IIIB (6.1).

Stacks 095W. D_c(X_ét, Λ): the full subcategory of the unbounded derived category of sheaves of Λ-modules on the small étale site of X on the complexes all of whose cohomology sheaves are constructible sheaves of Λ-modules.

public abbrev ConstructibleEtaleDerivedCategory (B : BigEtaleSite.{u}) (X : B.Scheme)
    (Λ : Type r) [Ring Λ]
Tag 095X, a lemma

Tag 095X in the Stacks Project.

Stacks.EtaleCohomology.isConstructible_derivedRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/RestrictionExtensionByZero.lean, line 148. The attribute's comment: “part (1)”.

Let Λ be a Noetherian ring, let X be a scheme and let U be an object of the small étale site of X. If a complex K of étale sheaves of Λ-modules on X lies in D_c(X_étale, Λ), then its restriction K|_U lies in D_c(U_étale, Λ).

public theorem isConstructible_derivedRestriction
    (K : DerivedCategory (Sheaf (SmallEtale.topology B X.obj X.property)
      (ModuleCat.{max (u + 1) r} Λ)))
    (hK : IsConstructible B X Λ K) :
    IsConstructible B U.obj.left Λ
      ((moduleRestriction.{u, r, max (u + 1) r} B X.obj X.property U
        Λ).mapDerivedCategory.obj K)

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

Let Λ be a Noetherian ring, let X be a scheme and let U be an object of the small étale site of X whose structure morphism j : U ⟶ X is quasi-compact and quasi-separated. If a complex M of étale sheaves of Λ-modules on U lies in D_c(U_étale, Λ), then j_! M lies in D_c(X_étale, Λ).

public theorem isConstructible_derivedModuleExtensionByZero
    (hqc : QuasiCompact (B.inclusion.map U.obj.hom))
    (hqs : QuasiSeparated (B.inclusion.map U.obj.hom))
    (M : DerivedCategory (Sheaf (SmallEtale.topology B U.obj.left.obj U.obj.left.property)
      (ModuleCat.{max (u + 1) r} Λ)))
    (hM : IsConstructible B U.obj.left Λ M) :
    IsConstructible B X Λ
      ((moduleExtensionByZero.{u, r} B X.obj X.property U Λ).mapDerivedCategory.obj M)
Tag 095Y, a lemma

Tag 095Y in the Stacks Project.

Stacks.EtaleCohomology.isConstructible_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/InverseImage.lean, line 109.

Stacks 095Y. Let Λ be a Noetherian ring and f : X ⟶ Y a morphism of schemes. If a complex of étale sheaves of Λ-modules on Y lies in D_c(Y_étale, Λ), that is has constructible cohomology sheaves in every degree, then its derived inverse image Lf^*K lies in D_c(X_étale, Λ).

public theorem isConstructible_derivedPullback {X Y : B.Scheme} (f : X ⟶ Y)
    [HasSheafify (SmallEtale.topology B Y.obj Y.property) (ModuleCat.{max (u + 1) w} Λ)]
    [HasSheafify (SmallEtale.topology B X.obj X.property) (ModuleCat.{max (u + 1) w} Λ)]
    [∀ (S T : B.Scheme) (g : T ⟶ S),
      ((smallEtaleBaseChange B g).sheafPushforwardContinuous (ModuleCat.{max (u + 1) w} Λ)
        (SmallEtale.topology B S.obj S.property)
        (SmallEtale.topology B T.obj T.property)).IsRightAdjoint]
    [∀ (T : B.Scheme) (V : SmallEtale B T.obj T.property),
      HasWeakSheafify ((SmallEtale.topology B T.obj T.property).over V)
        (ModuleCat.{max (u + 1) w} Λ)]
    (K : DerivedCategory (Sheaf (SmallEtale.topology B Y.obj Y.property)
      (ModuleCat.{max (u + 1) w} Λ)))
    (hK : IsConstructible B Y Λ K) :
    IsConstructible B X Λ
      (((smallEtaleBaseChange B f).sheafPullback (ModuleCat.{max (u + 1) w} Λ)
        (SmallEtale.topology B Y.obj Y.property)
        (SmallEtale.topology B X.obj X.property)).mapDerivedCategory.obj K)

Stacks.EtaleCohomology.isConstructible_mapDerivedCategory_smallEtaleSheafPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/InverseImageUnconditional.lean, line 68.

Stacks 095Y. Let Λ be a Noetherian ring and f : X ⟶ Y a morphism of schemes. If K ∈ D_c(Y_étale, Λ), that is the cohomology sheaves of K are constructible in every degree, then Lf^*K ∈ D_c(X_étale, Λ).

Inverse image of module sheaves is exact, so Lf^* is the termwise functor CategoryTheory.Functor.mapDerivedCategory and Hⁱ(Lf^*K) ≅ f⁻¹(HⁱK), which is constructible by Tag 095G; this is Stacks.EtaleCohomology.isConstructible_derivedPullback, whose sheafification and inverse-image instances are supplied by the small étale site.

public theorem isConstructible_mapDerivedCategory_smallEtaleSheafPullback {X Y : B.Scheme}
    (f : X ⟶ Y)
    (K : DerivedCategory (Sheaf (SmallEtale.topology B Y.obj Y.property)
      (ModuleCat.{max (u + 1) w} Λ)))
    (hK : IsConstructible B Y Λ K) :
    IsConstructible B X Λ
      (((smallEtaleBaseChange B f).sheafPullback (ModuleCat.{max (u + 1) w} Λ)
        (SmallEtale.topology B Y.obj Y.property)
        (SmallEtale.topology B X.obj X.property)).mapDerivedCategory.obj K)
Tag 095Z, a lemma

Tag 095Z in the Stacks Project.

Stacks.EtaleCohomology.exists_shriekConstant_cover_of_isConstructible_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/ShriekCoverOfCohomology.lean, line 168.

Stacks 095Z. Let X be a quasi-compact and quasi-separated scheme, let Λ be a Noetherian ring, let K ∈ D(X_étale, Λ) and let b be an integer for which H^b(K) is constructible. Then there are finitely many affine objects U i of the small étale site of X and a map F[-b] ⟶ K, where F = ⊕ᵢ j_{U i!} Λ-underline, inducing a surjection on degree-b cohomology.

A complex A representing K is chosen; AlgebraicGeometry.exists_finite_epi_comp_sigma_moduleShriekConstant_affine — Tags 093B and 095P in the shape the source's proof quotes them — covers the degree-b cocycles of A well enough for the canonical surjection onto H^b(K) to survive, and Stacks.Homology.exists_single_map_epi_derivedHomology turns that cover into the required map in the derived category.

Nothing is granted; see "What the proof rests on" in the module documentation.

public theorem exists_shriekConstant_cover_of_isConstructible_homology (X : B.Scheme)
    [CompactSpace X.obj] [QuasiSeparatedSpace X.obj]
    [HasSheafify (SmallEtale.topology B X.obj X.property) (ModuleCat.{max (u + 1) r} Λ)]
    [∀ (S T : B.Scheme) (g : T ⟶ S),
      ((smallEtaleBaseChange B g).sheafPushforwardContinuous (ModuleCat.{max (u + 1) r} Λ)
        (SmallEtale.topology B S.obj S.property)
        (SmallEtale.topology B T.obj T.property)).IsRightAdjoint]
    [∀ (T : B.Scheme) (V : SmallEtale B T.obj T.property),
      HasWeakSheafify ((SmallEtale.topology B T.obj T.property).over V)
        (ModuleCat.{max (u + 1) r} Λ)]
    (K : DerivedCategory (Sheaf (SmallEtale.topology B X.obj X.property)
      (ModuleCat.{max (u + 1) r} Λ))) (b : ℤ)
    (hK : IsConstructibleModuleSheaf B X Λ
      ((homologyFunctor (Sheaf (SmallEtale.topology B X.obj X.property)
        (ModuleCat.{max (u + 1) r} Λ)) b).obj K)) :
    ∃ (n : ℕ) (U : Fin n → SmallEtale B X.obj X.property),
      (∀ i, IsAffine ((SmallEtale.toScheme B X.obj X.property).obj (U i))) ∧
      ∃ f : (singleFunctor (Sheaf (SmallEtale.topology B X.obj X.property)
          (ModuleCat.{max (u + 1) r} Λ)) b).obj
          (∐ fun i : Fin n ↦ moduleShriekConstant.{u, r, r} B X Λ (U i)) ⟶ K,
        Epi ((homologyFunctor (Sheaf (SmallEtale.topology B X.obj X.property)
          (ModuleCat.{max (u + 1) r} Λ)) b).map f)

Stacks.EtaleCohomology.exists_shriekConstant_cover_of_isConstructibleModuleEtaleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/ShriekCoverOfCohomologyEtale.lean, line 68.

Stacks 095Z. Let X be a quasi-compact and quasi-separated scheme, let Λ be a Noetherian ring, let K ∈ D(X_étale, Λ) and let b be an integer such that H^b(K) is constructible. Then there exist a sheaf F = ⊕ᵢ j_{U i!} Λ-underline, a finite direct sum with every U i an affine object of X_étale, and a map F[-b] ⟶ K in D(X_étale, Λ) inducing a surjection F ⟶ H^b(K).

public theorem exists_shriekConstant_cover_of_isConstructibleModuleEtaleSheaf (X : B.Scheme)
    [CompactSpace X.obj] [QuasiSeparatedSpace X.obj]
    (K : DerivedCategory (Sheaf (SmallEtale.topology B X.obj X.property)
      (ModuleCat.{max (u + 1) r} Λ))) (b : ℤ)
    (hK : IsConstructibleModuleEtaleSheaf B X Λ
      ((homologyFunctor (Sheaf (SmallEtale.topology B X.obj X.property)
        (ModuleCat.{max (u + 1) r} Λ)) b).obj K)) :
    ∃ (n : ℕ) (U : Fin n → SmallEtale B X.obj X.property),
      (∀ i, IsAffine ((SmallEtale.toScheme B X.obj X.property).obj (U i))) ∧
      ∃ f : (singleFunctor (Sheaf (SmallEtale.topology B X.obj X.property)
          (ModuleCat.{max (u + 1) r} Λ)) b).obj
          (∐ fun i : Fin n ↦ moduleShriekConstant.{u, r, r} B X Λ (U i)) ⟶ K,
        Epi ((singleFunctorCompHomologyFunctorIso (Sheaf (SmallEtale.topology B X.obj X.property)
            (ModuleCat.{max (u + 1) r} Λ)) b).inv.app
              (∐ fun i : Fin n ↦ moduleShriekConstant.{u, r, r} B X Λ (U i)) ≫
          (homologyFunctor (Sheaf (SmallEtale.topology B X.obj X.property)
            (ModuleCat.{max (u + 1) r} Λ)) b).map f)
Tag 0960, a lemma

Tag 0960 in the Stacks Project.

Stacks.EtaleCohomology.isConstructible_of_isRepresentedByBoundedAboveConstructibleFlatComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/BoundedAboveShriekComplex.lean, line 373. The attribute's comment: “the implication (3) => (1), from the weak Serre property hSerre of the constructible sheaves of modules”.

Tag 0960, the implication (3) ⟹ (1). An object of D(X_étale, Λ) represented by a bounded above complex of flat constructible sheaves of Λ-modules has constructible cohomology sheaves.

A flat constructible sheaf is constructible, by AlgebraicGeometry.isConstructibleModuleSheaf_of_isConstructibleFlatModuleSheaf, and a complex of constructible sheaves has constructible cohomology, by Stacks.EtaleCohomology.isConstructible_of_forall_isConstructibleModuleSheaf, which is where the weak Serre hypothesis hSerre is used; see "Where the weak Serre property comes from" in the module documentation for why it is still a hypothesis at a free coefficient universe, and AlgebraicGeometry.isWeakSerreClass_isConstructibleModuleSheafProperty for what discharges it at max (u + 1) r. The bound is not needed for this implication and is not used.

public theorem isConstructible_of_isRepresentedByBoundedAboveConstructibleFlatComplex
    (hSerre : (isConstructibleModuleSheafProperty.{u, w, r} B X Λ).IsWeakSerreClass)
    (K : DerivedCategory
      (Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{w} Λ)))
    (hK : IsRepresentedByBoundedAboveConstructibleFlatComplex.{u, w, r} B X Λ K) :
    IsConstructible B X Λ K

Stacks.EtaleCohomology.isRepresentedByBoundedAboveConstructibleFlatComplex_of_shriekSum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/BoundedAboveShriekComplex.lean, line 430. The attribute's comment: “the implication (2) => (3)”.

Tag 0960, the implication (2) ⟹ (3). A bounded above complex whose terms are finite direct sums of sheaves j_{U!} Λ-underline with U affine is a bounded above complex of flat constructible sheaves of Λ-modules, so an object of D(X_étale, Λ) satisfying condition (2) satisfies condition (3).

The same complex is used; each term is isomorphic to a finite direct sum of affine shriek constants, which is flat constructible by AlgebraicGeometry.isConstructibleFlatModuleSheaf_sigma_moduleShriekConstant_of_quasiSeparated, and flat constructibility is invariant under isomorphism by AlgebraicGeometry.isConstructibleFlatModuleSheaf_congr. That input conjoins Tag 03S8 with the flatness of j_{U!} Λ-underline, which the source leaves unstated, and the closure of flat constructible sheaves under finite direct sums; see "Why quasi-separatedness is assumed" in the module documentation for why it is the only hypothesis on X that enters. Quasi-compactness of X is not needed for this implication and is not assumed.

public theorem isRepresentedByBoundedAboveConstructibleFlatComplex_of_shriekSum
    [QuasiSeparatedSpace X.obj]
    (K : DerivedCategory (Sheaf (SmallEtale.topology B X.obj X.property)
      (ModuleCat.{max (u + 1) r} Λ)))
    (hK : IsRepresentedByAffineShriekSumComplex.{u, r} B X Λ K) :
    IsRepresentedByBoundedAboveConstructibleFlatComplex.{u, max (u + 1) r, r} B X Λ K

Stacks.EtaleCohomology.isConstructible_of_isRepresentedByAffineShriekSumComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/BoundedAboveShriekComplex.lean, line 455. The attribute's comment: “the implication (2) => (1)”.

Tag 0960, the implication (2) ⟹ (1). An object of D(X_étale, Λ) represented by a bounded above complex whose terms are finite direct sums of sheaves j_{U!} Λ-underline with U affine has constructible cohomology sheaves, so it lies in the constructible derived category of Tag 095W.

This is the composite of the implications (2) ⟹ (3) and (3) ⟹ (1), and nothing is carried. The weak Serre property the second step needs is at this coefficient universe Stacks 03RZ (3), AlgebraicGeometry.isWeakSerreClass_isConstructibleModuleSheafProperty; the flat constructibility of a finite affine shriek sum which the first step needs is AlgebraicGeometry.isConstructibleFlatModuleSheaf_sigma_moduleShriekConstant_of_quasiSeparated, and that is the only reason X is asked to be quasi-separated. Quasi-compactness of X is not needed and is not assumed.

public theorem isConstructible_of_isRepresentedByAffineShriekSumComplex
    [QuasiSeparatedSpace X.obj]
    (K : DerivedCategory (Sheaf (SmallEtale.topology B X.obj X.property)
      (ModuleCat.{max (u + 1) r} Λ)))
    (hK : IsRepresentedByAffineShriekSumComplex.{u, r} B X Λ K) :
    IsConstructible B X Λ K

Stacks.EtaleCohomology.isRepresentedByAffineShriekSumComplex_of_isConstructible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/ShriekSumResolution.lean, line 307. The attribute's comment: “the implication (1) => (2)”.

Tag 0960, the implication (1) ⟹ (2). Let X be a quasi-compact and quasi-separated scheme, let Λ be a Noetherian ring and let K ∈ D^-(X_étale, Λ) have constructible cohomology sheaves. Then K is represented by a bounded above complex each of whose terms is a finite direct sum of sheaves j_{U!} Λ-underline with U an affine object of the small étale site of X.

Boundedness above of K is the vanishing hvan of H^i(K) for i > b, which by DerivedCategory.isLE_iff says exactly that K lies in D^-(X_étale, Λ); it is the standing assumption of the source's equivalence.

The proof chooses a cochain complex A with A^i = 0 for i > b representing K (DerivedCategory.exists_iso_Q_obj_of_isLE) and resolves it by the finite affine shriek sums using Stacks.Homology.BoundedAboveResolution.exists_quasiIso_isStrictlyLE_of_coversEpis. The three closure properties that engine needs of the class of finite affine shriek sums are Stacks.EtaleCohomology.isAffineShriekSum_zero, Stacks.EtaleCohomology.isAffineShriekSum_biprod and Stacks.EtaleCohomology.isAffineShriekSum_of_iso, and the covering property is Stacks.EtaleCohomology.coversEpis_isAffineShriekSum, which rests on Stacks 093B (2) with Stacks 095P and on Stacks 03S8 for sheaves of modules. The weak Serre class the engine tests its kernels against is the constructible sheaves of Λ-modules, Stacks 03RZ (3), supplied by AlgebraicGeometry.isWeakSerreClass_isConstructibleModuleSheafProperty. Nothing is carried.

public theorem isRepresentedByAffineShriekSumComplex_of_isConstructible
    [CompactSpace X.obj] [QuasiSeparatedSpace X.obj]
    (K : DerivedCategory (Sheaf (SmallEtale.topology B X.obj X.property)
      (ModuleCat.{max (u + 1) r} Λ))) (hK : IsConstructible B X Λ K) (b : ℤ)
    (hvan : ∀ i : ℤ, b < i → IsZero ((DerivedCategory.homologyFunctor
      (Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{max (u + 1) r} Λ)) i).obj K)) :
    IsRepresentedByAffineShriekSumComplex.{u, r} B X Λ K

Stacks.EtaleCohomology.isRepresentedByBoundedAboveConstructibleFlatComplex_of_isConstructible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/ShriekSumResolution.lean, line 346. The attribute's comment: “the implication (1) => (3)”. References: SGA 4½ Rapport (4.7), “partial”.

Tag 0960, the implication (1) ⟹ (3). Let X be a quasi-compact and quasi-separated scheme, let Λ be a Noetherian ring and let K ∈ D^-(X_étale, Λ) have constructible cohomology sheaves. Then K is represented by a bounded above complex of flat constructible sheaves of Λ-modules.

This is the composite of (1) ⟹ (2), Stacks.EtaleCohomology.isRepresentedByAffineShriekSumComplex_of_isConstructible, with (2) ⟹ (3), Stacks.EtaleCohomology.isRepresentedByBoundedAboveConstructibleFlatComplex_of_shriekSum. Both steps are unconditional.

public theorem isRepresentedByBoundedAboveConstructibleFlatComplex_of_isConstructible
    [CompactSpace X.obj] [QuasiSeparatedSpace X.obj]
    (K : DerivedCategory (Sheaf (SmallEtale.topology B X.obj X.property)
      (ModuleCat.{max (u + 1) r} Λ))) (hK : IsConstructible B X Λ K) (b : ℤ)
    (hvan : ∀ i : ℤ, b < i → IsZero ((DerivedCategory.homologyFunctor
      (Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{max (u + 1) r} Λ)) i).obj K)) :
    IsRepresentedByBoundedAboveConstructibleFlatComplex.{u, max (u + 1) r, r} B X Λ K

Stacks.EtaleCohomology.isRepresentedByAffineShriekSumComplex_of_constructibleFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/ShriekSumResolution.lean, line 368. The attribute's comment: “the implication (3) => (2)”.

Tag 0960, the implication (3) ⟹ (2). An object of D(X_étale, Λ) represented by a bounded above complex of flat constructible sheaves of Λ-modules is represented by a bounded above complex each of whose terms is a finite direct sum of sheaves j_{U!} Λ-underline with U an affine object of the small étale site of X.

This is the composite of (3) ⟹ (1), Stacks.EtaleCohomology.isConstructible_of_isRepresentedByBoundedAboveConstructibleFlatComplex, with (1) ⟹ (2), Stacks.EtaleCohomology.isRepresentedByAffineShriekSumComplex_of_isConstructible. No boundedness hypothesis on K is needed here: condition (3) exhibits a complex which vanishes above some degree a, and DerivedCategory.isLE_Q_obj_iff transports that bound to K.

public theorem isRepresentedByAffineShriekSumComplex_of_constructibleFlat
    [CompactSpace X.obj] [QuasiSeparatedSpace X.obj]
    (K : DerivedCategory (Sheaf (SmallEtale.topology B X.obj X.property)
      (ModuleCat.{max (u + 1) r} Λ)))
    (hK : IsRepresentedByBoundedAboveConstructibleFlatComplex.{u, max (u + 1) r, r} B X Λ K) :
    IsRepresentedByAffineShriekSumComplex.{u, r} B X Λ K

Stacks.EtaleCohomology.isConstructible_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/ShriekSumResolution.lean, line 400. References: SGA 4½ Rapport (4.7), “(1) ⇒ (3)”.

Tag 0960. Let X be a quasi-compact and quasi-separated scheme, let Λ be a Noetherian ring and let K ∈ D^-(X_étale, Λ), the bound being the hypothesis hvan. Then the following are equivalent:

  1. K lies in D_c(X_étale, Λ), i.e. every cohomology sheaf of K is constructible;
  2. K is represented by a bounded above complex whose terms are finite direct sums of sheaves j_{U!} Λ-underline with U an affine object of the small étale site of X;
  3. K is represented by a bounded above complex of flat constructible sheaves of Λ-modules.

The equivalence is closed along the cycle (1) ⟹ (2) ⟹ (3) ⟹ (1), by Stacks.EtaleCohomology.isRepresentedByAffineShriekSumComplex_of_isConstructible, Stacks.EtaleCohomology.isRepresentedByBoundedAboveConstructibleFlatComplex_of_shriekSum and Stacks.EtaleCohomology.isConstructible_of_isRepresentedByBoundedAboveConstructibleFlatComplex, whose weak Serre hypothesis is discharged at this coefficient universe by Stacks 03RZ (3), AlgebraicGeometry.isWeakSerreClass_isConstructibleModuleSheafProperty. The three remaining implications are also stated separately, as the composites they are; hvan is used only in (1) ⟹ (2), the other two steps producing their own bound.

public theorem isConstructible_tfae
    [CompactSpace X.obj] [QuasiSeparatedSpace X.obj]
    (K : DerivedCategory (Sheaf (SmallEtale.topology B X.obj X.property)
      (ModuleCat.{max (u + 1) r} Λ))) (b : ℤ)
    (hvan : ∀ i : ℤ, b < i → IsZero ((DerivedCategory.homologyFunctor
      (Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{max (u + 1) r} Λ)) i).obj K)) :
    List.TFAE
      [IsConstructible B X Λ K,
        IsRepresentedByAffineShriekSumComplex.{u, r} B X Λ K,
        IsRepresentedByBoundedAboveConstructibleFlatComplex.{u, max (u + 1) r, r} B X Λ K]
Tag 0961, a lemma

Tag 0961 in the Stacks Project.

Stacks.EtaleCohomology.minus_and_isConstructible_derivedTensor_of_arbitraryScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/DerivedTensorArbitraryScheme.lean, line 334. The attribute's comment: “for an arbitrary scheme: both halves of the conclusion, the boundedness estimate for the derived tensor product and the constructible case alike, from the bounded above representative with flat etale stalks of Stacks 05T7 and 093B (2), the quasi-compact quasi-separated case of Stacks 0960 and 095I, and Zariski descent for constructibility, Stacks 095F”.

Stacks 0961. Let X be a scheme, Λ a Noetherian ring and K, L ∈ D_c^-(X_étale, Λ). Then K ⊗_Λ^L L is in D_c^-(X_étale, Λ): it is bounded above, and all of its cohomology sheaves are constructible.

Nothing is asked of the scheme, and no part of the conclusion is assumed. The only thing asked of the derived tensor product T is hcomp, which says that T is the derived tensor product: its value on a pair of complexes whose right member is a bounded above complex of flat sheaves is the total tensor complex. Both halves of the conclusion come from one complex Tot(P ⊗_Λ G), where P and G are the bounded above representatives with flat étale stalks of AlgebraicGeometry.exists_isStrictlyLE_flat_etaleModuleStalk_of_isLE — boundedness above with the bound a + b, and constructibility of the cohomology sheaves by Stacks.EtaleCohomology.isConstructibleModuleSheaf_homology_mapBifunctor.

public theorem minus_and_isConstructible_derivedTensor_of_arbitraryScheme
    (hcomp : IsDerivedTensorOnFlatComplexes.{u, w} B X Λ T)
    (K L : DerivedCategory.Minus (Sheaf (SmallEtale.topology B X.obj X.property)
      (ModuleCat.{max (u + 1) w} Λ)))
    (hK : IsConstructible B X Λ K.obj) (hL : IsConstructible B X Λ L.obj) :
    (DerivedCategory.TStructure.t (C := Sheaf (SmallEtale.topology B X.obj X.property)
        (ModuleCat.{max (u + 1) w} Λ))).minus ((T.obj K.obj).obj L.obj) ∧
      IsConstructible B X Λ ((T.obj K.obj).obj L.obj)

Stacks.EtaleCohomology.minus_and_isConstructible_etaleModuleSheafDerivedTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/EtaleModuleSheafDerivedTensor.lean, line 299. The attribute's comment: “for the derived tensor product of sheaves of Lambda-modules on the small etale site of an arbitrary scheme, built on K-flat resolutions (Stacks 06YS, 06YU) and shown to be computed by total tensor complexes on bounded above complexes of flat sheaves (Stacks 06YQ)”.

Stacks 0961. Let X be a scheme, Λ a Noetherian ring and K, L ∈ D_c^-(X_étale, Λ). Then K ⊗_Λ^L L is in D_c^-(X_étale, Λ): it is bounded above, and all of its cohomology sheaves are constructible.

The derived tensor product is Stacks.EtaleCohomology.etaleModuleSheafDerivedTensor, the derived functor of the tensor product of sheaves of Λ-modules on K-flat resolutions, and nothing is assumed of it or of X. That it is computed by the total tensor complex on a bounded above complex of flat sheaves is proved, Stacks.EtaleCohomology.isDerivedTensorOnFlatComplexes_etaleModuleSheafDerivedTensor, and the rest is the arbitrary-scheme argument of Stacks.EtaleCohomology.minus_and_isConstructible_derivedTensor_of_arbitraryScheme.

theorem minus_and_isConstructible_etaleModuleSheafDerivedTensor (X : B.Scheme)
    (K L : DerivedCategory.Minus (Sheaf (SmallEtale.topology B X.obj X.property)
      (ModuleCat.{max (u + 1) w} Λ)))
    (hK : IsConstructible B X Λ K.obj) (hL : IsConstructible B X Λ L.obj) :
    (DerivedCategory.TStructure.t (C := Sheaf (SmallEtale.topology B X.obj X.property)
        (ModuleCat.{max (u + 1) w} Λ))).minus
        (((etaleModuleSheafDerivedTensor B X Λ).obj K.obj).obj L.obj) ∧
      IsConstructible B X Λ (((etaleModuleSheafDerivedTensor B X Λ).obj K.obj).obj L.obj)
Sources
LeanStacks.EtaleCohomology.ConstructibleDerivedCategory · Stacks.EtaleCohomology.ConstructibleEtaleDerivedCategory · Stacks.EtaleCohomology.isConstructible_derivedRestriction · Stacks.EtaleCohomology.isConstructible_derivedModuleExtensionByZero · Stacks.EtaleCohomology.isConstructible_derivedPullback · Stacks.EtaleCohomology.isConstructible_mapDerivedCategory_smallEtaleSheafPullback · Stacks.EtaleCohomology.exists_shriekConstant_cover_of_isConstructible_homology · Stacks.EtaleCohomology.exists_shriekConstant_cover_of_isConstructibleModuleEtaleSheaf

Section59.77 Tor finite with constructible cohomology#

Section 59.77 of the Stacks Project, Tag 0F4M. 6 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03TQ, a definition

Tag 03TQ in the Stacks Project.

Stacks.EtaleCohomology.CanonicalConstructibleFiniteTorDerivedCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/CanonicalFiniteTorDimension.lean, line 135. The attribute's comment: “the derived tensor products on the slices of the constant-coefficient étale ringed site are constructed here, by Stacks 06YU at free universes, so no derived tensor product is assumed”. References: SGA 5 III (1.1), “D_ctf(X) definition”; SGA 4½ Rapport (4.6), “ii)”; SGA 5 IIIB (6.1), “D_ctf(-)”; SGA 4½ Th finitude (1.7).

Stacks 03TQ. The category D_{ctf}(X_étale, Λ): the full subcategory of the constructible derived category of Stacks 095W consisting of the objects whose image in the derived category of modules over the constant coefficient ring sheaf has locally finite Tor dimension in the sense of Stacks 08FZ.

Tor dimension is measured against the derived tensor products Stacks.EtaleCohomology.canonicalSliceDerivedTensorProduct of Stacks 06YU on the slices of that ringed site.

abbrev CanonicalConstructibleFiniteTorDerivedCategory

Stacks.EtaleCohomology.ConstructibleFiniteTorDerivedCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/FiniteTorDimension.lean, line 106. References: SGA 5 III (1.1), “D_ctf(X) definition”; SGA 4½ Rapport (4.6), “ii)”; SGA 5 IIIB (6.1), “D_ctf(-)”.

Stacks 03TQ. The category D_{ctf}(X_étale, Λ): the full subcategory of the constructible derived category of Stacks 095W consisting of the objects whose image in the derived category of modules over the constant coefficient ring sheaf has locally finite Tor dimension in the sense of Stacks 08FZ, measured against the derived tensor products T on the slices of that ringed site.

abbrev ConstructibleFiniteTorDerivedCategory
    (T : ∀ U : (constantCoefficientRingedSite.{u, w, r} B X Λ).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, max (u + 1) w r, d}
        ((constantCoefficientRingedSite.{u, w, r} B X Λ).over U))
Tag 03TT, a lemma

Tag 03TT in the Stacks Project.

Stacks.EtaleCohomology.exists_constructibleFiniteTor_iff_isRepresentedByConstructibleFlatComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/ConstructibleFiniteTorRepresentation.lean, line 556. The attribute's comment: “the equivalence of (1) and (2)”. References: SGA 4½ Rapport (4.6), “special case”.

Let Λ be a Noetherian ring and X a quasi-compact and quasi-separated scheme. An object K of D(X_étale, Λ) lies in D_ctf(X_étale, Λ) (Tag 03TQ) if and only if it can be represented by a finite complex of constructible flat sheaves of Λ-modules.

D_ctf(X_étale, Λ) is the category of Tag 03TQ, measured against the given derived tensor products T on the slices; membership of K is the existence of an object of that category isomorphic to K.

public theorem exists_constructibleFiniteTor_iff_isRepresentedByConstructibleFlatComplex
    (T : ∀ U : (constantCoefficientRingedSite.{u, max (u + 1) r, r} B X Λ).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, max (u + 1) r, d}
        ((constantCoefficientRingedSite.{u, max (u + 1) r, r} B X Λ).over U))
    (K : DerivedCategory
      (Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{max (u + 1) r} Λ))) :
    (∃ L : ConstructibleFiniteTorDerivedCategory.{u, max (u + 1) r, r, d} B X Λ T,
        Nonempty (L.obj.obj ≅ K)) ↔
      IsRepresentedByConstructibleFlatComplex.{u, max (u + 1) r, r} B X Λ K

Stacks.EtaleCohomology.exists_constructibleFlat_representative_of_hasTorAmplitude, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/ConstructibleFiniteTorRepresentation.lean, line 682. The attribute's comment: “the last sentence: Tor amplitude in [a, b] gives a representative F^a → ⋯ → F^b by constructible flat sheaves”.

Let Λ be a Noetherian ring and X a quasi-compact and quasi-separated scheme. If K ∈ D_ctf(X_étale, Λ) has Tor amplitude in [a, b], then K can be represented by a complex F^a → ⋯ → F^b of constructible flat sheaves of Λ-modules.

Tor amplitude is that of the associated object of D(𝒪), 𝒪 the constant coefficient ring sheaf, against a derived tensor product T₀ on 𝒪 (Stacks 08FZ (1)); the hypothesis hK is the constructibility of the cohomology sheaves of K.

public theorem exists_constructibleFlat_representative_of_hasTorAmplitude
    (T₀ : Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, max (u + 1) r, d}
      (constantCoefficientRingedSite.{u, max (u + 1) r, r} B X Λ))
    (K : DerivedCategory
      (Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{max (u + 1) r} Λ)))
    (hK : IsConstructible B X Λ K) (a b : ℤ)
    (hamp : HasTorAmplitude T₀
      ((moduleSheafOverConstantCoefficientsFunctor.{u, max (u + 1) r, r}
        B X Λ).mapDerivedCategory.obj K) a b) :
    ∃ F : CochainComplex
        (Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{max (u + 1) r} Λ)) ℤ,
      F.IsStrictlyGE a ∧ F.IsStrictlyLE b ∧
        (∀ i : ℤ, IsConstructibleFlatModuleSheaf B X Λ (F.X i)) ∧
        Nonempty (DerivedCategory.Q.obj F ≅ K)

Stacks.EtaleCohomology.isConstructible_of_isRepresentedByConstructibleFlatComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/ConstructibleFlat.lean, line 275. The attribute's comment: “the direction (2) => (1), the constructible-cohomology half, from the weak Serre property hSerre of the constructible sheaves of modules”.

Tag 03TT, the direction (2) ⟹ (1) for the constructible-cohomology condition. An object of D(X_étale, Λ) represented by a bounded complex of constructible flat sheaves of Λ-modules has constructible cohomology sheaves, so it lies in the constructible derived category of Tag 095W.

The cohomology sheaf in degree i is a cokernel of a map from the term in degree i - 1 into the sheaf of cycles, which is a kernel of a map between the terms in degrees i and i + 1; each term is constructible, and the hypothesis hSerre that the constructible sheaves of Λ-modules form a weak Serre subcategory of all sheaves of Λ-modules — Tag 0754, closure under kernels, cokernels, extensions and isomorphism — carries constructibility to the kernel and then to the cokernel.

public theorem isConstructible_of_isRepresentedByConstructibleFlatComplex
    (hSerre : (isConstructibleModuleSheafProperty.{u, w, r} B X Λ).IsWeakSerreClass)
    (K : DerivedCategory
      (Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{w} Λ)))
    (hK : IsRepresentedByConstructibleFlatComplex.{u, w, r} B X Λ K) :
    IsConstructible B X Λ K

Stacks.EtaleCohomology.isConstructibleFiniteTor_iff_isRepresentedByFlatConstructibleComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/ConstructibleFlatCharacterization.lean, line 583. References: SGA 4½ Rapport (4.6), “special case”.

Stacks 03TT. Let Λ be a Noetherian ring, let X be a quasi-compact and quasi-separated scheme and let K ∈ D(X_étale, Λ). The following are equivalent:

  1. K ∈ D_ctf(X_étale, Λ), that is, K has constructible cohomology sheaves and the image of K over the constant coefficient ringed site of Tag 03TR has locally finite Tor dimension in the sense of Tag 08FZ;
  2. K is represented by a finite complex of constructible flat sheaves of Λ-modules.

In fact, if K has Tor amplitude in [a, b] then it can be represented by a complex F^a → ⋯ → F^b with each F^p a constructible flat sheaf of Λ-modules.

Condition (1) is membership of Stacks.EtaleCohomology.ConstructibleFiniteTorDerivedCategory, whose defining property is exactly this conjunction; condition (2) is Stacks.EtaleCohomology.IsRepresentedByFlatConstructibleComplex.

Condition (1) is stated absolutely: the derived tensor products against which finite Tor dimension and Tor amplitude are measured are not parameters of the statement but the canonical ones, Stacks.SheafOfModules.canonicalDerivedTensorProduct of Tag 06YU on the constant coefficient ringed site and on each of its slices. Those exist at the universes this chapter works in — the site is an AlgebraicGeometry.RingedSite.{u + 1, u, max (u + 1) r}, whose morphisms and whose sections lie in different universes — because the K-flat resolutions Tag 06YU is built from resolve by flat modules supplied by a flat cover and so relate none of the three universes of the site. The two directions and the refinement are proved above against an arbitrary datum, which is the more general statement; the tag is carried here, where the quantifier over the datum is gone and the equivalence is therefore not vacuous.

public theorem isConstructibleFiniteTor_iff_isRepresentedByFlatConstructibleComplex
    (K : DerivedCategory (Sheaf (SmallEtale.topology B X.obj X.property)
      (ModuleCat.{max (u + 1) r} Λ))) :
    ((IsConstructible B X Λ K ∧
        Stacks.SheafOfModules.DerivedTensorProduct.LocallyHasFiniteTorDimension
          (X := constantCoefficientRingedSite.{u, max (u + 1) r, r} B X Λ)
          (fun U => Stacks.SheafOfModules.canonicalDerivedTensorProductGeneral.{u + 1, u,
            max (u + 1) r, d}
            ((constantCoefficientRingedSite.{u, max (u + 1) r, r} B X Λ).over U))
          ((moduleSheafOverConstantCoefficientsFunctor.{u, max (u + 1) r,
            r} B X Λ).mapDerivedCategory.obj K)) ↔
      IsRepresentedByFlatConstructibleComplex.{u, r} B X Λ K) ∧
    ∀ a b : ℤ, a ≤ b → IsConstructible B X Λ K →
      Stacks.SheafOfModules.DerivedTensorProduct.HasTorAmplitude
        (Stacks.SheafOfModules.canonicalDerivedTensorProductGeneral.{u + 1, u, max (u + 1) r, d}
          (constantCoefficientRingedSite.{u, max (u + 1) r, r} B X Λ))
        ((moduleSheafOverConstantCoefficientsFunctor.{u, max (u + 1) r,
          r} B X Λ).mapDerivedCategory.obj K) a b →
      ∃ F : CochainComplex (Sheaf (SmallEtale.topology B X.obj X.property)
          (ModuleCat.{max (u + 1) r} Λ)) ℤ,
        F.IsStrictlyGE a ∧ F.IsStrictlyLE b ∧
        (∀ i : ℤ, IsConstructibleModuleSheaf B X Λ (F.X i)) ∧
        (∀ i : ℤ, AlgebraicGeometry.SheafOfModules.IsFlat.{u, u + 1, max (u + 1) r,
          max (u + 1) r} (O := (constantCoefficientRingedSite.{u, max (u + 1) r, r} B X Λ).O)
          ((moduleSheafOverConstantCoefficientsFunctor.{u, max (u + 1) r,
            r} B X Λ).obj (F.X i))) ∧
        Nonempty (DerivedCategory.Q.obj F ≅ K)

Stacks.EtaleCohomology.locallyHasFiniteTorDimension_of_isRepresentedByConstructibleFlatComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/ConstructibleFlatFiniteTor.lean, line 239. The attribute's comment: “the finite-tor-dimension half of the direction (2) => (1), at a free coefficient universe; the constructible-cohomology half of that direction is Stacks.EtaleCohomology.isConstructible_of_isRepresentedByConstructibleFlatComplex and the two are combined in Stacks.EtaleCohomology.constructibleFiniteTorDerivedCategoryOfConstructibleFlatComplex”. References: SGA 4½ Rapport (4.6), “partial”.

Tag 03TT, the finite-Tor-dimension half of the direction (2) ⟹ (1). An object of D(X_étale, Λ) represented by a bounded complex of constructible flat sheaves of Λ-modules has locally finite Tor dimension in the sense of Tag 08FZ, read on its image under the change of coefficients of Tag 03TR and measured against the derived tensor products T on the slices of the constant coefficient ringed site.

Each term of the complex becomes a flat module over the constant coefficient ring sheaf, by AlgebraicGeometry.isFlat_moduleSheafOverConstantCoefficients_of_isConstructibleFlatModuleSheaf; the change of coefficients is exact, so applied degreewise it carries the complex to a representative of the image of K; and Stacks.SheafOfModules.DerivedTensorProduct.FreeModuleUniverse.locallyHasFiniteTorDimension_of_flatRepresentative reads Stacks 08G1 on every slice.

theorem locallyHasFiniteTorDimension_of_isRepresentedByConstructibleFlatComplex
    (T : ∀ U : (constantCoefficientRingedSite.{u, w, r} B X Λ).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, max (u + 1) w r, d}
        ((constantCoefficientRingedSite.{u, w, r} B X Λ).over U))
    (K : DerivedCategory
      (Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{w} Λ)))
    (hK : IsRepresentedByConstructibleFlatComplex.{u, w, r} B X Λ K) :
    Stacks.SheafOfModules.DerivedTensorProduct.LocallyHasFiniteTorDimension
      (X := constantCoefficientRingedSite.{u, w, r} B X Λ) T
      ((moduleSheafOverConstantCoefficientsFunctor.{u, w, r} B X Λ).mapDerivedCategory.obj K)

Stacks.EtaleCohomology.constructibleFiniteTorDerivedCategoryOfConstructibleFlatComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/ConstructibleFlatFiniteTor.lean, line 320. The attribute's comment: “the direction (2) => (1), both halves, with the weak Serre property of the constructible sheaves of modules discharged by Tag 03RZ (3) at the coefficient universe max (u + 1) r. The direction (1) => (2) and the sharpened bound on the length of the representative are not proved”. References: SGA 4½ Rapport (4.6), “partial”.

Tag 03TT, the direction (2) ⟹ (1). An object of D(X_étale, Λ) represented by a bounded complex of constructible flat sheaves of Λ-modules is an object of D_{ctf}(X_étale, Λ): its cohomology sheaves are constructible and its image under the change of coefficients of Tag 03TR has locally finite Tor dimension.

The two halves are Stacks.EtaleCohomology.isConstructible_of_isRepresentedByConstructibleFlatComplex and Stacks.EtaleCohomology.locallyHasFiniteTorDimension_of_isRepresentedByConstructibleFlatComplex. The weak Serre property of the constructible sheaves of modules, which the first of them asks for, is Tag 03RZ (3) at the coefficient universe max (u + 1) r; that is why the module sections are fixed there rather than left free, and it is why nothing is carried as a hypothesis.

def constructibleFiniteTorDerivedCategoryOfConstructibleFlatComplex
    (T : ∀ U : (constantCoefficientRingedSite.{u, max (u + 1) r, r} B X Λ).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, max (u + 1) r, d}
        ((constantCoefficientRingedSite.{u, max (u + 1) r, r} B X Λ).over U))
    (K : DerivedCategory
      (Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{max (u + 1) r} Λ)))
    (hK : IsRepresentedByConstructibleFlatComplex.{u, max (u + 1) r, r} B X Λ K) :
    ConstructibleFiniteTorDerivedCategory.{u, max (u + 1) r, r, d} B X Λ T
Tag 03TR, a remark

Tag 03TR in the Stacks Project.

AlgebraicGeometry.stalk_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstantCoefficients.lean, line 681. The attribute's comment: “finiteness in each degree”.

Every term of the stalk at a geometric point of a complex of constructible sheaves of Λ-modules is a finite Λ-module.

The constructibility hypothesis is spelled out as stratumwise local constancy with finitely generated values, which is what AlgebraicGeometry.IsConstructibleModuleSheaf — Tag 03RW part (3) — unfolds to; stating it this way is what makes the statement available for a coefficient ring that is not commutative, the definition of Tag 03RW being given for a Noetherian ring.

theorem stalk_finite
    [∀ (S T : B.Scheme) (f : T ⟶ S),
      ((smallEtaleBaseChange B f).sheafPushforwardContinuous
        (ModuleCat.{w} Λ) (SmallEtale.topology B S.obj S.property)
        (SmallEtale.topology B T.obj T.property)).IsRightAdjoint]
    [∀ (T : B.Scheme) (V : SmallEtale B T.obj T.property),
      HasWeakSheafify ((SmallEtale.topology B T.obj T.property).over V) (ModuleCat.{w} Λ)]
    (K : CochainComplex
      (Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{w} Λ)) ℤ)
    (hconstructible : ∀ i : ℤ,
      IsStratifiedLocallyConstantWith B X Λ (ModuleCat.isFG Λ) (K.X i))
    (s : GeometricPoint X.obj) (i : ℤ) :
    Module.Finite Λ ((etaleModuleStalkFunctor B X Λ s).obj (K.X i))

AlgebraicGeometry.stalk_projective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstantCoefficients.lean, line 971. The attribute's comment: “projectivity in each degree”.

Every term of the stalk at a geometric point of a complex of constructible sheaves of Λ-modules which are flat over the constant coefficient ring sheaf is a projective Λ-module.

theorem stalk_projective
    [∀ (S T : B.Scheme) (f : T ⟶ S),
      ((smallEtaleBaseChange B f).sheafPushforwardContinuous
        (ModuleCat.{w} Λ) (SmallEtale.topology B S.obj S.property)
        (SmallEtale.topology B T.obj T.property)).IsRightAdjoint]
    [∀ (T : B.Scheme) (V : SmallEtale B T.obj T.property),
      HasWeakSheafify ((SmallEtale.topology B T.obj T.property).over V) (ModuleCat.{w} Λ)]
    (K : CochainComplex
      (Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{w} Λ)) ℤ)
    (hconstructible : ∀ i : ℤ, IsConstructibleModuleSheaf B X Λ (K.X i))
    (hflat : ∀ i : ℤ, Stacks.SheafOfModules.IsFlat.{u, u + 1, max (u + 1) w r, max (u + 1) w r}
      (moduleSheafOverConstantCoefficients.{u, w, r} B X Λ (K.X i)))
    (s : GeometricPoint X.obj) (i : ℤ) :
    Module.Projective Λ ((etaleModuleStalkFunctor B X Λ s).obj (K.X i))

AlgebraicGeometry.stalk_isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstantCoefficients.lean, line 992. The attribute's comment: “perfection of the stalk complex”.

The stalk at a geometric point of a bounded complex of constructible sheaves of Λ-modules which are flat over the constant coefficient ring sheaf is a perfect object of the derived category of Λ-modules.

theorem stalk_isPerfect
    [∀ (S T : B.Scheme) (f : T ⟶ S),
      ((smallEtaleBaseChange B f).sheafPushforwardContinuous
        (ModuleCat.{w} Λ) (SmallEtale.topology B S.obj S.property)
        (SmallEtale.topology B T.obj T.property)).IsRightAdjoint]
    [∀ (T : B.Scheme) (V : SmallEtale B T.obj T.property),
      HasWeakSheafify ((SmallEtale.topology B T.obj T.property).over V) (ModuleCat.{w} Λ)]
    (K : CochainComplex
      (Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{w} Λ)) ℤ)
    (hbounded : (CochainComplex.plus _ K) ∧ (CochainComplex.minus _ K))
    (hconstructible : ∀ i : ℤ, IsConstructibleModuleSheaf B X Λ (K.X i))
    (hflat : ∀ i : ℤ, Stacks.SheafOfModules.IsFlat.{u, u + 1, max (u + 1) w r, max (u + 1) w r}
      (moduleSheafOverConstantCoefficients.{u, w, r} B X Λ (K.X i)))
    (s : GeometricPoint X.obj)
    [HasDerivedCategory (ModuleCat.{w} Λ)] :
    StacksDraft.Perfect.IsPerfect
      (DerivedCategory.Q.obj (etaleModuleStalkComplex B X Λ s K))
Tag 0962, a lemma

Tag 0962 in the Stacks Project.

Stacks.EtaleCohomology.isConstructibleFiniteTor_derivedRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/RestrictionExtensionByZeroMembership.lean, line 231. The attribute's comment: “part (1): for K in D_ctf(X_et, Λ), the restriction K|_U — the image of K under the derived restriction functor of Tag 03S3 — satisfies membership of D_ctf(U_et, Λ)”.

Stacks 0962, part (1). Let Λ be a Noetherian ring and let j : U ⟶ X be an étale morphism of schemes, the object U of the small étale site of X. If K lies in D_ctf(X_étale, Λ), then its restriction K|_U, the image of K under the derived functor of the restriction functor of Tag 03S3, lies in D_ctf(U_étale, Λ).

This is Stacks.EtaleCohomology.constructibleFiniteTorDerivedCategoryRestriction, whose output is K|_U by construction: constructibility by Tag 095X part (1), and locally finite Tor dimension by the finite-Tor-dimension half of Tag 0963 at the structure morphism of U, transported along Tag 03S3 part (3).

public theorem isConstructibleFiniteTor_derivedRestriction
    (T : ∀ V : (constantCoefficientRingedSite.{u, max (u + 1) r, r} B X Λ).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, max (u + 1) r, d}
        ((constantCoefficientRingedSite.{u, max (u + 1) r, r} B X Λ).over V))
    (T' : ∀ V : (constantCoefficientRingedSite.{u, max (u + 1) r, r} B U.obj.left Λ).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, max (u + 1) r, d}
        ((constantCoefficientRingedSite.{u, max (u + 1) r, r} B U.obj.left Λ).over V))
    (K : DerivedCategory (Sheaf (SmallEtale.topology B X.obj X.property)
      (ModuleCat.{max (u + 1) r} Λ)))
    (hK : IsConstructibleFiniteTor.{u, max (u + 1) r, r, d} B X Λ T K) :
    IsConstructibleFiniteTor.{u, max (u + 1) r, r, d} B U.obj.left Λ T'
      ((moduleRestriction.{u, r, max (u + 1) r} B X.obj X.property U Λ).mapDerivedCategory.obj
        K)

Stacks.EtaleCohomology.isConstructibleFiniteTor_derivedExtensionByZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/RestrictionExtensionByZeroMembership.lean, line 260. The attribute's comment: “part (2): for j quasi-compact and quasi-separated and M in D_ctf(U_et, Λ), the extension by zero j_! M — the image of M under the derived extension-by-zero functor of Tag 03S3 — satisfies membership of D_ctf(X_et, Λ)”.

Stacks 0962, part (2). Let Λ be a Noetherian ring and let j : U ⟶ X be an étale morphism of schemes, the object U of the small étale site of X, which is quasi-compact and quasi-separated. If M lies in D_ctf(U_étale, Λ), then its extension by zero j_! M, the image of M under the derived functor of the extension-by-zero functor of Tag 03S3, lies in D_ctf(X_étale, Λ).

This is Stacks.EtaleCohomology.constructibleFiniteTorDerivedCategoryExtensionByZero, whose output is j_! M by construction: constructibility by Tag 095X part (2), and locally finite Tor dimension read at the stalks by Tag 03S5 and Tag 0DJJ.

public theorem isConstructibleFiniteTor_derivedExtensionByZero
    (hqc : QuasiCompact (B.inclusion.map U.obj.hom))
    (hqs : QuasiSeparated (B.inclusion.map U.obj.hom))
    (T : ∀ V : (constantCoefficientRingedSite.{u, max (u + 1) r, r} B X Λ).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, max (u + 1) r, d}
        ((constantCoefficientRingedSite.{u, max (u + 1) r, r} B X Λ).over V))
    (T' : ∀ V : (constantCoefficientRingedSite.{u, max (u + 1) r, r} B U.obj.left Λ).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, max (u + 1) r, d}
        ((constantCoefficientRingedSite.{u, max (u + 1) r, r} B U.obj.left Λ).over V))
    (M : DerivedCategory (Sheaf (SmallEtale.topology B U.obj.left.obj U.obj.left.property)
      (ModuleCat.{max (u + 1) r} Λ)))
    (hM : IsConstructibleFiniteTor.{u, max (u + 1) r, r, d} B U.obj.left Λ T' M) :
    IsConstructibleFiniteTor.{u, max (u + 1) r, r, d} B X Λ T
      ((moduleExtensionByZero.{u, r} B X.obj X.property U Λ).mapDerivedCategory.obj M)

Stacks.EtaleCohomology.constructibleFiniteTorDerivedCategoryEtale, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/ShriekFiniteTor.lean, line 479. The attribute's comment: “both parts, in the two components of the pair: part (1) with K|_U the restriction of Tag 03S3, part (2) with the quasi-compactness and quasi-separatedness of j as the premises of that component. The constructible-cohomology halves are the two parts of Tag 095X; the finite-Tor-dimension half of part (1) is that of Tag 0963 at the structure morphism of U, and that of part (2) is read at the stalks, by Tag 03S5 for sheaves of modules and Tag 0DJJ on the slices over affine objects, over which U ×_X V' is quasi-compact”.

Stacks 0962. Let Λ be a Noetherian ring and let j : U ⟶ X be an étale morphism of schemes, that is an object U of the small étale site of X. Then

  1. the restriction K|_U of an object K of D_ctf(X_étale, Λ) is an object of D_ctf(U_étale, Λ), and
  2. the extension by zero j_! M of an object M of D_ctf(U_étale, Λ) is an object of D_ctf(X_étale, Λ), when j is quasi-compact and quasi-separated.

The two clauses are the two components of the pair; the quasi-compactness and quasi-separatedness of j, which the source asks for in part (2) only, are hypotheses of the second component alone. The first component is Stacks.EtaleCohomology.constructibleFiniteTorDerivedCategoryRestriction and the second Stacks.EtaleCohomology.constructibleFiniteTorDerivedCategoryExtensionByZero.

public def constructibleFiniteTorDerivedCategoryEtale
    (T : ∀ V : (constantCoefficientRingedSite.{u, max (u + 1) r, r} B X Λ).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, max (u + 1) r, d}
        ((constantCoefficientRingedSite.{u, max (u + 1) r, r} B X Λ).over V))
    (T' : ∀ V : (constantCoefficientRingedSite.{u, max (u + 1) r, r} B U.obj.left Λ).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, max (u + 1) r, d}
        ((constantCoefficientRingedSite.{u, max (u + 1) r, r} B U.obj.left Λ).over V)) :
    (ConstructibleFiniteTorDerivedCategory.{u, max (u + 1) r, r, d} B X Λ T →
        ConstructibleFiniteTorDerivedCategory.{u, max (u + 1) r, r, d} B U.obj.left Λ T') ×
      (QuasiCompact (B.inclusion.map U.obj.hom) →
        QuasiSeparated (B.inclusion.map U.obj.hom) →
        ConstructibleFiniteTorDerivedCategory.{u, max (u + 1) r, r, d} B U.obj.left Λ T' →
        ConstructibleFiniteTorDerivedCategory.{u, max (u + 1) r, r, d} B X Λ T)
Tag 0963, a lemma

Tag 0963 in the Stacks Project.

Stacks.EtaleCohomology.constructibleFiniteTorDerivedCategoryPullback_unconditional, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstructibleComplexes/PullbackFiniteTorStalkwise.lean, line 431. The attribute's comment: “the constructible-cohomology half by Tag 095Y, the finite-Tor-dimension half by Tag 0DJJ read at the stalks on the slices of the constant coefficient ringed sites”. References: SGA 5 III (1.2), “more general”; SGA 5 IIIB (6.2), “special case”.

Stacks 0963. Let Λ be a Noetherian ring and f : X ⟶ Y a morphism of schemes. The derived inverse image of an object of D_{ctf}(Y_étale, Λ) is an object of D_{ctf}(X_étale, Λ).

Constructibility of the cohomology sheaves of Lf^*K is Tag 095Y, which is Stacks.EtaleCohomology.constructibleDerivedCategoryPullback. Locally finite Tor dimension of its image under the change of coefficients is Stacks.EtaleCohomology.pullbackPreservesLocallyFiniteTorDimension.

Stacks.EtaleCohomology.constructibleFiniteTorDerivedCategoryPullback is the same statement taking the finite-Tor-dimension half as a hypothesis, which this one discharges.

public def constructibleFiniteTorDerivedCategoryPullback_unconditional
    (T : ∀ U : (constantCoefficientRingedSite.{u, max (u + 1) w, r} B Y Λ).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, max (u + 1) w r, d}
        ((constantCoefficientRingedSite.{u, max (u + 1) w, r} B Y Λ).over U))
    (T' : ∀ U : (constantCoefficientRingedSite.{u, max (u + 1) w, r} B X Λ).C,
      Stacks.SheafOfModules.DerivedTensorProduct.{u + 1, u, max (u + 1) w r, d}
        ((constantCoefficientRingedSite.{u, max (u + 1) w, r} B X Λ).over U))
    (K : ConstructibleFiniteTorDerivedCategory.{u, max (u + 1) w, r, d} B Y Λ T) :
    ConstructibleFiniteTorDerivedCategory.{u, max (u + 1) w, r, d} B X Λ T'
Tag 09BI, a lemma

Tag 09BI in the Stacks Project.

AlgebraicGeometry.exists_etaleCover_constantFiniteProjectiveComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ConstantPerfectComplexEtale.lean, line 141.

Tag 09BI, with its finite-Tor-dimension input named at the points of the site.

Let X be a connected scheme in a big étale site and Λ a Noetherian ring. Let K be a bounded object of the derived category of sheaves of Λ-modules on the small étale site of X whose cohomology sheaves are locally constant of finite type, and suppose that at every point q of the site lifting to an object V the derived fibre of the restriction to the slice over V of a representative of K has a bounded flat representative over Λ — the finite-Tor-dimension half of membership in D_{ctf}(X_{étale}, Λ). Then there is a single finite complex E of finite projective Λ-modules and an étale covering of X over every member of which K becomes the constant complex attached to E.

theorem exists_etaleCover_constantFiniteProjectiveComplex
    (K : DerivedCategory.Bounded
      (Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} Λ)))
    (hK : ∀ n : ℤ, Stacks.ConstantSheaf.IsFiniteTypeLocallyConstantModuleSheaf.{u, u + 1, u, u}
      (SmallEtale.topology B X.obj X.property) Λ
      ((DerivedCategory.homologyFunctor
        (Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} Λ)) n).obj K.obj))
    (hflat : ∀ (T : CochainComplex
        (Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} Λ)) ℤ)
      (V : SmallEtale B X.obj X.property)
      (q : (SmallEtale.topology B X.obj X.property).Point.{u + 1}) (z : q.fiber.obj V),
      (K.obj ≅ DerivedCategory.Q.obj T) →
      ∃ c d : ℤ, StacksDraft.Perfect.HasFlatRepresentative.{u, u + 1}
        (((q.over z).sheafFiber (A := ModuleCat.{u + 1} Λ)).mapDerivedCategory.obj
          (DerivedCategory.Q.obj
            ((((SmallEtale.topology B X.obj X.property).overPullback
              (ModuleCat.{u + 1} Λ) V).mapHomologicalComplex (ComplexShape.up ℤ)).obj T))) c d) :
    ∃ (E : CochainComplex (ModuleCat.{u + 1} Λ) ℤ) (a b : ℤ)
      (T : CochainComplex
        (Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} Λ)) ℤ)
      (_e : K.obj ≅ DerivedCategory.Q.obj T),
      E.IsStrictlyGE a ∧ E.IsStrictlyLE b ∧
      (∀ n : ℤ, Module.Finite Λ (E.X n)) ∧ (∀ n : ℤ, Module.Projective Λ (E.X n)) ∧
      ∃ (I : Type (u + 1)) (U : I → SmallEtale B X.obj X.property)
        (f : ∀ i, U i ⟶ SmallEtale.final B X.obj X.property),
        Sieve.ofArrows U f ∈ SmallEtale.topology B X.obj X.property
          (SmallEtale.final B X.obj X.property) ∧
        ∀ i, Nonempty (DerivedCategory.Q.obj
            ((((SmallEtale.topology B X.obj X.property).overPullback
              (ModuleCat.{u + 1} Λ) (U i)).mapHomologicalComplex (ComplexShape.up ℤ)).obj T) ≅
          DerivedCategory.Q.obj
            (((constantSheaf ((SmallEtale.topology B X.obj X.property).over (U i))
              (ModuleCat.{u + 1} Λ)).mapHomologicalComplex (ComplexShape.up ℤ)).obj E))
Sources
LeanStacks.EtaleCohomology.CanonicalConstructibleFiniteTorDerivedCategory · Stacks.EtaleCohomology.ConstructibleFiniteTorDerivedCategory · Stacks.EtaleCohomology.exists_constructibleFiniteTor_iff_isRepresentedByConstructibleFlatComplex · Stacks.EtaleCohomology.exists_constructibleFlat_representative_of_hasTorAmplitude · Stacks.EtaleCohomology.isConstructible_of_isRepresentedByConstructibleFlatComplex · Stacks.EtaleCohomology.isConstructibleFiniteTor_iff_isRepresentedByFlatConstructibleComplex · Stacks.EtaleCohomology.locallyHasFiniteTorDimension_of_isRepresentedByConstructibleFlatComplex · Stacks.EtaleCohomology.constructibleFiniteTorDerivedCategoryOfConstructibleFlatComplex

Section59.78 Torsion sheaves#

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

Tag 0DDC, a lemma

Tag 0DDC in the Stacks Project.

Stacks.EtaleCohomology.etaleCohomology_isAddTorsion_and_derivedEtaleCohomology_isAddTorsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionDerivedEtaleCohomology.lean, line 182. The attribute's comment: “parts (1) and (2), as the conjunction of the sheaf case and the D⁺ case”.

Stacks 0DDC. Let X be a quasi-compact and quasi-separated scheme.

  1. If 𝓕 is a torsion abelian sheaf on X_étale, then H^n_étale(X, 𝓕) is a torsion abelian group for all n.
  2. If K in D⁺(X_étale) has torsion cohomology sheaves, then H^n_étale(X, K) is a torsion abelian group for all n.

Part (1) is etaleCohomology_isAddTorsion and part (2) is derivedEtaleCohomology_isAddTorsion; both hold under exactly the source's hypotheses on X, so the tag's assertion is their conjunction. Here H^n_étale(X, -) is the right derived functor of global sections on the small étale site, and H^n_étale(X, K) the homology of its total right derived functor on D⁺.

theorem etaleCohomology_isAddTorsion_and_derivedEtaleCohomology_isAddTorsion (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X] :
    (∀ (F : Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}),
        Stacks.Torsion.torsionSheafProperty X.smallEtaleTopology F → ∀ n : ℕ,
        IsAddTorsion
          (((Sheaf.Γ X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}).rightDerived n).obj F)) ∧
      ∀ (K : DerivedCategory.Plus
          (Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})),
        Stacks.Torsion.torsionCohomologyProperty.{max (u + 1) v} X.smallEtaleTopology K.obj →
        ∀ n : ℤ,
        IsAddTorsion
          ((DerivedCategory.Plus.homologyFunctor AddCommGrpCat.{max (u + 1) v} n).obj
            ((Sheaf.Γ X.smallEtaleTopology
              AddCommGrpCat.{max (u + 1) v}).rightDerivedFunctorPlus.obj K))

Stacks.EtaleCohomology.etaleCohomology_isAddTorsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionEtaleCohomology.lean, line 337. The attribute's comment: “part (1) only, with no extra hypothesis; étale cohomology is the right derived functor of global sections on the small étale site. Part (2) is not proved here”. References: SGA 4 IX (1.2), “(ii), (v)”.

Stacks 0DDC (1). Let X be a quasi-compact and quasi-separated scheme. If 𝓕 is a torsion abelian sheaf on the small étale site of X, then H^n_étale(X, 𝓕) is a torsion abelian group for every n. Indeed 𝓕 is the colimit of its torsion subsheaves, étale cohomology of a quasi-compact and quasi-separated scheme commutes with filtered colimits, and the cohomology of the d-torsion subsheaf is annihilated by d.

theorem etaleCohomology_isAddTorsion (X : Scheme.{u})
    [CompactSpace X] [QuasiSeparatedSpace X]
    (F : Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})
    (hF : Stacks.Torsion.torsionSheafProperty X.smallEtaleTopology F) (n : ℕ) :
    IsAddTorsion
      (((Sheaf.Γ X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}).rightDerived n).obj F)
Tag 0DDD, a lemma

Tag 0DDD in the Stacks Project.

Stacks.EtaleCohomology.smallEtaleDerivedDirectImage, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionHigherDirectImage.lean, line 277. The attribute's comment: “part (2), the bounded-below clause: the derived direct image of an object of D^+(X_étale) is an object of D^+(Y_étale), this being the codomain of the right derived functor of f_* on bounded-below derived categories”.

The derived direct image on bounded-below derived categories of abelian étale sheaves: Rf_* : D^+(X_étale) ⥤ D^+(Y_étale), the right derived functor of f_* on bounded-below derived categories.

This definition states the first clause of part (2) of [Stacks, Tag 0DDD] — that Rf_* K is again an object of D^+(Y_étale) — which is the codomain of this functor. The remaining clause, that its cohomology sheaves are torsion when those of K are, is torsionCohomologyProperty_smallEtaleDerivedDirectImage.

public abbrev smallEtaleDerivedDirectImage :
    DerivedCategory.Plus (Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}) ⥤
      DerivedCategory.Plus (Sheaf Y.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})

Stacks.EtaleCohomology.torsionSheafProperty_rightDerived_smallEtaleDirectImageAb, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionHigherDirectImage.lean, line 346. The attribute's comment: “part (1): for f quasi-compact and quasi-separated and F a torsion abelian sheaf on X_étale, every higher direct image R^n f_* F is a torsion abelian sheaf on Y_étale”.

Part (1) of [Stacks, Tag 0DDD]. For a quasi-compact and quasi-separated morphism of schemes f : X ⟶ Y and a torsion abelian sheaf F on X_étale, the higher direct image R^n f_* F is a torsion abelian sheaf on Y_étale, for every n.

Tag 072W for abelian sheaves identifies R^n f_* F with the sheafification of the cohomology presheaf and identifies that presheaf's values with étale cohomology over V ×_Y X; affine objects are cover dense in the small étale site of Y, and for V affine the scheme V ×_Y X is quasi-compact and quasi-separated, which is where the quasi-compactness and quasi-separatedness of f enter, through compactSpace_smallEtaleBaseChange_obj and quasiSeparatedSpace_smallEtaleBaseChange_obj; Tag 0DDC (1) over that object then makes H^n(V ×_Y X, F) torsion, which is where the torsion hypothesis on F is consumed. So the cohomology presheaf is locally torsion, and the sheafification of a locally torsion presheaf is a torsion abelian sheaf.

public theorem torsionSheafProperty_rightDerived_smallEtaleDirectImageAb
    [QuasiCompact f] [QuasiSeparated f] (n : ℕ)
    (F : Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})
    (hF : torsionSheafProperty X.smallEtaleTopology F) :
    torsionSheafProperty Y.smallEtaleTopology
      (((smallEtaleDirectImageAb.{max (u + 1) v} f).rightDerived n).obj F)

Stacks.EtaleCohomology.torsionCohomologyProperty_smallEtaleDerivedDirectImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionHigherDirectImage.lean, line 405. The attribute's comment: “part (2), the torsion clause: for f quasi-compact and quasi-separated and K in D^+(X_étale) with torsion cohomology sheaves, every cohomology sheaf of Rf_* K is a torsion abelian sheaf on Y_étale. The bounded-below clause is the codomain of smallEtaleDerivedDirectImage”.

Part (2) of [Stacks, Tag 0DDD], the torsion clause. For a quasi-compact and quasi-separated morphism of schemes f : X ⟶ Y and an object K of D^+(X_étale) whose cohomology sheaves are torsion, all cohomology sheaves of Rf_* K are torsion abelian sheaves on Y_étale. That Rf_* K is again an object of D^+(Y_étale) is the codomain of smallEtaleDerivedDirectImage, which states that clause of the tag.

This is dévissage from part (1). The torsion abelian sheaves on Y_étale form a Serre subcategory ([Stacks, Tag 0DD7]), hence a weak Serre class; part (1) says that R^p f_* carries torsion abelian sheaves on X_étale into it; and CategoryTheory.Functor.derivedCategoryBPlus_rightDerivedFunctorPlus_obj propagates that from the second page E_2^{p,q} = R^p f_* H^q(K) of the spectral sequence of a Cartan--Eilenberg resolution to its abutment H^{p+q}(Rf_* K).

public theorem torsionCohomologyProperty_smallEtaleDerivedDirectImage
    [QuasiCompact f] [QuasiSeparated f]
    (K : DerivedCategory.Plus (Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}))
    (hK : torsionCohomologyProperty.{max (u + 1) v} X.smallEtaleTopology
      (DerivedCategory.Plus.ι.obj K)) :
    torsionCohomologyProperty.{max (u + 1) v} Y.smallEtaleTopology
      (DerivedCategory.Plus.ι.obj ((smallEtaleDerivedDirectImage.{v} f).obj K))
Sources
LeanStacks.EtaleCohomology.etaleCohomology_isAddTorsion_and_derivedEtaleCohomology_isAddTorsion · Stacks.EtaleCohomology.etaleCohomology_isAddTorsion · Stacks.EtaleCohomology.smallEtaleDerivedDirectImage · Stacks.EtaleCohomology.torsionSheafProperty_rightDerived_smallEtaleDirectImageAb · Stacks.EtaleCohomology.torsionCohomologyProperty_smallEtaleDerivedDirectImage

Section59.79 Cohomology with support in a closed subscheme#

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

Tag 09XQ, a lemma

Tag 09XQ in the Stacks Project.

AlgebraicGeometry.injective_supportedSections_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SupportedSectionsInjective.lean, line 313.

Stacks 09XQ. The sections with support in a closed subscheme of an injective abelian sheaf on the small étale site of the ambient scheme form an injective abelian sheaf on the small étale site of that subscheme.

public theorem injective_supportedSections_obj (I : SmallEtaleAbelianSheaf B X) [Injective I] :
    Injective ((supportedSections B i).obj I)
Tag 09XR, a lemma

Tag 09XR in the Stacks Project.

AlgebraicGeometry.isZero_rightDerivedPlus_supportedSections_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/CohomologyWithSupport.lean, line 230.

Stacks 09XR. The cohomology sheaves with support in a closed subscheme of the direct image of an injective abelian sheaf on that subscheme vanish in positive degrees.

public theorem isZero_rightDerivedPlus_supportedSections_pushforward
    (G : SmallEtaleAbelianSheaf B Z) [Injective G] (p : ℤ) (hp : 0 < p) :
    IsZero (((supportedSections B i).rightDerivedPlus p).obj
      (((smallEtaleBaseChange B i).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
        (SmallEtale.topology B X.obj X.property)
        (SmallEtale.topology B Z.obj Z.property)).obj G))
Tag 0A45, a lemma

Tag 0A45 in the Stacks Project.

AlgebraicGeometry.mono_supportedSectionsPushforwardInclusion_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/CohomologyWithSupportSequence.lean, line 211. The attribute's comment: “exactness of 0 ⟶ i_ℋ_Z(F) ⟶ F ⟶ j_(F|_U): the first map is a monomorphism”.

Stacks 0A45. The sections with support in the closed subscheme include into an abelian sheaf: the first map of the sequence 0 ⟶ i_*ℋ_Z(F) ⟶ F ⟶ j_*(F|_U) is a monomorphism.

public theorem mono_supportedSectionsPushforwardInclusion_app
    (F : SmallEtaleAbelianSheaf B X) :
    Mono ((supportedSectionsPushforwardInclusion B i).app F)

AlgebraicGeometry.supportedSectionsShortComplex_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/CohomologyWithSupportSequence.lean, line 223. The attribute's comment: “exactness of 0 ⟶ i_ℋ_Z(F) ⟶ F ⟶ j_(F|_U): exactness at F”.

Stacks 0A45. The sequence 0 ⟶ i_*ℋ_Z(F) ⟶ F ⟶ j_*(F|_U) is exact at F: a section restricting to zero on the open complement has support in the closed subscheme. Together with mono_supportedSectionsPushforwardInclusion_app this is the exactness of that sequence.

public theorem supportedSectionsShortComplex_exact (F : SmallEtaleAbelianSheaf B X) :
    (supportedSectionsShortComplex B i F).Exact

AlgebraicGeometry.cohomologyWithSupportSequences, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/CohomologyWithSupportTriangle.lean, line 369.

Stacks 0A45. Let i : Z ⟶ X be a closed immersion of schemes and let j : U ⟶ X be the inclusion of the complement of Z. For an abelian sheaf F on X_étale there is a distinguished triangle

i_*Rℋ_Z(F) ⟶ F ⟶ Rj_*(F|_U) ⟶ i_*Rℋ_Z(F)⟦1⟧

in D(X_étale), hence a four-term exact sequence

0 ⟶ i_*ℋ_Z(F) ⟶ F ⟶ j_*(F|_U) ⟶ i_*ℋ¹_Z(F) ⟶ 0

and isomorphisms R^p j_*(F|_U) ≅ i_*ℋ^{p+1}_Z(F) for p ≥ 1.

All three assertions are stated at once, as the three fields of AlgebraicGeometry.CohomologyWithSupportSequences. The triangle is given for an arbitrary triple of right derived functors of i_*ℋ_Z, of the identity and of j_*(-|_U) on the whole unbounded derived category, so it applies to every model of i_*Rℋ_Z and Rj_*(-|_U) and is functorial in the object; the other two assertions are given at every abelian sheaf, naturally in it. The open complement U and its inclusion j are constructed from i rather than assumed.

R^p is Mathlib's ℕ-indexed CategoryTheory.Functor.rightDerived; the comparison with the ℤ-indexed CategoryTheory.Functor.rightDerivedPlus of AlgebraicGeometry.isZero_rightDerivedPlus_supportedSections_pushforward ([Stacks, Tag 09XR]) is Stacks.DerivedIndexing.rightDerivedIso.

public def cohomologyWithSupportSequences : CohomologyWithSupportSequences B i
Tag 0AEG, a lemma

Tag 0AEG in the Stacks Project.

AlgebraicGeometry.closedImmersionSupportedDerivedEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ClosedImmersionSupportedDerivedEquivalence.lean, line 341.

Stacks 0AEG. Let i : Z ⟶ X be a closed immersion of schemes. Direct image of abelian sheaves along i is exact, so Ri_{small,*} = i_{small,*} : D(Z_étale) ⟶ D(X_étale), and it induces an equivalence of D(Z_étale) with the full subcategory D_Z(X_étale) of D(X_étale) of complexes whose cohomology sheaves are supported on Z. A quasi-inverse of that equivalence is given on D_Z(X_étale) by the exact inverse image i_{small}^{-1}, and also by the right derived functor Rℋ_Z of sections with support in Z.

public def closedImmersionSupportedDerivedEquivalence :
    ClosedImmersionSupportedDerivedEquivalence.{w₁, w₂} B i

AlgebraicGeometry.smallEtalePushforward_exact_ab, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SupportedDerivedEquivalence.lean, line 359. The attribute's comment: “Ri_ = i_ : direct image is exact, hence equal to its right derived functor”.

Stacks 0AEG. Direct image of abelian sheaves along a closed immersion is exact, so it coincides with its own right derived functor: Ri_{small,*} = i_{small,*}.

public theorem smallEtalePushforward_exact_ab :
    exactFunctor (SmallEtaleAbelianSheaf B Z) (SmallEtaleAbelianSheaf B X)
      ((smallEtaleBaseChange B i).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
        (SmallEtale.topology B X.1 X.property)
        (SmallEtale.topology B Z.1 Z.property))

AlgebraicGeometry.smallEtalePushforwardSupportedEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SupportedDerivedEquivalence.lean, line 464. The attribute's comment: “i_* induces an equivalence D(Z_étale) → D_Z(X_étale)”.

Stacks 0AEG. Direct image along a closed immersion induces an equivalence of D(Z_étale) with the full subcategory D_Z(X_étale) of D(X_étale) of complexes whose cohomology sheaves are supported on Z.

public def smallEtalePushforwardSupportedEquivalence :
    DerivedCategory (SmallEtaleAbelianSheaf B Z) ≌ SupportedDerivedCategory.{w₂} B i

AlgebraicGeometry.smallEtalePushforwardSupportedEquivalence_functor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SupportedDerivedEquivalence.lean, line 473. The attribute's comment: “the equivalence is induced by i_*”.

Stacks 0AEG. The equivalence is given by direct image: composed with the inclusion of D_Z(X_étale) into D(X_étale) it is the functor induced by i_*.

public def smallEtalePushforwardSupportedEquivalence_functor :
    (smallEtalePushforwardSupportedEquivalence.{w₁, w₂} B i).functor ⋙
        (supportedDerivedProperty.{w₂} B i).ι ≅
      ((smallEtaleBaseChange B i).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
        (SmallEtale.topology B X.obj X.property)
        (SmallEtale.topology B Z.obj Z.property)).mapDerivedCategory

AlgebraicGeometry.smallEtalePushforwardSupportedEquivalence_inverse, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SupportedDerivedEquivalence.lean, line 484. The attribute's comment: “the quasi-inverse is i^{-1} restricted to D_Z(X_étale)”.

Stacks 0AEG. The quasi-inverse of the equivalence is inverse image restricted to D_Z(X_étale): i^{-1}|_{D_Z(X_étale)}.

public def smallEtalePushforwardSupportedEquivalence_inverse :
    (smallEtalePushforwardSupportedEquivalence.{w₁, w₂} B i).inverse ≅
      (supportedDerivedProperty.{w₂} B i).ι ⋙
        ((smallEtaleBaseChange B i).sheafPullback AddCommGrpCat.{u + 1}
          (SmallEtale.topology B X.obj X.property)
          (SmallEtale.topology B Z.obj Z.property)).mapDerivedCategory
Tag 0A46, a lemma

Tag 0A46 in the Stacks Project.

AlgebraicGeometry.supportedCohomologyEtaleIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/CohomologyWithSupportEtaleZariski.lean, line 226. The attribute's comment: “clause (1): cohomology with support in a closed subset agrees between the small etale site and the Zariski site, for a quasi-coherent module, in every degree, with no hypothesis beyond the source's. Clause (2) is supportedCohomology_isQuasicoherent_and_associatedSheaf, on the size-bounded small etale site”.

Stacks 0A46, clause (1). For a quasi-coherent 𝒪_X-module F and a closed subset Z of a scheme X, cohomology with support in Z of the associated sheaf Fᵃ on the small étale site of X agrees, in every degree, with cohomology with support in Z of F on the small Zariski site.

Both sides are right derived functors of the functor of global sections vanishing on the open complement of Z, taken on the respective site. There is no hypothesis beyond those of the source: the vanishing of the higher direct images R^nε_*(Fᵃ) for n > 0 is AlgebraicGeometry.isZero_rightDerived_pushforward_opensToEtale and the identification of ε_*(Fᵃ) with F is AlgebraicGeometry.smallEtaleSectionsUnitIso, those two being the two halves of Stacks 03P2 for 𝒞 = X_étale.

public def supportedCohomologyEtaleIso (F : X.Modules) [F.IsQuasicoherent] (q : ℕ) :
    ((smallEtaleSectionsWithSupport X Z hZ).rightDerived q).obj
        (smallEtaleAssociatedSheaf X F) ≅
      ((SmallEtale.zariskiSectionsWithSupport X Z hZ).rightDerived q).obj
        ((SheafOfModules.toSheaf X.ringCatSheaf).obj F)

AlgebraicGeometry.supportedCohomology_isQuasicoherent_and_associatedSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/CohomologyWithSupportQuasicoherent.lean, line 181. The attribute's comment: “clause (2): for a closed immersion with retrocompact open complement and a quasi-coherent module F, i_H^q_Z(F) is quasi-coherent and i_H^q_Z(F^a) = (i_*H^q_Z(F))^a on the small etale site, for every q”.

Let i : Z ⟶ X be a closed immersion whose open complement is retrocompact in X, and let 𝓕 be a quasi-coherent 𝒪_X-module. Then for every q the Zariski sheaf i_*ℋ^q_Z(𝓕) is a quasi-coherent 𝒪_X-module, and the étale sheaf i_*ℋ^q_Z(𝓕ᵃ) is its associated sheaf (i_*ℋ^q_Z(𝓕))ᵃ.

The étale i_*ℋ^q_Z is the library's, on abelian sheaves of the small étale site with coefficients in the universe after that of the schemes, and 𝓕ᵃ is AlgebraicGeometry.SmallEtale.associatedModuleOfSheaf, read as an abelian sheaf and then by the universe lift, which is fully faithful and exact; see the implementation notes. The first half is [Stacks, Tag 0G7G] (1) in one degree, the second AlgebraicGeometry.supportedCohomologyAssociatedSheafIso.

public theorem supportedCohomology_isQuasicoherent_and_associatedSheaf
    (hU : IsRetrocompact (Set.range (B.inclusion.map i).base)ᶜ) (𝓕 : X.obj.Modules)
    [𝓕.IsQuasicoherent] (q : ℕ) :
    (((supportedSectionsFunctor X.obj.toRingedSpace
        (Set.range (B.inclusion.map i).base)).rightDerived q).obj 𝓕).IsQuasicoherent ∧
      Nonempty (((supportedSectionsPushforward B i).rightDerived q).obj
          ((Stacks.Sheaves.UniverseLift.uliftSheafFunctor.{u + 1, u}
            (SmallEtale.topology B X.obj X.property)).obj
            ((SheafOfModules.toSheaf.{u} (SmallEtale.structureSheaf B X.obj X.property)).obj
              ((SmallEtale.associatedModuleOfSheaf B X.obj X.property).obj 𝓕))) ≅
        (Stacks.Sheaves.UniverseLift.uliftSheafFunctor.{u + 1, u}
          (SmallEtale.topology B X.obj X.property)).obj
          ((SheafOfModules.toSheaf.{u} (SmallEtale.structureSheaf B X.obj X.property)).obj
            ((SmallEtale.associatedModuleOfSheaf B X.obj X.property).obj
              (((supportedSectionsFunctor X.obj.toRingedSpace
                (Set.range (B.inclusion.map i).base)).rightDerived q).obj 𝓕))))
Sources
LeanAlgebraicGeometry.injective_supportedSections_obj · AlgebraicGeometry.isZero_rightDerivedPlus_supportedSections_pushforward · AlgebraicGeometry.mono_supportedSectionsPushforwardInclusion_app · AlgebraicGeometry.supportedSectionsShortComplex_exact · AlgebraicGeometry.cohomologyWithSupportSequences · AlgebraicGeometry.closedImmersionSupportedDerivedEquivalence · AlgebraicGeometry.smallEtalePushforward_exact_ab · AlgebraicGeometry.smallEtalePushforwardSupportedEquivalence

Section59.80 Schemes with strictly henselian local rings#

Section 59.80 of the Stacks Project, Tag 0EZN. 9 tags here are carried by 11 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09AX, a lemma

Tag 09AX in the Stacks Project.

AlgebraicGeometry.etaleZariskiSheafHAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/EtaleZariskiCohomology.lean, line 194.

Let S be a scheme all of whose local rings are strictly henselian. Then for every abelian sheaf F on the small étale site of S and every degree p, étale cohomology H^p(S_étale, F) agrees with Zariski cohomology H^p(S_Zariski, ε_* F) of its restriction to the open subschemes of S.

public def etaleZariskiSheafHAddEquiv
    (hlocal : ∀ x : S, StrictlyHenselianLocalRing ↥(S.presheaf.stalk x))
    (F : Sheaf (Scheme.smallEtaleTopology S) AddCommGrpCat.{u + 1}) (p : ℕ) :
    Sheaf.H.{w, u + 1} F p ≃+ Sheaf.H.{w, u + 1} ((zariskiPushforward S).obj F) p
Tag 0GY0, a lemma

Tag 0GY0 in the Stacks Project.

Stacks.EtaleCohomology.StrictlyHenselian.subsingleton_H_of_degreeOne_kernel_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/StrictlyHenselianSpectrumVanishing.lean, line 419.

Let R be a ring all of whose local rings are strictly henselian and let F be an abelian sheaf on the small étale site of Spec R. If for all f, g ∈ R the kernel of

H¹(D(f + g), F) ⟶ H¹(D(f(f + g)), F) ⊕ H¹(D(g(f + g)), F)

is zero, then H^q(Spec R, F) = 0 for every q > 0.

public theorem subsingleton_H_of_degreeOne_kernel_eq_zero
    (hlocal : ∀ x : Spec (CommRingCat.of R), StrictlyHenselianLocalRing
      ↥((Spec (CommRingCat.of R)).presheaf.stalk x))
    (F : Sheaf (MayerVietoris.topology (Spec (CommRingCat.of R))) AddCommGrpCat.{u + 1})
    (h₁ : ∀ f g : R, ∀ y : (opensCohomology F 1).obj (op (PrimeSpectrum.basicOpen (f + g))),
      (opensCohomology F 1).map
          (homOfLE (PrimeSpectrum.basicOpen_mul_le_right f (f + g))).op y = 0 →
      (opensCohomology F 1).map
          (homOfLE (PrimeSpectrum.basicOpen_mul_le_right g (f + g))).op y = 0 → y = 0)
    (q : ℕ) (hq : 0 < q) :
    Subsingleton (Sheaf.H.{u + 1} F q)
Tag 09AY, a lemma

Tag 09AY in the Stacks Project.

AlgebraicGeometry.subsingleton_etaleCohomology_of_closed_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ClosedPointsVanishing.lean, line 200.

Positive-degree étale cohomology vanishes on an affine scheme all of whose points are closed and all of whose residue fields are separably closed.

public theorem subsingleton_etaleCohomology_of_closed_points
    (hclosed : ∀ x : S, IsClosed ({x} : Set S))
    (hsep : ∀ x : S, IsSepClosed ↥(S.residueField x))
    [HasSheafify (Scheme.smallEtaleTopology S) AddCommGrpCat.{max u v}]
    [(Scheme.smallEtaleTopology S).WEqualsLocallyBijective AddCommGrpCat.{max u v}]
    [HasExt.{w} (Sheaf (Scheme.smallEtaleTopology S) AddCommGrpCat.{max u v})]
    (F : Sheaf (Scheme.smallEtaleTopology S) AddCommGrpCat.{max u v}) (q : ℕ) (hq : 0 < q) :
    Subsingleton (Sheaf.H.{w, max u v} F q)

AlgebraicGeometry.subsingleton_etaleCohomology_of_closed_points', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ClosedPointsVanishing.lean, line 216. The attribute's comment: “at the coefficient universe of the small étale site”.

Positive-degree étale cohomology vanishes on an affine scheme all of whose points are closed and all of whose residue fields are separably closed, for abelian sheaves at the coefficient universe u + 1 of the small étale site itself.

public theorem subsingleton_etaleCohomology_of_closed_points'
    (hclosed : ∀ x : S, IsClosed ({x} : Set S))
    (hsep : ∀ x : S, IsSepClosed ↥(S.residueField x))
    [HasExt.{w} (Sheaf (Scheme.smallEtaleTopology S) AddCommGrpCat.{u + 1})]
    (F : Sheaf (Scheme.smallEtaleTopology S) AddCommGrpCat.{u + 1}) (q : ℕ) (hq : 0 < q) :
    Subsingleton (Sheaf.H.{w, u + 1} F q)
Tag 09Z9, a lemma

Tag 09Z9 in the Stacks Project.

AlgebraicGeometry.exists_coproduct_open_immersions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/NormalSepClosedFunctionField.lean, line 216. The attribute's comment: “part (1)”.

A separated étale morphism to an integral normal scheme with separably closed function field is a disjoint union of open immersions.

theorem exists_coproduct_open_immersions
    (X : Scheme.{u}) [IsIntegral X] [IsNormal X]
    [IsSepClosed X.functionField]
    (U : Scheme.{u}) (f : U ⟶ X) [Etale f] [IsSeparated f] :
    ∃ (I : Type u) (V : I → Scheme.{u}) (j : ∀ i, V i ⟶ X)
      (_ : ∀ i, IsOpenImmersion (j i)) (e : U ≅ ∐ V),
      e.hom ≫ Sigma.desc j = f

AlgebraicGeometry.stalk_strictlyHenselian, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/NormalSepClosedFunctionField.lean, line 260. The attribute's comment: “part (2)”.

Every local ring of an integral normal scheme with separably closed function field is strictly henselian.

instance stalk_strictlyHenselian
    (X : Scheme.{u}) [IsIntegral X] [IsNormal X]
    [IsSepClosed X.functionField] (x : X) :
    _root_.StrictlyHenselianLocalRing (X.presheaf.stalk x)
Tag 0EZP, a lemma

Tag 0EZP in the Stacks Project.

Stacks.EtaleCohomology.isZero_rightDerived_smallEtalePushforward_constantSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/NormalSepClosedConstantDirectImage.lean, line 804.

Stacks Project, Tag 0EZP. Higher direct images of a constant abelian étale sheaf vanish when the source is integral, normal, and has separably closed function field.

public theorem isZero_rightDerived_smallEtalePushforward_constantSheaf
    {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsIntegral X] [IsNormal X] [IsSepClosed X.functionField]
    [HasSheafify X.smallEtaleTopology AddCommGrpCat.{w}]
    [HasSheafify Y.smallEtaleTopology AddCommGrpCat.{w}]
    [HasInjectiveResolutions (Sheaf X.smallEtaleTopology AddCommGrpCat.{w})]
    (M : AddCommGrpCat.{w}) (q : ℕ) (hq : 0 < q) :
    IsZero ((((smallEtaleBaseChange f).sheafPushforwardContinuous
      AddCommGrpCat.{w} Y.smallEtaleTopology X.smallEtaleTopology).rightDerived q).obj
        ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{w}).obj M))
Tag 09ZA, a lemma

Tag 09ZA in the Stacks Project.

AlgebraicGeometry.exists_finite_coproduct_open_immersions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ClosedSubschemeOfNormal.lean, line 284. The attribute's comment: “finite disjoint union”.

Stacks Project, Tag 09ZA, first assertion. An affine etale scheme over a closed subscheme of an integral normal affine scheme with separably closed function field is a finite disjoint union of open subschemes of the closed subscheme.

theorem exists_finite_coproduct_open_immersions
    (X : Scheme.{u}) [IsAffine X] [IsIntegral X] [IsNormal X]
    [IsSepClosed X.functionField]
    (Z : Scheme.{u}) (i : Z ⟶ X) [IsClosedImmersion i]
    (V : Scheme.{u}) [IsAffine V] (f : V ⟶ Z) [Etale f] :
    ∃ (n : ℕ) (U : Fin n → Scheme.{u}) (j : ∀ a, U a ⟶ Z)
      (_ : ∀ a, IsOpenImmersion (j a)) (e : V ≅ ∐ U),
      e.hom ≫ Sigma.desc j = f

AlgebraicGeometry.exists_section_of_surjective_finite_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ClosedSubschemeOfNormal.lean, line 457. The attribute's comment: “section”.

Stacks Project, Tag 09ZA, final assertion. A surjective finite etale morphism over a closed subscheme of an integral normal affine scheme with separably closed function field has a section.

theorem exists_section_of_surjective_finite_etale
    (X : Scheme.{u}) [IsAffine X] [IsIntegral X] [IsNormal X]
    [IsSepClosed X.functionField]
    (Z : Scheme.{u}) (i : Z ⟶ X) [IsClosedImmersion i]
    (V : Scheme.{u}) [IsAffine V] (f : V ⟶ Z)
    [Surjective f] [IsFinite f] [Etale f] :
    ∃ s : Z ⟶ V, s ≫ f = 𝟙 Z
Tag 09ZB, a lemma

Tag 09ZB in the Stacks Project.

AlgebraicGeometry.subsingleton_smallEtaleH1_constantSheaf', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ClosedSubschemeOfNormal.lean, line 899.

Stacks Project, Tag 09ZB. The first cohomology of the small étale site of a closed subscheme of an integral normal affine scheme with separably closed function field, with coefficients in a finite constant abelian group, vanishes.

This is AlgebraicGeometry.subsingleton_smallEtaleH1_constantSheaf with its descent hypothesis discharged: a torsor under the constant sheaf is finite locally constant, hence representable by a scheme finite étale over Z by the unconditional Stacks.EtaleCohomology.isFiniteLocallyConstant_iff_finiteEtaleRepresentable, and that scheme has a section because Z is a closed subscheme of a normal integral affine scheme with separably closed function field.

theorem subsingleton_smallEtaleH1_constantSheaf'
    (B : BigEtaleSite.{u})
    (X : Scheme.{u}) [IsAffine X] [IsIntegral X] [IsNormal X]
    [IsSepClosed X.functionField]
    (Z : Scheme.{u}) (i : Z ⟶ X) [IsClosedImmersion i] (hZ : B.Contains Z)
    (M : AddCommGrpCat.{u + 1}) [Finite M]
    [HasSheafify (SmallEtale.topology B Z hZ) AddCommGrpCat.{u + 1}]
    [HasExt.{w} (Sheaf (SmallEtale.topology B Z hZ) AddCommGrpCat.{u + 1})] :
    Subsingleton (Sheaf.H ((constantSheaf (SmallEtale.topology B Z hZ)
      AddCommGrpCat.{u + 1}).obj M) 1)
Tag 09ZC, a lemma

Tag 09ZC in the Stacks Project.

AlgebraicGeometry.subsingleton_smallEtaleH_constantSheaf', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/ClosedSubschemeOfNormal.lean, line 1086.

Stacks Project, Tag 09ZC. The étale cohomology of a closed subscheme of a normal integral affine scheme with separably closed function field, with coefficients in a finite constant abelian group, vanishes in every positive degree.

This is AlgebraicGeometry.subsingleton_smallEtaleH_constantSheaf with its descent hypothesis discharged: the degree-one input is the unconditional AlgebraicGeometry.subsingleton_smallEtaleH1_constantSheaf' on the basic opens of Z, and the passage to all positive degrees is the vanishing criterion of Stacks 0GY0.

theorem subsingleton_smallEtaleH_constantSheaf'
    (B : BigEtaleSite.{u})
    (X : Scheme.{u}) [IsAffine X] [IsIntegral X] [IsNormal X]
    [IsSepClosed X.functionField]
    (Z : Scheme.{u}) (i : Z ⟶ X) [IsClosedImmersion i] (hZ : B.Contains Z)
    (M : AddCommGrpCat.{u + 1}) [Finite M]
    [HasSheafify (SmallEtale.topology B Z hZ) AddCommGrpCat.{u + 1}]
    [HasExt.{w} (Sheaf (SmallEtale.topology B Z hZ) AddCommGrpCat.{u + 1})]
    (q : ℕ) (hq : 0 < q) :
    Subsingleton (Sheaf.H ((constantSheaf (SmallEtale.topology B Z hZ)
      AddCommGrpCat.{u + 1}).obj M) q)
Tag 09ZD, a lemma

Tag 09ZD in the Stacks Project.

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.etaleZariskiSheafHAddEquiv · Stacks.EtaleCohomology.StrictlyHenselian.subsingleton_H_of_degreeOne_kernel_eq_zero · AlgebraicGeometry.subsingleton_etaleCohomology_of_closed_points · AlgebraicGeometry.subsingleton_etaleCohomology_of_closed_points' · AlgebraicGeometry.exists_coproduct_open_immersions · AlgebraicGeometry.stalk_strictlyHenselian · Stacks.EtaleCohomology.isZero_rightDerived_smallEtalePushforward_constantSheaf · AlgebraicGeometry.exists_finite_coproduct_open_immersions

Section59.81 Absolutely integrally closed vanishing#

Section 59.81 of the Stacks Project, Tag 0GY1. 6 tags here are carried by 13 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0GY2, a lemma

Tag 0GY2 in the Stacks Project.

exists_monic_adjoinRoot_isUnit_sub_mul_root, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AbsolutelyIntegrallyClosed/MonogenicExtension.lean, line 78.

A monogenic extension in which a - b y is a unit, when a and b are coprime and a is a root of unity modulo b.

public theorem exists_monic_adjoinRoot_isUnit_sub_mul_root
    {A : Type*} [CommRing A] (a b : A)
    (hab : IsCoprime a b)
    (ha : IsOfFinOrder (Ideal.Quotient.mk (Ideal.span {b}) a)) :
    ∃ P : A[X], P.Monic ∧ Function.Injective (algebraMap A (AdjoinRoot P)) ∧
      IsUnit (algebraMap A (AdjoinRoot P) a -
        algebraMap A (AdjoinRoot P) b * AdjoinRoot.root P)
Tag 0GY3, a lemma

Tag 0GY3 in the Stacks Project.

localizationMap_X, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AbsolutelyIntegrallyClosed/MonogenicPresentation.lean, line 73. The attribute's comment: “the canonical substitution map on the generator”.

The canonical map sends t to Φ(s).

theorem localizationMap_X
    (A : Type*) [CommRing A] (π : A) (ℓ : ℕ) (Φ : A[X])
    (hΦ : (C π * X + 1) ^ ℓ = C (π ^ ℓ) * Φ + 1) :
    localizationMap A π ℓ Φ hΦ
      (algebraMap A[X] (Localization.Away (C (π ^ ℓ) * X + 1)) X) =
      aeval (algebraMap A[X] (Localization.Away (C π * X + 1)) X) Φ

localization_isAdjoinRootMonic_of_power_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AbsolutelyIntegrallyClosed/MonogenicPresentation.lean, line 91. The attribute's comment: “the monic presentation”.

For Φ monic of positive degree, the target localization is obtained from the source localization by adjoining the target variable as a root of the monic equation Φ(s) - t.

theorem localization_isAdjoinRootMonic_of_power_eq
    (A : Type*) [CommRing A] (π : A) (ℓ : ℕ) (Φ : A[X])
    (hΦ : (C π * X + 1) ^ ℓ = C (π ^ ℓ) * Φ + 1)
    (hMonic : Φ.Monic) (hDegree : 0 < Φ.natDegree) :
    ∃ h : @IsAdjoinRootMonic (Localization.Away (C (π ^ ℓ) * X + 1))
        (Localization.Away (C π * X + 1)) _ _
        (localizationMap A π ℓ Φ hΦ).toRingHom.toAlgebra
        (Φ.map (algebraMap A (Localization.Away (C (π ^ ℓ) * X + 1))) -
          C (algebraMap A[X] (Localization.Away (C (π ^ ℓ) * X + 1)) X)),
      @IsAdjoinRoot.map (Localization.Away (C (π ^ ℓ) * X + 1))
        (Localization.Away (C π * X + 1)) _ _
        (localizationMap A π ℓ Φ hΦ).toRingHom.toAlgebra _
        (@IsAdjoinRootMonic.toIsAdjoinRoot
          (Localization.Away (C (π ^ ℓ) * X + 1))
          (Localization.Away (C π * X + 1)) _ _
          (localizationMap A π ℓ Φ hΦ).toRingHom.toAlgebra _ h) X =
        algebraMap A[X] (Localization.Away (C π * X + 1)) X
Tag 0GY4, an equation

Tag 0GY4 in the Stacks Project.

AlgebraicGeometry.MultiplicativeDeformation.isogenyOnPoints_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/MultiplicativeDeformation/Exactness.lean, line 485.

The map f is a morphism of group schemes: it is additive on points.

theorem isogenyOnPoints_add {R : Type v} [CommRing R] [Algebra A R]
    (x y : DeformedPoint (ζ - 1) R) :
    isogenyOnPoints ℓ ζ hsplit (x + y)
      = isogenyOnPoints ℓ ζ hsplit x + isogenyOnPoints ℓ ζ hsplit y

AlgebraicGeometry.MultiplicativeDeformation.constantPoint_add, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/MultiplicativeDeformation/Exactness.lean, line 524.

The points σ_i form a homomorphism from ℤ/ℓℤ to the A-points of G^{(ζ - 1)}, as in σ_i +_G σ_j = σ_{i + j}.

theorem constantPoint_add
    (hsplit : ∏ k : ZMod ℓ, (X - C (ζ ^ k.val)) = X ^ ℓ - 1)
    (i j : ZMod ℓ) :
    constantPoint ℓ ζ hζ (i + j) = constantPoint ℓ ζ hζ i + constantPoint ℓ ζ hζ j

AlgebraicGeometry.MultiplicativeDeformation.isogenyOnPoints_constantPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/MultiplicativeDeformation/Exactness.lean, line 543.

The composition of ℤ/ℓℤ → G^{(ζ - 1)} with f is trivial: the points σ_i lie in the kernel of f.

theorem isogenyOnPoints_constantPoint (i : ZMod ℓ) :
    isogenyOnPoints ℓ ζ hsplit (constantPoint ℓ ζ hζ i) = 0

AlgebraicGeometry.MultiplicativeDeformation.kernelCoordinateRing_algEquiv_pi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/MultiplicativeDeformation/Exactness.lean, line 660.

Exactness at G^{(ζ - 1)}: for ℓ prime, the closed immersion of the constant group scheme of ℤ/ℓℤ into the kernel of f which sends i to σ_i is an isomorphism. Dually, the A-algebra map from the coordinate ring of the kernel to the functions on ℤ/ℓℤ sending s to i ↦ σ_i is an isomorphism.

theorem kernelCoordinateRing_algEquiv_pi (hℓ : ℓ.Prime) :
    ∃ e : kernelCoordinateRing ℓ ζ hsplit ≃ₐ[A] (ZMod ℓ → A),
      ∀ i : ZMod ℓ,
        e (Ideal.Quotient.mk _ (coordinateGenerator (ζ - 1))) i = sigmaPoint ℓ ζ i

AlgebraicGeometry.MultiplicativeDeformation.isogeny_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/MultiplicativeDeformation/Exactness.lean, line 673.

Exactness at G^{((ζ - 1) ^ ℓ)}: the morphism f is faithfully flat.

theorem isogeny_faithfullyFlat : (isogeny ℓ ζ hsplit).toRingHom.FaithfullyFlat

AlgebraicGeometry.MultiplicativeDeformation.exists_shortExactSequence_of_groupSchemes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GroupScheme/Examples/MultiplicativeDeformation/GroupSchemes.lean, line 744.

The short exact sequence 0 → ℤ/ℓℤ → G^{(ζ - 1)} → G^{((ζ - 1) ^ ℓ)} → 0 is a sequence of group schemes over Spec A, not merely a sequence of groups of A-points. The left-hand group scheme is the constant group scheme of ℤ/ℓℤ; the right-hand map is the scheme morphism dual to the explicitly specified algebra homomorphism isogeny. The coordinate of the left-hand map is pinned to the points σ_i, and the pullback square says that it identifies the constant group scheme with the kernel.

theorem exists_shortExactSequence_of_groupSchemes (hℓ : ℓ.Prime) :
    ∃ (g : Grp (Over (Spec (.of A)))) (h : Grp (Over (Spec (.of A))))
      (i : constantGroupScheme (Multiplicative (ZMod ℓ)) (Spec (.of A)) ⟶ g) (f : g ⟶ h),
      ∃ (eg : g.X ≅ (Spec (.of (coordinateRing (ζ - 1)))).asOver (Spec (.of A)))
        (eh : h.X ≅ (Spec (.of (coordinateRing ((ζ - 1) ^ ℓ)))).asOver (Spec (.of A))),
        (((eg.inv ⊗ₘ eg.inv) ≫ MonObj.mul (X := g.X) ≫ eg.hom).left =
          (pullbackSpecIso A (coordinateRing (ζ - 1)) (coordinateRing (ζ - 1))).hom ≫
            Spec.map (CommRingCat.ofHom (comultiplication (ζ - 1)).toRingHom)) ∧
        (((eh.inv ⊗ₘ eh.inv) ≫ MonObj.mul (X := h.X) ≫ eh.hom).left =
          (pullbackSpecIso A (coordinateRing ((ζ - 1) ^ ℓ))
            (coordinateRing ((ζ - 1) ^ ℓ))).hom ≫
            Spec.map (CommRingCat.ofHom (comultiplication ((ζ - 1) ^ ℓ)).toRingHom)) ∧
        (CategoryTheory.IsPullback i.hom.hom (toUnit _)
          f.hom.hom (MonObj.one : (𝟙_ (Over (Spec (.of A)))) ⟶ h.X)) ∧
        (Flat f.hom.hom.left ∧ Surjective f.hom.hom.left) ∧
        (eg.inv ≫ f.hom.hom ≫ eh.hom).left =
          Spec.map (CommRingCat.ofHom (isogeny ℓ ζ hsplit).toRingHom) ∧
        (∀ j : ZMod ℓ,
          (Spec.preimage
            (constantComponentOver (A := A) ℓ (Multiplicative.ofAdd j) ≫
              i.hom.hom ≫ eg.hom).left).hom
            (coordinateGenerator (ζ - 1)) = sigmaPoint ℓ ζ j)
Tag 0GY5, a lemma

Tag 0GY5 in the Stacks Project.

surjective_precomp_localizationMap_of_isAbsolutelyIntegrallyClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AbsolutelyIntegrallyClosed/LiftingPoints.lean, line 41.

Every point of the target of the monogenic map lifts over an absolutely integrally closed A-algebra.

public theorem surjective_precomp_localizationMap_of_isAbsolutelyIntegrallyClosed
    (A : Type*) [CommRing A] (π : A) (ℓ : ℕ) (Φ : A[X])
    (hΦ : (C π * X + 1) ^ ℓ = C (π ^ ℓ) * Φ + 1)
    (hMonic : Φ.Monic)
    (hDegree : 0 < Φ.natDegree)
    (R : Type*) [CommRing R] [Algebra A R]
    (hR : IsAbsolutelyIntegrallyClosed R) :
    Function.Surjective (fun g : Localization.Away (C π * X + 1) →ₐ[A] R =>
      g.comp (localizationMap A π ℓ Φ hΦ))
Tag 0GY6, a lemma

Tag 0GY6 in the Stacks Project.

exists_isUnit_one_add_mul_of_comaximal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AbsolutelyIntegrallyClosed/Interpolation.lean, line 51.

Let R be absolutely integrally closed and π ∈ R with 1 + π of finite order. For comaximal ideals I and J of R there is s ∈ I with s - 1 ∈ J and 1 + π s a unit.

public theorem exists_isUnit_one_add_mul_of_comaximal
    {R : Type*} [CommRing R]
    (hR : IsAbsolutelyIntegrallyClosed R) (π : R) (hπ : IsOfFinOrder (1 + π))
    (I J : Ideal R) (hIJ : I + J = ⊤) :
    ∃ s : R, IsUnit (1 + π * s) ∧ s ∈ I ∧ s - 1 ∈ J
Tag 0GY7, a proposition

Tag 0GY7 in the Stacks Project.

Stacks.EtaleCohomology.AbsolutelyIntegrallyClosed.subsingleton_H_constantSheaf_smallEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AbsolutelyIntegrallyClosed/Vanishing.lean, line 182.

Stacks 0GY7. Let R be an absolutely integrally closed ring and let M be a finite abelian group. Then H^i_étale(Spec R, M) = 0 for i > 0.

This is subsingleton_H_constantSheaf_of_finite read on Mathlib's small étale site of Spec R, to which the one-universe model used there is a dense subsite.

theorem subsingleton_H_constantSheaf_smallEtale (hR : IsAbsolutelyIntegrallyClosed R)
    (M : AddCommGrpCat.{u + 1}) [Finite M] (q : ℕ) (hq : 0 < q) :
    Subsingleton (Sheaf.H.{u + 1}
      ((constantSheaf (Spec (CommRingCat.of R)).smallEtaleTopology
        AddCommGrpCat.{u + 1}).obj M) q)

Stacks.EtaleCohomology.AbsolutelyIntegrallyClosed.subsingleton_H_constantSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AbsolutelyIntegrallyClosedVanishing.lean, line 225. The attribute's comment: “assuming degree-zero sections over an overlap are differences (hypothesis hsub)”.

Stacks 0GY7, with the degree-zero gluing hypothesis hsub carried. Let R be an absolutely integrally closed ring and let M be a finite abelian group. Then the étale cohomology of Spec R with coefficients in the constant sheaf M vanishes in every positive degree, provided every section of that constant sheaf over D(f(f + g)) ∩ D(g(f + g)) is a difference of sections over D(f(f + g)) and over D(g(f + g)).

This is weaker than Stacks 0GY7, which carries no such hypothesis. In the source, the gluing statement is where finiteness of M is used, through the group-scheme argument of Stacks 0GY4, 0GY5 and 0GY6; here it is a hypothesis, and [Finite M] is therefore not used by the proof.

theorem subsingleton_H_constantSheaf (hR : IsAbsolutelyIntegrallyClosed R)
    (M : AddCommGrpCat.{u + 1}) [Finite M]
    (hsub : ∀ f g : R,
      SectionsSub ((constantSheaf (MayerVietoris.topology (Spec (CommRingCat.of R)))
          AddCommGrpCat.{u + 1}).obj M)
        (PrimeSpectrum.basicOpen (f * (f + g))) (PrimeSpectrum.basicOpen (g * (f + g))))
    (q : ℕ) (hq : 0 < q) :
    Subsingleton (Sheaf.H.{u + 1}
      ((constantSheaf (MayerVietoris.topology (Spec (CommRingCat.of R)))
        AddCommGrpCat.{u + 1}).obj M) q)
Sources
Leanexists_monic_adjoinRoot_isUnit_sub_mul_root · localizationMap_X · localization_isAdjoinRootMonic_of_power_eq · AlgebraicGeometry.MultiplicativeDeformation.isogenyOnPoints_add · AlgebraicGeometry.MultiplicativeDeformation.constantPoint_add · AlgebraicGeometry.MultiplicativeDeformation.isogenyOnPoints_constantPoint · AlgebraicGeometry.MultiplicativeDeformation.kernelCoordinateRing_algEquiv_pi · AlgebraicGeometry.MultiplicativeDeformation.isogeny_faithfullyFlat

Section59.82 Affine analog of proper base change#

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

Tag 09ZE, a lemma

Tag 09ZE in the Stacks Project.

Stacks.EtaleCohomology.exists_mono_comp_etaleAbelianInverseImage_eq_zero_of_torsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AffineAnalogProper/TorsionEffacement.lean, line 241.

Stacks 09ZE. Let X be an affine scheme, F a torsion abelian sheaf on X_étale, Z ⊂ X a closed subscheme (i : Z ⟶ X a closed immersion) and ξ ∈ H^q_ét(Z, F|_Z) for some q > 0. Then there exists an injective map F ⟶ F' of torsion abelian sheaves on X_étale such that the image of ξ in H^q_ét(Z, F'|_Z) is zero.

Restriction to Z is the inverse image etaleAbelianInverseImage i, and the image of ξ is its composite with the degree-zero class of i⁻¹(F ⟶ F'). Torsion is the local condition of Stacks 0DD7, Stacks.Torsion.torsionSheafProperty.

theorem exists_mono_comp_etaleAbelianInverseImage_eq_zero_of_torsion
    {X Z : Scheme.{u}} [IsAffine X] (i : Z ⟶ X) [IsClosedImmersion i]
    (F : Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1})
    (hF : Stacks.Torsion.torsionSheafProperty X.smallEtaleTopology F) (q : ℕ) (hq : 0 < q)
    (ξ : Sheaf.H.{u + 1} ((etaleAbelianInverseImage.{u, 0} i).obj F) q) :
    ∃ (F' : Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1}) (φ : F ⟶ F'), Mono φ ∧
      Stacks.Torsion.torsionSheafProperty X.smallEtaleTopology F' ∧
        ξ.comp (Ext.mk₀ ((etaleAbelianInverseImage.{u, 0} i).map φ)) (add_zero q) = 0
Tag 09ZF, a lemma

Tag 09ZF in the Stacks Project.

Stacks.EtaleCohomology.isIso_globalSectionsSmallEtaleInverseImageComparison_of_zariskiBijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GlobalSectionsClosed/FiniteSurjectiveDescent.lean, line 3312. The attribute's comment: “the conclusion Γ(X, ℱ) = Γ(Z, i⁻¹_{small}ℱ) for every sheaf of sets on the small étale site of X, under the source's own hypotheses: X quasi-compact and quasi-separated, i a closed immersion, and the two Zariski hypotheses (1) and (2) of the tag”.

[Stacks, Tag 09ZF] (Gabber). Let X be a quasi-compact quasi-separated scheme and i : Z ⟶ X a closed immersion such that

  1. for every sheaf of sets ℱ on the Zariski site of X the restriction Γ(X, ℱ) ⟶ Γ(Z, i⁻¹ℱ) is bijective, and
  2. the same holds for the base change Z ×_X X' ⟶ X' along every finite morphism X' ⟶ X.

Then Γ(X, ℱ) = Γ(Z, i⁻¹_{small}ℱ) for every sheaf of sets ℱ on the small étale site of X: the canonical comparison Stacks.EtaleCohomology.globalSectionsSmallEtaleInverseImageComparison is an isomorphism.

Injectivity uses only hypothesis (1): a global section of i⁻¹ℱ is, near each point of Z, pulled back from a section of ℱ over an object of the small étale site of X whose open image is forced by (1) to be all of X. Surjectivity is where (2) enters. A global section t of i⁻¹ℱ is, on a covering family, pulled back from sections of ℱ over objects W j of the small étale site whose images cover X; each W j is shrunk so that V j ⟶ W j ×_X Z is surjective; [Stacks, Tag 09Z0] produces a finite surjective X' ⟶ X factoring Zariski-locally through the family, so that over X' the pulled-back section lies in the Zariski subsheaf and (2) produces a section over X'; and that section descends to X by the equalizer presentation of [Stacks, Tag 09Z3], Stacks.EtaleCohomology.globalSectionsPullback_isEqualizer_of_isFinite_surjective.

Hypotheses (1) and (2) are asked only of those Zariski sheaves of sets whose values lie in the universe of the schemes themselves — Stacks.EtaleCohomology.zariskiGlobalSectionsMapAt at Type u — while the conclusion stays universe-polymorphic in the coefficients of the étale sheaf. That is all the proof uses: (1) is applied to the sheafification of a representable, and both (1) and (2) to the small model Stacks.EtaleCohomology.smallSheafModel of the subsheaf generated by a u-small family of local sections. Both have u-small values, so the hypotheses are weaker than the source's, which quantifies over every sheaf of sets.

public theorem isIso_globalSectionsSmallEtaleInverseImageComparison_of_zariskiBijective
    {X Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
    [CompactSpace X] [QuasiSeparatedSpace X]
    (hZar : ∀ F : Sheaf (Opens.grothendieckTopology X.carrier)
      (Type u),
      Function.Bijective (zariskiGlobalSectionsMapAt i F))
    (hFinite : ∀ {Y : Scheme.{u}} (f : Y ⟶ X) [IsFinite f],
      ∀ F : Sheaf (Opens.grothendieckTopology Y.carrier)
        (Type u),
        Function.Bijective
          (zariskiGlobalSectionsMapAt (pullback.fst f i) F)) :
    IsIso (globalSectionsSmallEtaleInverseImageComparison.{u, v} i).val
Tag 0CAM, a lemma

Tag 0CAM in the Stacks Project.

exists_isClosed_partition, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AffineAnalogProper/SpectralPartition.lean, line 133.

A partition of a closed subset Z into two relatively closed pieces extends to a partition of the ambient spectral space into two closed pieces, provided Z meets the closure of each point in a connected set.

public lemma exists_isClosed_partition
    {X : Type*} [TopologicalSpace X] [SpectralSpace X]
    {Z Z₁ Z₂ : Set X} (hZ : IsClosed Z)
    (hconnected : ∀ x : X, IsConnected (Z ∩ closure ({x} : Set X)))
    (hZ₁ : IsClosed ((Subtype.val : Z → X) ⁻¹' Z₁))
    (hZ₂ : IsClosed ((Subtype.val : Z → X) ⁻¹' Z₂))
    (hunion : Z₁ ∪ Z₂ = Z) (hdisjoint : Disjoint Z₁ Z₂) :
    ∃ X₁ X₂ : Set X,
      IsClosed X₁ ∧ IsClosed X₂ ∧ X₁ ∪ X₂ = univ ∧ Disjoint X₁ X₂ ∧
        Z₁ = Z ∩ X₁ ∧ Z₂ = Z ∩ X₂
Tag 09ZG, a lemma

Tag 09ZG in the Stacks Project.

Stacks.bijective_globalSectionsRestriction_of_isConnected_inter_closure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Spectral/ClosedSubsetGlobalSections.lean, line 1359.

Stacks Project, Tag 09ZG. Let Z be a closed subset of a spectral space X meeting the closure of every point of X in a connected set. Then restriction to Z is a bijection on global sections of every sheaf of sets on X.

theorem bijective_globalSectionsRestriction_of_isConnected_inter_closure
    {X : Type u} [TopologicalSpace X] [SpectralSpace X]
    (Z : Set X) (hZ : IsClosed Z)
    (hconn : ∀ x : X, IsConnected (Z ∩ closure ({x} : Set X)))
    (F : TopCat.Sheaf (Type u) (TopCat.of X)) :
    Function.Bijective (globalSectionsRestriction Z F)
Tag 09ZH, a lemma

Tag 09ZH in the Stacks Project.

Stacks.EtaleCohomology.isIso_globalSectionsComparison_quotient_of_henselianPair, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AffineAnalogProper/HenselianPairEtaleSections.lean, line 66. The attribute's comment: “Γ(X, ℱ) = Γ(Z, ℱ|_Z) for every sheaf of sets ℱ on the small étale site of X = Spec A, where (A, I) is a henselian pair and Z = Spec (A/I): the canonical comparison of global sections along Z ⟶ X is an isomorphism. The ring A is not assumed local”. References: SGA 4 XII (6.13), “special case”.

[Stacks, Tag 09ZH]. Let (A, I) be a henselian pair, let X = Spec A and let Z = Spec (A ⧸ I). Then Γ(X, ℱ) = Γ(Z, ℱ|_Z) for every sheaf of sets ℱ on the small étale site of X: the canonical comparison of global sections along Z ⟶ X is an isomorphism.

There is no hypothesis that A be local. The two Zariski inputs are hypotheses (1) and (2) of [Stacks, Tag 09ZF] for Z ⟶ X, and they hold at an arbitrary henselian pair: Stacks.EtaleCohomology.bijective_zariskiGlobalSectionsMapAt_quotient_of_henselianPair is (1), proved from [Stacks, Tag 09ZG] because Spec A is a spectral space in which V(I) meets the closure of every point in a connected set, and Stacks.EtaleCohomology.bijective_zariskiGlobalSectionsMapAt_pullback_of_henselianPair is (2), because a scheme finite over Spec A is the spectrum of an integral A-algebra B and (B, IB) is again a henselian pair.

public theorem isIso_globalSectionsComparison_quotient_of_henselianPair
    (h : HenselianPair A I) :
    IsIso (globalSectionsSmallEtaleInverseImageComparison.{u, v}
      (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))).val
Tag 09ZI, a theorem

Tag 09ZI in the Stacks Project.

Stacks.EtaleCohomology.etaleCohomologyRestrictionMap_bijective_of_henselianPair, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AffineAnalogProper/Gabber/Theorem.lean, line 189. The attribute's comment: “Gabber's theorem: for a henselian pair (A, I), every torsion abelian sheaf F on the small étale site of X = Spec A and every q, restriction H^q(X, F) → H^q(Z, F|_Z) to Z = Spec (A/I) is bijective”. References: SGA 4 XII (6.13), “more general”.

Gabber's theorem. Let (A, I) be a henselian pair, X = Spec A and Z = Spec (A ⧸ I). For every torsion abelian sheaf F on X_étale and every q ≥ 0 the restriction map H^q_étale(X, F) → H^q_étale(Z, F|_Z) is bijective.

Torsion is the local condition of Stacks 0DD7, Stacks.Torsion.torsionSheafProperty: every section is annihilated by a positive integer after restriction along a covering. Cohomology is Mathlib's CategoryTheory.Sheaf.H, the restricted sheaf is the étale inverse image along Spec (A ⧸ I) ⟶ Spec A, and the map is Stacks.EtaleCohomology.etaleCohomologyRestrictionMap.

theorem etaleCohomologyRestrictionMap_bijective_of_henselianPair
    (F : Sheaf (Spec (.of A)).smallEtaleTopology AddCommGrpCat.{u + 1})
    (hF : Stacks.Torsion.torsionSheafProperty (Spec (.of A)).smallEtaleTopology F) (q : ℕ) :
    Function.Bijective (etaleCohomologyRestrictionMap.{u, 0, u + 1}
      (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) F q)
Tag 0A51, a lemma

Tag 0A51 in the Stacks Project.

Stacks.EtaleCohomology.subsingleton_H_closed_of_injective_of_affine_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AffineAnalogProper/InjectiveClosedVanishing.lean, line 200. The attribute's comment: “X with affine diagonal covered by n + 1 affine opens, Z a closed subscheme, 𝒜 a torsion sheaf of rings on X_et, ℐ an injective 𝒜-module: H^q_et(Z, ℐ|_Z) = 0 for q > n”.

[Stacks, Tag 0A51]. Let X be a scheme with affine diagonal which can be covered by n + 1 affine opens, let i : Z ⟶ X be a closed immersion, let 𝒜 be a torsion sheaf of rings on X_étale and let ℐ be an injective sheaf of 𝒜-modules on X_étale. Then H^q_étale(Z, ℐ|_Z) = 0 for every q > n.

Affine diagonal is IsAffineHom (pullback.diagonal (terminal.from X)), the diagonal of X over Spec ℤ. The sheaf 𝒜 is torsion in the sense of Stacks 0DD7: every local section of its underlying abelian sheaf is locally annihilated by a positive integer. The restriction ℐ|_Z is the étale inverse image along i of the underlying abelian sheaf of ℐ, and H^q_étale is its étale cohomology CategoryTheory.Sheaf.H.

theorem subsingleton_H_closed_of_injective_of_affine_cover {X Z : Scheme.{u}}
    [IsAffineHom (pullback.diagonal (terminal.from X))] (n : ℕ)
    (hX : ∃ U : Fin (n + 1) → X.Opens, (∀ k, IsAffineOpen (U k)) ∧ ⨆ k, U k = ⊤)
    (i : Z ⟶ X) [IsClosedImmersion i] (𝒜 : Sheaf X.smallEtaleTopology RingCat.{u + 1})
    (h𝒜 : Stacks.Torsion.torsionSheafProperty X.smallEtaleTopology
      ((sheafCompose X.smallEtaleTopology (forget₂ RingCat AddCommGrpCat)).obj 𝒜))
    (ℐ : SheafOfModules.{u + 1} 𝒜) [Injective ℐ] (q : ℕ) (hq : n < q) :
    Subsingleton (Sheaf.H.{u + 1} ((etaleAbelianInverseImage.{u, 0} i).obj
      ((SheafOfModules.toSheaf 𝒜).obj ℐ)) q)
Sources
LeanStacks.EtaleCohomology.exists_mono_comp_etaleAbelianInverseImage_eq_zero_of_torsion · Stacks.EtaleCohomology.isIso_globalSectionsSmallEtaleInverseImageComparison_of_zariskiBijective · exists_isClosed_partition · Stacks.bijective_globalSectionsRestriction_of_isConnected_inter_closure · Stacks.EtaleCohomology.isIso_globalSectionsComparison_quotient_of_henselianPair · Stacks.EtaleCohomology.etaleCohomologyRestrictionMap_bijective_of_henselianPair · Stacks.EtaleCohomology.subsingleton_H_closed_of_injective_of_affine_cover

Section59.83 Cohomology of torsion sheaves on curves#

Section 59.83 of the Stacks Project, Tag 03SB. 20 tags here are carried by 47 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0A52, a situation

Tag 0A52 in the Stacks Project.

Stacks.EtaleCohomology.TorsionSheafSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/TorsionSheafSituation.lean, line 42.

An algebraically closed field k, a separated scheme X of finite type over k whose underlying space has Krull dimension at most one, and a torsion abelian sheaf F on the small étale site of X.

public structure TorsionSheafSituation
Tag 0A53, an item

Tag 0A53 in the Stacks Project.

Stacks.EtaleCohomology.TorsionSheafSituation.isVanishingAboveDegreeTwo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/CurveCohomologyTheorem.lean, line 79.

Stacks Project, Tag 0A53, statement (1) of Situation 0A52: H^q(X, F) = 0 for q > 2.

theorem isVanishingAboveDegreeTwo
    [HasExt.{w} (Sheaf S.X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})] :
    IsVanishingAboveDegreeTwo.{u, v, w} S.F

Stacks.EtaleCohomology.IsVanishingAboveDegreeTwo, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/VanishingAboveDegreeTwo.lean, line 91. The attribute's comment: “item (1) of 0A52: H^q(X, F) = 0 for q > 2”.

Stacks Project, Tag 0A53. Statement (1) of the list of Situation 0A52: the étale cohomology H^q_étale(X, F) vanishes for every degree q > 2.

def IsVanishingAboveDegreeTwo
    (F : Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}) : Prop
Tag 0A54, an item

Tag 0A54 in the Stacks Project.

Stacks.EtaleCohomology.IsAffineVanishingAboveDegreeOne, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/AffineVanishingAboveDegreeOne.lean, line 54. The attribute's comment: “item (2) of 0A52: H^q(X, F) = 0 for q > 1 if X is affine”.

Statement (2) of the list of Situation 0A52: the étale cohomology H^q_étale(X, F) vanishes for every q > 1 if X is affine.

def IsAffineVanishingAboveDegreeOne
    (F : Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}) : Prop

Stacks.EtaleCohomology.TorsionSheafSituation.isAffineVanishingAboveDegreeOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/CurveCohomologyTheorem.lean, line 87.

Stacks Project, Tag 0A54, statement (2) of Situation 0A52: if X is affine then H^q(X, F) = 0 for q > 1.

theorem isAffineVanishingAboveDegreeOne
    [HasExt.{w} (Sheaf S.X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})] :
    IsAffineVanishingAboveDegreeOne.{u, v, w} S.F
Tag 0A55, an item

Tag 0A55 in the Stacks Project.

Stacks.EtaleCohomology.TorsionSheafSituation.isPrimePowerTorsionVanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/CurveCohomologyTheorem.lean, line 95.

Stacks Project, Tag 0A55, statement (3) of Situation 0A52: if p = char(k) > 0 and F is p-power torsion then H^q(X, F) = 0 for q > 1.

theorem isPrimePowerTorsionVanishing
    [HasExt.{w} (Sheaf S.X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})]
    (p : ℕ) [CharP S.k p] :
    IsPrimePowerTorsionVanishing.{u, v, w} S.structureMorphism p S.F

Stacks.EtaleCohomology.IsPrimePowerTorsionVanishing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/PrimePowerVanishingStatement.lean, line 200. The attribute's comment: “item (3) of 0A52: H^q(X, F) = 0 for q > 1 if p = char(k) > 0 and F is p-power torsion”.

Stacks Project, Tag 0A55, item (3) of Situation 0A52:

H^q_étale(X, F) = 0 for q > 1 if p = char(k) > 0 and F is p-power torsion.

Here X is a scheme with a morphism π to the spectrum of a field k of characteristic p, and F is an abelian sheaf on the small étale site of X. The source states this as one entry of the list of eight statements that Situation 0A52 asks for, not as an assertion, so it is a predicate on the data; the situation's further hypotheses — k algebraically closed, X separated of finite type of dimension at most one, F torsion — are what make the item a theorem at Tag 03SC, and are not imposed here.

def IsPrimePowerTorsionVanishing (π : X ⟶ Spec (.of k)) (p : ℕ) [CharP k p]
    (F : Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})
    [HasExt.{w} (Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})] : Prop
Tag 0A56, an item

Tag 0A56 in the Stacks Project.

Stacks.EtaleCohomology.TorsionSheafSituation.finiteCohomologyOfPrimeToCharacteristic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/CurveCohomologyTheorem.lean, line 104. References: SGA 5 VI (3.1), “Finite length of H^i(X”.

Stacks Project, Tag 0A56, statement (4) of Situation 0A52: if F is constructible and torsion prime to char(k) then H^q(X, F) is finite.

theorem finiteCohomologyOfPrimeToCharacteristic (B : BigEtaleSite.{u}) (hX : B.Contains S.X)
    [HasExt.{w} (Sheaf S.X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})] :
    S.FiniteCohomologyOfPrimeToCharacteristic.{u, v, w} B hX

Stacks.EtaleCohomology.TorsionSheafSituation.FiniteCohomologyOfPrimeToCharacteristic, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/PrimeToCharacteristicFiniteness.lean, line 89. The attribute's comment: “statement (4) of Situation 0A52, as a predicate on the situation”.

Statement (4) of Situation 0A52. For an algebraically closed field k, a separated finite-type scheme X of dimension at most one over k and a torsion abelian sheaf F on the small étale site of X: if F is constructible and its torsion is prime to the characteristic of k, then H^q_étale(X, F) is finite for every q.

"Torsion prime to the characteristic" is taken at the exponential characteristic.

def FiniteCohomologyOfPrimeToCharacteristic : Prop
Tag 0A57, an item

Tag 0A57 in the Stacks Project.

Stacks.EtaleCohomology.TorsionSheafSituation.finiteCohomologyOfIsProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/CurveCohomologyTheorem.lean, line 114.

Stacks Project, Tag 0A57, statement (5) of Situation 0A52: if X is proper and F is constructible then H^q(X, F) is finite.

theorem finiteCohomologyOfIsProper (B : BigEtaleSite.{u}) (hX : B.Contains S.X)
    [HasExt.{w} (Sheaf S.X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})] :
    S.FiniteCohomologyOfIsProper.{u, v, w} B hX

Stacks.EtaleCohomology.TorsionSheafSituation.FiniteCohomologyOfIsProper, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/ProperFinitenessStatement.lean, line 151. The attribute's comment: “statement (5) of Situation 0A52, as a predicate on the situation”.

Stacks Project, Tag 0A57, statement (5) of Situation 0A52. For an algebraically closed field k, a separated finite-type scheme X of dimension at most one over k and a torsion abelian sheaf F on the small étale site of X: if the structure morphism of X is proper and F is constructible, then H^q_étale(X, F) is finite for every q.

The source states this as one entry of the list of eight statements that Situation 0A52 asks for, not as an assertion, so it is a predicate on the data of the situation.

def TorsionSheafSituation.FiniteCohomologyOfIsProper (S : TorsionSheafSituation.{u, v})
    (B : BigEtaleSite.{u}) (hX : B.Contains S.X)
    [HasExt.{w} (Sheaf S.X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})] : Prop
Tag 0A58, an item

Tag 0A58 in the Stacks Project.

Stacks.EtaleCohomology.TorsionSheafSituation.BaseChangePrimeToCharacteristic, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/BaseChangePrimeToCharacteristic.lean, line 63. The attribute's comment: “statement (6) of Situation 0A52, as a predicate on the situation”.

Statement (6) of the list of statements of Situation 0A52: if the torsion of the situation's abelian sheaf F is prime to the characteristic of the algebraically closed ground field k, then for every algebraically closed extension k'/k and every degree q the restriction map H^q_étale(X, F) → H^q_étale(X_{k'}, F|_{X_{k'}}) is bijective.

"Torsion prime to the characteristic" is taken at the exponential characteristic, so that in characteristic zero it is the torsion condition the situation already carries.

def TorsionSheafSituation.BaseChangePrimeToCharacteristic
    (S : TorsionSheafSituation.{u, v}) : Prop

Stacks.EtaleCohomology.TorsionSheafSituation.baseChangePrimeToCharacteristic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/CurveCohomologyTheorem.lean, line 125.

Stacks Project, Tag 0A58, statement (6) of Situation 0A52: if F is torsion prime to char(k) then H^q(X, F) → H^q(X_{k'}, F|_{X_{k'}}) is bijective for every extension k'/k of algebraically closed fields.

theorem baseChangePrimeToCharacteristic : S.BaseChangePrimeToCharacteristic.{u, v, w}
Tag 0A59, an item

Tag 0A59 in the Stacks Project.

Stacks.EtaleCohomology.TorsionSheafSituation.ProperBaseChangeStatement, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/ProperBaseChangeStatement.lean, line 58. The attribute's comment: “item (7) of Situation 0A52, as a predicate on the situation”.

Statement (7) of Situation 0A52. For an algebraically closed field k, a separated finite-type scheme X of dimension at most one over k and a torsion abelian sheaf F on the small étale site of X: if the structure morphism of X is proper then H^q_étale(X, F) → H^q_étale(X_{k'}, F|_{X_{k'}}) is an isomorphism in every degree, for every extension k'/k of algebraically closed fields.

def TorsionSheafSituation.ProperBaseChangeStatement (S : TorsionSheafSituation.{u, v}) : Prop

Stacks.EtaleCohomology.TorsionSheafSituation.properBaseChangeStatement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/CurveCohomologyTheorem.lean, line 133.

Stacks Project, Tag 0A59, statement (7) of Situation 0A52: if X is proper then H^q(X, F) → H^q(X_{k'}, F|_{X_{k'}}) is bijective for every extension k'/k of algebraically closed fields.

theorem properBaseChangeStatement : S.ProperBaseChangeStatement.{u, v, w}
Tag 0A5A, an item

Tag 0A5A in the Stacks Project.

Stacks.EtaleCohomology.TorsionSheafSituation.isDegreeTwoOpenRestrictionSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/CurveCohomologyTheorem.lean, line 140.

Stacks Project, Tag 0A5A, statement (8) of Situation 0A52: H²(X, F) → H²(U, F) is surjective for every open U ⊆ X.

theorem isDegreeTwoOpenRestrictionSurjective
    [HasExt.{w} (Sheaf S.X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})] :
    IsDegreeTwoOpenRestrictionSurjective.{u, v, w} S.F

Stacks.EtaleCohomology.IsDegreeTwoOpenRestrictionSurjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/DegreeTwoOpenRestrictionSurjectivity.lean, line 48. The attribute's comment: “item (8) of 0A52: H²(X, F) → H²(U, F) surjective for all open U ⊆ X”.

The restriction map H²_étale(X, F) → H²_étale(U, F) is surjective for every open subscheme U ⊆ X.

def IsDegreeTwoOpenRestrictionSurjective
    (F : Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}) : Prop
Tag 0A5B, a lemma

Tag 0A5B in the Stacks Project.

Stacks.EtaleCohomology.curveStatements_constantSheaf_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/SmoothConstantCurveStatements.lean, line 98.

Stacks Project, Lemma 0A5B. In Situation 0A52 — k algebraically closed, X separated, of finite type and of dimension at most one over k — assume X is smooth over k and let F = 𝐙/ℓ𝐙 be the constant sheaf on X_étale for a prime ℓ, with value any abelian group E cyclic of order ℓ. Then statements (1) -- (8) of Situation 0A52 hold for F, in the sense of Stacks.EtaleCohomology.CurveStatements, at every coefficient universe and every Ext universe.

On the smooth curve components of X this is curveStatementsConstantOnSmoothCurves_of_prime (Cases I and II of the source); the reduction theorem curveStatements_of_torsionSheafProperty_max carries it to X and to the coefficients AddCommGrpCat.{max (u + 1) v}, the constant sheaf with finite value being torsion.

theorem curveStatements_constantSheaf_of_smooth {k : Type u} [Field k] [IsAlgClosed k]
    {X : Scheme.{u}} (π : X ⟶ Spec (.of k)) [IsSeparated π] [LocallyOfFiniteType π]
    [QuasiCompact π] [Smooth π] (hdim : topologicalKrullDim X ≤ 1) {ℓ : ℕ} (hℓ : ℓ.Prime)
    (E : AddCommGrpCat.{max (u + 1) v}) (hE : Nonempty (E ≃+ ZMod ℓ))
    [HasExt.{w} (Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})] :
    CurveStatements.{u, v, w} π
      ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}).obj E)
Tag 0A47, a remark

Tag 0A47 in the Stacks Project.

Stacks.ArtinSchreier.exact_affineLineBoundary, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/AffineLine.lean, line 113. The attribute's comment: “the exact sequence k[x] → k[x] → H¹(A¹_k, Z/p) → 0, first arrow f ↦ f^p - f”.

The exact sequence k[x] ⟶ k[x] ⟶ H¹(𝐀¹_k, 𝐙/p𝐙) ⟶ 0. Let k be a field of characteristic p > 0. The boundary of the Artin–Schreier sequence on the affine line is onto H¹(𝐀¹_k, 𝐙/p𝐙) and its kernel is the image of f ↦ f ^ p - f.

The source states this for k algebraically closed; only the characteristic of k is needed.

theorem exact_affineLineBoundary :
    Function.Exact (ringArtinSchreier k[X] p) (affineLineBoundary.{w} k p) ∧
      Function.Surjective (affineLineBoundary.{w} k p)

Stacks.ArtinSchreier.existsUnique_affineLineBoundary_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/AffineLine.lean, line 137. The attribute's comment: “every class of H¹(A¹_k, Z/p) is the image of exactly one sum over p ∤ n of λ_n x^n”.

The representatives, read in cohomology. Let k be an algebraically closed field of characteristic p > 0. Every class in H¹(𝐀¹_k, 𝐙/p𝐙) is the boundary of exactly one polynomial ∑_{p ∤ n} λₙ xⁿ.

theorem existsUnique_affineLineBoundary_eq [IsAlgClosed k]
    (c : Sheaf.H.{w} (etaleConstantZMod (affineLine k) p) 1) :
    ∃! f : k[X], (∀ n, p ∣ n → f.coeff n = 0) ∧ affineLineBoundary.{w} k p f = c

Stacks.ArtinSchreier.not_surjective_etaleCohomologyRestrictionMap_affineLine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/AffineLine.lean, line 238. The attribute's comment: “H¹(A¹_k, Z/p) → H¹(A¹_{k'}, Z/p) is not surjective when k ⊊ k'”.

H¹(𝐀¹_k, 𝐙/p𝐙) → H¹(𝐀¹_{k'}, 𝐙/p𝐙) is not surjective. Let k be an algebraically closed field of characteristic p > 0 and k'/k an extension with k' ≠ k. Then the restriction map H¹(𝐀¹_k, 𝐙/p𝐙) → H¹(𝐀¹_{k'}, 𝐙/p𝐙) along 𝐀¹_{k'} ⟶ 𝐀¹_k is not surjective — in particular not an isomorphism: for λ ∈ k' ∖ k the class of λ x is not in its image.

The source takes k' algebraically closed; that is not used.

theorem not_surjective_etaleCohomologyRestrictionMap_affineLine [IsAlgClosed k]
    (hk : ¬ Function.Surjective (algebraMap k k'))
    [HasExt.{w} (Sheaf (affineLine k).smallEtaleTopology AddCommGrpCat.{u + 1})]
    [HasExt.{w} (Sheaf (scalarExtension k k' (affineLineStructure k)).smallEtaleTopology
      AddCommGrpCat.{u + 1})] :
    ¬ Function.Surjective (etaleCohomologyRestrictionMap.{u, 0, w}
      (scalarExtensionFst k k' (affineLineStructure k))
      (etaleConstantZMod (affineLine k) p) 1)

Stacks.ArtinSchreier.exists_not_bijective_etaleCohomologyRestrictionMap_affineLine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/AffineLine.lean, line 291. The attribute's comment: “so H¹(A¹_k, Z/p) → H¹(A¹_{k'}, Z/p) is not an isomorphism in general”.

The restriction map is not an isomorphism in general. For every algebraically closed field k of characteristic p > 0 there is an algebraically closed extension k'/k — an algebraic closure of k(t) — for which H¹(𝐀¹_k, 𝐙/p𝐙) → H¹(𝐀¹_{k'}, 𝐙/p𝐙) is not an isomorphism.

theorem exists_not_bijective_etaleCohomologyRestrictionMap_affineLine [IsAlgClosed k] :
    ∃ (k' : Type u) (_ : Field k') (_ : Algebra k k') (_ : IsAlgClosed k'),
      ∀ [HasExt.{w} (Sheaf (affineLine k).smallEtaleTopology AddCommGrpCat.{u + 1})]
        [HasExt.{w} (Sheaf (scalarExtension k k' (affineLineStructure k)).smallEtaleTopology
          AddCommGrpCat.{u + 1})],
        ¬ Function.Bijective (etaleCohomologyRestrictionMap.{u, 0, w}
          (scalarExtensionFst k k' (affineLineStructure k))
          (etaleConstantZMod (affineLine k) p) 1)

Stacks.ArtinSchreier.bijective_etaleCohomologyRestrictionMap_affineLine_of_isUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/AffineLine.lean, line 338. The attribute's comment: “only in characteristic p with p-power torsion: bijective for Z/n, n invertible in k”.

The phenomenon only occurs with p-power torsion coefficients. Let k'/k be an extension of algebraically closed fields and let n be invertible in k. Then H^q(𝐀¹_k, 𝐙/n𝐙) → H^q(𝐀¹_{k'}, 𝐙/n𝐙) is bijective in every degree q: this is statement (6) of Situation 0A52 (Tag 0A58) for the affine line. In characteristic 0 every n ≥ 1 is invertible, so the base change map is an isomorphism for every finite cyclic coefficient group.

theorem bijective_etaleCohomologyRestrictionMap_affineLine_of_isUnit {n : ℕ} (hn : IsUnit (n : k))
    [HasExt.{w} (Sheaf (affineLine k).smallEtaleTopology AddCommGrpCat.{max (u + 1) v})]
    [HasExt.{w} (Sheaf (scalarExtension k k' (affineLineStructure k)).smallEtaleTopology
      AddCommGrpCat.{max (u + 1) v})] (q : ℕ) :
    Function.Bijective (etaleCohomologyRestrictionMap.{u, v, w}
      (scalarExtensionFst k k' (affineLineStructure k))
      ((constantSheaf (affineLine k).smallEtaleTopology AddCommGrpCat.{max (u + 1) v}).obj
        (AddCommGrpCat.of (ULift.{max (u + 1) v} (ZMod n)))) q)

Stacks.ArtinSchreier.not_bijective_etaleFundamentalGroupMap_affineLine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/AffineLineScalarExtension.lean, line 223. The attribute's comment: “π₁(A¹_{k'}) → π₁(A¹_k) is not an isomorphism for algebraically closed k ⊊ k'”. References: SGA 1 IX (6.3), “more general”; SGA 1 X (1.10), “partial”; SGA 1 XIII (2.13), “partial”.

[Stacks, Tag 0A47]: π₁(𝐀¹_{k'}) → π₁(𝐀¹_k) is not an isomorphism. Let k'/k be an extension of algebraically closed fields of characteristic p > 0 with k' ≠ k. Then for every geometric point x of 𝐀¹_{k'} the map of étale fundamental groups π₁(𝐀¹_{k'}, x) → π₁(𝐀¹_k, x) induced by 𝐀¹_{k'} ⟶ 𝐀¹_k is not bijective.

theorem not_bijective_etaleFundamentalGroupMap_affineLine {p : ℕ} [hp : Fact p.Prime] [CharP k p]
    [IsAlgClosed k] [IsAlgClosed k'] (hk : ¬ Function.Surjective (algebraMap k k'))
    (x : GeometricPoint (scalarExtension k k' (affineLineStructure k))) :
    ¬ Function.Bijective
      (etaleFundamentalGroupMap (scalarExtensionFst k k' (affineLineStructure k)) x)

Stacks.ArtinSchreier.exists_not_bijective_etaleFundamentalGroupMap_affineLine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/AffineLineScalarExtension.lean, line 273. The attribute's comment: “so the étale fundamental group of A¹ depends on the algebraically closed field”. References: SGA 1 IX (6.3); SGA 1 X (1.10), “partial”.

[Stacks, Tag 0A47]: the étale fundamental group of the affine line depends on the algebraically closed ground field. For every algebraically closed field k of characteristic p > 0 there is an algebraically closed extension k'/k — an algebraic closure of k(t) — for which π₁(𝐀¹_{k'}, x) → π₁(𝐀¹_k, x) is not bijective at any geometric point x.

The source concludes that the étale homotopy type of the affine line depends on the algebraically closed ground field; the étale homotopy type is not available here, and this statement, with Stacks.ArtinSchreier.exists_not_bijective_etaleCohomologyRestrictionMap_affineLine for H¹, is the content of that conclusion for the invariants π₁ and H¹ of the homotopy type.

theorem exists_not_bijective_etaleFundamentalGroupMap_affineLine {p : ℕ} [Fact p.Prime]
    [CharP k p] [IsAlgClosed k] :
    ∃ (k' : Type u) (_ : Field k') (_ : Algebra k k') (_ : IsAlgClosed k'),
      ∀ x : GeometricPoint (scalarExtension k k' (affineLineStructure k)),
        ¬ Function.Bijective
          (etaleFundamentalGroupMap (scalarExtensionFst k k' (affineLineStructure k)) x)

Polynomial.existsUnique_sub_mem_range_ringArtinSchreier, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Polynomial/ArtinSchreierCokernel.lean, line 171. The attribute's comment: “the polynomials sum over p ∤ n of λ_n x^n represent the cokernel of f ↦ f^p - f”.

[Stacks, Tag 0A47], the representatives of the cokernel. Let k be an algebraically closed field of characteristic p > 0. Every polynomial g ∈ k[x] is congruent modulo the image of f ↦ f ^ p - f to exactly one polynomial ∑_{p ∤ n} λₙ xⁿ, that is, to exactly one polynomial with no coefficient in a degree divisible by p (the degree 0 included). In other words these polynomials form a set of representatives for the cokernel of k[x] → k[x], f ↦ f ^ p - f.

theorem existsUnique_sub_mem_range_ringArtinSchreier [IsAlgClosed k] (g : k[X]) :
    ∃! f : k[X], (∀ n, p ∣ n → f.coeff n = 0) ∧
      g - f ∈ (ringArtinSchreier k[X] p).range

Polynomial.exists_sub_mem_range_ringArtinSchreier_of_perfectRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Polynomial/ArtinSchreierCokernel.lean, line 225. The attribute's comment: “if k is not algebraically closed, constants have to be added (k perfect)”.

[Stacks, Tag 0A47], the parenthetical case of a field that is not algebraically closed. Let k be a perfect field of characteristic p > 0. Then the representatives of the cokernel of f ↦ f ^ p - f on k[x] need constants added: every g ∈ k[x] is congruent to a polynomial ∑_{p ∤ n} λₙ xⁿ + c, and two such polynomials are congruent exactly when their coefficients λₙ agree and their constant terms differ by a value a ^ p - a of k. So the constants needed are a set of representatives of k / {a ^ p - a}, which is zero for algebraically closed k.

The source says "if k is not algebraically closed"; perfectness is needed and is assumed here: over an imperfect field the description fails, by Polynomial.not_exists_sub_mem_range_ringArtinSchreier_of_not_pth_power.

theorem exists_sub_mem_range_ringArtinSchreier_of_perfectRing [PerfectRing k p] :
    (∀ g : k[X], ∃ f : k[X], (∀ n, 0 < n → p ∣ n → f.coeff n = 0) ∧
      g - f ∈ (ringArtinSchreier k[X] p).range) ∧
    ∀ f f' : k[X], (∀ n, 0 < n → p ∣ n → f.coeff n = 0) →
      (∀ n, 0 < n → p ∣ n → f'.coeff n = 0) →
      (f - f' ∈ (ringArtinSchreier k[X] p).range ↔
        (∀ n, n ≠ 0 → f.coeff n = f'.coeff n) ∧
          f.coeff 0 - f'.coeff 0 ∈ (ringArtinSchreier k p).range)
Tag 0A5C, a lemma

Tag 0A5C in the Stacks Project.

Stacks.EtaleCohomology.CurveStatements.of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/CurveStatementsShortExactConstructible.lean, line 101. The attribute's comment: “all eight statements of 0A52 at once, at the coefficients AddCommGrpCat.{u+1}”.

Let 0 → F₁ → F → F₂ → 0 be a short exact sequence of abelian sheaves on the small étale site of a Noetherian scheme X over a field. If statements (1) -- (8) of Situation 0A52 hold for F₁ and F₂, then they hold for F.

theorem CurveStatements.of_shortExact (hS : S.ShortExact)
    (h₁ : CurveStatements.{u, 0, w} π S.X₁) (h₃ : CurveStatements.{u, 0, w} π S.X₃) :
    CurveStatements.{u, 0, w} π S.X₂

Stacks.EtaleCohomology.curveCohomologyStatements_X₂_of_shortExact_isConstructible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/ShortExactCurveStatements.lean, line 210. The attribute's comment: “the eight statements of Situation 0A52 pass to the middle term of a short exact sequence of abelian sheaves, with constructibility of the sub- and the quotient sheaf supplied by Proposition 09BH (2)”.

Stacks Project, Tag 0A5C. Let X be a Noetherian scheme, let π be a morphism from X to the spectrum of a field, let i be a morphism of schemes to X, and let 0 → S.X₁ → S.X₂ → S.X₃ → 0 be a short exact sequence of abelian sheaves on the small étale site of X. If the eight statements of Situation 0A52 hold for S.X₁ and for S.X₃, then they hold for S.X₂.

The eight statements, bundled as Stacks.EtaleCohomology.CurveCohomologyStatements, are: the vanishing of H^q(X, -) above degree two; its vanishing above degree one over an affine X; its vanishing above degree one for coefficients of l-power torsion; the finiteness of H^q(X, -) for constructible coefficients of torsion prime to p; its finiteness for constructible coefficients over a proper X; the bijectivity of restriction along i for coefficients of torsion prime to p; the bijectivity of restriction along i over a proper X; and the surjectivity of restriction along i in degree two. In the source l and p are the characteristic and the exponential characteristic of the base field, and i is the projection of a scalar extension along an extension of algebraically closed fields in statements (6) and (7) and the inclusion of an open subscheme in statement (8); none of those identifications is imposed here, so this statement is stronger than the one the source makes.

Constructibility of an abelian sheaf is AlgebraicGeometry.IsConstructibleEtaleSiteAbelianSheaf, read on the small étale site of Stacks 021B across its dense subsite comparison with the site AlgebraicGeometry.Scheme.smallEtaleTopology that carries the cohomology. Its descent to the sub- and the quotient sheaf of a short exact sequence, which statements (4) and (5) need, is Proposition 09BH (2) and is what the Noetherian hypothesis is for; the other six transfers use no hypothesis on X at all. Situation 0A52 asks X to be separated of finite type over an algebraically closed field and of dimension at most one, and asks the sheaves to be torsion; finite type over a field makes X Noetherian, and the remaining hypotheses are not used and so do not appear.

theorem curveCohomologyStatements_X₂_of_shortExact_isConstructible [IsNoetherian X.obj]
    {k : Type u} [Field k] (π : X.obj ⟶ Spec (.of k)) (l p : ℕ) (hS : S.ShortExact)
    (h₁ : CurveCohomologyStatements.{u, u + 1, w} i π l p
      (IsConstructibleEtaleSiteAbelianSheaf B X) S.X₁)
    (h₃ : CurveCohomologyStatements.{u, u + 1, w} i π l p
      (IsConstructibleEtaleSiteAbelianSheaf B X) S.X₃) :
    CurveCohomologyStatements.{u, u + 1, w} i π l p
      (IsConstructibleEtaleSiteAbelianSheaf B X) S.X₂

Stacks.EtaleCohomology.finite_etaleCohomology_X₂_of_shortExact_of_isPrimeToCharacteristicTorsion_isConstructible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/ShortExactCurveStatements.lean, line 236. The attribute's comment: “statement (4): the finiteness of etale cohomology for constructible coefficients of torsion prime to the characteristic passes to the middle term of a short exact sequence, with the constructibility of the sub- and the quotient sheaf supplied by Proposition 09BH (2)”.

Statement (4) of Situation 0A52 passes to extensions, for constructible coefficients. Let X be a Noetherian scheme, let p be a natural number — the characteristic of the base field in the source — and let 0 → S.X₁ → S.X₂ → S.X₃ → 0 be a short exact sequence of abelian sheaves on the small étale site of X. If the finiteness of étale cohomology for coefficients that are constructible and torsion prime to p holds for the sub- and the quotient sheaf, then it holds for the middle sheaf.

This is finite_etaleCohomology_X₂_of_shortExact_of_isPrimeToCharacteristicTorsion with the coefficient condition taken to be constructibility of an abelian sheaf and its descent to the sub- and the quotient sheaf discharged, by Proposition 09BH (2), rather than assumed: that descent is what Tag 0A5C cites at this point, and it is the only use of the Noetherian hypothesis.

theorem finite_etaleCohomology_X₂_of_shortExact_of_isPrimeToCharacteristicTorsion_isConstructible
    [IsNoetherian X.obj] (p : ℕ) (hS : S.ShortExact)
    (h₁ : IsConstructibleEtaleSiteAbelianSheaf B X S.X₁ →
      Stacks.Torsion.IsPrimeToCharacteristicTorsion X.obj.smallEtaleTopology p S.X₁ →
      ∀ q : ℕ, Finite (Sheaf.H.{w} S.X₁ q))
    (h₃ : IsConstructibleEtaleSiteAbelianSheaf B X S.X₃ →
      Stacks.Torsion.IsPrimeToCharacteristicTorsion X.obj.smallEtaleTopology p S.X₃ →
      ∀ q : ℕ, Finite (Sheaf.H.{w} S.X₃ q))
    (hc : IsConstructibleEtaleSiteAbelianSheaf B X S.X₂)
    (ht : Stacks.Torsion.IsPrimeToCharacteristicTorsion X.obj.smallEtaleTopology p S.X₂)
    (q : ℕ) :
    Finite (Sheaf.H.{w} S.X₂ q)

Stacks.EtaleCohomology.finite_etaleCohomology_X₂_of_shortExact_of_isProper_isConstructible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/ShortExactCurveStatements.lean, line 266. The attribute's comment: “statement (5): the finiteness of etale cohomology for constructible coefficients over a proper scheme passes to the middle term of a short exact sequence, with the constructibility of the sub- and the quotient sheaf supplied by Proposition 09BH (2)”.

Statement (5) of Situation 0A52 passes to extensions, for constructible coefficients. Let X be a Noetherian scheme, let π be its structure morphism to the spectrum of a field, and let 0 → S.X₁ → S.X₂ → S.X₃ → 0 be a short exact sequence of abelian sheaves on the small étale site of X. If the finiteness of étale cohomology for constructible coefficients over a proper X holds for the sub- and the quotient sheaf, then it holds for the middle sheaf.

This is Stacks.EtaleCohomology.finite_etaleCohomology_X₂_of_shortExact_of_isProper with the coefficient condition taken to be constructibility of an abelian sheaf and its descent to the sub- and the quotient sheaf discharged by Proposition 09BH (2), exactly as in statement (4). The properness condition constrains the scheme and is passed to the outer terms unchanged.

theorem finite_etaleCohomology_X₂_of_shortExact_of_isProper_isConstructible
    [IsNoetherian X.obj] {k : Type u} [Field k] (π : X.obj ⟶ Spec (.of k)) (hS : S.ShortExact)
    (h₁ : IsConstructibleEtaleSiteAbelianSheaf B X S.X₁ → IsProper π →
      ∀ q : ℕ, Finite (Sheaf.H.{w} S.X₁ q))
    (h₃ : IsConstructibleEtaleSiteAbelianSheaf B X S.X₃ → IsProper π →
      ∀ q : ℕ, Finite (Sheaf.H.{w} S.X₃ q))
    (hc : IsConstructibleEtaleSiteAbelianSheaf B X S.X₂) (hπ : IsProper π) (q : ℕ) :
    Finite (Sheaf.H.{w} S.X₂ q)

Stacks.EtaleCohomology.subsingleton_etaleCohomology_X₂_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/ShortExactExtension.lean, line 72. The attribute's comment: “vanishing”.

If the étale cohomology of the sub- and the quotient sheaf of a short exact sequence of abelian sheaves vanishes above degree two, then so does that of the middle sheaf.

theorem subsingleton_etaleCohomology_X₂_of_shortExact (hS : S.ShortExact)
    (h₁ : ∀ q : ℕ, 2 < q → Subsingleton (Sheaf.H.{w} S.X₁ q))
    (h₃ : ∀ q : ℕ, 2 < q → Subsingleton (Sheaf.H.{w} S.X₃ q))
    (q : ℕ) (hq : 2 < q) :
    Subsingleton (Sheaf.H.{w} S.X₂ q)

Stacks.EtaleCohomology.subsingleton_etaleCohomology_X₂_of_shortExact_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/ShortExactExtension.lean, line 85. The attribute's comment: “affine vanishing”.

If, for an affine scheme, the étale cohomology of the sub- and the quotient sheaf of a short exact sequence of abelian sheaves vanishes above degree one, then so does that of the middle sheaf.

theorem subsingleton_etaleCohomology_X₂_of_shortExact_of_isAffine (hS : S.ShortExact)
    (h₁ : IsAffine X → ∀ q : ℕ, 1 < q → Subsingleton (Sheaf.H.{w} S.X₁ q))
    (h₃ : IsAffine X → ∀ q : ℕ, 1 < q → Subsingleton (Sheaf.H.{w} S.X₃ q))
    (hX : IsAffine X) (q : ℕ) (hq : 1 < q) :
    Subsingleton (Sheaf.H.{w} S.X₂ q)

Stacks.EtaleCohomology.subsingleton_etaleCohomology_X₂_of_shortExact_of_isPrimePowerTorsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/ShortExactExtension.lean, line 98. The attribute's comment: “characteristic-primary vanishing”.

Let l be a natural number. If the vanishing of étale cohomology above degree one for l-power torsion coefficients holds for the sub- and the quotient sheaf of a short exact sequence of abelian sheaves, then it holds for the middle sheaf.

theorem subsingleton_etaleCohomology_X₂_of_shortExact_of_isPrimePowerTorsion
    (l : ℕ) (hS : S.ShortExact)
    (h₁ : Stacks.Torsion.IsPrimePowerTorsion X.smallEtaleTopology l S.X₁ →
      ∀ q : ℕ, 1 < q → Subsingleton (Sheaf.H.{w} S.X₁ q))
    (h₃ : Stacks.Torsion.IsPrimePowerTorsion X.smallEtaleTopology l S.X₃ →
      ∀ q : ℕ, 1 < q → Subsingleton (Sheaf.H.{w} S.X₃ q))
    (h₂ : Stacks.Torsion.IsPrimePowerTorsion X.smallEtaleTopology l S.X₂) (q : ℕ) (hq : 1 < q) :
    Subsingleton (Sheaf.H.{w} S.X₂ q)

Stacks.EtaleCohomology.bijective_etaleCohomologyRestrictionMap_X₂_of_shortExact_of_isPrimeToCharacteristicTorsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/ShortExactExtension.lean, line 171. The attribute's comment: “prime-to-characteristic base change”.

Let p be a natural number and let i be a morphism of schemes. If the bijectivity of restriction along i for coefficients of torsion prime to p holds in every degree for the sub- and the quotient sheaf of a short exact sequence of abelian sheaves, then it holds for the middle sheaf.

theorem bijective_etaleCohomologyRestrictionMap_X₂_of_shortExact_of_isPrimeToCharacteristicTorsion
    (p : ℕ) (hS : S.ShortExact)
    (h₁ : Stacks.Torsion.IsPrimeToCharacteristicTorsion X.smallEtaleTopology p S.X₁ →
      ∀ q, Function.Bijective (etaleCohomologyRestrictionMap.{u, v, w} i S.X₁ q))
    (h₃ : Stacks.Torsion.IsPrimeToCharacteristicTorsion X.smallEtaleTopology p S.X₃ →
      ∀ q, Function.Bijective (etaleCohomologyRestrictionMap.{u, v, w} i S.X₃ q))
    (h₂ : Stacks.Torsion.IsPrimeToCharacteristicTorsion X.smallEtaleTopology p S.X₂) (q : ℕ) :
    Function.Bijective (etaleCohomologyRestrictionMap.{u, v, w} i S.X₂ q)

Stacks.EtaleCohomology.bijective_etaleCohomologyRestrictionMap_X₂_of_shortExact_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/ShortExactExtension.lean, line 187. The attribute's comment: “proper base change”.

Let π be a morphism from X to the spectrum of a field k and let i be a morphism of schemes. If the bijectivity of restriction along i when π is proper holds in every degree for the sub- and the quotient sheaf of a short exact sequence of abelian sheaves, then it holds for the middle sheaf.

theorem bijective_etaleCohomologyRestrictionMap_X₂_of_shortExact_of_isProper
    {k : Type u} [Field k] (π : X ⟶ Spec (.of k)) (hS : S.ShortExact)
    (h₁ : IsProper π → ∀ q, Function.Bijective (etaleCohomologyRestrictionMap.{u, v, w} i S.X₁ q))
    (h₃ : IsProper π → ∀ q, Function.Bijective (etaleCohomologyRestrictionMap.{u, v, w} i S.X₃ q))
    (hπ : IsProper π) (q : ℕ) :
    Function.Bijective (etaleCohomologyRestrictionMap.{u, v, w} i S.X₂ q)

Stacks.EtaleCohomology.surjective_etaleCohomologyRestrictionMap_X₂_of_shortExact_of_vanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/ShortExactExtension.lean, line 200. The attribute's comment: “restriction surjectivity”.

Let i be a morphism of schemes. If restriction along i is surjective in degree two for the sub- and the quotient sheaf of a short exact sequence of abelian sheaves, and the étale cohomology of the sub-sheaf vanishes above degree two, then restriction is surjective in degree two for the middle sheaf.

theorem surjective_etaleCohomologyRestrictionMap_X₂_of_shortExact_of_vanishing (hS : S.ShortExact)
    (hvanishing : ∀ q : ℕ, 2 < q → Subsingleton (Sheaf.H.{w} S.X₁ q))
    (h₁ : Function.Surjective (etaleCohomologyRestrictionMap.{u, v, w} i S.X₁ 2))
    (h₃ : Function.Surjective (etaleCohomologyRestrictionMap.{u, v, w} i S.X₃ 2)) :
    Function.Surjective (etaleCohomologyRestrictionMap.{u, v, w} i S.X₂ 2)
Tag 0A5D, a lemma

Tag 0A5D in the Stacks Project.

Stacks.EtaleCohomology.CurveStatements.directImage_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/CurveStatementsFiniteDirectImageGeneral.lean, line 104. The attribute's comment: “all eight statements of 0A52 at once, at the coefficients AddCommGrpCat.{u+1}; only f finite and X Noetherian are used”.

Stacks Project, Lemma 0A5D. Let f : X ⟶ Y be a finite morphism of schemes over a field k, with X Noetherian, and let F be an abelian sheaf on X_étale. If statements (1) -- (8) of Situation 0A52 hold for F, they hold for f_* F.

theorem CurveStatements.directImage_of_isFinite [IsNoetherian X]
    [HasExt.{u + 1} (Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1})]
    [HasExt.{u + 1} (Sheaf Y.smallEtaleTopology AddCommGrpCat.{u + 1})]
    {F : Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1}}
    (h : CurveStatements.{u, 0, u + 1} (f ≫ π) F) :
    CurveStatements.{u, 0, u + 1} π ((etaleAbelianDirectImage.{u, 0} f).obj F)

Stacks.EtaleCohomology.curveCohomologyStatements_smallEtaleDirectImageAb, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/FiniteDirectImage.lean, line 303. The attribute's comment: “the eight statements of Situation 0A52 pass to a finite direct image, over the Leray comparison and over the transfer of the torsion and constructibility side conditions”.

Let f : X ⟶ Y be a finite morphism of schemes and let F be an abelian sheaf on the small étale site of X. If the eight statements of Situation 0A52 hold for F, relative to the structure morphism f ≫ π of X and to restriction along j, then they hold for the direct image f_* F, relative to the structure morphism π of Y and to restriction along i.

The input is the comparison c of the étale cohomology of F with that of f_* F, which for a finite morphism comes from the vanishing of the higher direct images and the Leray spectral sequence. Beyond it the proof needs that the side conditions of the eight statements move between the two sheaves. The two conditions on the scheme move by finiteness of f: an affine Y forces an affine X, and a proper π forces a proper f ≫ π. The three conditions on the coefficient sheaf are carried: hprimePower and hprimeToChar for the two torsion conditions and hconstructible for constructibility, each in the direction from f_* F to F, which for a finite morphism holds because the stalks of f_* F are the sums of the stalks of F over the fibres.

theorem curveCohomologyStatements_smallEtaleDirectImageAb {k : Type u} [Field k]
    (π : Y ⟶ Spec (.of k)) (l p : ℕ) [IsFinite f]
    {constructibleSource : Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v} → Prop}
    {constructibleTarget : Sheaf Y.smallEtaleTopology AddCommGrpCat.{max (u + 1) v} → Prop}
    (c : DirectImageCohomologyComparison.{u, v, w} f i j F)
    (hprimePower : Stacks.Torsion.IsPrimePowerTorsion Y.smallEtaleTopology l
        ((smallEtaleDirectImageAb f).obj F) →
      Stacks.Torsion.IsPrimePowerTorsion X.smallEtaleTopology l F)
    (hprimeToChar : Stacks.Torsion.IsPrimeToCharacteristicTorsion Y.smallEtaleTopology p
        ((smallEtaleDirectImageAb f).obj F) →
      Stacks.Torsion.IsPrimeToCharacteristicTorsion X.smallEtaleTopology p F)
    (hconstructible : constructibleTarget ((smallEtaleDirectImageAb f).obj F) →
      constructibleSource F)
    (h : CurveCohomologyStatements.{u, v, w} j (f ≫ π) l p constructibleSource F) :
    CurveCohomologyStatements.{u, v, w} i π l p constructibleTarget
      ((smallEtaleDirectImageAb f).obj F)

Stacks.EtaleCohomology.curveCohomologyAssertions_smallEtaleDirectImageAb, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/FiniteDirectImageCurveAssertions.lean, line 498. The attribute's comment: “statements (1)-(8) of Situation 0A52 pass to f_* for finite f”.

Let k be a field, let f : X ⟶ Y be a finite morphism of schemes of finite type over k, and let F be an abelian sheaf on the small étale site of X. If statements (1) – (8) of Situation 0A52 hold for F, then they hold for f_* F.

Statements (1) – (8) are Stacks.EtaleCohomology.CurveCohomologyAssertions, read on X relative to its structure morphism f ≫ π and on Y relative to π, with constructibility read in a big étale site B containing both schemes. The remaining hypotheses of Situation 0A52 — that k is algebraically closed, that X and Y are separated of dimension at most one, and that F is torsion — are not assumed.

theorem curveCohomologyAssertions_smallEtaleDirectImageAb (π : Y ⟶ Spec (.of k))
    [LocallyOfFiniteType π] [QuasiCompact π] (f : X ⟶ Y) [IsFinite f]
    {F : Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1}}
    (h : CurveCohomologyAssertions B hX (f ≫ π) F) :
    CurveCohomologyAssertions B hY π ((smallEtaleDirectImageAb f).obj F)
Tag 0GJA, a lemma

Tag 0GJA in the Stacks Project.

Stacks.EtaleCohomology.curveStatements_iff_curveStatements_extensionByZero_of_dense, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/CurveCohomologyTheorem.lean, line 163. The attribute's comment: “for every torsion sheaf F, not only constructible ones”.

In Situation 0A52 let j : X' → X be the inclusion of a dense open subscheme. Then statements (1) -- (8) hold for F if and only if they hold for j_! j^{-1} F.

The source assumes F constructible; that is not needed here, both sides being true for every torsion F by Theorem 03SC (j_! j^{-1} F is a subsheaf of F, hence torsion). The direction from j_! j^{-1} F to F is the dense-open reduction of Stacks.EtaleCohomology.curveStatements_of_curveStatements_extensionByZero_of_dense.

theorem curveStatements_iff_curveStatements_extensionByZero_of_dense
    (F : Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})
    (hF : Stacks.Torsion.torsionSheafProperty X.smallEtaleTopology F) :
    CurveStatements.{u, v, w} π F ↔ CurveStatements.{u, v, w} π
      ((extensionByZero.{u, v} j).obj ((etaleRestriction.{u, v} j).obj F))
Tag 03SG, a lemma

Tag 03SG in the Stacks Project.

Stacks.EtaleCohomology.curveStatements_extensionByZero_zmod_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/SmoothExtensionByZeroCurveStatements.lean, line 66.

Stacks Project, Lemma 03SG. In Situation 0A52 — k algebraically closed, X separated, of finite type and of dimension at most one over k — assume X is smooth over k. Let j : U ⟶ X be an open immersion, ℓ a prime and F = j_! 𝐙/ℓ𝐙 the extension by zero of the constant sheaf on U_étale with value an abelian group E cyclic of order ℓ. Then statements (1) -- (8) of Situation 0A52 hold for F, in the sense of Stacks.EtaleCohomology.CurveStatements, at every coefficient universe and every Ext universe.

A smooth X over a field is reduced, so this is Lemma 0A3Q, curveStatements_extensionByZero_constantSheaf_of_prime.

theorem curveStatements_extensionByZero_zmod_of_smooth {k : Type u} [Field k] [IsAlgClosed k]
    {X U : Scheme.{u}} (π : X ⟶ Spec (.of k)) [IsSeparated π] [LocallyOfFiniteType π]
    [QuasiCompact π] [Smooth π] (hdim : topologicalKrullDim X ≤ 1) (j : U ⟶ X)
    [IsOpenImmersion j] {ℓ : ℕ} (hℓ : ℓ.Prime) (E : AddCommGrpCat.{max (u + 1) v})
    (hE : Nonempty (E ≃+ ZMod ℓ))
    [HasExt.{w} (Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})] :
    CurveStatements.{u, v, w} π ((extensionByZero.{u, v} j).obj
      ((constantSheaf U.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}).obj E))
Tag 0A3Q, a lemma

Tag 0A3Q in the Stacks Project.

Stacks.EtaleCohomology.curveStatements_extensionByZero_constantSheaf_of_prime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/ReducedExtensionByZeroStatements.lean, line 82.

Stacks Project, Lemma 0A3Q. In Situation 0A52 — k algebraically closed, X separated, of finite type and of dimension at most one over k — assume X is reduced. Let j : U → X be an open immersion, ℓ a prime, and F = j_! 𝐙/ℓ𝐙 the extension by zero of the constant sheaf on U_étale with value any abelian group E cyclic of order ℓ. Then statements (1) -- (8) of Situation 0A52 hold for F, in the sense of Stacks.EtaleCohomology.CurveStatements, at every coefficient universe and every Ext universe.

The sheaf F is killed by ℓ, hence torsion, so this is the reduction theorem curveStatements_of_torsionSheafProperty_max applied with Lemma 0A5B on smooth curves (curveStatementsConstantOnSmoothCurves_of_prime).

theorem curveStatements_extensionByZero_constantSheaf_of_prime {k : Type u} [Field k]
    [IsAlgClosed k] {X U : Scheme.{u}} (π : X ⟶ Spec (.of k)) [IsSeparated π]
    [LocallyOfFiniteType π] [QuasiCompact π] [IsReduced X] (hdim : topologicalKrullDim X ≤ 1)
    (j : U ⟶ X) [IsOpenImmersion j] {ℓ : ℕ} (hℓ : ℓ.Prime) (E : AddCommGrpCat.{max (u + 1) v})
    (hE : Nonempty (E ≃+ ZMod ℓ))
    [HasExt.{w} (Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})] :
    CurveStatements.{u, v, w} π ((extensionByZero.{u, v} j).obj
      ((constantSheaf U.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}).obj E))
Tag 03SD, a lemma

Tag 03SD in the Stacks Project.

Stacks.EtaleCohomology.curveStatements_extensionByZero_forget₂_of_isFiniteLocallyConstant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/LocallyConstantCurveStatements.lean, line 63. References: SGA 4 XVI (5.2), “partial”.

Stacks Project, Lemma 03SD. In Situation 0A52 — k algebraically closed, X separated, of finite type and of dimension at most one over k — assume X is reduced. Let j : U ⟶ X be an open immersion with U connected, ℓ a prime and G a finite locally constant sheaf of F_ℓ-vector spaces (ZMod ℓ-modules) on U_étale. Then statements (1) -- (8) of Situation 0A52 (Stacks.EtaleCohomology.CurveStatements) hold for the abelian sheaf F = j_! G, at every coefficient universe and every Ext universe.

j_! G is killed by ℓ, hence torsion, so this is the reduction theorem curveStatements_of_torsionSheafProperty_max applied with Lemma 0A5B on smooth curves (curveStatementsConstantOnSmoothCurves_of_prime). The hypotheses that X is reduced, that U is connected and that G is finite locally constant are those of the source; the proof does not use them.

theorem curveStatements_extensionByZero_forget₂_of_isFiniteLocallyConstant {k : Type u}
    [Field k] [IsAlgClosed k] {X U : Scheme.{u}} (π : X ⟶ Spec (.of k)) [IsSeparated π]
    [LocallyOfFiniteType π] [QuasiCompact π] [IsReduced X] (hdim : topologicalKrullDim X ≤ 1)
    (j : U ⟶ X) [IsOpenImmersion j] [ConnectedSpace U] {ℓ : ℕ} (hℓ : ℓ.Prime)
    (G : Sheaf U.smallEtaleTopology (ModuleCat.{max (u + 1) v} (ZMod ℓ)))
    [Stacks.ConstantSheaf.IsFiniteLocallyConstant U.smallEtaleTopology G]
    [HasExt.{w} (Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})] :
    CurveStatements.{u, v, w} π ((extensionByZero.{u, v} j).obj
      ((sheafCompose U.smallEtaleTopology
        (forget₂ (ModuleCat.{max (u + 1) v} (ZMod ℓ)) AddCommGrpCat.{max (u + 1) v})).obj G))
Tag 03SC, a theorem

Tag 03SC in the Stacks Project.

Stacks.EtaleCohomology.torsionCurveAssertions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/ScalarExtensionColimit.lean, line 257. References: SGA 4 IX (5.7), “special case”; SGA 4 X (5.2), “special case”; SGA 4 XIV (1.2), “special case”; SGA 4½ Arcata (3.3.6); SGA 5 VI (2.2.1), “special case”.

Stacks Project, Tag 03SC. Let k be an algebraically closed field, let X be a separated scheme of finite type over k of dimension at most one, with structure morphism f, and let F be a torsion abelian sheaf on X_étale. Then 1. H^q(X, F) = 0 for q > 2; 2. H^q(X, F) = 0 for q > 1 if X is affine; 3. H^q(X, F) = 0 for q > 1 if char k = p > 0 and F is p-power torsion; 4. H^q(X, F) is finite if F is constructible and torsion prime to char k; 5. H^q(X, F) is finite if X is proper and F is constructible; 6. H^q(X, F) → H^q(X_{k'}, F|_{X_{k'}}) is an isomorphism for every extension k'/k of algebraically closed fields if F is torsion prime to char k; 7. the same map is an isomorphism if X is proper; 8. H^2(X, F) → H^2(U, F|_U) is surjective for every open U ⊂ X.

These are the fields of Stacks.EtaleCohomology.TorsionCurveAssertions (étale cohomology is CategoryTheory.Sheaf.H on Mathlib's small étale site, at coefficients AddCommGrpCat.{u + 1}). "Finite type" is LocallyOfFiniteType f together with QuasiCompact f; the dimension is the topological Krull dimension.

theorem torsionCurveAssertions {k : Type u} [Field k] [IsAlgClosed k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
    [HasExt.{u + 1} (Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1})]
    (hdim : topologicalKrullDim X ≤ 1) (F : Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1})
    (hF : Stacks.Torsion.torsionSheafProperty X.smallEtaleTopology F) :
    TorsionCurveAssertions f F
Tag 03RT, a theorem

Tag 03RT in the Stacks Project.

Stacks.EtaleCohomology.subsingleton_sheafH_of_three_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/NonseparatedCurveVanishing.lean, line 263. The attribute's comment: “H^q(X, F) = 0 for q ≥ 3”. References: SGA 4 XVII (5.2.8.1), “special case”; SGA 4½ Arcata (3.3.6), “more general”.

Stacks Project, Tag 03RT. Let X be a scheme of finite type and of dimension at most one over an algebraically closed field k, and let F be a torsion abelian sheaf on X_étale. Then H^q_étale(X, F) = 0 for every q ≥ 3.

No separatedness is assumed. The source's "dimension 1" is the case of equality of the bound topologicalKrullDim X ≤ 1.

theorem subsingleton_sheafH_of_three_le (q : ℕ) (hq : 3 ≤ q) :
    Subsingleton (Sheaf.H.{w} F q)

Stacks.EtaleCohomology.subsingleton_sheafH_two_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionSheavesCurves/NonseparatedCurveVanishing.lean, line 289. The attribute's comment: “H^2(X, F) = 0 if X is affine”. References: SGA 4½ Arcata (3.3.6), “(ii), degree q=2”.

Stacks Project, Tag 03RT. Let X be an affine scheme of finite type and of dimension at most one over an algebraically closed field k, and let F be a torsion abelian sheaf on X_étale. Then H^2_étale(X, F) = 0.

An affine scheme is separated over k, so this is Theorem 03SC (2), Tag 0A54.

theorem subsingleton_sheafH_two_of_isAffine [IsAffine X] : Subsingleton (Sheaf.H.{w} F 2)
Tag 0A5E, a lemma

Tag 0A5E in the Stacks Project.

Declarations registered for the tag:

Sources
LeanStacks.EtaleCohomology.TorsionSheafSituation · Stacks.EtaleCohomology.TorsionSheafSituation.isVanishingAboveDegreeTwo · Stacks.EtaleCohomology.IsVanishingAboveDegreeTwo · Stacks.EtaleCohomology.IsAffineVanishingAboveDegreeOne · Stacks.EtaleCohomology.TorsionSheafSituation.isAffineVanishingAboveDegreeOne · Stacks.EtaleCohomology.TorsionSheafSituation.isPrimePowerTorsionVanishing · Stacks.EtaleCohomology.IsPrimePowerTorsionVanishing · Stacks.EtaleCohomology.TorsionSheafSituation.finiteCohomologyOfPrimeToCharacteristic

Section59.84 Cohomology of torsion modules on curves#

Section 59.84 of the Stacks Project, Tag 0GJB. 9 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0GJC, a lemma

Tag 0GJC in the Stacks Project.

Stacks.EtaleCohomology.TorsionModules.module_finite_etaleCohomology_constantSheaf_of_coprime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionModules/CurveConstantCoefficientsFinite.lean, line 103. The attribute's comment: “part (1): n prime to char(k)”.

Stacks Project, Tag 0GJC, part (1). Let Λ be a Noetherian ring, M a finite Λ-module annihilated by an integer n > 0, k an algebraically closed field and X a separated scheme of finite type over k of dimension at most one. If n is prime to the characteristic of k, then H^q(X, M̲) is a finite Λ-module for every q.

Here X is a scheme with a separated, locally of finite type and quasi-compact structure morphism π : X ⟶ Spec k, the dimension is the Krull dimension of the underlying space, M̲ is the constant sheaf of Λ-modules on X_étale and H^q(X, M̲) is the q-th right derived functor of global sections of sheaves of Λ-modules on X_étale. "Prime to the characteristic" is read with the exponential characteristic, so that it is no condition in characteristic zero.

The proof is the source's (module_finite_etaleCohomology_constantSheaf), with the input Tag 03SC supplied by curveTorsionCohomologyStatement_holds.

theorem module_finite_etaleCohomology_constantSheaf_of_coprime
    {k : Type u} [Field k] [IsAlgClosed k] {X : Scheme.{u}} (π : X ⟶ Spec (.of k))
    [IsSeparated π] [LocallyOfFiniteType π] [QuasiCompact π] (hX : topologicalKrullDim X ≤ 1)
    (M : ModuleCat.{max (u + 1) r} Λ) [Module.Finite Λ M] (n : ℕ) (hn : 0 < n)
    (hM : ∀ m : M, n • m = 0) (hnk : n.Coprime (ringExpChar k)) (q : ℕ) :
    Module.Finite Λ (((etaleModuleGlobalSections.{u, r} Λ X).rightDerived q).obj
      ((constantSheaf X.smallEtaleTopology (ModuleCat.{max (u + 1) r} Λ)).obj M))

Stacks.EtaleCohomology.TorsionModules.module_finite_etaleCohomology_constantSheaf_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionModules/CurveConstantCoefficientsFinite.lean, line 126. The attribute's comment: “part (2): X proper over k”.

Stacks Project, Tag 0GJC, part (2). Let Λ be a Noetherian ring, M a finite Λ-module annihilated by an integer n > 0, k an algebraically closed field and X a separated scheme of finite type over k of dimension at most one. If X is proper over k, then H^q(X, M̲) is a finite Λ-module for every q.

Here X is a scheme with a separated, locally of finite type and quasi-compact structure morphism π : X ⟶ Spec k, the dimension is the Krull dimension of the underlying space, M̲ is the constant sheaf of Λ-modules on X_étale and H^q(X, M̲) is the q-th right derived functor of global sections of sheaves of Λ-modules on X_étale.

The proof is the source's (module_finite_etaleCohomology_constantSheaf), with the input Tag 03SC supplied by curveTorsionCohomologyStatement_holds.

theorem module_finite_etaleCohomology_constantSheaf_of_isProper
    {k : Type u} [Field k] [IsAlgClosed k] {X : Scheme.{u}} (π : X ⟶ Spec (.of k))
    [IsSeparated π] [LocallyOfFiniteType π] [QuasiCompact π] [IsProper π]
    (hX : topologicalKrullDim X ≤ 1) (M : ModuleCat.{max (u + 1) r} Λ) [Module.Finite Λ M]
    (n : ℕ) (hn : 0 < n) (hM : ∀ m : M, n • m = 0) (q : ℕ) :
    Module.Finite Λ (((etaleModuleGlobalSections.{u, r} Λ X).rightDerived q).obj
      ((constantSheaf X.smallEtaleTopology (ModuleCat.{max (u + 1) r} Λ)).obj M))

Stacks.EtaleCohomology.TorsionModules.finite_etaleCohomology_constantSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionModules/CurveTorsionStatementsHold.lean, line 62. The attribute's comment: “both parts: n prime to char(k), or X proper”.

Stacks Project, Tag 0GJC. Let Λ be a Noetherian ring, M a finite Λ-module annihilated by an integer n > 0, k an algebraically closed field and X a separated scheme of finite type over k of dimension at most one. Then H^q_étale(X, M̲) is a finite Λ-module for every q

  1. if n is prime to the characteristic of k, and
  2. if X is proper over k.

The two parts are the two sides of the disjunction n.Coprime (ringExpChar k) ∨ IsProper π; the exponential characteristic makes the coprimality condition vacuous in characteristic zero, as in the source. This is Stacks.EtaleCohomology.TorsionModules.module_finite_etaleCohomology_constantSheaf with its input, the statement of Tag 03SC, discharged by Stacks.EtaleCohomology.curveTorsionCohomologyStatement_holds.

theorem finite_etaleCohomology_constantSheaf
    {k : Type u} [Field k] [IsAlgClosed k] {X : Scheme.{u}} (π : X ⟶ Spec (.of k))
    [IsSeparated π] [LocallyOfFiniteType π] [QuasiCompact π] (hX : topologicalKrullDim X ≤ 1)
    (M : ModuleCat.{max (u + 1) r} Λ) [Module.Finite Λ M] (n : ℕ) (hn : 0 < n)
    (hM : ∀ m : M, n • m = 0) (hnp : n.Coprime (ringExpChar k) ∨ IsProper π) (q : ℕ) :
    Module.Finite Λ (((etaleModuleGlobalSections.{u, r} Λ X).rightDerived q).obj
      ((constantSheaf X.smallEtaleTopology (ModuleCat.{max (u + 1) r} Λ)).obj M))
Tag 0GJD, a lemma

Tag 0GJD in the Stacks Project.

Stacks.EtaleCohomology.TorsionModules.module_finite_cohomology_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionModulesCurves/FinitePushforward.lean, line 227. The attribute's comment: “granted Tag 03QP for sheaves of Λ-modules, as the hypothesis h03QP”.

Stacks Project, Tag 0GJD, granted Tag 03QP for sheaves of Λ-modules as the hypothesis h03QP.

Let Λ be a ring, let f : X ⟶ Y be a morphism of a big étale site whose underlying morphism of schemes is finite, and let ℱ be a sheaf of Λ-modules on the small étale site of X. If H^q_étale(X, ℱ) is a finite Λ-module, then so is H^q_étale(Y, f_*ℱ).

The hypothesis h03QP is the general statement of part (2) of Stacks 03QP for sheaves of Λ-modules: for every morphism of the big étale site with finite underlying morphism of schemes, every sheaf of Λ-modules on its source and every positive degree, the higher direct image vanishes. It is a different tag from the one being proved, it quantifies over all of its own inputs, and it is instantiated only inside the proof, at f and ℱ. Nothing about H^q_étale(Y, f_*ℱ) — the conclusion — is assumed.

The remaining hypotheses of the source statement (Λ Noetherian, k algebraically closed, X and Y separated of finite type over k of dimension at most one) are not needed: the source's proof does not use them, and neither does this one.

theorem module_finite_cohomology_pushforward
    [∀ Z : B.Scheme,
      HasSheafify (SmallEtale.topology B Z.obj Z.property) (ModuleCat.{max (u + 1) w} Λ)]
    [∀ Z : B.Scheme, HasInjectiveResolutions
      (Sheaf (SmallEtale.topology B Z.obj Z.property) (ModuleCat.{max (u + 1) w} Λ))]
    [∀ (Z W : B.Scheme) (g : Z ⟶ W), (modulePushforward.{u, w} B Λ g).IsRightAdjoint]
    (h03QP : ∀ (Z W : B.Scheme) (g : Z ⟶ W), IsFinite (B.inclusion.map g) →
      ∀ (𝒢 : Sheaf (SmallEtale.topology B Z.obj Z.property) (ModuleCat.{max (u + 1) w} Λ))
        (q : ℕ), 0 < q → IsZero (((modulePushforward.{u, w} B Λ g).rightDerived q).obj 𝒢))
    (hf : IsFinite (B.inclusion.map f))
    (ℱ : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{max (u + 1) w} Λ))
    (q : ℕ)
    (hfin : Module.Finite Λ (((moduleGlobalSections.{u, w} B Λ X).rightDerived q).obj ℱ)) :
    Module.Finite Λ (((moduleGlobalSections.{u, w} B Λ Y).rightDerived q).obj
      ((modulePushforward.{u, w} B Λ f).obj ℱ))

Stacks.EtaleCohomology.TorsionModules.module_finite_cohomology_pushforward_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionModulesCurves/FinitePushforwardAcyclic.lean, line 179. The attribute's comment: “stated for an arbitrary ring Λ and an arbitrary finite morphism f of the big étale site; the source's further hypotheses (Λ Noetherian, k algebraically closed, X and Y separated of finite type over k of dimension at most one) are unused by its proof and dropped”.

Stacks Project, Tag 0GJD. Let Λ be a ring, let f : X ⟶ Y be a morphism of a big étale site whose underlying morphism of schemes is finite, and let ℱ be a sheaf of Λ-modules on the small étale site of X. If H^q_étale(X, ℱ) is a finite Λ-module, then so is H^q_étale(Y, f_*ℱ).

The source states this for Λ Noetherian, k an algebraically closed field and f a finite morphism of separated schemes of finite type over k of dimension at most one. None of that is used by the source's proof, and none of it is assumed here: the source's statement is the special case in which those hypotheses hold. The proof is the source's: the higher direct images of f vanish (isZero_rightDerived_modulePushforward_of_isIntegralHom, Stacks 03QP), so the Leray spectral sequence collapses to H^q_étale(X, ℱ) ≅ H^q_étale(Y, f_*ℱ) (moduleCohomologyPushforwardIso, Stacks 0733), and finiteness transports along it.

theorem module_finite_cohomology_pushforward_of_isFinite [IsFinite (B.inclusion.map f)]
    (ℱ : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{max (u + 1) w r} Λ))
    (q : ℕ)
    (hfin : Module.Finite Λ
      (((moduleGlobalSections.{u, max w r} B Λ X).rightDerived q).obj ℱ)) :
    Module.Finite Λ (((moduleGlobalSections.{u, max w r} B Λ Y).rightDerived q).obj
      ((modulePushforward.{u, max w r} B Λ f).obj ℱ))
Tag 0GJE, a lemma

Tag 0GJE in the Stacks Project.

Stacks.EtaleCohomology.TorsionModules.module_finite_cohomology_iff_extensionByZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionModulesCurves/RestrictToDenseOpen.lean, line 261. The attribute's comment: “granted 095L for Λ-module sheaves as h095L; closed part's cohomology as h0, hpos”.

Stacks Project, Tag 0GJE, granted Tag 095L for sheaves of Λ-modules as the hypothesis h095L, and the cohomology of i_*i^{-1}ℱ as the hypotheses h0 and hpos.

Let Λ be a Noetherian ring, let X be a scheme, let j : X' ⟶ X be an open immersion and let i : Z ⟶ X be a closed immersion whose image is the complement of the image of j. Let ℱ be a sheaf of Λ-modules on X_étale. If H^0_étale(X, i_*i^{-1}ℱ) is a finite Λ-module and H^q_étale(X, i_*i^{-1}ℱ) = 0 for q > 0, then for every q

H^q_étale(X, ℱ) is a finite Λ-module ↔ H^q_étale(X, j_!j^{-1}ℱ) is a finite Λ-module.

The hypothesis h095L is the general statement of Tag 095L for sheaves of Λ-modules: for every scheme, every closed immersion into it, every open immersion onto the complement and every sheaf of Λ-modules, the localization short complex exists and is short exact. It is a different tag, it quantifies over all of its own inputs, it is instantiated only inside the proof, and it says nothing about cohomology or finiteness.

The hypotheses h0 and hpos are not a Stacks tag. They are the cohomological consequence of the geometric hypotheses of the source — X separated of finite type of dimension at most one over an algebraically closed field, X' dense, ℱ constructible — and are the part of Tag 0GJE this declaration does not prove; see the implementation notes of this file for the chain of four absent results they stand in for. They concern i_*i^{-1}ℱ only, and so are independent of the conclusion, which concerns ℱ and j_!j^{-1}ℱ.

theorem module_finite_cohomology_iff_extensionByZero
    {X Z X' : Scheme.{u}} (i : Z ⟶ X) (j : X' ⟶ X) [IsClosedImmersion i] [IsOpenImmersion j]
    (hij : Set.range j.base = (Set.range i.base)ᶜ)
    (h095L : ∀ {W Z' U' : Scheme.{u}} (i' : Z' ⟶ W) (j' : U' ⟶ W) [IsClosedImmersion i']
        [IsOpenImmersion j'], Set.range j'.base = (Set.range i'.base)ᶜ →
      ∀ 𝒢 : Sheaf W.smallEtaleTopology (ModuleCat.{max (u + 1) w r} Λ),
        ∃ hz : (moduleExtensionByZeroAdj.{u, w, r} Λ j').counit.app 𝒢 ≫
            (moduleInverseImageDirectImageAdj.{u, w, r} Λ i').unit.app 𝒢 = 0,
          (openClosedModuleShortComplex.{u, w, r} Λ i' j' 𝒢 hz).ShortExact)
    (ℱ : Sheaf X.smallEtaleTopology (ModuleCat.{max (u + 1) w r} Λ))
    (h0 : Module.Finite Λ ((moduleEtaleCohomology.{u, w, r} Λ X 0).obj
      ((moduleDirectImage.{u, w, r} Λ i).obj ((moduleInverseImage.{u, w, r} Λ i).obj ℱ))))
    (hpos : ∀ q, 0 < q → IsZero ((moduleEtaleCohomology.{u, w, r} Λ X q).obj
      ((moduleDirectImage.{u, w, r} Λ i).obj ((moduleInverseImage.{u, w, r} Λ i).obj ℱ))))
    (q : ℕ) :
    Module.Finite Λ ((moduleEtaleCohomology.{u, w, r} Λ X q).obj ℱ) ↔
      Module.Finite Λ ((moduleEtaleCohomology.{u, w, r} Λ X q).obj
        ((moduleExtensionByZero.{u, w, r} Λ j).obj
          ((moduleRestriction.{u, w, r} Λ j).obj ℱ)))

Stacks.EtaleCohomology.TorsionModules.module_finite_cohomology_iff_extensionByZero_of_dense, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionModulesCurves/RestrictToDenseOpenCurve.lean, line 125.

Stacks Project, Tag 0GJE. Let Λ be a Noetherian ring, k an algebraically closed field, X a separated scheme of finite type over k of dimension at most one, ℱ a constructible sheaf of Λ-modules on X_étale, and j : X' ⟶ X the inclusion of a dense open subscheme. Then H^q_étale(X, ℱ) is a finite Λ-module if and only if H^q_étale(X, j_!j^{-1}ℱ) is a finite Λ-module.

theorem module_finite_cohomology_iff_extensionByZero_of_dense
    (B : BigEtaleSite.{u}) (Λ : Type r) [CommRing Λ] [IsNoetherianRing Λ]
    {k : Type u} [Field k] [IsAlgClosed k]
    (X : B.Scheme) (p : X.obj ⟶ Spec (CommRingCat.of k))
    [IsSeparated p] [LocallyOfFiniteType p] [QuasiCompact p]
    (hdim : topologicalKrullDim X.obj ≤ 1)
    (ℱ : Sheaf X.obj.smallEtaleTopology (ModuleCat.{max (u + 1) r} Λ))
    (hℱ : IsConstructibleEtaleSiteModuleSheaf B X Λ ℱ)
    {X' : Scheme.{u}} (j : X' ⟶ X.obj) [IsOpenImmersion j]
    (hdense : Dense (Set.range j.base)) (q : ℕ) :
    Module.Finite Λ ((moduleEtaleCohomology.{u, r, r} Λ X.obj q).obj ℱ) ↔
      Module.Finite Λ ((moduleEtaleCohomology.{u, r, r} Λ X.obj q).obj
        ((moduleExtensionByZero.{u, r, r} Λ j).obj
          ((moduleRestriction.{u, r, r} Λ j).obj ℱ)))
Tag 0GJF, a lemma

Tag 0GJF in the Stacks Project.

Stacks.EtaleCohomology.TorsionModules.module_finite_cohomology_extensionByZero_of_coprime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionModulesCurves/FiniteCohomologyUnconditional.lean, line 86. The attribute's comment: “part (1): n prime to char(k)”.

Stacks Project, Tag 0GJF, part (1). Let Λ be a Noetherian ring, let M be a finite Λ-module annihilated by an integer n > 0, let k be an algebraically closed field, let X be a separated scheme of finite type over k of dimension at most one, and let j : U ⟶ X be an open immersion. If n is prime to the characteristic of k, then H^q_étale(X, j_!M̲) is a finite Λ-module for every q.

Here X is a scheme with a separated, locally of finite type and quasi-compact structure morphism π : X ⟶ Spec k, the dimension is the Krull dimension of the underlying space, M̲ is the constant sheaf of Λ-modules on U_étale, j_! is extension by zero and H^q is the q-th right derived functor of global sections of sheaves of Λ-modules on X_étale. "Prime to the characteristic" is read with the exponential characteristic, so that it is no condition in characteristic zero.

theorem module_finite_cohomology_extensionByZero_of_coprime
    {k : Type u} [Field k] [IsAlgClosed k] {X : Scheme.{u}} (π : X ⟶ Spec (.of k))
    [IsSeparated π] [LocallyOfFiniteType π] [QuasiCompact π] (hX : topologicalKrullDim X ≤ 1)
    (M : ModuleCat.{max (u + 1) r} Λ) [Module.Finite Λ M] (n : ℕ) (hn : 0 < n)
    (hM : ∀ m : M, n • m = 0) (hnk : n.Coprime (ringExpChar k))
    {U : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j] (q : ℕ) :
    Module.Finite Λ (((etaleModuleGlobalSections.{u, r} Λ X).rightDerived q).obj
      ((etaleModuleExtensionByZero.{u, r} Λ j).obj
        ((constantSheaf U.smallEtaleTopology (ModuleCat.{max (u + 1) r} Λ)).obj M)))

Stacks.EtaleCohomology.TorsionModules.module_finite_cohomology_extensionByZero_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionModulesCurves/FiniteCohomologyUnconditional.lean, line 114. The attribute's comment: “part (2): X proper over k”.

Stacks Project, Tag 0GJF, part (2). Let Λ be a Noetherian ring, let M be a finite Λ-module annihilated by an integer n > 0, let k be an algebraically closed field, let X be a separated scheme of finite type over k of dimension at most one, and let j : U ⟶ X be an open immersion. If X is proper over k, then H^q_étale(X, j_!M̲) is a finite Λ-module for every q.

Here X is a scheme with a separated, locally of finite type and quasi-compact structure morphism π : X ⟶ Spec k, the dimension is the Krull dimension of the underlying space, M̲ is the constant sheaf of Λ-modules on U_étale, j_! is extension by zero and H^q is the q-th right derived functor of global sections of sheaves of Λ-modules on X_étale.

theorem module_finite_cohomology_extensionByZero_of_isProper
    {k : Type u} [Field k] [IsAlgClosed k] {X : Scheme.{u}} (π : X ⟶ Spec (.of k))
    [IsSeparated π] [LocallyOfFiniteType π] [QuasiCompact π] [IsProper π]
    (hX : topologicalKrullDim X ≤ 1) (M : ModuleCat.{max (u + 1) r} Λ) [Module.Finite Λ M]
    (n : ℕ) (hn : 0 < n) (hM : ∀ m : M, n • m = 0)
    {U : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j] (q : ℕ) :
    Module.Finite Λ (((etaleModuleGlobalSections.{u, r} Λ X).rightDerived q).obj
      ((etaleModuleExtensionByZero.{u, r} Λ j).obj
        ((constantSheaf U.smallEtaleTopology (ModuleCat.{max (u + 1) r} Λ)).obj M)))
Tag 0GJG, a lemma

Tag 0GJG in the Stacks Project.

Stacks.Cohomology.module_finite_cohomology_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/Modules/FiniteCohomologyOfShortExact.lean, line 52.

Stacks Project, Tag 0GJG. In a short exact sequence of coefficient sheaves, the middle sheaf has finite cohomology in degree q if both outer sheaves do.

public theorem module_finite_cohomology_of_shortExact
    {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
    (Λ : Type r) [CommRing Λ] [IsNoetherianRing Λ]
    [HasSheafify J (ModuleCat.{w} Λ)]
    [HasInjectiveResolutions (Sheaf J (ModuleCat.{w} Λ))]
    [HasGlobalSectionsFunctor J (ModuleCat.{w} Λ)]
    [(Sheaf.Γ J (ModuleCat.{w} Λ)).Additive]
    (S : ShortComplex (Sheaf J (ModuleCat.{w} Λ))) (hS : S.ShortExact)
    (q : ℕ)
    (h₁ : Module.Finite Λ (((Sheaf.Γ J (ModuleCat.{w} Λ)).rightDerived q).obj S.X₁))
    (h₃ : Module.Finite Λ (((Sheaf.Γ J (ModuleCat.{w} Λ)).rightDerived q).obj S.X₃)) :
    Module.Finite Λ (((Sheaf.Γ J (ModuleCat.{w} Λ)).rightDerived q).obj S.X₂)
Tag 0GJH, a lemma

Tag 0GJH in the Stacks Project.

Stacks.EtaleCohomology.TorsionModules.module_finite_cohomology_extensionByZero_of_isFiniteTypeLocallyConstant_of_coprime, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionModulesCurves/LocallyConstantCoefficients/FiniteCohomologyExtensionByZero.lean, line 300. The attribute's comment: “part (1): ℓ prime to char(k)”.

Stacks Project, Tag 0GJH, part (1). Let Λ be a Noetherian ring, let k be an algebraically closed field, let X be a separated scheme of finite type over k of dimension at most one, let j : U ⟶ X be an open immersion with U connected, let ℓ be a prime number prime to the characteristic of k, let n > 0 and let 𝒢 be a finite type, locally constant sheaf of Λ-modules on U_étale annihilated by ℓ ^ n. Then H^q_étale(X, j_! 𝒢) is a finite Λ-module for every q.

"Separated of finite type over k" is IsSeparated π, LocallyOfFiniteType π and QuasiCompact π for the structure morphism π : X ⟶ Spec k, and "of dimension at most one" is topologicalKrullDim X ≤ 1. "Prime to the characteristic" is read with the exponential characteristic, so it is no condition in characteristic zero. H^q_étale(X, -) is the q-th right derived functor of global sections of sheaves of Λ-modules on X_étale. The connectedness of U is a hypothesis of the source and is kept; the proof does not use it.

theorem module_finite_cohomology_extensionByZero_of_isFiniteTypeLocallyConstant_of_coprime
    {k : Type u} [Field k] [IsAlgClosed k] {X : Scheme.{u}} (π : X ⟶ Spec (.of k))
    [IsSeparated π] [LocallyOfFiniteType π] [QuasiCompact π]
    (hX : topologicalKrullDim X ≤ 1) {U : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
    [ConnectedSpace U] {ℓ n : ℕ} (hℓ : ℓ.Prime) (hn : 0 < n) (hℓk : ℓ.Coprime (ringExpChar k))
    (G : EtaleModules.{u, r} Λ U)
    (hG : Stacks.ConstantSheaf.IsFiniteTypeLocallyConstantModuleSheaf.{u, u + 1, r}
      U.smallEtaleTopology Λ G)
    (hGn : ℓ ^ n • 𝟙 G = 0) (q : ℕ) :
    Module.Finite Λ (((etaleModuleGlobalSections.{u, r} Λ X).rightDerived q).obj
      ((etaleModuleExtensionByZero.{u, r} Λ j).obj G))

Stacks.EtaleCohomology.TorsionModules.module_finite_cohomology_extensionByZero_of_isFiniteTypeLocallyConstant_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionModulesCurves/LocallyConstantCoefficients/FiniteCohomologyExtensionByZero.lean, line 325. The attribute's comment: “part (2): X proper over k”.

Stacks Project, Tag 0GJH, part (2). Let Λ be a Noetherian ring, let k be an algebraically closed field, let X be a proper scheme over k of dimension at most one (proper implies separated and of finite type), let j : U ⟶ X be an open immersion with U connected, let ℓ be a prime number, let n > 0 and let 𝒢 be a finite type, locally constant sheaf of Λ-modules on U_étale annihilated by ℓ ^ n. Then H^q_étale(X, j_! 𝒢) is a finite Λ-module for every q.

The encoding is that of part (1), module_finite_cohomology_extensionByZero_of_isFiniteTypeLocallyConstant_of_coprime, with the coprimality hypothesis replaced by IsProper π.

theorem module_finite_cohomology_extensionByZero_of_isFiniteTypeLocallyConstant_of_isProper
    {k : Type u} [Field k] [IsAlgClosed k] {X : Scheme.{u}} (π : X ⟶ Spec (.of k))
    [IsSeparated π] [LocallyOfFiniteType π] [QuasiCompact π] [IsProper π]
    (hX : topologicalKrullDim X ≤ 1) {U : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
    [ConnectedSpace U] {ℓ n : ℕ} (hℓ : ℓ.Prime) (hn : 0 < n) (G : EtaleModules.{u, r} Λ U)
    (hG : Stacks.ConstantSheaf.IsFiniteTypeLocallyConstantModuleSheaf.{u, u + 1, r}
      U.smallEtaleTopology Λ G)
    (hGn : ℓ ^ n • 𝟙 G = 0) (q : ℕ) :
    Module.Finite Λ (((etaleModuleGlobalSections.{u, r} Λ X).rightDerived q).obj
      ((etaleModuleExtensionByZero.{u, r} Λ j).obj G))
Tag 0GJI, a theorem

Tag 0GJI in the Stacks Project.

Stacks.EtaleCohomology.TorsionModules.module_finite_etaleCohomology_of_isPrimeToCharacteristicTorsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionModules/ConstructibleCurveCohomology.lean, line 585. The attribute's comment: “part (1): F torsion prime to char(k)”. References: SGA 5 VI (3.1), “partial”.

Stacks Project, Tag 0GJI, part (1) (Tag 0GJJ). Let Λ be a Noetherian ring, k an algebraically closed field, X a separated scheme of finite type over k of dimension at most one, and F a constructible sheaf of Λ-modules on X_étale which is torsion prime to the characteristic of k. Then H^q_étale(X, F) is a finite Λ-module for every q.

"Torsion prime to char(k)" is Stacks.Torsion.IsPrimeToCharacteristicTorsion of the underlying abelian sheaf at the exponential characteristic of k: every local section is, locally, killed by a positive integer prime to it. It implies that F is torsion, and in characteristic zero it is exactly that. Constructibility is Stacks.EtaleCohomology.IsBigSiteConstructibleEtaleModule (Tag 03RW (3), read on the small étale site of Tag 021B of a big étale site B containing X).

theorem module_finite_etaleCohomology_of_isPrimeToCharacteristicTorsion
    (F : EtaleModules.{u, r} Λ X.obj) (hc : IsBigSiteConstructibleEtaleModule B X Λ F)
    (ht : Stacks.Torsion.IsPrimeToCharacteristicTorsion X.obj.smallEtaleTopology (ringExpChar k)
      ((etaleModuleForgetAb.{u, r} Λ X.obj).obj F)) (q : ℕ) :
    Module.Finite Λ
      (((Sheaf.Γ X.obj.smallEtaleTopology (ModuleCat.{max (u + 1) r} Λ)).rightDerived q).obj F)

Stacks.EtaleCohomology.TorsionModules.module_finite_etaleCohomology_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionModules/ConstructibleCurveCohomology.lean, line 603. The attribute's comment: “part (2): X proper”.

Stacks Project, Tag 0GJI, part (2) (Tag 0GJK). Let Λ be a Noetherian ring, k an algebraically closed field, X a proper scheme over k of dimension at most one, and F a constructible sheaf of Λ-modules on X_étale which is torsion. Then H^q_étale(X, F) is a finite Λ-module for every q.

Torsion is Stacks.EtaleCohomology.IsTorsionEtaleModule: every local section is, locally, killed by a positive integer.

theorem module_finite_etaleCohomology_of_isProper [IsProper π]
    (F : EtaleModules.{u, r} Λ X.obj) (hc : IsBigSiteConstructibleEtaleModule B X Λ F)
    (ht : IsTorsionEtaleModule.{u, r} Λ X.obj F) (q : ℕ) :
    Module.Finite Λ
      (((Sheaf.Γ X.obj.smallEtaleTopology (ModuleCat.{max (u + 1) r} Λ)).rightDerived q).obj F)
Tag 0GJJ, an item

Tag 0GJJ in the Stacks Project.

Stacks.EtaleCohomology.TorsionModules.module_finite_etaleCohomology_of_isPrimeToCharacteristicTorsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionModules/ConstructibleCurveCohomology.lean, line 585. References: SGA 5 VI (3.1), “partial”.

Stacks Project, Tag 0GJI, part (1) (Tag 0GJJ). Let Λ be a Noetherian ring, k an algebraically closed field, X a separated scheme of finite type over k of dimension at most one, and F a constructible sheaf of Λ-modules on X_étale which is torsion prime to the characteristic of k. Then H^q_étale(X, F) is a finite Λ-module for every q.

"Torsion prime to char(k)" is Stacks.Torsion.IsPrimeToCharacteristicTorsion of the underlying abelian sheaf at the exponential characteristic of k: every local section is, locally, killed by a positive integer prime to it. It implies that F is torsion, and in characteristic zero it is exactly that. Constructibility is Stacks.EtaleCohomology.IsBigSiteConstructibleEtaleModule (Tag 03RW (3), read on the small étale site of Tag 021B of a big étale site B containing X).

theorem module_finite_etaleCohomology_of_isPrimeToCharacteristicTorsion
    (F : EtaleModules.{u, r} Λ X.obj) (hc : IsBigSiteConstructibleEtaleModule B X Λ F)
    (ht : Stacks.Torsion.IsPrimeToCharacteristicTorsion X.obj.smallEtaleTopology (ringExpChar k)
      ((etaleModuleForgetAb.{u, r} Λ X.obj).obj F)) (q : ℕ) :
    Module.Finite Λ
      (((Sheaf.Γ X.obj.smallEtaleTopology (ModuleCat.{max (u + 1) r} Λ)).rightDerived q).obj F)
Tag 0GJK, an item

Tag 0GJK in the Stacks Project.

Stacks.EtaleCohomology.TorsionModules.module_finite_etaleCohomology_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionModules/ConstructibleCurveCohomology.lean, line 603.

Stacks Project, Tag 0GJI, part (2) (Tag 0GJK). Let Λ be a Noetherian ring, k an algebraically closed field, X a proper scheme over k of dimension at most one, and F a constructible sheaf of Λ-modules on X_étale which is torsion. Then H^q_étale(X, F) is a finite Λ-module for every q.

Torsion is Stacks.EtaleCohomology.IsTorsionEtaleModule: every local section is, locally, killed by a positive integer.

theorem module_finite_etaleCohomology_of_isProper [IsProper π]
    (F : EtaleModules.{u, r} Λ X.obj) (hc : IsBigSiteConstructibleEtaleModule B X Λ F)
    (ht : IsTorsionEtaleModule.{u, r} Λ X.obj F) (q : ℕ) :
    Module.Finite Λ
      (((Sheaf.Γ X.obj.smallEtaleTopology (ModuleCat.{max (u + 1) r} Λ)).rightDerived q).obj F)
Sources
LeanStacks.EtaleCohomology.TorsionModules.module_finite_etaleCohomology_constantSheaf_of_coprime · Stacks.EtaleCohomology.TorsionModules.module_finite_etaleCohomology_constantSheaf_of_isProper · Stacks.EtaleCohomology.TorsionModules.finite_etaleCohomology_constantSheaf · Stacks.EtaleCohomology.TorsionModules.module_finite_cohomology_pushforward · Stacks.EtaleCohomology.TorsionModules.module_finite_cohomology_pushforward_of_isFinite · Stacks.EtaleCohomology.TorsionModules.module_finite_cohomology_iff_extensionByZero · Stacks.EtaleCohomology.TorsionModules.module_finite_cohomology_iff_extensionByZero_of_dense · Stacks.EtaleCohomology.TorsionModules.module_finite_cohomology_extensionByZero_of_coprime

Section59.85 First cohomology of proper schemes#

Section 59.85 of the Stacks Project, Tag 0A5F. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0A5G, a lemma

Tag 0A5G in the Stacks Project.

Stacks.EtaleCohomology.bijective_etaleConstantCohomologyRestriction_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ProperHenselianFirstCohomology.lean, line 268. The attribute's comment: “the reduction of the tag to an Ext computation, in every degree q: the canonical map H^q(X, M) -> H^q(X_0, M) is bijective if and only if etale inverse image along the closed-fibre inclusion is bijective on Ext^q out of the constant sheaf Z. The geometric content of the tag -- that this holds in degree one for a proper morphism over a henselian local ring -- is not proved here. The inputs the source's degree-one argument needs ARE available: Stacks 03AJ as Stacks.Cohomology.Torsors.torsorIsoClassesEquivH1, Stacks 03RV as AlgebraicGeometry.finiteLocallyConstantFiniteEtaleEquivalence, and Stacks 0A48 as AlgebraicGeometry.isEquivalence_finiteEtaleBaseChange_of_isProper_of_henselianLocalRing. What is missing is the bridge between them: no result transports an Ext^1 or Sheaf.H map along a CHANGE OF SITE into torsor language -- torsorIsoClassesEquivH1_naturality is naturality in the coefficient sheaf on a fixed site -- and the restriction map here lives on Mathlib's Scheme.smallEtaleTopology while 03RV lives on SmallEtale.topology of a BigEtaleSite, with no comparison. Nor does anything say that a torsor under a finite constant sheaf is finite locally constant”.

Stacks 0A5G reduced to an Ext computation. Restriction to the closed fibre is bijective in degree q exactly when the étale inverse-image functor along the closed-fibre inclusion is bijective on Ext^q out of the constant sheaf ℤ: the two maps differ by composition with the two canonical constant-sheaf comparison isomorphisms, and composing with an isomorphism is bijective on Ext.

Nothing here is special to a proper morphism over a henselian local ring, and nothing here computes either side. What Stacks 0A5G asserts is that in degree one the right-hand side holds when A is henselian local, f is proper and M is finite; that is the geometric content, and it rests on Stacks 03AJ, 03RV, 0A48 and 0A0C.

theorem bijective_etaleConstantCohomologyRestriction_iff :
    Function.Bijective (etaleConstantCohomologyRestriction.{u, v, w} A f M q) ↔
      Function.Bijective
        ((etaleAbelianInverseImage.{u, v} (closedFibreInclusion A f)).mapExtAddHom.{w, w}
          ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}).obj
            (AddCommGrpCat.of (ULift ℤ)))
          (etaleConstantSheaf.{u, v} X M) q)

Stacks.EtaleCohomology.bijective_etaleConstantCohomologyRestriction_one_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ProperHenselianFirstCohomologyBijective.lean, line 370.

For A a henselian local ring, X proper over A and M a finite abelian group, restriction H¹(X, M) ⟶ H¹(X₀, M) to the closed fibre is bijective.

Surjectivity is surjective_etaleConstantCohomologyRestriction_one_of_isProper. Injectivity (Stacks.EtaleCohomology.injective_etaleCohomologyRestrictionMap_constantSheaf_one): a class on X dies on a surjective finite étale cover π, hence is a boundary of a section of the quotient Q of M ⟶ π_* π⁻¹ M; restriction to X₀ is surjective on sections of π_* π⁻¹ M and injective on sections of Q, both being finite locally constant and base change to X₀ being fully faithful on finite étale covers (Stacks 0A48).

theorem bijective_etaleConstantCohomologyRestriction_one_of_isProper
    (A : Type u) [CommRing A] [HenselianLocalRing A] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of A)) [IsProper f] (M : Type) [AddCommGroup M] [Finite M] :
    Function.Bijective (etaleConstantCohomologyRestriction.{u, 0, u + 1} A f M 1)
Tag 0A5H, a lemma

Tag 0A5H in the Stacks Project.

Declarations registered for the tag:

Sources
LeanStacks.EtaleCohomology.bijective_etaleConstantCohomologyRestriction_iff · Stacks.EtaleCohomology.bijective_etaleConstantCohomologyRestriction_one_of_isProper · Stacks.EtaleCohomology.subsingleton_H_closedFibre_projectiveLine_of_injective

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.