Cohomology of skyscraper sheaves of residue fields

For a point x of a scheme X over a field k, the zeroth cohomology of the skyscraper sheaf κ(x)ₓ is its residue field κ(x). Its dimension over k is therefore the residue degree [κ(x) : k]. Since κ(x)ₓ is flasque, its higher cohomology vanishes. Consequently all of its cohomology is finite-dimensional when κ(x) is finite over k.

Main declarations

• Scheme.finrank_cohomology_zero_skyscraperResidueField: the dimension of H⁰(X, κ(x)ₓ) is the residue degree [κ(x) : k];
• Scheme.finiteDimensional_cohomology_skyscraperResidueField: if the residue degree is nonzero, the cohomology of κ(x)ₓ is finite-dimensional in every degree.

@[simp]

theorem AlgebraicGeometry.Scheme.finrank_cohomology_zero_skyscraperResidueField {X : Scheme} (k : Type u) [Field k] [X.Over (Spec ↧k)] (x : ↥X) : Module.finrank k ↑((skyscraperResidueField x).presheaf.obj (Opposite.op ⊤)) = Hom.residueDegree (X ↘ Spec ↧k) x

The dimension of the global sections of a skyscraper sheaf. Over a field k, the zeroth cohomology H⁰(X, κ(x)ₓ) = κ(x) has dimension the residue degree [κ(x) : k] of the structure morphism at x (which is 0 by convention when κ(x) is infinite over k).

theorem AlgebraicGeometry.Scheme.finiteDimensional_cohomology_skyscraperResidueField {X : Scheme} (k : Type u) [Field k] [X.Over (Spec ↧k)] {x : ↥X} (hx : Hom.residueDegree (X ↘ Spec ↧k) x ≠ 0) (i : ℕ) : FiniteDimensional k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (skyscraperResidueField x) i)

At a point whose residue field is finite over k, the skyscraper sheaf κ(x)ₓ has finite-dimensional cohomology in every degree: κ(x) in degree zero and 0 above.