Module

PrincipalLocalizationComplex.lean

Nyll.EtaleFundamentalGroups.Purity.PrincipalLocalizationComplex

7 declarations indexed from sourceView source ↗

Module documentation

The two-term principal localization complex

The complex has a coefficient module in degree zero, its localization in degree one, and zero in higher degrees. Its positive cohomology vanishes on injective modules over Noetherian rings, and its terms preserve flatness.

Imports5

Nyll.EtaleFundamentalGroups.Purity.InjectiveModuleLocalization
Mathlib.Algebra.Category.ModuleCat.Abelian
Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Mathlib.RingTheory.Flat.Localization

Imported by5

def

principalLocalizationTerm

L31 ↗

EtaleFundamentalGroups.Purity.principalLocalizationTerm

Source context 5 commands

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

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

Lean source · full declaration

def principalLocalizationTerm (x : R) (M : ModuleCat.{u} R) :
    ℕ → ModuleCat.{u} R
  | 0 => M
  | 1 => ModuleCat.of R (LocalizedModule (Submonoid.powers x) M)
  | _ + 2 => ModuleCat.of R PUnit

def

principalLocalizationDifferential

L37 ↗

EtaleFundamentalGroups.Purity.principalLocalizationDifferential

Source context 5 commands

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

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

Lean source · full declaration

def principalLocalizationDifferential (x : R) (M : ModuleCat.{u} R) :
    ∀ n, principalLocalizationTerm x M n ⟶ principalLocalizationTerm x M (n + 1)
  | 0 => ModuleCat.ofHom (LocalizedModule.mkLinearMap (Submonoid.powers x) M)
  | _ + 1 => 0

def

principalLocalizationComplex

L44 ↗

EtaleFundamentalGroups.Purity.principalLocalizationComplex

Documentation

The augmented principal Čech complex M → M[1/x], in degrees zero and one.

Source context 5 commands

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

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

Lean source · statement

def principalLocalizationComplex (x : R) (M : ModuleCat.{u} R) :
    CochainComplex (ModuleCat.{u} R) ℕ

theorem

principalLocalizationComplex_isZero_X

L54 ↗

EtaleFundamentalGroups.Purity.principalLocalizationComplex_isZero_X

Documentation

No terms of a principal localization complex occur above degree one.

Source context 5 commands

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

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

Lean source · statement

theorem principalLocalizationComplex_isZero_X (x : R) (M : ModuleCat.{u} R)
    (n : ℕ) (hn : 1 < n) :
    IsZero ((principalLocalizationComplex x M).X n)

theorem

principalLocalizationComplex_ker_d_zero

L63 ↗

EtaleFundamentalGroups.Purity.principalLocalizationComplex_ker_d_zero

Documentation

The degree-zero cycles are exactly the elements annihilated by some power of the principal ideal.

Source context 5 commands

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

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

Lean source · statement

theorem principalLocalizationComplex_ker_d_zero (x : R) (M : ModuleCat.{u} R) :
    LinearMap.ker ((principalLocalizationComplex x M).d 0 1).hom =
      Ideal.primaryComponent M (Ideal.span {x})

theorem

principalLocalizationComplex_exactAt_succ

L71 ↗

EtaleFundamentalGroups.Purity.principalLocalizationComplex_exactAt_succ

Documentation

A principal localization complex of an injective module is exact in all strictly positive degrees.

Source context 5 commands

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

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

Lean source · statement

theorem principalLocalizationComplex_exactAt_succ
    [IsNoetherianRing R] (x : R) (M : ModuleCat.{u} R) [Module.Injective R M]
    (n : ℕ) : (principalLocalizationComplex x M).ExactAt (n + 1)

theorem

principalLocalizationComplex_flat_X

L89 ↗

EtaleFundamentalGroups.Purity.principalLocalizationComplex_flat_X

Documentation

Every term of the principal localization complex of a flat module is flat over the original ring.

Source context 5 commands

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

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

Lean source · statement

theorem principalLocalizationComplex_flat_X (x : R) (M : ModuleCat.{u} R)
    [Module.Flat R M] (n : ℕ) :
    Module.Flat R ((principalLocalizationComplex x M).X n)

Module documentation

The two-term principal localization complex

Declarations

principalLocalizationTerm

principalLocalizationDifferential

principalLocalizationComplex

principalLocalizationComplex_isZero_X

principalLocalizationComplex_ker_d_zero

principalLocalizationComplex_exactAt_succ

principalLocalizationComplex_flat_X