DerivedLocalCohomologyTopMultiplication.lean

theorem derivedLocalCohomologyCoefficientsFirstMap_ι_apply
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (i n : ℕ)
    (α : CategoryTheory.Abelian.Ext.{u}
      (ModuleCat.of R (R ⧸ I ^ n)) S.X₁ i) :
    derivedLocalCohomologyCoefficientsFirstMap I hS i
        (colimit.ι (derivedLocalCohomologyPowersDiagram I S.X₁ i)
          (op (op n)) α) =
      colimit.ι (derivedLocalCohomologyPowersDiagram I S.X₂ i)
        (op (op n))
        (α.comp (CategoryTheory.Abelian.Ext.mk₀ S.f) (add_zero i))

theorem derivedLocalCohomologyCoefficientsFirstMap_smulShortComplex
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ)
    (x : R) (hx : IsSMulRegular M x) :
    derivedLocalCohomologyCoefficientsFirstMap I
        hx.smulShortComplex_shortExact i =
      derivedLocalCohomologyScalarMap I M i x

theorem smulShortComplex_smul_id_third_eq_zero
    (M : ModuleCat.{u} R) (x : R) :
    x • 𝟙 (M.smulShortComplex x).X₃ = 0

theorem derivedLocalCohomologyScalarMap_maximalIdeal_epi_succ
    [IsDomain R] [IsLocalRing R] [IsNoetherianRing R]
    (d : ℕ) (hdim : ringKrullDim R = ((d + 1 : ℕ) : WithBot ℕ∞))
    (x : R) (hx0 : x ≠ 0) (hxmem : x ∈ maximalIdeal R) :
    Epi (derivedLocalCohomologyScalarMap
      (maximalIdeal R) (ModuleCat.of R R) (d + 1) x)

theorem derivedLocalCohomologyScalarMap_maximalIdeal_surjective_succ
    [IsDomain R] [IsLocalRing R] [IsNoetherianRing R]
    (d : ℕ) (hdim : ringKrullDim R = ((d + 1 : ℕ) : WithBot ℕ∞))
    (x : R) (hx0 : x ≠ 0) (hxmem : x ∈ maximalIdeal R) :
    Function.Surjective (derivedLocalCohomologyScalarMap
      (maximalIdeal R) (ModuleCat.of R R) (d + 1) x)