NYLL
Module

DerivedLocalCohomologySimultaneousPowers.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologySimultaneousPowers
9 declarations indexed from sourceView source ↗

Module documentation

Simultaneous ideal powers and derived local cohomology

The ideal-quotient Mayer--Vietoris diagram uses I ^ n ⊓ J ^ n and I ^ n ⊔ J ^ n, whereas local cohomology is defined from powers of a single ideal. The supremum comparison is elementary. For intersections, Artin--Rees shows that the simultaneous-power filtration is cofinal with the powers of I ⊓ J.

Imports2
Imported by2

Declarations

def

idealInfPowersDiagram

L31 ↗
EtaleFundamentalGroups.idealInfPowersDiagram
Documentation

The diagram of simultaneous intersections of powers.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · full declaration
def idealInfPowersDiagram (I J : Ideal R) : ℕᵒᵖ ⥤ Ideal R where
  obj n := I ^ unop n ⊓ J ^ unop n
  map f := ⟨⟨inf_le_inf
    (Ideal.pow_le_pow_right f.unop.down.down)
    (Ideal.pow_le_pow_right f.unop.down.down)⟩⟩
def

idealSupPowersDiagram

L38 ↗
EtaleFundamentalGroups.idealSupPowersDiagram
Documentation

The diagram of simultaneous suprema of powers.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · full declaration
def idealSupPowersDiagram (I J : Ideal R) : ℕᵒᵖ ⥤ Ideal R where
  obj n := I ^ unop n ⊔ J ^ unop n
  map f := ⟨⟨sup_le_sup
    (Ideal.pow_le_pow_right f.unop.down.down)
    (Ideal.pow_le_pow_right f.unop.down.down)⟩⟩
theorem

exists_inf_pow_le_inf_pow

L46 ↗
EtaleFundamentalGroups.exists_inf_pow_le_inf_pow
Documentation

Artin--Rees makes the simultaneous intersections of powers cofinal with the powers of the intersection.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem exists_inf_pow_le_inf_pow (I J : Ideal R) [IsNoetherianRing R]
    (m : ℕ) : ∃ n : ℕ, I ^ n ⊓ J ^ n ≤ (I ⊓ J) ^ m
def

idealInfPowersToSelfLERadical

L77 ↗
EtaleFundamentalGroups.idealInfPowersToSelfLERadical
Documentation

Lift simultaneous intersection powers to the full support category.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
section Noetherian
variable [IsNoetherianRing R]
Lean source · statement
def idealInfPowersToSelfLERadical (I J : Ideal R) :
    ℕᵒᵖ ⥤ localCohomology.SelfLERadical (I ⊓ J)
def

idealSupPowersToSelfLERadical

L87 ↗
EtaleFundamentalGroups.idealSupPowersToSelfLERadical
Documentation

Lift simultaneous supremum powers to the full support category.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
section Noetherian
variable [IsNoetherianRing R]
Lean source · statement
def idealSupPowersToSelfLERadical (I J : Ideal R) :
    ℕᵒᵖ ⥤ localCohomology.SelfLERadical (I ⊔ J)
instance

idealInfPowersToSelfLERadical_initial

L104 ↗
EtaleFundamentalGroups.idealInfPowersToSelfLERadical_initial
Documentation

The simultaneous intersection-power diagram is initial in the full category of ideals with radical containing I ⊓ J.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
section Noetherian
variable [IsNoetherianRing R]
Lean source · full declaration
instance idealInfPowersToSelfLERadical_initial (I J : Ideal R) :
    Functor.Initial (idealInfPowersToSelfLERadical I J) where
  out K := by
    apply +allowSynthFailures zigzag_isConnected
    · obtain ⟨m, hm⟩ := Ideal.exists_pow_le_of_le_radical_of_fg
        K.2 (isNoetherian_def.mp (inferInstance : IsNoetherian R R) _)
      obtain ⟨n, hn⟩ := exists_inf_pow_le_inf_pow I J m
      exact ⟨CostructuredArrow.mk
        (⟨⟨⟨hn.trans hm⟩⟩⟩ :
          (idealInfPowersToSelfLERadical I J).obj (op n) ⟶ K)⟩
    · intro x y
      apply Relation.ReflTransGen.single
      rcases le_total (unop x.left) (unop y.left) with h | h
      · right
        exact ⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩
      · left
        exact ⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩
instance

idealSupPowersToSelfLERadical_initial

L124 ↗
EtaleFundamentalGroups.idealSupPowersToSelfLERadical_initial
Documentation

The simultaneous supremum-power diagram is initial in the full category of ideals with radical containing I ⊔ J.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
section Noetherian
variable [IsNoetherianRing R]
Lean source · full declaration
instance idealSupPowersToSelfLERadical_initial (I J : Ideal R) :
    Functor.Initial (idealSupPowersToSelfLERadical I J) where
  out K := by
    apply +allowSynthFailures zigzag_isConnected
    · obtain ⟨n, hn⟩ := Ideal.exists_pow_le_of_le_radical_of_fg
        K.2 (isNoetherian_def.mp (inferInstance : IsNoetherian R R) _)
      have hsup : I ^ n ⊔ J ^ n ≤ (I ⊔ J) ^ n :=
        sup_le
          (pow_le_pow_left' le_sup_left n)
          (pow_le_pow_left' le_sup_right n)
      exact ⟨CostructuredArrow.mk
        (⟨⟨⟨hsup.trans hn⟩⟩⟩ :
          (idealSupPowersToSelfLERadical I J).obj (op n) ⟶ K)⟩
    · intro x y
      apply Relation.ReflTransGen.single
      rcases le_total (unop x.left) (unop y.left) with h | h
      · right
        exact ⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩
      · left
        exact ⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩
def

derivedLocalCohomologyOfInfPowersIso

L147 ↗
EtaleFundamentalGroups.derivedLocalCohomologyOfInfPowersIso
Documentation

The derived-Ext colimit over simultaneous intersection powers computes local cohomology supported on I ⊓ J.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
section Noetherian
variable [IsNoetherianRing R]
Lean source · statement
def derivedLocalCohomologyOfInfPowersIso
    (I J : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) :
    derivedLocalCohomologyOfDiagram (idealInfPowersDiagram I J) M i ≅
      derivedLocalCohomology (I ⊓ J) M i
def

derivedLocalCohomologyOfSupPowersIso

L159 ↗
EtaleFundamentalGroups.derivedLocalCohomologyOfSupPowersIso
Documentation

The derived-Ext colimit over simultaneous supremum powers computes local cohomology supported on I ⊔ J.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
section Noetherian
variable [IsNoetherianRing R]
Lean source · statement
def derivedLocalCohomologyOfSupPowersIso
    (I J : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) :
    derivedLocalCohomologyOfDiagram (idealSupPowersDiagram I J) M i ≅
      derivedLocalCohomology (I ⊔ J) M i

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.