Documentation

DerivedAlgGeo.AlgebraicGeometry.Cohomology.Derived.UnitExtLinear

The linear unit-Ext/cohomology comparison #

On a variety over a field, the additive comparison

Extⁿ_{X.Modules}(𝒪_X, F) ≃+ Hⁿ(X, F)

is compatible with the canonical base-field actions on both sides. The proof identifies both actions with postcomposition by multiplication by the scalar on F: on Ext this is Abelian.Ext.smul_eq_comp_mk₀, while on cohomology it is the action used to construct linearCoherentH.

This file remains on the all-module-sheaf side. It does not compare Ext in Coh X with Ext in X.Modules; that is the separate CoherentExtComparison boundary.

Main result #

source
theorem AlgebraicGeometry.Scheme.Modules.extUnitAddEquivDerivedH_smul {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] (F : Coh X) (n : ℕ) (r : k) (e : CategoryTheory.Abelian.Ext (unit X) ((Coh.ι X).obj F) n) :
(((Coh.ι X).obj F).extUnitAddEquivDerivedH n) (r • e) = ((Cohomology.coherentHScalarAction k X n F) r) ((((Coh.ι X).obj F).extUnitAddEquivDerivedH n) e)

The unit-Ext/cohomology comparison respects the canonical base-field action.

source
noncomputable def AlgebraicGeometry.Scheme.Modules.extUnitLinearEquivCoherentH {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] (F : Coh X) (n : ℕ) :
CategoryTheory.Abelian.Ext (unit X) ((Coh.ι X).obj F) n ≃ₗ[k] ↑((Cohomology.linearCoherentH k X n).obj F)

Ext from the structure sheaf is linearly equivalent to coherent cohomology.

The target is the canonical linearCoherentH realization, not an independently chosen vector space structure on the underlying cohomology group.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Modules.extUnitLinearEquivCoherentH_apply {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] (F : Coh X) (n : ℕ) (e : CategoryTheory.Abelian.Ext (unit X) ((Coh.ι X).obj F) n) :
    (extUnitLinearEquivCoherentH F n) e = (((Coh.ι X).obj F).extUnitAddEquivDerivedH n) e