`lim` and `lim¹` of the multiplication-by-`p` tower #

Let p be a prime and consider the tower of integers ℤ ← ℤ ← ℤ ← ⋯ whose transition maps are multiplication by p, ModuleTower.multiplicationTower (p : ℤ). Its limit vanishes (ModuleTower.lim_multiplicationTower_eq_bot), but its first derived limit is the nonzero group ℤ_p ⧸ ℤ: sending a family (aₙ) to the p-adically convergent sum ∑ₙ pⁿ aₙ induces an isomorphism lim¹ ≃ ℤ_[p] ⧸ ℤ. Consequently the tower is not Mittag-Leffler, so the hypothesis of ModuleTower.subsingleton_limOne_of_isMittagLeffler cannot be dropped. The tower is the basic example of a nonvanishing lim¹: for instance the degree-zero homology of the tower of complexes ℤ → ℤ/pⁿ⁺¹ is the multiplication-by-p tower (up to isomorphism), and its lim¹ appears in the Milnor sequence of that tower.

Main declarations #

TauCeti.ModuleTower.padicSum: the p-adic summation map (aₙ) ↦ ∑ₙ pⁿ aₙ on the product of the terms, with TauCeti.ModuleTower.hasSum_padicSum.
TauCeti.ModuleTower.padicSum_shift: the telescoping identity ∑ₙ pⁿ (xₙ - p xₙ₊₁) = x₀.
TauCeti.ModuleTower.padicSum_surjective: every p-adic integer is such a sum.
TauCeti.ModuleTower.mem_range_shift_multiplicationTower_iff: a family lies in the image of the shift map iff its p-adic sum is an integer.
TauCeti.ModuleTower.limOneMultiplicationTowerEquiv: the isomorphism lim¹ ≃ ℤ_[p] ⧸ ℤ.
TauCeti.ModuleTower.not_isMittagLeffler_multiplicationTower: the tower is not Mittag-Leffler.

References #

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

source

noncomputable def TauCeti.ModuleTower.padicSum (p : ℕ) [Fact (Nat.Prime p)] :

(multiplicationTower ↑p).Product →+ ℤ_[p]

The p-adic summation map (aₙ) ↦ ∑ₙ pⁿ aₙ from the product of the terms of the multiplication-by-p tower of integers to ℤ_[p].

Instances For

source

theorem TauCeti.ModuleTower.padicSum_apply (p : ℕ) [Fact (Nat.Prime p)] (a : (multiplicationTower ↑p).Product) :

(padicSum p) a = ∑' (n : ℕ), ↑p ^ n * ↑((multiplicationTowerProductEquiv ↑p) a n)

source

theorem TauCeti.ModuleTower.hasSum_padicSum (p : ℕ) [Fact (Nat.Prime p)] (a : (multiplicationTower ↑p).Product) :

HasSum (fun (n : ℕ) => ↑p ^ n * ↑((multiplicationTowerProductEquiv ↑p) a n)) ((padicSum p) a)

The series ∑ₙ pⁿ aₙ converges in ℤ_[p] to padicSum p a.

source

@[simp]

theorem TauCeti.ModuleTower.padicSum_shift (p : ℕ) [Fact (Nat.Prime p)] (x : (multiplicationTower ↑p).Product) :

(padicSum p) ((multiplicationTower ↑p).shift x) = ↑((multiplicationTowerProductEquiv ↑p) x 0)

Telescoping: the p-adic sum of the shift of a family x is its zeroth term, ∑ₙ pⁿ (xₙ - xₙ₊₁ p) = x₀.

source

theorem TauCeti.ModuleTower.padicSum_surjective (p : ℕ) [Fact (Nat.Prime p)] :

Function.Surjective ⇑(padicSum p)

Every p-adic integer is a p-adic sum ∑ₙ pⁿ aₙ of integers: take for aₙ the n-th base-p digit, read off from the truncations PadicInt.appr.

source

theorem TauCeti.ModuleTower.mem_range_shift_multiplicationTower_iff (p : ℕ) [Fact (Nat.Prime p)] {a : (multiplicationTower ↑p).Product} :

a ∈ (multiplicationTower ↑p).shift.range ↔ ∃ (m : ℤ), ↑m = (padicSum p) a

The image of the shift map of the multiplication-by-p tower consists exactly of the families (aₙ) whose p-adic sum ∑ₙ pⁿ aₙ is an integer.

source

noncomputable def TauCeti.ModuleTower.limOneMultiplicationTowerEquiv (p : ℕ) [Fact (Nat.Prime p)] :

(multiplicationTower ↑p).limOne ≃+ ℤ_[p] ⧸ (Int.castAddHom ℤ_[p]).range

lim¹ of the multiplication-by-p tower is ℤ_[p] ⧸ ℤ, the isomorphism being induced by the p-adic summation map (aₙ) ↦ ∑ₙ pⁿ aₙ (limOneMultiplicationTowerEquiv_mk).

Instances For

source

@[simp]