Quasi-isomorphisms detected by module stalks

Module stalks preserve homology. A map of complexes of scheme-module sheaves is a quasi-isomorphism precisely when it is so at every module stalk.

Main definitions

The existing AlgebraicGeometry.Scheme.Modules.moduleStalkFunctor is the only stalk functor used here.

Main results

AlgebraicGeometry.Scheme.Modules.moduleStalkFunctor_preservesHomology and AlgebraicGeometry.Scheme.Modules.quasiIso_iff_stalkwise provide the exactness and detection statements.

Implementation notes

Additivity follows from finite-product preservation. Kernels and cokernels are preserved by finite-limit and parallel-pair-colimit preservation.

References

The proof uses Mathlib's homology-preservation criterion and the existing joint isomorphism reflection theorem for module stalks.

Tags

module stalk, quasi-isomorphism, homology

theorem AlgebraicGeometry.Scheme.Modules.moduleStalkFunctor_additive (X : Scheme) (x : ↥X) : (moduleStalkFunctor X x).Additive

Additivity follows from finite-product preservation, without computing with stalk representatives.

theorem AlgebraicGeometry.Scheme.Modules.moduleStalkFunctor_preservesParallelPairColimits (X : Scheme) (x : ↥X) : CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (moduleStalkFunctor X x)

Coequalizer preservation is a specialization of the small-colimit theorem for the existing module-stalk functor.

theorem AlgebraicGeometry.Scheme.Modules.moduleStalkFunctor_preservesHomology (X : Scheme) (x : ↥X) : (moduleStalkFunctor X x).PreservesHomology

Finite limits supply kernels and coequalizers supply cokernels, giving preservation of homology by module stalks.

theorem AlgebraicGeometry.Scheme.Modules.quasiIso_iff_stalkwise (X : Scheme) {ι : Type v} {c : ComplexShape ι} {K L : HomologicalComplex X.Modules c} (g : K ⟶ L) : QuasiIso g ↔ ∀ (x : ↥X), QuasiIso (((moduleStalkFunctor X x).mapHomologicalComplex c).map g)

Apply the pinned jointly-reflecting exact-functor criterion to all module stalks. This detects quasi-isomorphisms for every complex shape.