Documentation

DerivedAlgGeo.AlgebraicGeometry.Cohomology.Derived.UnitExt

Ext (𝒪_X, M) in X.Modules is sheaf cohomology #

SheafOfModules.extUnitAddEquivDerivedH for the wrapper X.Modules on a scheme. The wrapper's category instance is a copy of that of SheafOfModules X.ringCatSheaf, so the equivalence is reassembled from extComparisonAddEquiv in X.Modules rather than transported: the degree-zero bijection is a statement about hom-sets, which the wrapper shares on the nose, and acyclicity of injectives comes from Scheme.Modules.isFlasque_toSheaf_of_injective.

HasExt.{u + 1} X.Modules is obtained from HasDerivedCategory.standard, the same route as AlgebraicGeometry/DerivedCategory/Dqc/Identification.lean, so the Ext groups here are the ones CoherentExtComparison is stated for.

Main results #

source
@[reducible, inline]
noncomputable abbrev AlgebraicGeometry.Scheme.Modules.unit (X : Scheme) :
X.Modules

The structure sheaf 𝒪_X as an object of X.Modules.

Equations
Instances For
    source
    noncomputable def AlgebraicGeometry.Scheme.Modules.unitFromConstant (X : Scheme) :
    (CategoryTheory.constantSheaf (Opens.grothendieckTopology ↥X) AddCommGrpCat).obj (AddCommGrpCat.of (ULift.{u, 0} ℤ)) ⟶ (toSheaf X).obj (unit X)

    The map from the constant sheaf ℤ to the underlying abelian sheaf of 𝒪_X sending 1 to 1.

    Equations
    Instances For
      source
      theorem AlgebraicGeometry.Scheme.Modules.bijective_unitFromConstant_comp {X : Scheme} (M : X.Modules) :
      Function.Bijective fun (f : unit X ⟶ M) => CategoryTheory.CategoryStruct.comp (unitFromConstant X) ((toSheaf X).map f)

      Degree zero. f ↦ unitFromConstant ≫ toSheaf.map f is a bijection from 𝒪_X ⟶ M to maps ℤ ⟶ toSheaf M.

      source
      theorem AlgebraicGeometry.Scheme.Modules.subsingleton_derivedH_toSheaf_of_injective {X : Scheme} [hExt : CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↥X) AddCommGrpCat)] (I : X.Modules) [CategoryTheory.Injective I] (n : ℕ) :
      Subsingleton (CategoryTheory.Sheaf.derivedH hExt ((toSheaf X).obj I) (n + 1))

      Injective 𝒪_X-modules are acyclic for Sheaf.H.

      source
      noncomputable def AlgebraicGeometry.Scheme.Modules.extUnitAddEquivDerivedH {X : Scheme} [hExt : CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↥X) AddCommGrpCat)] (M : X.Modules) (n : ℕ) :
      CategoryTheory.Abelian.Ext (unit X) M n ≃+ CategoryTheory.Sheaf.derivedH hExt ((toSheaf X).obj M) n

      Ext (𝒪_X, M) is sheaf cohomology. Ext^n (𝒪_X) M ≃+ H^n (toSheaf M) for every 𝒪_X-module M.

      Equations
      Instances For