Module

CechLocalizationComplex.lean

Nyll.EtaleFundamentalGroups.Purity.CechLocalizationComplex

5 declarations indexed from sourceView source ↗

Module documentation

The bounded flat Čech complex of a finite list

Tensoring the two-term principal localization complexes gives a complex whose terms are flat and which ends in the degree given by the length of the list. All signs, summands, and differentials are supplied by the standard tensor product of homological complexes.

Imports5

Nyll.EtaleFundamentalGroups.Purity.PrincipalLocalizationComplex
Mathlib.Algebra.Category.ModuleCat.Biproducts
Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Mathlib.Algebra.Homology.Monoidal
Mathlib.LinearAlgebra.DFinsupp

Imported by5

instance

cochainNatTensorSigns

EtaleFundamentalGroups.Purity.cochainNatTensorSigns

Source context 6 commands

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

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

Lean source · full declaration

instance cochainNatTensorSigns : (ComplexShape.up ℕ).TensorSigns where
  ε' := MonoidHom.mk' (fun n : ℕ => (-1 : ℤˣ) ^ n) (pow_add (-1 : ℤˣ))
  rel_add p q r hpq := by
    change p + 1 = q at hpq
    change (p + r) + 1 = q + r
    omega
  add_rel p q r hpq := by
    change p + 1 = q at hpq
    change (r + p) + 1 = r + q
    omega
  ε'_succ := by
    intro p q hpq
    change p + 1 = q at hpq
    subst q
    change (-1 : ℤˣ) ^ (p + 1) = -((-1 : ℤˣ) ^ p)
    rw [pow_succ, mul_neg, mul_one]

def

cechLocalizationComplex

EtaleFundamentalGroups.Purity.cechLocalizationComplex

Documentation

The augmented Čech complex associated to a finite list of ring elements, constructed by tensoring the actual principal localization maps.

Source context 6 commands

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

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

Lean source · full declaration

def cechLocalizationComplex : List R → CochainComplex (ModuleCat.{u} R) ℕ
  | [] => HomologicalComplex.tensorUnit (ModuleCat.{u} R) (ComplexShape.up ℕ)
  | x :: xs => HomologicalComplex.tensorObj
      (principalLocalizationComplex x (ModuleCat.of R R)) (cechLocalizationComplex xs)

theorem

cechLocalizationComplex_isZero_X

EtaleFundamentalGroups.Purity.cechLocalizationComplex_isZero_X

Documentation

A finite Čech complex has no terms above the length of its list.

Source context 6 commands

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

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

Lean source · statement

theorem cechLocalizationComplex_isZero_X (xs : List R) (n : ℕ)
    (hn : xs.length < n) : IsZero ((cechLocalizationComplex xs).X n)

theorem

flat_finite_coproduct

EtaleFundamentalGroups.Purity.flat_finite_coproduct

Source context 6 commands

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

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

Lean source · statement

theorem flat_finite_coproduct {ι : Type} [Finite ι]
    (M : ι → ModuleCat.{u} R) (hM : ∀ i, Module.Flat R (M i)) :
    Module.Flat R (∐ M : ModuleCat.{u} R)

theorem

cechLocalizationComplex_flat_X

EtaleFundamentalGroups.Purity.cechLocalizationComplex_flat_X

Documentation

Every term of a finite Čech complex is flat over the original ring.

Source context 6 commands

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

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

Lean source · statement

theorem cechLocalizationComplex_flat_X (xs : List R) (n : ℕ) :
    Module.Flat R ((cechLocalizationComplex xs).X n)