Module

IdealPowerTorsionFunctor.lean

Nyll.EtaleFundamentalGroups.Purity.IdealPowerTorsionFunctor

6 declarations indexed from sourceView source ↗

Module documentation

The ideal-power torsion functor and its injective-resolution complex

The functor takes the submodule of elements killed by a power of an ideal. Its maps are restrictions of the original linear maps, so its inclusion into the identity functor is natural and it is additive. Applying it termwise to an injective resolution gives the concrete complex used to compute derived ideal-power torsion.

Imports5

Mathlib.Algebra.Category.ModuleCat.Basic
Mathlib.Algebra.Homology.Additive
Mathlib.Algebra.Module.Torsion.PrimaryComponent
Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Imported by8

def

idealPowerTorsionFunctor

L35 ↗

EtaleFundamentalGroups.Purity.idealPowerTorsionFunctor

Documentation

The submodule of elements annihilated by some power of I, functorially in the coefficient module.

Source context 5 commands

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

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

Lean source · full declaration

def idealPowerTorsionFunctor (I : Ideal R) :
    ModuleCat.{u} R ⥤ ModuleCat.{u} R where
  obj M := ModuleCat.of R (Ideal.primaryComponent M I)
  map f := ModuleCat.ofHom (Ideal.primaryComponent.map I f.hom)
  map_id M := by
    ext z
    rfl
  map_comp f g := by
    ext z
    rfl

instance

(anonymous instance)

L46 ↗

Source context 5 commands

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

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

Lean source · full declaration

instance (I : Ideal R) : (idealPowerTorsionFunctor I).Additive where
  map_add := by
    intro M N f g
    ext z
    rfl

def

idealPowerTorsionInclusion

L53 ↗

EtaleFundamentalGroups.Purity.idealPowerTorsionInclusion

Documentation

The canonical inclusion of power torsion into the original module.

Source context 5 commands

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

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

Lean source · full declaration

def idealPowerTorsionInclusion (I : Ideal R) :
    idealPowerTorsionFunctor I ⟶ 𝟭 (ModuleCat.{u} R) where
  app M := ModuleCat.ofHom (Ideal.primaryComponent M I).subtype
  naturality _ _ f := by
    ext z
    rfl

def

idealPowerTorsionComplex

L61 ↗

EtaleFundamentalGroups.Purity.idealPowerTorsionComplex

Documentation

Applying ideal-power torsion to every term and differential.

Source context 5 commands

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

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

Lean source · statement

def idealPowerTorsionComplex (I : Ideal R)
    (K : CochainComplex (ModuleCat.{u} R) ℕ) :
    CochainComplex (ModuleCat.{u} R) ℕ

def

derivedLocalCohomologyInjectiveComplex

L67 ↗

EtaleFundamentalGroups.Purity.derivedLocalCohomologyInjectiveComplex

Documentation

The torsion complex of an explicitly chosen injective resolution.

Source context 5 commands

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

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

Lean source · statement

def derivedLocalCohomologyInjectiveComplex (I : Ideal R)
    {M : ModuleCat.{u} R} (J : InjectiveResolution M) :
    CochainComplex (ModuleCat.{u} R) ℕ

theorem

idealPowerTorsionComplex_d_apply

L73 ↗

EtaleFundamentalGroups.Purity.idealPowerTorsionComplex_d_apply

Documentation

The differential is the original differential restricted to torsion.

Source context 5 commands

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

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

Lean source · full declaration

theorem idealPowerTorsionComplex_d_apply (I : Ideal R)
    (K : CochainComplex (ModuleCat.{u} R) ℕ) (p q : ℕ)
    (z : (idealPowerTorsionComplex I K).X p) :
    ((show Ideal.primaryComponent (K.X q) I from
        ((idealPowerTorsionComplex I K).d p q) z) : K.X q) =
      K.d p q ((show Ideal.primaryComponent (K.X p) I from z) : K.X p) :=
  rfl

Module documentation

The ideal-power torsion functor and its injective-resolution complex

Declarations

idealPowerTorsionFunctor

(anonymous instance)

idealPowerTorsionInclusion

idealPowerTorsionComplex

derivedLocalCohomologyInjectiveComplex

idealPowerTorsionComplex_d_apply