Module

ProjSpaceCech_GradedModule_finite_cohomology_of_isFG.lean

Nyll.SchemeTheory.Cohomology.Cech.ProjSpaceCech_GradedModule_finite_cohomology_of_isFG

2 declarations indexed from sourceView source ↗

Module documentation

Finite Cech cohomology of a finitely generated graded module over a noetherian ring.

Imports5

Imported by2

theorem

finite_cohomology_of_isFG'

L46 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_finite_cohomology_of_isFG.ProjSpaceCech.GradedModule.finite_cohomology_of_isFG'

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_GradedModule_finite_cohomology_of_isFG
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Main
variable {R : Type u} [CommRing R] {n : ℕ}
open scoped _root_.ProjSpaceCech.GradedModule in

Lean source · statement

theorem GradedModule.finite_cohomology_of_isFG' [IsNoetherianRing R] (D : GradedModule R n)
    (hD : GradedModule.IsFG D) (i : ℕ) :
    Module.Finite R (GradedModule.H D i)

theorem

finite_cohomology_of_isFG

L67 ↗

ProjSpaceCech.GradedModule.finite_cohomology_of_isFG

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_GradedModule_finite_cohomology_of_isFG
universe u
noncomputable section
open Finset Function MvPolynomial

Lean source · statement

theorem _root_.ProjSpaceCech.GradedModule.finite_cohomology_of_isFG {R : Type u} [CommRing R]
    [IsNoetherianRing R] {n : ℕ} (D : ProjSpaceCech.GradedModule R n)
    (hD : ProjSpaceCech.GradedModule.IsFG D) (i : ℕ) : Module.Finite R
      (ProjSpaceCech.GradedModule.H D i)

Module documentation

Declarations

finite_cohomology_of_isFG'

finite_cohomology_of_isFG