Cofinal subsequences of module towers

Restriction of compatible families to a cofinal monotone sequence of indices is a linear equivalence. Repeated indices are allowed, and no surjectivity or Mittag--Leffler condition on the transitions is needed. The inverse is characterized at any original index by transition from any later index in the subsequence. In particular it makes no choice of an inverse to a transition map.

The equivalence is natural in morphisms of towers. It uses Mathlib's cofinality criterion Monotone.final_functor_iff and Functor.Initial.isLimitWhiskerEquiv, applied to ModuleTower.isLimitLimCone, rather than reconstructing the categorical limit.

References

• C. A. Weibel, An introduction to homological algebra, §3.5.

@[reducible, inline]

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

The module tower sampled along a monotone sequence of indices.

@[simp]

theorem TauCeti.ModuleTower.subsequence_transitionOfLE {R : Type u} [Ring R] (F : ModuleTower R) (φ : ℕ →o ℕ) {n m : ℕ} (h : n ≤ m) : (F.subsequence φ).transitionOfLE h = F.transitionOfLE ⋯

@[simp]

theorem TauCeti.ModuleTower.subsequence_transition {R : Type u} [Ring R] (F : ModuleTower R) (φ : ℕ →o ℕ) (n : ℕ) : (F.subsequence φ).transition n = F.transitionOfLE ⋯

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

Restriction of a product family along φ.

@[simp]

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

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

Restricting compatible families to a cofinal monotone sequence preserves the inverse limit. The forward map is restriction, even when the sequence repeats indices.

@[simp]

theorem TauCeti.ModuleTower.coe_limSubsequenceEquiv_apply {R : Type u} [Ring R] (F : ModuleTower R) (φ : ℕ →o ℕ) (hφ : ∀ (n : ℕ), ∃ (m : ℕ), n ≤ φ m) (x : ↥F.lim) (n : ℕ) : ↑((F.limSubsequenceEquiv φ hφ) x) n = ↑x (φ n)

The cofinal comparison restricts a compatible family to the selected indices.

theorem TauCeti.ModuleTower.coe_limSubsequenceEquiv_symm_apply {R : Type u} [Ring R] (F : ModuleTower R) (φ : ℕ →o ℕ) (hφ : ∀ (n : ℕ), ∃ (m : ℕ), n ≤ φ m) (x : ↥(F.subsequence φ).lim) {n m : ℕ} (hnm : n ≤ φ m) : ↑((F.limSubsequenceEquiv φ hφ).symm x) n = (F.transitionOfLE hnm) (↑x m)

Recover an original coordinate by transition from any later selected coordinate. This also shows that reconstruction is independent of the selected later index.

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

Cofinal restriction is natural in morphisms of module towers.

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

Restriction along φ commutes with the product map of a morphism of towers.