Reduction modulo p of finite free ℤ_p-modules

A finite free ℤ_p-module M of rank r is isomorphic to ℤ_p ^ r, so its reduction M / pM is isomorphic to (ℤ_p / p) ^ r ≃ 𝔽_p ^ r and has p ^ r elements.

For the free ℤ_p-module ℤ_p[X] = X →₀ ℤ_[p], the integral lattice ℤ[X] = X →₀ ℤ, embedded by the integral cast Finsupp.mapRange.addMonoidHom (Int.castAddHom ℤ_[p]), already surjects onto ℤ_p[X] / p ℤ_p[X], and it is p-saturated in ℤ_p[X]. So the cokernel of ℤ[X] → ℤ_p[X] is uniquely p-divisible.

Main results

• TauCeti.natCard_quotient_padicInt_smul_top: reduction modulo p of a finite free ℤ_p-module of rank r has p^r elements.
• TauCeti.PadicInt.exists_finsupp_eq_mapRange_intCast_add: every element of ℤ_p[X] lies in ℤ[X] modulo p.
• TauCeti.PadicInt.mem_range_finsupp_mapRange_intCast_of_smul_mem: an element of ℤ_p[X] whose p-fold lies in ℤ[X] lies in ℤ[X].

theorem TauCeti.natCard_quotient_padicInt_smul_top (p : ℕ) [Fact (Nat.Prime p)] (M : Type u) [AddCommGroup M] [Module ℤ_[p] M] [Module.Free ℤ_[p] M] [Module.Finite ℤ_[p] M] : Nat.card (M ⧸ ↑p • ⊤) = p ^ Module.finrank ℤ_[p] M

The reduction of a finite free ℤ_p-module has the expected cardinality. If M is free of finite rank over ℤ_p, then M / pM has p ^ finrank M elements.

theorem TauCeti.PadicInt.exists_finsupp_eq_mapRange_intCast_add {p : ℕ} [Fact (Nat.Prime p)] {X : Type u_1} (v : X →₀ ℤ_[p]) : ∃ (w : X →₀ ℤ) (y : X →₀ ℤ_[p]), v = (Finsupp.mapRange.addMonoidHom (Int.castAddHom ℤ_[p])) w + ↑p • y

Every element of ℤ_p[X] = X →₀ ℤ_[p] lies in the integral lattice ℤ[X] modulo p: every p-adic integer is congruent to an integer modulo p.

theorem TauCeti.PadicInt.mem_range_finsupp_mapRange_intCast_of_smul_mem {p : ℕ} [Fact (Nat.Prime p)] {X : Type u_1} {v : X →₀ ℤ_[p]} (h : ↑p • v ∈ (Finsupp.mapRange.addMonoidHom (Int.castAddHom ℤ_[p])).range) : v ∈ (Finsupp.mapRange.addMonoidHom (Int.castAddHom ℤ_[p])).range

An element of ℤ_p[X] = X →₀ ℤ_[p] whose p-fold lies in the integral lattice ℤ[X] lies in ℤ[X] itself: if p a = n for an integer n, then ‖n‖ < 1, so p ∣ n and a = n / p.