Torsion and continuous maps in topological groups

Let A be a topological abelian group topologically isomorphic to Multiplicative (M × T), where M is a torsion-free additive group and T is a torsion additive group. The algebraic identification of A ⧸ torsion A with M from TauCeti.GroupTheory.Torsion is then a topological isomorphism for the quotient topology.

Continuous maps from a compact space into a discrete p-primary torsion group also form a p-primary torsion group, since each map has finite image.

Main definitions

• TauCeti.quotientTorsionContinuousMulEquiv: the quotient of A by its torsion subgroup is topologically isomorphic to M.
• TauCeti.IsPPrimaryTorsion.continuousMap: compact-to-discrete continuous maps preserve p-primary torsion.

noncomputable def TauCeti.quotientTorsionContinuousMulEquiv {A : Type u_1} {M : Type u_2} {T : Type u_3} [CommGroup A] [AddGroup M] [IsAddTorsionFree M] [AddMonoid T] [TopologicalSpace A] [TopologicalSpace M] [TopologicalSpace T] (hT : IsAddTorsion T) (e : A ≃ₜ* Multiplicative (M × T)) : A ⧸ CommGroup.torsion A ≃ₜ* Multiplicative M

Under a topological isomorphism A ≃ₜ* Multiplicative (M × T) with M torsion-free and T torsion, the quotient of A by its torsion subgroup is topologically isomorphic to M.

Equations

• TauCeti.quotientTorsionContinuousMulEquiv hT e = { toMulEquiv := TauCeti.quotientTorsionMulEquiv hT e.toMulEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.quotientTorsionContinuousMulEquiv_mk {A : Type u_1} {M : Type u_2} {T : Type u_3} [CommGroup A] [AddGroup M] [IsAddTorsionFree M] [AddMonoid T] [TopologicalSpace A] [TopologicalSpace M] [TopologicalSpace T] (hT : IsAddTorsion T) (e : A ≃ₜ* Multiplicative (M × T)) (x : A) : (quotientTorsionContinuousMulEquiv hT e) ↑x = Multiplicative.ofAdd (Multiplicative.toAdd (e x)).1

@[simp]

theorem TauCeti.quotientTorsionContinuousMulEquiv_symm_apply {A : Type u_1} {M : Type u_2} {T : Type u_3} [CommGroup A] [AddGroup M] [IsAddTorsionFree M] [AddMonoid T] [TopologicalSpace A] [TopologicalSpace M] [TopologicalSpace T] (hT : IsAddTorsion T) (e : A ≃ₜ* Multiplicative (M × T)) (v : Multiplicative M) : (quotientTorsionContinuousMulEquiv hT e).symm v = ↑(e.symm (Multiplicative.ofAdd (Multiplicative.toAdd v, 0)))

theorem TauCeti.IsPPrimaryTorsion.continuousMap {p : ℕ} {V : Type u_4} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] (h : IsPPrimaryTorsion p V) (X : Type u_5) [TopologicalSpace X] [CompactSpace X] : IsPPrimaryTorsion p C(X, V)

The continuous maps from a compact space into a discrete p-primary torsion group form a p-primary torsion group: such a map has finite image, so one power of p kills all its values at once.