Finiteness of toric H^1 in a Laurent module

import Mathlib
import Definitions.Def_MaximalSeshadriConstants
import Definitions.Def_SeshadriPrelim6

namespace OAI

section

namespace MaximalSeshadri.PlaneCech
noncomputable section
open LaurentPlane
variable {K M : Type*} [Field K] [AddCommGroup M]
  [Module K M]

variable [Module (LaurentPlane.Ring K) M] [IsScalarTower K (LaurentPlane.Ring K) M]

theorem toric_H1_finite (V : Fin 3 → Submodule K M)
    (stable : ∀ i z, z ∈ vertexCone i → ∀ x ∈ V i, T (K := K) z • x ∈ V i)
    {ι : Fin 3 → Type*} [∀ i, Fintype (ι i)] (g : ∀ i, ι i → M)
    (hg : ∀ i a, g i a ∈ V i)
    (clear : ∀ i j (x : M), x ∈ V j →
      ∃ d : ℕ, T (K := K) (d • (weight j-weight i)) • x ∈ V i)
    (A B C : Submodule K M)
    (hA : ∀ z ∈ coneA, ∀ x ∈ A, T (K := K) z • x ∈ A)
    (hB : ∀ z ∈ coneB, ∀ x ∈ B, T (K := K) z • x ∈ B)
    (hC : ∀ z ∈ coneC 0, ∀ x ∈ C, T (K := K) z • x ∈ C)
    (incA : V 0 ≤ A) (incB : V 0 ≤ B) (incC : V 1 ≤ C)
    (genA : A = monomialSpan (K := K) coneA (g 0)) (genB : B = monomialSpan (K := K) coneB (g 0))
    (genC : C = monomialSpan (K := K) (coneC 0) (g 1)) :
    Module.Finite K ((cycles A B C) ⧸ vertexBoundaries A B C V) := by
  sorry

end
end MaximalSeshadri.PlaneCech
end
end OAI