AlgebraicGeometry.OModulePresheaf.cechFinrank
The rank of Čech cohomology in the specified degree.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
namespace AlgebraicGeometry.OModulePresheaf
open CategoryTheory
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)Lean source · full declaration
def cechFinrank : ℕ → ℕ
| 0 => Module.finrank R (F.H0 K)
| i + 1 => Module.finrank R (F.HSucc K i)