NYLL
Module

ProjSpaceCech_GradedModule_finite_cohomology_FD.lean

Nyll.SchemeTheory.Cohomology.Cech.ProjSpaceCech_GradedModule_finite_cohomology_FD
1 declaration indexed from sourceView source ↗

Module documentation

Finite Cech cohomology of a shifted free graded module on projective space.

Imports4
Imported by2

Declarations

theorem

finite_cohomology_FD

L32 ↗
ProjSpaceCech.GradedModule.finite_cohomology_FD
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_finite_cohomology_FD
universe u
noncomputable section
open Finset Function MvPolynomial
Lean source · statement
theorem _root_.ProjSpaceCech.GradedModule.finite_cohomology_FD (R : Type u) [CommRing R] (n : ℕ)
    (d₀ : ℤ) (i : ℕ) :
    Module.Finite R (ProjSpaceCech.GradedModule.H (ProjSpaceCech.GradedModule.FD R n d₀) i)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.