HartshorneLichtenbaumVanishing.lean

def tensorRingComplexIso
    (C : CochainComplex (ModuleCat.{u} R) ℕ) :
    ((tensorLeft (ModuleCat.of R R)).mapHomologicalComplex
      (ComplexShape.up ℕ)).obj C ≅ C

def cechMaximalLocalCohomologyLinearEquiv
    [IsNoetherianRing R] [IsLocalRing R]
    (xs : List R) (hrad : (Ideal.ofList xs).radical = maximalIdeal R)
    (M : ModuleCat.{u} R) (n : ℕ) :
    ((((tensorLeft M).mapHomologicalComplex (ComplexShape.up ℕ)).obj
      (cechLocalizationComplex xs)).homology n) ≃ₗ[R]
        derivedLocalCohomologyModule (maximalIdeal R) M n

def cechRingMaximalLocalCohomologyLinearEquiv
    [IsNoetherianRing R] [IsLocalRing R]
    (xs : List R) (hrad : (Ideal.ofList xs).radical = maximalIdeal R) (n : ℕ) :
    (cechLocalizationComplex xs).homology n ≃ₗ[R]
      derivedLocalCohomologyModule (maximalIdeal R) (ModuleCat.of R R) n

theorem derivedLocalCohomology_isZero_of_completeLocalDomain_of_radical_ne
    [IsDomain R] [IsLocalRing R] [IsNoetherianRing R]
    [IsAdicComplete (maximalIdeal R) R]
    (I : Ideal R) (hI : I ≠ ⊤) (hIradical : I.radical ≠ maximalIdeal R)
    (d : ℕ) (hdim : ringKrullDim R = ((d + 1 : ℕ) : WithBot ℕ∞)) :
    IsZero (derivedLocalCohomology I (ModuleCat.of R R) (d + 1))