24.1. Keystones🔗

serre_surjectivity_dim_core — source · report an issue

theorem serre_surjectivity_dim_core
    {K : Type*} [Field K] {V : ℕ → Type*}
    [∀ n, AddCommGroup (V n)] [∀ n, Module K (V n)] [∀ n, FiniteDimensional K (V n)]
    (Λ I : ∀ n, Submodule K (V n)) (g d k₀ : ℤ)
    (hΛ : ∀ n : ℕ, (1 : ℤ) - g + n ≤ (finrank K (Λ n) : ℤ))
    (hI : ∀ n : ℕ, (n : ℤ) + k₀ - d ≤ (finrank K (I n) : ℤ))
    (hV : ∀ n : ℕ, d < n → ((finrank K (V n) : ℤ)) = n + g - 1 - d) :
    ∃ N : ℕ, ∀ n ≥ N, Λ n ⊓ I n ≠ ⊥

SerreDualityData ladder — source · report an issue

structure SerreDualityData (𝔘 : FiniteCover X) where