The first derived limit of a cofinal subsequence

Let φ : ℕ →o ℕ be cofinal, that is, every n is at most some φ m. Sampling a tower A along φ gives the tower n ↦ A_{φ n} with the composite transition maps; this covers subsequences, deleting finitely many initial terms, and repeating terms. By ModuleTower.limSubsequenceEquiv sampling does not change lim; this file shows that it does not change lim¹ either.

On products, restriction x ↦ (x_{φ n})ₙ does not commute with the shift maps δ(x)ₙ = xₙ - tₙ(xₙ₊₁), where tₙ is the transition map. Instead δ' ∘ res = Σ ∘ δ, where Σ sums the images in A_{φ n} of the coordinates φ n ≤ k < φ (n + 1). The pair (res, Σ) is a map between the two-term complexes δ and δ' whose kernels and cokernels are lim and lim¹, and it induces the lim¹ comparison. The key step is that a family x whose sum Σ x is a shift δ' w is itself a shift δ z with res z = w: the element z_k is the image of w_n plus the images of the x_j with k ≤ j < φ n, which is independent of the choice of n with k ≤ φ n. No surjectivity or Mittag-Leffler hypothesis is needed. The comparison is natural in morphisms of towers and, together with ModuleTower.limSubsequenceEquiv, compatible with the connecting map of the six-term sequence of a levelwise short exact sequence of towers. Consequently, a tower whose transitions are surjective from some index on has vanishing lim¹.

Main declarations

• TauCeti.ModuleTower.subsequenceSum: the map of products, intertwining the shift maps with TauCeti.ModuleTower.subsequenceRestriction (TauCeti.ModuleTower.subsequenceSum_comp_shift).
• TauCeti.ModuleTower.limOneSubsequenceEquiv: lim¹ A ≃ lim¹ (A ∘ φ), induced by subsequenceSum.
• TauCeti.ModuleTower.limOneSubsequenceEquiv_comp_connecting: compatibility with the connecting map lim C → lim¹ A.
• TauCeti.ModuleTower.subsingleton_limOne_of_surjective_of_le: towers with eventually surjective transitions have vanishing lim¹.

References

• Stacks: More on Algebra, Lemma 15.88.1, Tag 07KW
• C. A. Weibel, An introduction to homological algebra, §3.5.

def TauCeti.ModuleTower.subsequenceSum {R : Type u} [Ring R] (F : ModuleTower R) (φ : ℕ →o ℕ) : F.Product →ₗ[R] (F.subsequence φ).Product

The map of products sending x to the family whose n-th term is the sum of the images in A_{φ n} of the coordinates x_k, φ n ≤ k < φ (n + 1). It intertwines the shift maps with subsequenceRestriction (subsequenceSum_comp_shift).

@[simp]

theorem TauCeti.ModuleTower.subsequenceSum_apply {R : Type u} [Ring R] (F : ModuleTower R) (φ : ℕ →o ℕ) (x : F.Product) (n : ℕ) : (F.subsequenceSum φ) x n = ∑ i ∈ Finset.range (φ (n + 1) - φ n), (F.transitionOfLE ⋯) (x (φ n + i))

theorem TauCeti.ModuleTower.subsequenceSum_comp_shift {R : Type u} [Ring R] (F : ModuleTower R) (φ : ℕ →o ℕ) : F.subsequenceSum φ ∘ₗ F.shift = (F.subsequence φ).shift ∘ₗ F.subsequenceRestriction φ

Summing over the coordinates φ n ≤ k < φ (n + 1) intertwines the shift maps with restriction: Σ ∘ δ = δ' ∘ res.

theorem TauCeti.ModuleTower.subsequenceSum_shift {R : Type u} [Ring R] (F : ModuleTower R) (φ : ℕ →o ℕ) (x : F.Product) : (F.subsequenceSum φ) (F.shift x) = (F.subsequence φ).shift ((F.subsequenceRestriction φ) x)

noncomputable def TauCeti.ModuleTower.limOneSubsequenceEquiv {R : Type u} [Ring R] (F : ModuleTower R) (φ : ℕ →o ℕ) (hφ : ∀ (n : ℕ), ∃ (m : ℕ), n ≤ φ m) : F.limOne ≃ₗ[R] (F.subsequence φ).limOne

Cofinal subsequences preserve lim¹. The map is induced by subsequenceSum; no condition on the transition maps is needed.

@[simp]

theorem TauCeti.ModuleTower.limOneSubsequenceEquiv_mk {R : Type u} [Ring R] (F : ModuleTower R) (φ : ℕ →o ℕ) (hφ : ∀ (n : ℕ), ∃ (m : ℕ), n ≤ φ m) (x : F.Product) : (F.limOneSubsequenceEquiv φ hφ) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((F.subsequenceSum φ) x)

theorem TauCeti.ModuleTower.subsequenceSum_natural_apply {R : Type u} [Ring R] {F G : ModuleTower R} (φ : ℕ →o ℕ) (f : F ⟶ G) (x : F.Product) : (G.subsequenceSum φ) ((productMap f) x) = (productMap (⋯.functor.op.whiskerLeft f)) ((F.subsequenceSum φ) x)

subsequenceSum commutes with the product map of a morphism of towers.

theorem TauCeti.ModuleTower.limOneSubsequenceEquiv_naturality {R : Type u} [Ring R] {F G : ModuleTower R} (φ : ℕ →o ℕ) (hφ : ∀ (n : ℕ), ∃ (m : ℕ), n ≤ φ m) (f : F ⟶ G) : ↑(G.limOneSubsequenceEquiv φ hφ) ∘ₗ limOneMap f = limOneMap (⋯.functor.op.whiskerLeft f) ∘ₗ ↑(F.limOneSubsequenceEquiv φ hφ)

The comparison limOneSubsequenceEquiv is natural in morphisms of towers.

theorem TauCeti.ModuleTower.limOneSubsequenceEquiv_comp_connecting {R : Type u} [Ring R] {F G H : ModuleTower R} (φ : ℕ →o ℕ) (hφ : ∀ (n : ℕ), ∃ (m : ℕ), n ≤ φ m) {f : F ⟶ G} {g : G ⟶ H} (hf : ∀ (n : ℕ), Function.Injective ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n)))) (hfg : ∀ (n : ℕ), Function.Exact ⇑(ModuleCat.Hom.hom (f.app (Opposite.op n))) ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) (hg : ∀ (n : ℕ), Function.Surjective ⇑(ModuleCat.Hom.hom (g.app (Opposite.op n)))) : ↑(F.limOneSubsequenceEquiv φ hφ) ∘ₗ connecting f g hf hfg hg = connecting (⋯.functor.op.whiskerLeft f) (⋯.functor.op.whiskerLeft g) ⋯ ⋯ ⋯ ∘ₗ ↑(H.limSubsequenceEquiv φ hφ)

Cofinal restriction commutes with the connecting map. For a levelwise short exact sequence of towers 0 → A → B → C → 0, the comparisons lim C ≃ lim (C ∘ φ) (limSubsequenceEquiv) and lim¹ A ≃ lim¹ (A ∘ φ) intertwine the connecting maps of 0 → A → B → C → 0 and of its restriction along φ.

theorem TauCeti.ModuleTower.subsingleton_limOne_of_surjective_of_le {R : Type u} [Ring R] (F : ModuleTower R) (k : ℕ) (h : ∀ (n : ℕ), k ≤ n → Function.Surjective ⇑(F.transition n)) : Subsingleton F.limOne

Eventually surjective towers have vanishing lim¹. If the transition maps Aₙ₊₁ → Aₙ are surjective for all n ≥ k, then lim¹ A vanishes.