theorem
L32 ↗finite_cohomology_pi_FD
ProjSpaceCech.GradedModule.finite_cohomology_pi_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_pi_FD
universe u
noncomputable section
open Finset Function MvPolynomialLean source · full declaration
theorem _root_.ProjSpaceCech.GradedModule.finite_cohomology_pi_FD (R : Type u) [CommRing R] (n :
ℕ) {ι : Type} [Fintype ι] (d₀ : ι → ℤ) (i : ℕ) :
Module.Finite R (ProjSpaceCech.GradedModule.H (ProjSpaceCech.GradedModule.pi (fun k =>
ProjSpaceCech.GradedModule.FD R n (d₀ k))) i) :=
by
have : ∀ k, Module.Finite R (ProjSpaceCech.GradedModule.H (ProjSpaceCech.GradedModule.FD R n (d₀
k)) i) :=
fun k => ProjSpaceCech.GradedModule.finite_cohomology_FD R n (d₀ k) i
obtain ⟨e⟩ := ProjSpaceCech.GradedModule.nonempty_HEquiv_pi (fun k =>
ProjSpaceCech.GradedModule.FD R n (d₀ k)) i
exact Module.Finite.equiv e.symm