EtaleFundamentalGroups.derivedLocalCohomologyModule_smul_surjective_of_finite_torsionFree
Every nonzero scalar acts surjectively on top local cohomology of a finite torsion-free module, with arbitrary support ideal.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups
universe u
open CategoryTheory Limits
open scoped Pointwise
variable {R : Type u} [CommRing R] [IsDomain R]
variable [IsLocalRing R] [IsNoetherianRing R]Lean source · full declaration
theorem derivedLocalCohomologyModule_smul_surjective_of_finite_torsionFree
(I : Ideal R) (M : ModuleCat.{u} R)
[Module.Finite R M] [Module.IsTorsionFree R M]
(d : ℕ) (hdim : ringKrullDim R = (d : WithBot ℕ∞))
(a : R) (ha : a ≠ 0) :
Function.Surjective (fun z : derivedLocalCohomologyModule I M d => a • z) := by
have hreg : IsSMulRegular M a := IsSMulRegular.of_ne_zero ha
let : Module.Finite R (M.smulShortComplex a).X₃ := by
change Module.Finite R (M ⧸ (a • (⊤ : Submodule R M)))
infer_instance
have hdimQ : Module.supportDim R (M.smulShortComplex a).X₃ < (d : WithBot ℕ∞) := by
have hle : Module.supportDim R (M.smulShortComplex a).X₃ + 1 ≤
(d : WithBot ℕ∞) := by
calc
_ ≤ Module.supportDim R M :=
Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes
(fun _ hp => hreg.notMem_of_mem_minimalPrimes hp)
_ ≤ ringKrullDim R := Module.supportDim_le_ringKrullDim R M
_ = _ := hdim
by_contra h
have hleft : (d : WithBot ℕ∞) + 1 ≤
Module.supportDim R (M.smulShortComplex a).X₃ + 1 :=
by simpa only [add_comm] using add_le_add_right (le_of_not_gt h) 1
have hbad : (d : WithBot ℕ∞) + 1 ≤ (d : WithBot ℕ∞) := hleft.trans hle
have hlt : (d : WithBot ℕ∞) < ((d + 1 : ℕ) : WithBot ℕ∞) :=
WithBot.coe_lt_coe.mpr (ENat.natCast_lt_natCast.mpr (Nat.lt_succ_self d))
exact (not_le_of_gt hlt)
(by simpa only [Nat.cast_add, Nat.cast_one] using hbad)
have hz : IsZero (derivedLocalCohomology I (M.smulShortComplex a).X₃ d) :=
derivedLocalCohomology_isZero_of_supportDim_lt I _ d hdimQ
have hsurj := (AddCommGrpCat.epi_iff_surjective _).mp
(derivedLocalCohomologyCoefficientsFirstMap_epi_of_third_isZero
I hreg.smulShortComplex_shortExact d hz)
rw [derivedLocalCohomologyCoefficientsFirstMap_smulShortComplex I M d a hreg] at hsurj
exact hsurj