Tor of modules: flatness, short exact sequences and locally nilpotent endomorphisms #
Let A be a commutative ring and φ i a family of endomorphisms of an A-module Y that is
locally nilpotent: every element of Y is killed by all sufficiently long composites of the maps
φ i, which is to say ⨆ d, Module.End.wordKer (fun i ↦ (φ i).hom) d = ⊤. Then for every
A-module N and every n, the induced family of endomorphisms of Mathlib's
Tor'ₙ^A(N, Y), the derived functor of the tensor product in its first variable, is again
locally nilpotent (CategoryTheory.iSup_wordKer_Tor'_map_eq_top).
Indeed Tor'ₙ^A(N, Y) is the homology of P ⊗ Y for a projective resolution P of N, with
the maps φ i acting through the second factor. Local nilpotence passes to tensor products
(Module.End.iSup_wordKer_lTensor_eq_top) and from a complex to its homology
(HomologicalComplex.iSup_wordKer_homologyMap_eq_top).
A typical family is that of operators lowering a grading of Y by ℕ, such as the
divided-difference operators on a polynomial ring. This is how the divided-difference argument
for the invariants of a reflection group reaches Tor' without a grading on Tor' itself.
The vanishing of Tor'₁^A(N, M) for all N implies that M is flat
(ModuleCat.flat_of_isZero_Tor'_one). It suffices to apply this vanishing to N = A ⧸ I:
a projective resolution of I, augmented by its inclusion into A, computes this Tor'₁
and detects injectivity of I ⊗ M → A ⊗ M.
Mathlib's Tor, which derives the second variable, is computed by X ⊗ P for a projective
resolution P of M. The terms of P are flat, so a short exact sequence
0 → X₁ → X₂ → X₃ → 0 gives a short exact sequence of complexes Xᵢ ⊗ P, and its long exact
homology sequence relates the groups Torₙ(Xᵢ, M). We record the vanishing statements it gives:
Torₙ(X₂, M) vanishes with Torₙ(X₁, M) and Torₙ(X₃, M)
(CategoryTheory.ShortComplex.ShortExact.isZero_Tor_X₂), in particular Torₙ(X × Y, M) vanishes
with Torₙ(X, M) and Torₙ(Y, M) (ModuleCat.isZero_Tor_prod), Torₙ₊₁(X₃, M) vanishes with
Torₙ₊₁(X₂, M) and Torₙ(X₁, M) (CategoryTheory.ShortComplex.ShortExact.isZero_Tor_succ_X₃),
and Tor₁(X₃, M) vanishes with Tor₁(X₂, M) when X₁ ⊗ M → X₂ ⊗ M is injective
(CategoryTheory.ShortComplex.ShortExact.isZero_Tor_one_X₃). Flat modules have vanishing higher
Tor (ModuleCat.isZero_Tor_succ_of_flat), and Torₙ₊₁(X ⧸ N, M) vanishes when N is a directed
union of submodules Nᵢ with Torₙ₊₁(X ⧸ Nᵢ, M) = 0
(ModuleCat.isZero_Tor_succ_quotient_iSup), since an element of N ⊗ P already comes from a
finitely generated submodule of N.
Tor vanishing is invariant under flat base change: for a flat ring homomorphism f : A →+* B,
a B-module M and an A-module N, Torₙ^A(M, N) vanishes exactly when
Torₙ^B(M, B ⊗[A] N) does (ModuleCat.isZero_Tor_restrictScalars_iff). Extension of scalars
along f carries a projective resolution of N to one of B ⊗[A] N, and
M ⊗[B] (B ⊗[A] -) ≅ M ⊗[A] - (ModuleCat.extendScalarsCompTensorLeftIso).
References #
- C. A. Weibel, An Introduction to Homological Algebra, Cambridge Studies in Advanced
Mathematics 38, Cambridge University Press (1994), Section 2.4, for left derived functors
computed from a projective resolution, and Section 3.2 for
Torand flatness.
Tor' preserves local nilpotence in its underived variable. If every element of an
A-module Y is killed by all sufficiently long composites of the endomorphisms φ i, then every
element of Tor'ₙ^A(N, Y) is killed by all sufficiently long composites of the induced
endomorphisms.
A module is flat if its first Tor' with every module vanishes.
Tor along short exact sequences in the first variable #
Flat modules are Tor-acyclic. If X is flat, then Tor_{n+1}(X, M) = 0 for every
module M.
Tor of a quotient by a directed union. If N is a directed family of submodules of X
and Tor_{n+1}(X ⧸ N i, M) vanishes for every i, then Tor_{n+1}(X ⧸ ⨆ i, N i, M) vanishes.
Tor is half exact in the first variable: for a short exact sequence
0 → X₁ → X₂ → X₃ → 0, if Tor_n(X₁, M) and Tor_n(X₃, M) vanish then so does Tor_n(X₂, M).
Dimension shifting for Tor in the first variable: for a short exact sequence
0 → X₁ → X₂ → X₃ → 0, if Tor_{n+1}(X₂, M) and Tor_n(X₁, M) vanish then so does
Tor_{n+1}(X₃, M).
Tor₁ of a cokernel: for a short exact sequence 0 → X₁ → X₂ → X₃ → 0, if
Tor₁(X₂, M) vanishes and X₁ ⊗ M → X₂ ⊗ M is injective, then Tor₁(X₃, M) vanishes.
Tor of a product: if Torₙ(X, M) and Torₙ(Y, M) vanish then so does
Torₙ(X × Y, M), by half exactness along 0 → X → X × Y → Y → 0.
Flat base change #
Flat base change for the vanishing of Tor. For a flat ring homomorphism f : A →+* B, a
B-module M and an A-module N, Torₙ^A(M, N) vanishes exactly when Torₙ^B(M, B ⊗[A] N)
vanishes.