NYLL
Module

DerivedLocalCohomologyDegreeZeroModule.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyDegreeZeroModule
16 declarations indexed from sourceView source ↗

Module documentation

Degree-zero local cohomology inside the coefficient module

In degree zero, a representative is a map from a quotient ring to the coefficient module. Evaluation at one is compatible with the quotient transition maps and hence defines a linear map out of local cohomology. Each representative evaluation is injective, so the colimit map is injective. If every coefficient vector is killed by a power of the support ideal, the map is also surjective.

Imports10
Imported by10

Declarations

def

derivedExtZeroQuotientTorsionEquiv

L39 ↗
EtaleFundamentalGroups.derivedExtZeroQuotientTorsionEquiv
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
def derivedExtZeroQuotientTorsionEquiv (J : Ideal R) (M : ModuleCat.{u} R) :
    CategoryTheory.Abelian.Ext.{u} (ModuleCat.of R (R ⧸ J)) M 0 ≃ₗ[R]
      Submodule.torsionBySet R M J
def

derivedExtZeroQuotientEvaluation

L46 ↗
EtaleFundamentalGroups.derivedExtZeroQuotientEvaluation
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
def derivedExtZeroQuotientEvaluation (J : Ideal R) (M : ModuleCat.{u} R) :
    CategoryTheory.Abelian.Ext.{u} (ModuleCat.of R (R ⧸ J)) M 0 →ₗ[R] M
theorem

derivedExtZeroQuotientEvaluation_mk₀

L51 ↗
EtaleFundamentalGroups.derivedExtZeroQuotientEvaluation_mk₀
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 derivedExtZeroQuotientEvaluation_mk₀
    (J : Ideal R) (M : ModuleCat.{u} R)
    (f : ModuleCat.of R (R ⧸ J) ⟶ M) :
    derivedExtZeroQuotientEvaluation J M (CategoryTheory.Abelian.Ext.mk₀ f) =
      f.hom (Ideal.Quotient.mk J 1)
theorem

derivedExtZeroQuotientEvaluation_injective

L64 ↗
EtaleFundamentalGroups.derivedExtZeroQuotientEvaluation_injective
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 derivedExtZeroQuotientEvaluation_injective
    (J : Ideal R) (M : ModuleCat.{u} R) :
    Function.Injective (derivedExtZeroQuotientEvaluation J M)
theorem

derivedExtZeroQuotientEvaluation_exists_preimage

L70 ↗
EtaleFundamentalGroups.derivedExtZeroQuotientEvaluation_exists_preimage
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 derivedExtZeroQuotientEvaluation_exists_preimage
    (J : Ideal R) (M : ModuleCat.{u} R) (z : M)
    (hz : z ∈ Submodule.torsionBySet R M (J : Set R)) :
    ∃ α : CategoryTheory.Abelian.Ext.{u} (ModuleCat.of R (R ⧸ J)) M 0,
      derivedExtZeroQuotientEvaluation J M α = z
def

derivedLocalCohomologyZeroEvaluationCocone

L80 ↗
EtaleFundamentalGroups.derivedLocalCohomologyZeroEvaluationCocone
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 derivedLocalCohomologyZeroEvaluationCocone
    (I : Ideal R) (M : ModuleCat.{u} R) :
    Cocone (derivedLocalCohomologyPowersDiagram I M 0) where
  pt := AddCommGrpCat.of M
  ι :=
    { app := fun n => AddCommGrpCat.ofHom
        (derivedExtZeroQuotientEvaluation (I ^ unop (unop n)) M).toAddMonoidHom
      naturality := by
        intro j k g
        ext α
        let q : ModuleCat.of R (R ⧸ I ^ unop (unop k)) ⟶
            ModuleCat.of R (R ⧸ I ^ unop (unop j)) :=
          (localCohomology.ringModIdeals (localCohomology.idealPowersDiagram I)).map g.unop
        change derivedExtZeroQuotientEvaluation (I ^ unop (unop k)) M
            ((CategoryTheory.Abelian.Ext.mk₀ q).comp α (zero_add 0)) =
          derivedExtZeroQuotientEvaluation (I ^ unop (unop j)) M α
        obtain ⟨f, rfl⟩ := (CategoryTheory.Abelian.Ext.mk₀_bijective _ _).surjective α
        let f' : ModuleCat.of R (R ⧸ I ^ unop (unop j)) ⟶ M := f
        change derivedExtZeroQuotientEvaluation (I ^ unop (unop k)) M
            ((CategoryTheory.Abelian.Ext.mk₀ q).comp
              (CategoryTheory.Abelian.Ext.mk₀ f') (zero_add 0)) =
          derivedExtZeroQuotientEvaluation (I ^ unop (unop j)) M
            (CategoryTheory.Abelian.Ext.mk₀ f')
        rw [CategoryTheory.Abelian.Ext.mk₀_comp_mk₀,
          derivedExtZeroQuotientEvaluation_mk₀, derivedExtZeroQuotientEvaluation_mk₀]
        change f'.hom (q.hom (Ideal.Quotient.mk (I ^ unop (unop k)) (1 : R))) =
          f'.hom (Ideal.Quotient.mk (I ^ unop (unop j)) (1 : R))
        congr 1 }
def

derivedLocalCohomologyZeroEvaluation

L109 ↗
EtaleFundamentalGroups.derivedLocalCohomologyZeroEvaluation
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
def derivedLocalCohomologyZeroEvaluation
    (I : Ideal R) (M : ModuleCat.{u} R) :
    derivedLocalCohomology I M 0 ⟶ AddCommGrpCat.of M
theorem

derivedLocalCohomologyZeroEvaluation_ι

L115 ↗
EtaleFundamentalGroups.derivedLocalCohomologyZeroEvaluation_ι
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 derivedLocalCohomologyZeroEvaluation_ι
    (I : Ideal R) (M : ModuleCat.{u} R) (n : ℕ)
    (α : CategoryTheory.Abelian.Ext.{u} (ModuleCat.of R (R ⧸ I ^ n)) M 0) :
    derivedLocalCohomologyZeroEvaluation I M
        (colimit.ι (derivedLocalCohomologyPowersDiagram I M 0) (op (op n)) α) =
      derivedExtZeroQuotientEvaluation (I ^ n) M α
def

derivedLocalCohomologyZeroToModule

L126 ↗
EtaleFundamentalGroups.derivedLocalCohomologyZeroToModule
Documentation

Degree-zero local cohomology maps linearly to its coefficient module by evaluation of quotient homomorphisms at one.

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 derivedLocalCohomologyZeroToModule (I : Ideal R) (M : ModuleCat.{u} R) :
    derivedLocalCohomologyModule I M 0 →ₗ[R] M where
  toFun := ConcreteCategory.hom (derivedLocalCohomologyZeroEvaluation I M)
  map_add' := map_add (ConcreteCategory.hom
    (derivedLocalCohomologyZeroEvaluation I M))
  map_smul' a z := by
    let : PreservesFilteredColimitsOfSize.{0, 0} (forget AddCommGrpCat.{u}) :=
      preservesSmallestFilteredColimits_of_preservesFilteredColimits _
    obtain ⟨k, α, hα⟩ :=
      Concrete.colimit_exists_rep (derivedLocalCohomologyPowersDiagram I M 0) z
    rcases k with ⟨⟨n⟩⟩
    change derivedLocalCohomologyZeroEvaluation I M
      (derivedLocalCohomologyScalarMap I M 0 a z) =
        a • derivedLocalCohomologyZeroEvaluation I M z
    rw [← hα]
    change CategoryTheory.Abelian.Ext.{u} (ModuleCat.of R (R ⧸ I ^ n)) M 0 at α
    exact (congrArg (derivedLocalCohomologyZeroEvaluation I M)
      (derivedLocalCohomologyScalarMap_ι_apply I M 0 a n α)).trans
        ((derivedLocalCohomologyZeroEvaluation_ι I M n (a • α)).trans
          ((map_smul (derivedExtZeroQuotientEvaluation (I ^ n) M) a α).trans
            (congrArg (fun z : M => a • z)
              (derivedLocalCohomologyZeroEvaluation_ι I M n α).symm)))
theorem

derivedLocalCohomologyZeroToModule_ι

L149 ↗
EtaleFundamentalGroups.derivedLocalCohomologyZeroToModule_ι
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 derivedLocalCohomologyZeroToModule_ι
    (I : Ideal R) (M : ModuleCat.{u} R) (n : ℕ)
    (α : CategoryTheory.Abelian.Ext.{u} (ModuleCat.of R (R ⧸ I ^ n)) M 0) :
    derivedLocalCohomologyZeroToModule I M (derivedLocalCohomologyModuleι I M 0 n α) =
      derivedExtZeroQuotientEvaluation (I ^ n) M α
theorem

derivedLocalCohomologyZeroToModule_ι_mk₀

L158 ↗
EtaleFundamentalGroups.derivedLocalCohomologyZeroToModule_ι_mk₀
Documentation

Evaluation of a degree-zero representative given by a quotient homomorphism is its value at one.

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 derivedLocalCohomologyZeroToModule_ι_mk₀
    (I : Ideal R) (M : ModuleCat.{u} R) (n : ℕ)
    (f : ModuleCat.of R (R ⧸ I ^ n) ⟶ M) :
    derivedLocalCohomologyZeroToModule I M
        (derivedLocalCohomologyModuleι I M 0 n (CategoryTheory.Abelian.Ext.mk₀ f)) =
      f.hom (Ideal.Quotient.mk (I ^ n) 1)
theorem

eq_zero_of_map_eq_of_eq_zero

L167 ↗
EtaleFundamentalGroups.eq_zero_of_map_eq_of_eq_zero
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 eq_zero_of_map_eq_of_eq_zero
    {A B : AddCommGrpCat.{u}} (f : A ⟶ B) {x : A} {y : B}
    (hx : x = 0) (hy : f x = y) : y = 0
theorem

derivedLocalCohomologyZeroToModule_injective

L176 ↗
EtaleFundamentalGroups.derivedLocalCohomologyZeroToModule_injective
Documentation

No degree-zero class is lost on evaluation in the coefficient module.

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 derivedLocalCohomologyZeroToModule_injective (I : Ideal R) (M : ModuleCat.{u} R) :
    Function.Injective (derivedLocalCohomologyZeroToModule I M)
theorem

derivedLocalCohomologyZeroToModule_exists_preimage

L197 ↗
EtaleFundamentalGroups.derivedLocalCohomologyZeroToModule_exists_preimage
Documentation

Every ideal-power torsion vector is represented by a degree-zero local-cohomology class.

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 derivedLocalCohomologyZeroToModule_exists_preimage
    (I : Ideal R) (M : ModuleCat.{u} R) (z : M)
    (hz : ∃ n : ℕ, ∀ a ∈ I ^ n, a • z = 0) :
    ∃ α : derivedLocalCohomologyModule I M 0,
      derivedLocalCohomologyZeroToModule I M α = z
theorem

mem_range_derivedLocalCohomologyZeroToModule_iff

L213 ↗
EtaleFundamentalGroups.mem_range_derivedLocalCohomologyZeroToModule_iff
Documentation

The image of degree-zero evaluation consists exactly of the ideal-power torsion vectors.

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 mem_range_derivedLocalCohomologyZeroToModule_iff
    (I : Ideal R) (M : ModuleCat.{u} R) (z : M) :
    z ∈ LinearMap.range (derivedLocalCohomologyZeroToModule I M) ↔
      ∃ n : ℕ, ∀ a ∈ I ^ n, a • z = 0
theorem

derivedLocalCohomologyZeroToModule_bijective_of_power_torsion

L228 ↗
EtaleFundamentalGroups.derivedLocalCohomologyZeroToModule_bijective_of_power_torsion
Documentation

On an ideal-power torsion module, degree-zero local cohomology is the entire coefficient module.

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 derivedLocalCohomologyZeroToModule_bijective_of_power_torsion
    (I : Ideal R) (M : ModuleCat.{u} R)
    (hM : ∀ z : M, ∃ n : ℕ, ∀ a ∈ I ^ n, a • z = 0) :
    Function.Bijective (derivedLocalCohomologyZeroToModule I M)

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