NYLL
Module

PrincipalLocalizationHomotopy.lean

Nyll.EtaleFundamentalGroups.Purity.PrincipalLocalizationHomotopy
11 declarations indexed from sourceView source ↗

Module documentation

The principal localization complex of an injective module

The localization sequence splits because its kernel is an injective primary component. In particular the localized term is injective. The actual inclusion of the primary component in degree zero is a quasi-isomorphism between complexes of injectives, hence a homotopy equivalence.

Imports13
Imported by3

Declarations

theorem

primaryComponent_localization_comp_eq_zero

L41 ↗
EtaleFundamentalGroups.Purity.primaryComponent_localization_comp_eq_zero
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits
variable {R : Type u} [CommRing R]
Lean source · statement
theorem primaryComponent_localization_comp_eq_zero
    (x : R) (M : ModuleCat.{u} R) :
    (LocalizedModule.mkLinearMap (Submonoid.powers x) M).comp
      (Ideal.primaryComponent M (Ideal.span {x})).subtype = 0
def

principalLocalizationSequence

L51 ↗
EtaleFundamentalGroups.Purity.principalLocalizationSequence
Documentation

The principal primary component, the module, and its localization.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits
variable {R : Type u} [CommRing R]
Lean source · statement
def principalLocalizationSequence (x : R) (M : ModuleCat.{u} R) :
    ShortComplex (ModuleCat.{u} R)
theorem

principalLocalizationSequence_shortExact

L58 ↗
EtaleFundamentalGroups.Purity.principalLocalizationSequence_shortExact
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits
variable {R : Type u} [CommRing R]
Lean source · statement
theorem principalLocalizationSequence_shortExact
    [IsNoetherianRing R] (x : R) (M : ModuleCat.{u} R) [Module.Injective R M] :
    (principalLocalizationSequence x M).ShortExact
theorem

moduleInjective_localizedModule_powers

L71 ↗
EtaleFundamentalGroups.Purity.moduleInjective_localizedModule_powers
Documentation

Localization of an injective module at one element is injective, as a retract of the original module.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits
variable {R : Type u} [CommRing R]
Lean source · statement
theorem moduleInjective_localizedModule_powers
    [IsNoetherianRing R] (x : R) (M : ModuleCat.{u} R) [Module.Injective R M] :
    Module.Injective R (LocalizedModule (Submonoid.powers x) M)
def

principalLocalizationInclusion

L85 ↗
EtaleFundamentalGroups.Purity.principalLocalizationInclusion
Documentation

The inclusion of principal power torsion into the localization complex, concentrated in degree zero at the source.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits
variable {R : Type u} [CommRing R]
Lean source · statement
def principalLocalizationInclusion (x : R) (M : ModuleCat.{u} R) :
    (CochainComplex.single₀ (ModuleCat.{u} R)).obj
        (ModuleCat.of R (Ideal.primaryComponent M (Ideal.span {x}))) ⟶
      principalLocalizationComplex x M
theorem

principalLocalizationInclusion_quasiIsoAt_zero

L93 ↗
EtaleFundamentalGroups.Purity.principalLocalizationInclusion_quasiIsoAt_zero
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits
variable {R : Type u} [CommRing R]
Lean source · statement
theorem principalLocalizationInclusion_quasiIsoAt_zero
    (x : R) (M : ModuleCat.{u} R) :
    QuasiIsoAt (principalLocalizationInclusion x M) 0
theorem

principalLocalizationInclusion_quasiIso

L133 ↗
EtaleFundamentalGroups.Purity.principalLocalizationInclusion_quasiIso
Documentation

The torsion inclusion is a quasi-isomorphism for injective coefficients over a Noetherian ring.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits
variable {R : Type u} [CommRing R]
Lean source · statement
theorem principalLocalizationInclusion_quasiIso
    [IsNoetherianRing R] (x : R) (M : ModuleCat.{u} R) [Module.Injective R M] :
    QuasiIso (principalLocalizationInclusion x M)
def

principalLocalizationHomotopyData

L148 ↗
EtaleFundamentalGroups.Purity.principalLocalizationHomotopyData
Documentation

The principal localization complex of an injective module is homotopy equivalent to its primary component in degree zero.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits
variable {R : Type u} [CommRing R]
Lean source · statement
def principalLocalizationHomotopyData
    [IsNoetherianRing R] (x : R) (M : ModuleCat.{u} R) [Module.Injective R M] :
    {e : HomotopyEquiv
      ((CochainComplex.single₀ (ModuleCat.{u} R)).obj
        (ModuleCat.of R (Ideal.primaryComponent M (Ideal.span {x}))))
      (principalLocalizationComplex x M) // e.hom = principalLocalizationInclusion x M}
def

principalLocalizationHomotopyEquiv

L182 ↗
EtaleFundamentalGroups.Purity.principalLocalizationHomotopyEquiv
Documentation

The principal localization contraction with its specified forward map.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits
variable {R : Type u} [CommRing R]
Lean source · statement
def principalLocalizationHomotopyEquiv
    [IsNoetherianRing R] (x : R) (M : ModuleCat.{u} R) [Module.Injective R M] :
    HomotopyEquiv
      ((CochainComplex.single₀ (ModuleCat.{u} R)).obj
        (ModuleCat.of R (Ideal.primaryComponent M (Ideal.span {x}))))
      (principalLocalizationComplex x M)
theorem

principalLocalizationHomotopyEquiv_hom

L191 ↗
EtaleFundamentalGroups.Purity.principalLocalizationHomotopyEquiv_hom
Documentation

The forward map of the contraction is the specified torsion inclusion.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits
variable {R : Type u} [CommRing R]
Lean source · statement
theorem principalLocalizationHomotopyEquiv_hom
    [IsNoetherianRing R] (x : R) (M : ModuleCat.{u} R) [Module.Injective R M] :
    (principalLocalizationHomotopyEquiv x M).hom = principalLocalizationInclusion x M
theorem

principalLocalizationHomotopyEquiv_hom_f_zero

L197 ↗
EtaleFundamentalGroups.Purity.principalLocalizationHomotopyEquiv_hom_f_zero
Documentation

In degree zero the specified forward map is the inclusion of torsion.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits
variable {R : Type u} [CommRing R]
Lean source · statement
theorem principalLocalizationHomotopyEquiv_hom_f_zero
    [IsNoetherianRing R] (x : R) (M : ModuleCat.{u} R) [Module.Injective R M] :
    (principalLocalizationHomotopyEquiv x M).hom.f 0 =
      ModuleCat.ofHom (Ideal.primaryComponent M (Ideal.span {x})).subtype

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