Pro-zero towers of modules

A tower of modules A₀ ← A₁ ← A₂ ← ⋯ is pro-zero (CategoryTheory.Functor.IsProZero) when every term Aₙ is killed by some composite transition Aₘ → Aₙ. This file shows that a pro-zero tower has lim A = 0 and lim¹ A = 0, so pro-zero error terms are invisible to lim and lim¹.

The basic family of examples is the tower R ← R ← ⋯ whose transitions are right multiplication by an element a: it is pro-zero exactly when a is nilpotent. In particular, for a prime p the tower ℤ ← ℤ ← ⋯ with transitions multiplication by p is not pro-zero.

Main declarations

• TauCeti.ModuleTower.isProZero_iff_exists_transitionOfLE_eq_zero: a tower of modules is pro-zero exactly when every term is killed by some composite transition transitionOfLE.
• TauCeti.ModuleTower.lim_eq_bot_of_isProZero, TauCeti.ModuleTower.subsingleton_limOne_of_isProZero: pro-zero towers have vanishing lim and lim¹; TauCeti.ModuleTower.isMittagLeffler_of_isProZero: they are Mittag-Leffler.
• TauCeti.ModuleTower.multiplicationTower: the tower R ← R ← ⋯ with transitions right multiplication by a.
• TauCeti.ModuleTower.multiplicationTowerProductEquiv: the product of its terms is the module of sequences ℕ → R, on which the shift is δ(x)ₙ = xₙ - xₙ₊₁ * a (TauCeti.ModuleTower.multiplicationTowerProductEquiv_shift).
• TauCeti.ModuleTower.lim_multiplicationTower_eq_bot: for an integer p that is not a unit, the multiplication-by-p tower of integers has lim = 0.
• TauCeti.ModuleTower.isProZero_multiplicationTower_iff: it is pro-zero exactly when a is nilpotent; TauCeti.ModuleTower.isProZero_multiplicationTower_iff_eq_zero is the case of a reduced ring.

References

• B. Bhatt, On the direct summand conjecture and its derived variant, Invent. Math. 212 (2018), §3 (pro-zero towers, in their almost form).

theorem TauCeti.ModuleTower.isProZero_iff_exists_transitionOfLE_eq_zero {R : Type u} [Ring R] (F : ModuleTower R) : CategoryTheory.Functor.IsProZero F ↔ ∀ (n : ℕ), ∃ (m : ℕ) (h : n ≤ m), F.transitionOfLE h = 0

A tower of modules is pro-zero exactly when every term Aₙ is killed by some composite transition Aₘ → Aₙ.

theorem TauCeti.ModuleTower.lim_eq_bot_of_isProZero {R : Type u} [Ring R] {F : ModuleTower R} (hF : CategoryTheory.Functor.IsProZero F) : F.lim = ⊥

A pro-zero tower has lim A = 0.

theorem TauCeti.ModuleTower.isMittagLeffler_of_isProZero {R : Type u} [Ring R] {F : ModuleTower R} (hF : CategoryTheory.Functor.IsProZero F) : F.IsMittagLeffler

A pro-zero tower is Mittag-Leffler: the images of the composite transitions into each term are eventually zero.

theorem TauCeti.ModuleTower.subsingleton_limOne_of_isProZero {R : Type u} [Ring R] {F : ModuleTower R} (hF : CategoryTheory.Functor.IsProZero F) : Subsingleton F.limOne

A pro-zero tower has lim¹ A = 0.

def TauCeti.ModuleTower.multiplicationTower {R : Type u} [Ring R] (a : R) : ModuleTower R

The tower R ← R ← R ← ⋯ of left R-modules whose transition maps are right multiplication x ↦ x * a by an element a.

@[simp]

theorem TauCeti.ModuleTower.multiplicationTower_obj {R : Type u} [Ring R] (a : R) (n : ℕ) : (multiplicationTower a).obj (Opposite.op n) = ↧R

@[simp]

theorem TauCeti.ModuleTower.multiplicationTower_transition {R : Type u} [Ring R] (a : R) (n : ℕ) : (multiplicationTower a).transition n = LinearMap.toSpanSingleton R R a

@[simp]

theorem TauCeti.ModuleTower.multiplicationTower_transitionOfLE {R : Type u} [Ring R] (a : R) {n k : ℕ} (h : n ≤ k) : (multiplicationTower a).transitionOfLE h = LinearMap.toSpanSingleton R R (a ^ (k - n))

The composite transition Aₖ → Aₙ of multiplicationTower a is right multiplication by a ^ (k - n).

def TauCeti.ModuleTower.multiplicationTowerProductEquiv {R : Type u} [Ring R] (a : R) : (multiplicationTower a).Product ≃ₗ[R] ℕ → R

The terms of multiplicationTower a are R itself, so the product of its terms is the module of sequences ℕ → R.

theorem TauCeti.ModuleTower.multiplicationTowerProductEquiv_apply {R : Type u} [Ring R] (a : R) (x : (multiplicationTower a).Product) (n : ℕ) : (multiplicationTowerProductEquiv a) x n = x n

The n-th term of the sequence attached to a family x is its component xₙ. Not @[simp]: it would rewrite the left-hand side of multiplicationTowerProductEquiv_shift.

theorem TauCeti.ModuleTower.multiplicationTowerProductEquiv_symm_apply {R : Type u} [Ring R] (a : R) (x : ℕ → R) (n : ℕ) : (multiplicationTowerProductEquiv a).symm x n = x n

The component xₙ of the family attached to a sequence x is its n-th term.

@[simp]

theorem TauCeti.ModuleTower.multiplicationTowerProductEquiv_shift {R : Type u} [Ring R] (a : R) (x : (multiplicationTower a).Product) (n : ℕ) : (multiplicationTowerProductEquiv a) ((multiplicationTower a).shift x) n = (multiplicationTowerProductEquiv a) x n - (multiplicationTowerProductEquiv a) x (n + 1) * a

The shift map of multiplicationTower a, as a map of sequences: δ(x)ₙ = xₙ - xₙ₊₁ * a.

theorem TauCeti.ModuleTower.mem_lim_multiplicationTower_iff {R : Type u} [Ring R] {a : R} {x : (multiplicationTower a).Product} : x ∈ (multiplicationTower a).lim ↔ ∀ (n : ℕ), (multiplicationTowerProductEquiv a) x (n + 1) * a = (multiplicationTowerProductEquiv a) x n

A sequence lies in lim of multiplicationTower a exactly when xₙ₊₁ * a = xₙ for all n.

theorem TauCeti.ModuleTower.lim_multiplicationTower_eq_bot {p : ℤ} (hp : ¬IsUnit p) : (multiplicationTower p).lim = ⊥

The multiplication-by-p tower has vanishing limit for every integer p that is not a unit: every term of a compatible family is divisible by every power of p.

theorem TauCeti.ModuleTower.isProZero_multiplicationTower_iff {R : Type u} [Ring R] (a : R) : CategoryTheory.Functor.IsProZero (multiplicationTower a) ↔ IsNilpotent a

The multiplication tower is pro-zero exactly for nilpotent elements.

theorem TauCeti.ModuleTower.isProZero_multiplicationTower_iff_eq_zero {R : Type u} [Ring R] [IsReduced R] (a : R) : CategoryTheory.Functor.IsProZero (multiplicationTower a) ↔ a = 0

Over a reduced ring the multiplication tower by a is pro-zero only for a = 0. For instance, for a prime p the tower ℤ ← ℤ ← ⋯ with transitions multiplication by p is not pro-zero.