Module

DerivedLocalCohomologyDimensionZero.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyDimensionZero

4 declarations indexed from sourceView source ↗

Module documentation

Degree-zero nonvanishing for derived local cohomology

The degree-zero base case of Grothendieck nonvanishing is already visible in the ideal-powers Ext diagram. For the zero ideal, every positive power is again zero, and the identity class of R ⧸ (0) survives every later transition.

Imports3

Nyll.EtaleFundamentalGroups.Purity.HartshorneLichtenbaumReduction
Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyGeneratorCountDomain
Mathlib.RingTheory.KrullDimension.Zero

Imported by1

Nyll.EtaleFundamentalGroups.Purity.All

theorem

ringModIdeals_bot_transition_eq_quotEquiv

L30 ↗

EtaleFundamentalGroups.ringModIdeals_bot_transition_eq_quotEquiv

Documentation

The quotient map between two positive powers of the zero ideal is the canonical isomorphism induced by equality of those powers.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u

Lean source · full declaration

theorem ringModIdeals_bot_transition_eq_quotEquiv
    {R : Type u} [CommRing R]
    {n m : ℕ} (hn : 1 ≤ n) (hm : 1 ≤ m) (hnm : n ≤ m) :
    (localCohomology.ringModIdeals
      (localCohomology.idealPowersDiagram (⊥ : Ideal R))).map
        (homOfLE hnm).op =
      (Submodule.quotEquivOfEq
        ((⊥ : Ideal R) ^ m) ((⊥ : Ideal R) ^ n)
        (by simp [Ideal.bot_pow (Nat.ne_of_gt hn),
          Ideal.bot_pow (Nat.ne_of_gt hm)])).toModuleIso.hom := by
  ext x
  induction x using Submodule.Quotient.induction_on with
  | _ x =>
      simp only [localCohomology.ringModIdeals,
        localCohomology.idealPowersDiagram]
      rfl

theorem

derivedLocalCohomology_bot_not_isZero_zero

L49 ↗

EtaleFundamentalGroups.derivedLocalCohomology_bot_not_isZero_zero

Documentation

Derived local cohomology supported at the zero ideal is nonzero in degree zero over every nontrivial commutative ring.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem derivedLocalCohomology_bot_not_isZero_zero
    {R : Type u} [CommRing R] [Nontrivial R] :
    ¬ IsZero
      (derivedLocalCohomology (⊥ : Ideal R) (ModuleCat.of R R) 0)

theorem

derivedLocalCohomology_maximalIdeal_not_isZero_zero_of_ringKrullDim_eq_zero

L105 ↗

EtaleFundamentalGroups.derivedLocalCohomology_maximalIdeal_not_isZero_zero_of_ringKrullDim_eq_zero

Documentation

Grothendieck nonvanishing in dimension zero: a zero-dimensional local domain is a field, so its maximal ideal is zero and the preceding persistent degree-zero class applies.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem derivedLocalCohomology_maximalIdeal_not_isZero_zero_of_ringKrullDim_eq_zero
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    (hdim : ringKrullDim R = 0) :
    ¬ IsZero
      (derivedLocalCohomology (IsLocalRing.maximalIdeal R)
        (ModuleCat.of R R) 0)

theorem

derivedLocalCohomology_isZero_of_isRadical_ne_maximalIdeal_of_ringKrullDim_eq_zero

L122 ↗

EtaleFundamentalGroups.derivedLocalCohomology_isZero_of_isRadical_ne_maximalIdeal_of_ringKrullDim_eq_zero

Documentation

Hartshorne--Lichtenbaum vanishing is vacuous in dimension zero: a radical ideal distinct from the unique maximal ideal must be the unit ideal.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem derivedLocalCohomology_isZero_of_isRadical_ne_maximalIdeal_of_ringKrullDim_eq_zero
    {R : Type u} [CommRing R] [IsLocalRing R]
    (hdim : ringKrullDim R = 0)
    (J : Ideal R) (hJradical : J.IsRadical)
    (hJnonmax : J ≠ IsLocalRing.maximalIdeal R) (i : ℕ) :
    IsZero (derivedLocalCohomology J (ModuleCat.of R R) i)

Module documentation

Degree-zero nonvanishing for derived local cohomology

Declarations

ringModIdeals_bot_transition_eq_quotEquiv

derivedLocalCohomology_bot_not_isZero_zero

derivedLocalCohomology_maximalIdeal_not_isZero_zero_of_ringKrullDim_eq_zero

derivedLocalCohomology_isZero_of_isRadical_ne_maximalIdeal_of_ringKrullDim_eq_zero