CompactPadic.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Compact p-adic modules

The map 1 - shift is surjective on the product of a tower of finite abelian groups, without any surjectivity assumption on the transition maps. A compact Hausdorff module vanishes if a topologically nilpotent scalar acts surjectively. This implies compact p-adic Nakayama: a compact Hausdorff ℤ_[p]-module with continuous operations is finitely generated exactly when its quotient modulo p is finite. Finitely generated ℤ_[p]-modules also have finite p-torsion.

These are algebraic support results. The K(n)-local sphere, its homotopy groups, their p-adic topology and module structure, and their ranks are not constructed here.

theorem OAI.KnLocalSphere.IntegralRecovery.one_sub_shift_surjective line 27

Source documentation

The map 1 - shift is surjective for any tower of finite abelian groups.

theorem one_sub_shift_surjective (A : ℕ → Type u)
    [∀ n, AddCommGroup (A n)] [∀ n, Finite (A n)]
    (f : ∀ n, A (n + 1) →+ A n) :
    Function.Surjective (fun x : (n : ℕ) → A n => fun n => x n - f n (x (n + 1))) := by
…

theorem OAI.KnLocalSphere.IntegralRecovery.eq_zero_of_surjective_smul line 46

Source documentation

A surjective topologically nilpotent scalar annihilates a compact Hausdorff module.

theorem eq_zero_of_surjective_smul {R : Type u} {M : Type v}
    [Semiring R] [TopologicalSpace R] [AddCommMonoid M] [Module R M]
    [TopologicalSpace M] [CompactSpace M] [T2Space M] [ContinuousSMul R M]
    (a : R) (ha : Tendsto (fun n : ℕ => a ^ n) atTop (𝓝 0))
    (hs : Function.Surjective (fun x : M => a • x)) (x : M) : x = 0 := by
…

theorem OAI.KnLocalSphere.IntegralRecovery.finite_of_finite_mod_p line 85

Source documentation

Compact p-adic Nakayama: finiteness modulo p implies finite generation over ℤ_[p].

theorem finite_of_finite_mod_p (p : ℕ) [Fact p.Prime]
    (M : Type u) [AddCommGroup M] [Module ℤ_[p] M]
    [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul ℤ_[p] M]
    [CompactSpace M] [T2Space M]
    [Finite (M ⧸ LinearMap.range (LinearMap.lsmul ℤ_[p] M (p : ℤ_[p])))] :
    Module.Finite ℤ_[p] M := by
…

theorem OAI.KnLocalSphere.IntegralRecovery.finite_mod_p_of_finite_module line 127

Source documentation

A finitely generated ℤ_[p]-module has finite quotient modulo p.

theorem finite_mod_p_of_finite_module (p : ℕ) [Fact p.Prime]
    (M : Type u) [AddCommGroup M] [Module ℤ_[p] M] [Module.Finite ℤ_[p] M] :
    Finite (M ⧸ LinearMap.range (LinearMap.lsmul ℤ_[p] M (p : ℤ_[p]))) := by
…

theorem OAI.KnLocalSphere.IntegralRecovery.finite_of_finite_module_killed_by_p line 143

Source documentation

A finitely generated ℤ_[p]-module killed by p is finite.

theorem finite_of_finite_module_killed_by_p (p : ℕ) [Fact p.Prime]
    (M : Type u) [AddCommGroup M] [Module ℤ_[p] M] [Module.Finite ℤ_[p] M]
    (hp : ∀ x : M, (p : ℤ_[p]) • x = 0) : Finite M := by
…

theorem OAI.KnLocalSphere.IntegralRecovery.finite_p_torsion line 156

Source documentation

The p-torsion of a finitely generated ℤ_[p]-module is finite.

theorem finite_p_torsion (p : ℕ) [Fact p.Prime]
    (M : Type u) [AddCommGroup M] [Module ℤ_[p] M] [Module.Finite ℤ_[p] M] :
    Finite (LinearMap.ker (LinearMap.lsmul ℤ_[p] M (p : ℤ_[p]))) := by
…

theorem OAI.KnLocalSphere.IntegralRecovery.module_finite_iff_finite_mod_p line 167

Source documentation

A compact Hausdorff ℤ_[p]-module is finitely generated iff it is finite modulo p.

theorem module_finite_iff_finite_mod_p (p : ℕ) [Fact p.Prime]
    (M : Type u) [AddCommGroup M] [Module ℤ_[p] M]
    [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul ℤ_[p] M]
    [CompactSpace M] [T2Space M] :
    Module.Finite ℤ_[p] M ↔
      Finite (M ⧸ LinearMap.range (LinearMap.lsmul ℤ_[p] M (p : ℤ_[p]))) := by
…