Documentation

DerivedAlgGeo.AlgebraicGeometry.Cohomology.Derived.AffineVanishing

The affine derived-vanishing comparison #

The explicit affine calculation proves that the module-valued Čech complex of M~ on a finite standard distinguished-open cover is exact in every positive degree. This file transfers that calculation to Mathlib's derived cohomology Sheaf.H and transports the result across the affine module-sheaf comparison.

The comparison is obtained non-circularly from the compact distinguished-open basis and the basis/cofinal-cover criterion of Stacks Project, Lemma 20.11.9 (Tag 01EW). In particular, the positive comparison witness below does not assume that the same cover is already Leray-acyclic.

source
@[reducible, inline]
noncomputable abbrev AlgebraicGeometry.Cohomology.underlyingTildeSheaf {R : CommRingCat} (M : ModuleCat ↑R) :
CategoryTheory.Sheaf (Opens.grothendieckTopology ↥(Spec R)) AddCommGrpCat

The underlying abelian sheaf of the module sheaf associated to an affine module. This is the object to which Mathlib's Sheaf.H applies.

Equations
Instances For
    source
    @[reducible, inline]
    noncomputable abbrev AlgebraicGeometry.Cohomology.affineTildeCechComplex {R : CommRingCat} {ι : Type u} [Fintype ι] (f : ι → ↑R) (M : ModuleCat ↑R) :
    CochainComplex (ModuleCat ↑R) ℕ

    The explicit module-valued Čech complex used by the affine localization calculation.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def AlgebraicGeometry.Cohomology.AffineTildeCechDerivedComparisonAt {R : CommRingCat} {ι : Type u} [Fintype ι] (f : ι → ↑R) (M : ModuleCat ↑R) (k : ℕ) [CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↥(Spec R)) AddCommGrpCat)] :
      Prop

      A degreewise comparison between the explicit module-valued affine Cech complex and derived cohomology.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def AlgebraicGeometry.Cohomology.AffineTildeCechDerivedComparison {R : CommRingCat} {ι : Type u} [Fintype ι] (f : ι → ↑R) (M : ModuleCat ↑R) [CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↥(Spec R)) AddCommGrpCat)] :
        Prop

        Degreewise comparison between the explicit affine Čech complex and derived cohomology.

        Equations
        Instances For
          source
          theorem AlgebraicGeometry.Cohomology.affineTildeCechDerivedComparisonAt_of_pos {R : CommRingCat} {ι : Type u} [Fintype ι] (f : ι → ↑R) (hf : Ideal.span (Set.range f) = ⊤) (M : ModuleCat ↑R) (k : ℕ) (hk : 0 < k) [hExt : CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↥(Spec R)) AddCommGrpCat)] :
          AffineTildeCechDerivedComparisonAt f M k

          The compact distinguished-open basis supplies the positive-degree affine comparison witness without assuming derived acyclicity of the chosen cover.

          source
          theorem AlgebraicGeometry.Cohomology.tilde_H_subsingleton_of_comparisonAt {R : CommRingCat} {ι : Type u} [Fintype ι] (f : ι → ↑R) (hf : Ideal.span (Set.range f) = ⊤) (M : ModuleCat ↑R) (k : ℕ) (hk : 0 < k) [CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↥(Spec R)) AddCommGrpCat)] (hcomparison : AffineTildeCechDerivedComparisonAt f M k) :
          Subsingleton ((underlyingTildeSheaf M).H k)

          Positive exactness of the standard affine Čech complex kills Sheaf.H once the comparison with that explicit complex is available.

          source
          theorem AlgebraicGeometry.Cohomology.tilde_H_subsingleton_of_comparison {R : CommRingCat} {ι : Type u} [Fintype ι] (f : ι → ↑R) (hf : Ideal.span (Set.range f) = ⊤) (M : ModuleCat ↑R) [CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↥(Spec R)) AddCommGrpCat)] (hcomparison : AffineTildeCechDerivedComparison f M) (k : ℕ) (hk : 0 < k) :
          Subsingleton ((underlyingTildeSheaf M).H k)

          All-degree comparison gives affine derived vanishing in every positive degree.

          source
          theorem AlgebraicGeometry.Cohomology.H_subsingleton_of_iso_tilde_of_comparisonAt {R : CommRingCat} {ι : Type u} [Fintype ι] (f : ι → ↑R) (hf : Ideal.span (Set.range f) = ⊤) (M : ModuleCat ↑R) (F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↥(Spec R)) AddCommGrpCat) (e : F ≅ underlyingTildeSheaf M) (k : ℕ) (hk : 0 < k) [CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↥(Spec R)) AddCommGrpCat)] (hcomparison : AffineTildeCechDerivedComparisonAt f M k) :
          Subsingleton (F.H k)

          The lower-level comparison-dependent form of transport across an isomorphism of underlying abelian sheaves.

          source
          theorem AlgebraicGeometry.Cohomology.modules_H_subsingleton_of_iso_tilde_of_comparisonAt {R : CommRingCat} {ι : Type u} [Fintype ι] (f : ι → ↑R) (hf : Ideal.span (Set.range f) = ⊤) (M : ModuleCat ↑R) (G : (Spec R).Modules) (e : G ≅ tilde M) (k : ℕ) (hk : 0 < k) [CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↥(Spec R)) AddCommGrpCat)] (hcomparison : AffineTildeCechDerivedComparisonAt f M k) :
          Subsingleton (((Scheme.Modules.toSheaf (Spec R)).obj G).H k)

          The lower-level comparison-dependent form of transport for module sheaves identified with M~.

          source
          theorem AlgebraicGeometry.Cohomology.tilde_H_subsingleton {R : CommRingCat} (M : ModuleCat ↑R) (k : ℕ) (hk : 0 < k) [hExt : CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↥(Spec R)) AddCommGrpCat)] :
          Subsingleton ((underlyingTildeSheaf M).H k)

          Affine vanishing for a module sheaf associated to a module.

          For every positive degree, the derived cohomology of M~ on Spec R is trivial. No noetherian hypothesis is needed.

          source
          theorem AlgebraicGeometry.Cohomology.H_subsingleton_of_iso_tilde {R : CommRingCat} (M : ModuleCat ↑R) (F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↥(Spec R)) AddCommGrpCat) (e : F ≅ underlyingTildeSheaf M) (k : ℕ) (hk : 0 < k) [CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↥(Spec R)) AddCommGrpCat)] :
          Subsingleton (F.H k)

          Affine derived vanishing transports across an isomorphism of underlying abelian sheaves.

          source
          theorem AlgebraicGeometry.Cohomology.modules_H_subsingleton_of_iso_tilde {R : CommRingCat} (M : ModuleCat ↑R) (G : (Spec R).Modules) (e : G ≅ tilde M) (k : ℕ) (hk : 0 < k) [CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↥(Spec R)) AddCommGrpCat)] :
          Subsingleton (((Scheme.Modules.toSheaf (Spec R)).obj G).H k)

          Module sheaves identified with M~ inherit unconditional affine derived vanishing.

          source
          theorem AlgebraicGeometry.Cohomology.modules_H_subsingleton_of_isQuasicoherent {R : CommRingCat} (G : (Spec R).Modules) [SheafOfModules.IsQuasicoherent G] (k : ℕ) (hk : 0 < k) [CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↥(Spec R)) AddCommGrpCat)] :
          Subsingleton (((Scheme.Modules.toSheaf (Spec R)).obj G).H k)

          Affine vanishing for quasi-coherent module sheaves.

          Every quasi-coherent module sheaf on Spec R has trivial positive derived cohomology. The affine comparison identifies it with the tilde sheaf of its global sections, so neither a chosen presentation nor a noetherian hypothesis is required.