NYLL
Module

CechInjectiveHomotopy.lean

Nyll.EtaleFundamentalGroups.Purity.CechInjectiveHomotopy
9 declarations indexed from sourceView source ↗

Module documentation

Contraction of the Čech complex on injectives

The actual principal localization contraction is tensored with the remaining factors. Iteration identifies the Čech complex of an injective module with its ideal-power torsion, concentrated in degree zero.

Imports10
Imported by2

Declarations

def

tensorLeftHomotopyEquiv

L37 ↗
EtaleFundamentalGroups.Purity.tensorLeftHomotopyEquiv
Documentation

Tensoring a homotopy equivalence on the left preserves it.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
def tensorLeftHomotopyEquiv
    {K L : CochainComplex (ModuleCat.{u} R) ℕ}
    (e : HomotopyEquiv K L) (B : CochainComplex (ModuleCat.{u} R) ℕ) :
    HomotopyEquiv (HomologicalComplex.tensorObj K B)
      (HomologicalComplex.tensorObj L B)
def

cechNilHomotopyEquiv

L60 ↗
EtaleFundamentalGroups.Purity.cechNilHomotopyEquiv
Documentation

The empty-list contraction is formed at the coefficient-module level before any primary-component module is substituted.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
def cechNilHomotopyEquiv (M N : ModuleCat.{u} R) (e : M ≅ N) :
    HomotopyEquiv
      (((tensorLeft M).mapHomologicalComplex (ComplexShape.up ℕ)).obj
        (cechLocalizationComplex ([] : List R)))
      ((CochainComplex.single₀ (ModuleCat.{u} R)).obj N)
theorem

cechNilHomotopyEquiv_inv_f_zero

L72 ↗
EtaleFundamentalGroups.Purity.cechNilHomotopyEquiv_inv_f_zero
Documentation

The inverse empty-list contraction is the coefficient comparison followed by the inverse unit map in degree zero.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem cechNilHomotopyEquiv_inv_f_zero (M N : ModuleCat.{u} R) (e : M ≅ N) :
    (cechNilHomotopyEquiv M N e).inv.f 0 = e.inv ≫ (ρ_ M).inv
def

fullSubmoduleIso

L83 ↗
EtaleFundamentalGroups.Purity.fullSubmoduleIso
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
def fullSubmoduleIso (M : ModuleCat.{u} R)
    (N : Submodule R M) (hN : N = ⊤) : M ≅ ModuleCat.of R N
theorem

fullSubmoduleIso_inv

L88 ↗
EtaleFundamentalGroups.Purity.fullSubmoduleIso_inv
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem fullSubmoduleIso_inv (M : ModuleCat.{u} R)
    (N : Submodule R M) (hN : N = ⊤) :
    (fullSubmoduleIso M N hN).inv = ModuleCat.ofHom N.subtype
def

cechNilTorsionIso

L94 ↗
EtaleFundamentalGroups.Purity.cechNilTorsionIso
Documentation

Empty-support torsion is the whole module. Its inverse is constructed as the actual subtype map, avoiding transport through equal submodules.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
def cechNilTorsionIso (M : ModuleCat.{u} R) :
    M ≅ ModuleCat.of R (Ideal.primaryComponent M (Ideal.ofList ([] : List R)))
theorem

cechNilTorsionIso_inv

L107 ↗
EtaleFundamentalGroups.Purity.cechNilTorsionIso_inv
Documentation

The inverse empty-support identification is the specified inclusion.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem cechNilTorsionIso_inv (M : ModuleCat.{u} R) :
    (cechNilTorsionIso M).inv =
      ModuleCat.ofHom (Ideal.primaryComponent M (Ideal.ofList ([] : List R))).subtype
def

cechInjectiveHomotopyEquiv

L115 ↗
EtaleFundamentalGroups.Purity.cechInjectiveHomotopyEquiv
Documentation

The finite Čech complex with injective coefficients contracts to power torsion for the ideal generated by its list.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
def cechInjectiveHomotopyEquiv [IsNoetherianRing R]
    (xs : List R) (M : ModuleCat.{u} R) [Module.Injective R M] :
    HomotopyEquiv
      (((tensorLeft M).mapHomologicalComplex (ComplexShape.up ℕ)).obj
        (cechLocalizationComplex xs))
      ((CochainComplex.single₀ (ModuleCat.{u} R)).obj
        (ModuleCat.of R (Ideal.primaryComponent M (Ideal.ofList xs))))
theorem

cechInjective_exactAt_succ

L156 ↗
EtaleFundamentalGroups.Purity.cechInjective_exactAt_succ
Documentation

Positive Čech cohomology vanishes on injective modules.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem cechInjective_exactAt_succ [IsNoetherianRing R]
    (xs : List R) (M : ModuleCat.{u} R) [Module.Injective R M] (n : ℕ) :
    (((tensorLeft M).mapHomologicalComplex (ComplexShape.up ℕ)).obj
      (cechLocalizationComplex xs)).ExactAt (n + 1)

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