Module

DerivedLocalCohomologyModuleRadical.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyModuleRadical

8 declarations indexed from sourceView source ↗

Module documentation

Linear radical invariance of local cohomology

Ideals with the same radical define the same torsion submodule. Comparing these submodules before applying a common injective resolution gives an isomorphism on homology that retains its scalar action.

Imports6

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyInjectiveComplex
Nyll.EtaleFundamentalGroups.Purity.IdealPowerTorsionComplexZero
Nyll.EtaleFundamentalGroups.Purity.IdealPowerTorsionFunctor
Mathlib.Algebra.Category.ModuleCat.Injective
Mathlib.CategoryTheory.Abelian.Injective.Resolution
Mathlib.RingTheory.Finiteness.Ideal

Imported by2

theorem

primaryComponent_le_of_pow_le

L33 ↗

EtaleFundamentalGroups.Purity.primaryComponent_le_of_pow_le

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in

Lean source · statement

theorem primaryComponent_le_of_pow_le
    (M : ModuleCat.{u} R) {I J : Ideal R} {k : ℕ} (hk : J ^ k ≤ I) :
    Ideal.primaryComponent M I ≤ Ideal.primaryComponent M J

theorem

primaryComponent_eq_of_sameRadical

L49 ↗

EtaleFundamentalGroups.Purity.primaryComponent_eq_of_sameRadical

Documentation

Power torsion agrees as a submodule for ideals with the same radical.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory
variable {R : Type u} [CommRing R] [IsNoetherianRing R]

Lean source · statement

theorem primaryComponent_eq_of_sameRadical
    (M : ModuleCat.{u} R) {I J : Ideal R} (hIJ : I.radical = J.radical) :
    Ideal.primaryComponent M I = Ideal.primaryComponent M J

def

submoduleEqualityIso

L61 ↗

EtaleFundamentalGroups.Purity.submoduleEqualityIso

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory
variable {R : Type u} [CommRing R] [IsNoetherianRing R]

Lean source · full declaration

def submoduleEqualityIso (M : ModuleCat.{u} R)
    (N P : Submodule R M) (h : N = P) : ModuleCat.of R N ≅ ModuleCat.of R P where
  hom := ModuleCat.ofHom (Submodule.inclusion h.le)
  inv := ModuleCat.ofHom (Submodule.inclusion h.ge)
  hom_inv_id := by
    ext z
    rfl
  inv_hom_id := by
    ext z
    rfl

def

primaryComponentIsoOfSameRadical

L72 ↗

EtaleFundamentalGroups.Purity.primaryComponentIsoOfSameRadical

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory
variable {R : Type u} [CommRing R] [IsNoetherianRing R]

Lean source · statement

def primaryComponentIsoOfSameRadical
    (M : ModuleCat.{u} R) {I J : Ideal R} (hIJ : I.radical = J.radical) :
    ModuleCat.of R (Ideal.primaryComponent M I) ≅
      ModuleCat.of R (Ideal.primaryComponent M J)

theorem

submoduleEqualityIso_naturality

L79 ↗

EtaleFundamentalGroups.Purity.submoduleEqualityIso_naturality

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in

Lean source · statement

theorem submoduleEqualityIso_naturality
    (M N : ModuleCat.{u} R) (A B : Submodule R M) (C D : Submodule R N)
    (hAB : A = B) (hCD : C = D) (f : M →ₗ[R] N)
    (hAC : ∀ z : A, f z ∈ C) (hBD : ∀ z : B, f z ∈ D) :
    ModuleCat.ofHom ((f.domRestrict A).codRestrict C hAC) ≫
        (submoduleEqualityIso N C D hCD).hom =
      (submoduleEqualityIso M A B hAB).hom ≫
        ModuleCat.ofHom ((f.domRestrict B).codRestrict D hBD)

def

idealPowerTorsionFunctorIsoOfSameRadical

L91 ↗

EtaleFundamentalGroups.Purity.idealPowerTorsionFunctorIsoOfSameRadical

Documentation

The identity on torsion elements gives a natural linear comparison.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory
variable {R : Type u} [CommRing R] [IsNoetherianRing R]

Lean source · statement

def idealPowerTorsionFunctorIsoOfSameRadical
    {I J : Ideal R} (hIJ : I.radical = J.radical) :
    idealPowerTorsionFunctor I ≅ idealPowerTorsionFunctor J

def

idealPowerTorsionComplexIsoOfSameRadical

L104 ↗

EtaleFundamentalGroups.Purity.idealPowerTorsionComplexIsoOfSameRadical

Documentation

Comparing torsion term by term gives an actual isomorphism of complexes.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory
variable {R : Type u} [CommRing R] [IsNoetherianRing R]

Lean source · statement

def idealPowerTorsionComplexIsoOfSameRadical
    {I J : Ideal R} (hIJ : I.radical = J.radical)
    (K : CochainComplex (ModuleCat.{u} R) ℕ) :
    idealPowerTorsionComplex I K ≅ idealPowerTorsionComplex J K

def

derivedLocalCohomologyModuleLinearEquivOfSameRadical

L114 ↗

EtaleFundamentalGroups.Purity.derivedLocalCohomologyModuleLinearEquivOfSameRadical

Documentation

Radical invariance for the canonical local-cohomology module, retaining its full linear structure.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory
variable {R : Type u} [CommRing R] [IsNoetherianRing R]

Lean source · statement

def derivedLocalCohomologyModuleLinearEquivOfSameRadical
    {I J : Ideal R} (hIJ : I.radical = J.radical)
    (M : ModuleCat.{u} R) (n : ℕ) :
    derivedLocalCohomologyModule I M n ≃ₗ[R] derivedLocalCohomologyModule J M n

Module documentation

Linear radical invariance of local cohomology

Declarations