Topological ℤ_[p]-modules and their additive groups

A continuous additive map f : E →+ F between topological ℤ_[p]-modules with F Hausdorff is automatically ℤ_[p]-linear: for fixed x, the continuous maps c ↦ f (c • x) and c ↦ c • f x agree on the dense subset ℕ of ℤ_[p], and two continuous maps into a Hausdorff space that agree on a dense set are equal. So the ℤ_[p]-module structure of a Hausdorff topological ℤ_[p]-module is determined by its topological group structure, and continuous additive maps and isomorphisms between such modules can be treated as continuous ℤ_[p]-linear ones. In the automatic-linearity and rank results, the codomain F is assumed Hausdorff.

This file adapts Mathlib/Topology/Instances/RealVectorSpace.lean (Yury Kudryashov) from ℝ to ℤ_[p]: TauCeti.map_padicInt_smul, AddMonoidHom.toPadicIntLinearMap, and AddEquiv.toPadicIntLinearEquiv are the ℤ_[p] counterparts of map_real_smul, AddMonoidHom.toRealLinearMap, and AddEquiv.toRealLinearEquiv.

In particular the rank of a finite free ℤ_[p]-module is a topological invariant: a continuous additive isomorphism between two such modules preserves Module.finrank, and ℤ_[p] ^ r and ℤ_[p] ^ r' are topologically isomorphic groups only when r = r'.

Main results

• TauCeti.closedAddSubgroupPadicIntSubmoduleOrderIso: closed additive subgroups are precisely closed submodules. This correspondence needs neither compactness nor separation: closedness and density of the natural-number scalars give stability under all ℤ_[p]-scalars.
• TauCeti.map_padicInt_smul: a continuous additive map between topological ℤ_[p]-modules with Hausdorff codomain commutes with scalar multiplication by ℤ_[p].
• AddMonoidHom.toPadicIntLinearMap, AddEquiv.toPadicIntLinearEquiv: the resulting continuous ℤ_[p]-linear map and continuous ℤ_[p]-linear equivalence.
• AddEquiv.finrank_padicInt_eq: a continuous additive isomorphism preserves the ℤ_[p]-rank.
• TauCeti.eq_of_continuousMulEquiv_pi_padicInt: topologically isomorphic groups ℤ_[p] ^ r and ℤ_[p] ^ r' have r = r'.
• Submodule.torsion_padicInt: the torsion submodule of a ℤ_[p]-module is its torsion subgroup. This is purely algebraic, the ℤ_[p] counterpart of Submodule.torsion_int.
• TauCeti.restrictScalars_pPowerTorsion: over ℤ_p, the p-power torsion is the whole torsion submodule.
• TauCeti.isTorsionFree_quotient_pPowerTorsion: modulo its p-power torsion, a ℤ_p-module is torsion-free.
• LinearMap.padicIntCodRestrict: a ℚ_[p]-valued ℤ_[p]-linear map with values in ℤ_[p], as a ℤ_[p]-valued functional.

theorem TauCeti.map_padicInt_smul {E : Type u_1} [AddCommMonoid E] [TopologicalSpace E] {F : Type u_2} [AddCommMonoid F] [TopologicalSpace F] [T2Space F] {p : ℕ} [Fact (Nat.Prime p)] [Module ℤ_[p] E] [ContinuousSMul ℤ_[p] E] [Module ℤ_[p] F] [ContinuousSMul ℤ_[p] F] {G : Type u_3} [FunLike G E F] [AddMonoidHomClass G E F] (f : G) (hf : Continuous ⇑f) (c : ℤ_[p]) (x : E) : f (c • x) = c • f x

A continuous additive map between two topological ℤ_[p]-modules, the codomain being Hausdorff, is ℤ_[p]-linear.

theorem AddEquiv.finrank_padicInt_eq {E : Type u_1} [AddCommMonoid E] [TopologicalSpace E] {F : Type u_2} [AddCommMonoid F] [TopologicalSpace F] [T2Space F] {p : ℕ} [Fact (Nat.Prime p)] [Module ℤ_[p] E] [ContinuousSMul ℤ_[p] E] [Module ℤ_[p] F] [ContinuousSMul ℤ_[p] F] (e : E ≃+ F) (he : Continuous ⇑e) : Module.finrank ℤ_[p] E = Module.finrank ℤ_[p] F

A continuous additive isomorphism between topological ℤ_[p]-modules, the codomain being Hausdorff, preserves the ℤ_[p]-rank: the rank of a finite free ℤ_[p]-module is a topological invariant.

theorem TauCeti.eq_of_continuousMulEquiv_pi_padicInt {p : ℕ} [Fact (Nat.Prime p)] {r r' : ℕ} (e : Multiplicative (Fin r → ℤ_[p]) ≃ₜ* Multiplicative (Fin r' → ℤ_[p])) : r = r'

The rank of ℤ_[p] ^ r is a topological invariant: if the additive groups ℤ_[p] ^ r and ℤ_[p] ^ r', written multiplicatively, are topologically isomorphic, then r = r'.

theorem ClosedAddSubgroup.padicInt_smul_mem (p : ℕ) [Fact (Nat.Prime p)] {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [Module ℤ_[p] M] [ContinuousSMul ℤ_[p] M] (H : ClosedAddSubgroup M) {x : M} (hx : x ∈ H) (c : ℤ_[p]) : c • x ∈ H

A closed additive subgroup of a topological ℤ_[p]-module is stable under ℤ_[p]-scalars. No separation or compactness hypothesis is needed.

def ClosedAddSubgroup.toPadicIntSubmodule (p : ℕ) [Fact (Nat.Prime p)] {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [Module ℤ_[p] M] [ContinuousSMul ℤ_[p] M] (H : ClosedAddSubgroup M) : ClosedSubmodule ℤ_[p] M

The closed ℤ_[p]-submodule with the same carrier as a closed additive subgroup.

Equations

• ClosedAddSubgroup.toPadicIntSubmodule p H = { toSubmodule := let __src := ↑H; { toAddSubmonoid := __src.toAddSubmonoid, smul_mem' := ⋯ }, isClosed' := ⋯ }

@[simp]

theorem ClosedAddSubgroup.coe_toPadicIntSubmodule (p : ℕ) [Fact (Nat.Prime p)] {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [Module ℤ_[p] M] [ContinuousSMul ℤ_[p] M] (H : ClosedAddSubgroup M) : ↑(toPadicIntSubmodule p H) = ↑H

@[simp]

theorem ClosedAddSubgroup.mem_toPadicIntSubmodule (p : ℕ) [Fact (Nat.Prime p)] {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [Module ℤ_[p] M] [ContinuousSMul ℤ_[p] M] (H : ClosedAddSubgroup M) {x : M} : x ∈ toPadicIntSubmodule p H ↔ x ∈ H

@[simp]

theorem ClosedAddSubgroup.toAddSubgroup_toPadicIntSubmodule (p : ℕ) [Fact (Nat.Prime p)] {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [Module ℤ_[p] M] [ContinuousSMul ℤ_[p] M] (H : ClosedAddSubgroup M) : (↑(toPadicIntSubmodule p H)).toAddSubgroup = ↑H

noncomputable def TauCeti.closedAddSubgroupPadicIntSubmoduleOrderIso (p : ℕ) [Fact (Nat.Prime p)] {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [Module ℤ_[p] M] [ContinuousSMul ℤ_[p] M] : ClosedAddSubgroup M ≃o ClosedSubmodule ℤ_[p] M

Closed additive subgroups and closed ℤ_[p]-submodules of a topological ℤ_[p]-module are the same ordered collection of subsets.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.closedAddSubgroupPadicIntSubmoduleOrderIso_apply (p : ℕ) [Fact (Nat.Prime p)] {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [Module ℤ_[p] M] [ContinuousSMul ℤ_[p] M] (H : ClosedAddSubgroup M) : (closedAddSubgroupPadicIntSubmoduleOrderIso p) H = ClosedAddSubgroup.toPadicIntSubmodule p H

@[simp]

theorem TauCeti.closedAddSubgroupPadicIntSubmoduleOrderIso_symm_toAddSubgroup (p : ℕ) [Fact (Nat.Prime p)] {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [Module ℤ_[p] M] [ContinuousSMul ℤ_[p] M] (S : ClosedSubmodule ℤ_[p] M) : ↑((closedAddSubgroupPadicIntSubmoduleOrderIso p).symm S) = (↑S).toAddSubgroup

@[simp]

theorem TauCeti.mem_closedAddSubgroupPadicIntSubmoduleOrderIso_symm (p : ℕ) [Fact (Nat.Prime p)] {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [Module ℤ_[p] M] [ContinuousSMul ℤ_[p] M] (S : ClosedSubmodule ℤ_[p] M) {x : M} : x ∈ (closedAddSubgroupPadicIntSubmoduleOrderIso p).symm S ↔ x ∈ S

def AddMonoidHom.toPadicIntLinearMap {E : Type u_1} [AddCommMonoid E] [TopologicalSpace E] {F : Type u_2} [AddCommMonoid F] [TopologicalSpace F] [T2Space F] (p : ℕ) [Fact (Nat.Prime p)] [Module ℤ_[p] E] [ContinuousSMul ℤ_[p] E] [Module ℤ_[p] F] [ContinuousSMul ℤ_[p] F] (f : E →+ F) (hf : Continuous ⇑f) : E →L[ℤ_[p]] F

Reinterpret a continuous additive homomorphism between two topological ℤ_[p]-modules, the codomain being Hausdorff, as a continuous ℤ_[p]-linear map. The prime is explicit because the map does not determine it.

Equations

• AddMonoidHom.toPadicIntLinearMap p f hf = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯, cont := hf }

@[simp]

theorem AddMonoidHom.coe_toPadicIntLinearMap {E : Type u_1} [AddCommMonoid E] [TopologicalSpace E] {F : Type u_2} [AddCommMonoid F] [TopologicalSpace F] [T2Space F] (p : ℕ) [Fact (Nat.Prime p)] [Module ℤ_[p] E] [ContinuousSMul ℤ_[p] E] [Module ℤ_[p] F] [ContinuousSMul ℤ_[p] F] (f : E →+ F) (hf : Continuous ⇑f) : ⇑(toPadicIntLinearMap p f hf) = ⇑f

def AddEquiv.toPadicIntLinearEquiv {E : Type u_1} [AddCommMonoid E] [TopologicalSpace E] {F : Type u_2} [AddCommMonoid F] [TopologicalSpace F] [T2Space F] (p : ℕ) [Fact (Nat.Prime p)] [Module ℤ_[p] E] [ContinuousSMul ℤ_[p] E] [Module ℤ_[p] F] [ContinuousSMul ℤ_[p] F] (e : E ≃+ F) (h₁ : Continuous ⇑e) (h₂ : Continuous ⇑e.symm) : E ≃L[ℤ_[p]] F

Reinterpret a continuous additive equivalence between two topological ℤ_[p]-modules, the codomain being Hausdorff, as a continuous ℤ_[p]-linear equivalence. The prime is explicit because the equivalence does not determine it.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AddEquiv.coe_toPadicIntLinearEquiv {E : Type u_1} [AddCommMonoid E] [TopologicalSpace E] {F : Type u_2} [AddCommMonoid F] [TopologicalSpace F] [T2Space F] (p : ℕ) [Fact (Nat.Prime p)] [Module ℤ_[p] E] [ContinuousSMul ℤ_[p] E] [Module ℤ_[p] F] [ContinuousSMul ℤ_[p] F] (e : E ≃+ F) (h₁ : Continuous ⇑e) (h₂ : Continuous ⇑e.symm) : ⇑(toPadicIntLinearEquiv p e h₁ h₂) = ⇑e

@[simp]

theorem AddEquiv.coe_toPadicIntLinearEquiv_symm {E : Type u_1} [AddCommMonoid E] [TopologicalSpace E] {F : Type u_2} [AddCommMonoid F] [TopologicalSpace F] [T2Space F] (p : ℕ) [Fact (Nat.Prime p)] [Module ℤ_[p] E] [ContinuousSMul ℤ_[p] E] [Module ℤ_[p] F] [ContinuousSMul ℤ_[p] F] (e : E ≃+ F) (h₁ : Continuous ⇑e) (h₂ : Continuous ⇑e.symm) : ⇑(toPadicIntLinearEquiv p e h₁ h₂).symm = ⇑e.symm

theorem Submodule.torsion_padicInt (p : ℕ) [hp : Fact (Nat.Prime p)] {M : Type u_3} [AddCommGroup M] [Module ℤ_[p] M] : (torsion ℤ_[p] M).toAddSubgroup = AddCommGroup.torsion M

The torsion submodule of a ℤ_[p]-module is its torsion subgroup. This is the ℤ_[p] analogue of Submodule.torsion_int.

@[simp]

theorem TauCeti.restrictScalars_pPowerTorsion {p : ℕ} [Fact (Nat.Prime p)] {M : Type u_4} [AddCommGroup M] [Module ℤ_[p] M] {A : Type u_5} [Semiring A] [Module A M] [SMul ℤ_[p] A] [IsScalarTower ℤ_[p] A M] : Submodule.restrictScalars ℤ_[p] (pPowerTorsion p A M) = Submodule.torsion ℤ_[p] M

Over ℤ_p, the p-power torsion is the whole torsion submodule: a nonzero p-adic integer is a unit times a power of p.

instance TauCeti.isTorsionFree_quotient_pPowerTorsion {p : ℕ} [Fact (Nat.Prime p)] {M : Type u_4} [AddCommGroup M] [Module ℤ_[p] M] {A : Type u_5} [Ring A] [Module A M] [SMul ℤ_[p] A] [IsScalarTower ℤ_[p] A M] : Module.IsTorsionFree ℤ_[p] (M ⧸ pPowerTorsion p A M)

Modulo its p-power torsion, a module over ℤ_p is torsion-free: the quotient is the quotient by the whole torsion submodule.

def LinearMap.padicIntCodRestrict {p : ℕ} [Fact (Nat.Prime p)] {X : Type u_3} [AddCommGroup X] [Module ℤ_[p] X] (Φ : X →ₗ[ℤ_[p]] ℚ_[p]) (h : ∀ (x : X), Φ x ∈ 1) : Module.Dual ℤ_[p] X

A ℚ_[p]-valued ℤ_[p]-linear map whose values lie in ℤ_[p], as a ℤ_[p]-valued functional.

Equations

• Φ.padicIntCodRestrict h = { toFun := fun (x : X) => ⟨Φ x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.coe_padicIntCodRestrict_apply {p : ℕ} [Fact (Nat.Prime p)] {X : Type u_3} [AddCommGroup X] [Module ℤ_[p] X] (Φ : X →ₗ[ℤ_[p]] ℚ_[p]) (h : ∀ (x : X), Φ x ∈ 1) (x : X) : ↑((Φ.padicIntCodRestrict h) x) = Φ x