Tensoring torsion–reduction sequences

Tensoring over ℤ preserves injections whose target is killed by a prime: the injection splits additively. More generally it preserves exactness at any pair of maps whose final module is killed by a prime, because the inclusion of the second map's image splits. The tensor factor is an arbitrary abelian group; it need not be flat over ℤ. The additive splitting comes from AddMonoidHom.exists_comp_eq_of_injective in TauCeti.Algebra.Module.ZMod.Extend.

Applied to multiplication by p on a short exact sequence, this proves exactness of the scalar-extended six-term sequence of p-torsion and reduction modulo p. In particular it applies to a field of characteristic p, although that field is not flat over ℤ. This is the exactness input to additivity of the difference between reduction and torsion classes in the Grothendieck group of representations.

The two connecting-map lemmas below use TauCeti.torsionByδ, the multiplication-by-a-scalar snake map. The other terms follow from TauCeti.exact_torsionByMap and Mathlib's QuotSMulTop.map_exact; tensoring the first map preserves injectivity by LinearMap.lTensor_injective_of_isTorsionBy, and tensoring the last preserves surjectivity by Mathlib's LinearMap.lTensor_surjective.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, second edition, Section VII.3, (7.3.3).

theorem LinearMap.lTensor_injective_of_isTorsionBy (A : Type u_1) [AddCommGroup A] [Module ℤ A] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module ℤ M] [AddCommGroup N] [Module ℤ N] (f : M →ₗ[ℤ] N) (p : ℕ) [Fact (Nat.Prime p)] (hf : Function.Injective ⇑f) (hN : Module.IsTorsionBy ℤ N ↑p) : Function.Injective ⇑(lTensor A f)

Tensoring an injection into a module killed by a prime preserves injectivity, even when the tensor factor is not flat over ℤ.

theorem TauCeti.lTensor_exact_of_isTorsionBy (A : Type u_1) [AddCommGroup A] [Module ℤ A] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [Module ℤ M] [AddCommGroup N] [Module ℤ N] [AddCommGroup P] [Module ℤ P] {f : M →ₗ[ℤ] N} {g : N →ₗ[ℤ] P} (p : ℕ) [Fact (Nat.Prime p)] (hfg : Function.Exact ⇑f ⇑g) (hP : Module.IsTorsionBy ℤ P ↑p) : Function.Exact ⇑(LinearMap.lTensor A f) ⇑(LinearMap.lTensor A g)

Tensoring preserves exactness of a pair whose final module is killed by a prime. Neither surjectivity of the second map nor flatness of the tensor factor is required.

theorem TauCeti.lTensor_exact_torsionByMap_torsionByδ (A : Type u_1) [AddCommGroup A] [Module ℤ A] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [Module ℤ M] [AddCommGroup N] [Module ℤ N] [AddCommGroup P] [Module ℤ P] {f : M →ₗ[ℤ] N} {g : N →ₗ[ℤ] P} (p : ℕ) [Fact (Nat.Prime p)] (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) : Function.Exact ⇑(LinearMap.lTensor A (torsionByMap (↑p) g)) ⇑(LinearMap.lTensor A (torsionByδ (↑p) hfg hf hg))

Exactness at A ⊗[ℤ] P[p] in the tensor-extended torsion–reduction sequence.

theorem TauCeti.lTensor_exact_torsionByδ_quotSMulTop_map (A : Type u_1) [AddCommGroup A] [Module ℤ A] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [Module ℤ M] [AddCommGroup N] [Module ℤ N] [AddCommGroup P] [Module ℤ P] {f : M →ₗ[ℤ] N} {g : N →ₗ[ℤ] P} (p : ℕ) [Fact (Nat.Prime p)] (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) : Function.Exact ⇑(LinearMap.lTensor A (torsionByδ (↑p) hfg hf hg)) ⇑(LinearMap.lTensor A ((QuotSMulTop.map ↑p) f))

Exactness at A ⊗[ℤ] (M / pM) in the tensor-extended torsion–reduction sequence.