Module

HartshorneLichtenbaumReduction.lean

Nyll.EtaleFundamentalGroups.Purity.HartshorneLichtenbaumReduction

15 declarations indexed from sourceView source ↗

Module documentation

Reductions for top local-cohomology vanishing

This file isolates two source-level inputs used at the Hartshorne--Lichtenbaum frontier.

First, a colimit of additive groups vanishes when every object admits a later transition whose map is zero. Applied to the ideal-powers Ext diagram, this reduces derived local-cohomology vanishing to a concrete pro-zero statement about its transition maps.

Second, in a local ring, a proper ideal whose radical is not the maximal ideal is contained in a prime strictly below the maximal ideal. The radical condition is essential: merely requiring the ideal itself to differ from the maximal ideal does not exclude ideals with maximal radical.

Imports5

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyRadical
Mathlib.Algebra.Category.Grp.FilteredColimits
Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.Regular.RegularSequence

Imported by9

theorem

colimit_ι_eq_zero_iff_eventually_zero

L40 ↗

EtaleFundamentalGroups.colimit_ι_eq_zero_iff_eventually_zero

Documentation

In a filtered colimit of additive commutative groups, a canonical class is zero exactly when some later transition kills its representative.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v

Lean source · statement

theorem colimit_ι_eq_zero_iff_eventually_zero
    {J : Type v} [SmallCategory J] [IsFiltered J]
    (D : J ⥤ AddCommGrpCat.{u}) [HasColimit D]
    [PreservesColimit D (forget AddCommGrpCat)]
    (j : J) (x : D.obj j) :
    colimit.ι D j x = 0 ↔
      ∃ k : J, ∃ f : j ⟶ k, D.map f x = 0

theorem

colimit_isZero_of_elementwise_eventually_zero

L64 ↗

EtaleFundamentalGroups.colimit_isZero_of_elementwise_eventually_zero

Documentation

A colimit of additive groups is zero if every element at every stage is killed by some later transition.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v

Lean source · statement

theorem colimit_isZero_of_elementwise_eventually_zero
    {J : Type v} [SmallCategory J] (D : J ⥤ AddCommGrpCat.{u})
    [HasColimit D]
    (hzero : ∀ j : J, ∀ x : D.obj j,
      ∃ k : J, ∃ f : j ⟶ k, D.map f x = 0) :
    IsZero (colimit D)

theorem

colimit_isZero_iff_elementwise_eventually_zero

L83 ↗

EtaleFundamentalGroups.colimit_isZero_iff_elementwise_eventually_zero

Documentation

A filtered colimit of additive commutative groups is zero exactly when every representative is killed by some later transition.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v

Lean source · statement

theorem colimit_isZero_iff_elementwise_eventually_zero
    {J : Type v} [SmallCategory J] [IsFiltered J]
    (D : J ⥤ AddCommGrpCat.{u}) [HasColimit D]
    [PreservesColimit D (forget AddCommGrpCat)] :
    IsZero (colimit D) ↔
      ∀ j : J, ∀ x : D.obj j,
        ∃ k : J, ∃ f : j ⟶ k, D.map f x = 0

theorem

colimit_isZero_of_eventually_zero_map

L101 ↗

EtaleFundamentalGroups.colimit_isZero_of_eventually_zero_map

Documentation

A colimit of additive groups is zero if every stage maps trivially to some later stage. Individual objects of the diagram need not be zero.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v

Lean source · statement

theorem colimit_isZero_of_eventually_zero_map
    {J : Type v} [SmallCategory J] (D : J ⥤ AddCommGrpCat.{u})
    [HasColimit D]
    (hzero : ∀ j : J, ∃ k : J, ∃ f : j ⟶ k, D.map f = 0) :
    IsZero (colimit D)

theorem

colimit_natDoubleOp_isZero_of_elementwise_eventually_zero

L115 ↗

EtaleFundamentalGroups.colimit_natDoubleOp_isZero_of_elementwise_eventually_zero

Documentation

The elementwise criterion for a diagram indexed by the double opposite of the natural numbers.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v

Lean source · statement

theorem colimit_natDoubleOp_isZero_of_elementwise_eventually_zero
    (D : (ℕᵒᵖ)ᵒᵖ ⥤ AddCommGrpCat.{u})
    (hzero : ∀ n : ℕ, ∀ x : D.obj (op (op n)),
      ∃ m : ℕ, ∃ hnm : n ≤ m,
        D.map (homOfLE hnm).op.op x = 0) :
    IsZero (colimit D)

theorem

colimit_natDoubleOp_isZero_of_eventually_zero_map

L128 ↗

EtaleFundamentalGroups.colimit_natDoubleOp_isZero_of_eventually_zero_map

Documentation

A natural-number form of the preceding criterion for the double-opposite indexing category used by ideal 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 v

Lean source · statement

theorem colimit_natDoubleOp_isZero_of_eventually_zero_map
    (D : (ℕᵒᵖ)ᵒᵖ ⥤ AddCommGrpCat.{u})
    (hzero : ∀ n : ℕ, ∃ m : ℕ, ∃ hnm : n ≤ m,
      D.map (homOfLE hnm).op.op = 0) :
    IsZero (colimit D)

theorem

derivedLocalCohomology_isZero_of_eventually_zero_transition

L140 ↗

EtaleFundamentalGroups.derivedLocalCohomology_isZero_of_eventually_zero_transition

Documentation

Derived local cohomology vanishes if the transition maps in its ideal-powers derived-Ext diagram are eventually zero.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v

Lean source · statement

theorem derivedLocalCohomology_isZero_of_eventually_zero_transition
    {R : Type u} [CommRing R]
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ)
    (hzero : ∀ n : ℕ, ∃ m : ℕ, ∃ hnm : n ≤ m,
      (derivedLocalCohomologyPowersDiagram I M i).map
        (homOfLE hnm).op.op = 0) :
    IsZero (derivedLocalCohomology I M i)

theorem

derivedLocalCohomology_isZero_of_elementwise_eventually_zero_transition

L152 ↗

EtaleFundamentalGroups.derivedLocalCohomology_isZero_of_elementwise_eventually_zero_transition

Documentation

It is enough to kill every individual derived-Ext class at a later power of the support 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 v

Lean source · statement

theorem derivedLocalCohomology_isZero_of_elementwise_eventually_zero_transition
    {R : Type u} [CommRing R]
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ)
    (hzero : ∀ n : ℕ,
      ∀ x : CategoryTheory.Abelian.Ext.{u}
        (ModuleCat.of R (R ⧸ I ^ n)) M i,
      ∃ m : ℕ, ∃ hnm : n ≤ m,
        (derivedLocalCohomologyPowersDiagram I M i).map
          (homOfLE hnm).op.op x = 0) :
    IsZero (derivedLocalCohomology I M i)

theorem

derivedLocalCohomology_isZero_iff_elementwise_eventually_zero_transition

L169 ↗

EtaleFundamentalGroups.derivedLocalCohomology_isZero_iff_elementwise_eventually_zero_transition

Documentation

Derived local cohomology is zero exactly when every derived-Ext class at one ideal power is killed after passing to some later power.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v

Lean source · statement

theorem derivedLocalCohomology_isZero_iff_elementwise_eventually_zero_transition
    {R : Type u} [CommRing R]
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) :
    IsZero (derivedLocalCohomology I M i) ↔
      ∀ n : ℕ,
        ∀ x : CategoryTheory.Abelian.Ext.{u}
          (ModuleCat.of R (R ⧸ I ^ n)) M i,
        ∃ m : ℕ, ∃ hnm : n ≤ m,
          (derivedLocalCohomologyPowersDiagram I M i).map
            (homOfLE hnm).op.op x = 0

theorem

derivedLocalCohomology_not_isZero_iff_exists_persistent_transition

L202 ↗

EtaleFundamentalGroups.derivedLocalCohomology_not_isZero_iff_exists_persistent_transition

Documentation

Nonvanishing of derived local cohomology is equivalently witnessed by one derived-Ext class which survives every later ideal-power transition.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v

Lean source · statement

theorem derivedLocalCohomology_not_isZero_iff_exists_persistent_transition
    {R : Type u} [CommRing R]
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) :
    ¬ IsZero (derivedLocalCohomology I M i) ↔
      ∃ n : ℕ,
        ∃ x : CategoryTheory.Abelian.Ext.{u}
          (ModuleCat.of R (R ⧸ I ^ n)) M i,
        ∀ m : ℕ, ∀ hnm : n ≤ m,
          (derivedLocalCohomologyPowersDiagram I M i).map
            (homOfLE hnm).op.op x ≠ 0

theorem

exists_ofList_radical_eq_maximalIdeal_of_ringKrullDim_eq

L221 ↗

EtaleFundamentalGroups.exists_ofList_radical_eq_maximalIdeal_of_ringKrullDim_eq

Documentation

A Noetherian local ring of dimension d admits a list of exactly d elements whose generated ideal has maximal radical. For d = 0, the list is empty and the assertion says that the nilradical is the maximal 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 v

Lean source · statement

theorem exists_ofList_radical_eq_maximalIdeal_of_ringKrullDim_eq
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (d : ℕ)
    (hdim : ringKrullDim R = (d : WithBot ℕ∞)) :
    ∃ xs : List R,
      xs.length = d ∧
      (Ideal.ofList xs).radical = IsLocalRing.maximalIdeal R

theorem

exists_derivedLocalCohomology_ofList_iso_maximalIdeal_of_ringKrullDim_eq

L271 ↗

EtaleFundamentalGroups.exists_derivedLocalCohomology_ofList_iso_maximalIdeal_of_ringKrullDim_eq

Documentation

In exact dimension d, maximal-support derived local cohomology can be computed using an ideal generated by a list of exactly d parameters.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v

Lean source · statement

theorem exists_derivedLocalCohomology_ofList_iso_maximalIdeal_of_ringKrullDim_eq
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (d : ℕ)
    (hdim : ringKrullDim R = (d : WithBot ℕ∞))
    (M : ModuleCat.{u} R) :
    ∃ xs : List R,
      xs.length = d ∧
      (Ideal.ofList xs).radical = IsLocalRing.maximalIdeal R ∧
      Nonempty
        (derivedLocalCohomology (Ideal.ofList xs) M d ≅
          derivedLocalCohomology (IsLocalRing.maximalIdeal R) M d)

theorem

derivedLocalCohomology_isZero_iff_radical

L295 ↗

EtaleFundamentalGroups.derivedLocalCohomology_isZero_iff_radical

Documentation

Derived local-cohomology vanishing can be checked after replacing the support ideal by its radical.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v

Lean source · statement

theorem derivedLocalCohomology_isZero_iff_radical
    {R : Type u} [CommRing R] [IsNoetherian R R]
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) :
    IsZero (derivedLocalCohomology I M i) ↔
      IsZero (derivedLocalCohomology I.radical M i)

theorem

exists_prime_over_lt_maximalIdeal_of_radical_ne

L305 ↗

EtaleFundamentalGroups.exists_prime_over_lt_maximalIdeal_of_radical_ne

Documentation

A proper ideal in a local ring with nonmaximal radical is contained in a prime ideal strictly below the maximal 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 v

Lean source · statement

theorem exists_prime_over_lt_maximalIdeal_of_radical_ne
    {R : Type u} [CommRing R] [IsLocalRing R]
    (I : Ideal R) (hI : I ≠ ⊤)
    (hradical : I.radical ≠ IsLocalRing.maximalIdeal R) :
    ∃ P : Ideal R,
      I ≤ P ∧ P.IsPrime ∧ P < IsLocalRing.maximalIdeal R

theorem

radical_ne_maximalIdeal_iff_exists_prime_over_lt

L340 ↗

EtaleFundamentalGroups.radical_ne_maximalIdeal_iff_exists_prime_over_lt

Documentation

For a proper ideal of a local ring, having nonmaximal radical is equivalent to the existence of a prime over it strictly below the maximal 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 v

Lean source · statement

theorem radical_ne_maximalIdeal_iff_exists_prime_over_lt
    {R : Type u} [CommRing R] [IsLocalRing R]
    (I : Ideal R) (hI : I ≠ ⊤) :
    I.radical ≠ IsLocalRing.maximalIdeal R ↔
      ∃ P : Ideal R,
        I ≤ P ∧ P.IsPrime ∧ P < IsLocalRing.maximalIdeal R

Module documentation

Reductions for top local-cohomology vanishing

Declarations