Assertion that a (multiplicative) topological group is isomorphic to ℤₚᵈ

In this file we define EquivMvZp G p ι which is an isomorphism of G and Multiplicative (ι → ℤ_[p]) as topological groups.

To state that G is isomorphic to Multiplicative (ι → ℤ_[p]) as topological groups, use Nonempty (EquivMvZp G p ι). As a special case, to state that G is isomorphic to ℤₚᵈ, use Nonempty (EquivMvZp G p (Fin d)).

Maybe these should be in mathlib

theorem Equiv.arrowCongr_eq_piCongrLeft {M : Type u_1} {N : Type u_2} {P : Type u_3} (f : M ≃ N) : f.arrowCongr (Equiv.refl P) = piCongrLeft (fun (x : N) => P) f

EquivMvZp

structure EquivMvZp (G : Type u_1) [Group G] [TopologicalSpace G] (p : ℕ) [Fact (Nat.Prime p)] (ι : Type u_2) : Type (max u_1 u_2)

An EquivMvZp G p ι is just an isomorphism of G and Multiplicative (ι → ℤ_[p]) as topological groups.

• continuousMulEquiv' : G ≃ₜ* Multiplicative (ι → ℤ_[p])

noncomputable def EquivMvZp.congr {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) {G' : Type u_3} [Group G'] [TopologicalSpace G'] (f : G ≃ₜ* G') {ι' : Type u_4} (e : ι ≃ ι') : EquivMvZp G' p ι'

Transfer EquivMvZp along isomorphisms.

Equations

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

@[reducible, inline]

abbrev EquivMvZp.Γ {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) : Type u_1

The EquivMvZp.Γ is just the group G itself.

Equations

• H.Γ = G

def EquivMvZp.continuousMulEquiv {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) : H.Γ ≃ₜ* Multiplicative (ι → ℤ_[p])

The isomorphism from Γ to ℤₚᵈ.

Equations

• H.continuousMulEquiv = H.continuousMulEquiv'

instance EquivMvZp.isMulCommutative {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) : IsMulCommutative H.Γ

The Γ is commutative.

noncomputable def EquivMvZp.Γpow' {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) (n : ℕ) : Subgroup H.Γ

The (normal) subgroup Γ ^ (p ^ n) of Γ.

This is only used internally, as later we only considered the case that ι is finite, in which case Γ ^ (p ^ n) is an open normal subgroup.

Equations

• H.Γpow' n = Subgroup.comap (↑H.continuousMulEquiv) (AddSubgroup.toSubgroup (Submodule.toAddSubgroup (Ideal.pi fun (x : ι) => Ideal.span {↑p ^ n})))

theorem EquivMvZp.mem_Γpow'_iff {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) (n : ℕ) (σ : H.Γ) : σ ∈ H.Γpow' n ↔ ∃ (τ : H.Γ), σ = τ ^ p ^ n

An element is in Γ ^ (p ^ n) if and only if it is p ^ n-th power of some element.

@[simp]

theorem EquivMvZp.Γpow'_zero {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) : H.Γpow' 0 = ⊤

Γ ^ (p ^ 0) = Γ.

theorem EquivMvZp.antitone_Γpow' {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) : Antitone H.Γpow'

If m ≤ n then Γ ^ (p ^ n) ≤ Γ ^ (p ^ m).

theorem EquivMvZp.strictAnti_Γpow' {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Nonempty ι] : StrictAnti H.Γpow'

If m < n then Γ ^ (p ^ n) < Γ ^ (p ^ m).

noncomputable def EquivMvZp.congrFinOfCardEq {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} [Finite ι] (H : EquivMvZp G p ι) {G' : Type u_3} [Group G'] [TopologicalSpace G'] (f : G ≃ₜ* G') {d : ℕ} (h : Nat.card ι = d) : EquivMvZp G' p (Fin d)

Version of EquivMvZp.congr for finite case.

Equations

• H.congrFinOfCardEq f h = H.congr f (Finite.equivFinOfCardEq h)

theorem EquivMvZp.isOpen_Γpow' {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Finite ι] (n : ℕ) : IsOpen ↑(H.Γpow' n)

The Γ ^ (p ^ n) is open.

noncomputable def EquivMvZp.Γpow {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Finite ι] (n : ℕ) : OpenNormalSubgroup H.Γ

The open normal subgroup Γ ^ (p ^ n) of Γ.

Equations

• H.Γpow n = { toSubgroup := H.Γpow' n, isOpen' := ⋯, isNormal' := ⋯ }

theorem EquivMvZp.toSubgroup_Γpow {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Finite ι] (n : ℕ) : ↑(H.Γpow n).toOpenSubgroup = H.Γpow' n

theorem EquivMvZp.mem_Γpow_iff {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Finite ι] (n : ℕ) (σ : H.Γ) : σ ∈ H.Γpow n ↔ ∃ (τ : H.Γ), σ = τ ^ p ^ n

An element is in Γ ^ (p ^ n) if and only if it is p ^ n-th power of some element.

@[simp]

theorem EquivMvZp.Γpow_zero {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Finite ι] : H.Γpow 0 = ⊤

Γ ^ (p ^ 0) = Γ.

@[simp]

theorem EquivMvZp.index_Γpow {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Finite ι] (n : ℕ) : (↑(H.Γpow n).toOpenSubgroup).index = p ^ (n * Nat.card ι)

Γ ^ (p ^ n) is of index p ^ (n * #ι).

theorem EquivMvZp.antitone_Γpow {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Finite ι] : Antitone H.Γpow

If m ≤ n then Γ ^ (p ^ n) ≤ Γ ^ (p ^ m).

theorem EquivMvZp.strictAnti_Γpow {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Finite ι] [Nonempty ι] : StrictAnti H.Γpow

If m < n then Γ ^ (p ^ n) < Γ ^ (p ^ m).

theorem EquivMvZp.closure_eq_Γpow_of_closure_eq {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Finite ι] {s : Set H.Γ} (h : closure ↑(Subgroup.closure s) = Set.univ) (n : ℕ) : closure ↑(Subgroup.closure ((fun (x : H.Γ) => x ^ p ^ n) '' s)) = ↑(H.Γpow n)

If the set s topologically generates Γ, then the set s ^ (p ^ n) topologically generates Γ ^ (p ^ n).

theorem EquivMvZp.closure_singleton_eq_Γpow_of_closure_singleton_eq {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Finite ι] {γ : H.Γ} (h : closure ↑(Subgroup.closure {γ}) = Set.univ) (n : ℕ) : closure ↑(Subgroup.closure {γ ^ p ^ n}) = ↑(H.Γpow n)

If γ is a topological generator of Γ, then γ ^ (p ^ n) is a topological generator of Γ ^ (p ^ n).

theorem EquivMvZp.nhds_one_hasAntitoneBasis {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Finite ι] : (nhds 1).HasAntitoneBasis fun (n : ℕ) => ↑(H.Γpow n)

Γ ^ (p ^ n) form a neighborhood basis of 1 in Γ.

theorem EquivMvZp.Γpow_le_of_isOpen {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Finite ι] (O : Subgroup H.Γ) (h : IsOpen ↑O) : ∃ (n : ℕ), ↑(H.Γpow n).toOpenSubgroup ≤ O

If O is an open subgroup of Γ, then it contains Γ ^ (p ^ n) for some n.

noncomputable def EquivMvZp.ofContinuousMulEquiv₁ {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} [Unique ι] (e : G ≃ₜ* Multiplicative ℤ_[p]) : EquivMvZp G p ι

An isomorphism from Γ to ℤₚ gives an EquivMvZp G p ι when ι consists of exactly one element.

Equations

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

noncomputable def EquivMvZp.continuousMulEquiv₁ {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Unique ι] : H.Γ ≃ₜ* Multiplicative ℤ_[p]

The isomorphism from Γ to ℤₚ.

Equations

• H.continuousMulEquiv₁ = H.continuousMulEquiv.trans { toMulEquiv := AddEquiv.toMultiplicative (AddEquiv.piUnique fun (x : ι) => ℤ_[p]), continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem EquivMvZp.nonempty_iff_of_unique {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} [Unique ι] : Nonempty (EquivMvZp G p ι) ↔ Nonempty (G ≃ₜ* Multiplicative ℤ_[p])

noncomputable def EquivMvZp.topologicalGenerator {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Unique ι] : H.Γ

A random topological generator γ of Γ.

Equations

• H.topologicalGenerator = H.continuousMulEquiv₁.symm (Multiplicative.ofAdd 1)

theorem EquivMvZp.topologicalGenerator_spec {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Unique ι] : closure ↑(Subgroup.closure {H.topologicalGenerator}) = ⊤

The γ is a topological generator of Γ.

theorem EquivMvZp.closure_topologicalGenerator_pow_eq {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Unique ι] (n : ℕ) : closure ↑(Subgroup.closure {H.topologicalGenerator ^ p ^ n}) = ↑(H.Γpow n)

The γ ^ (p ^ n) is a topological generator of Γ ^ (p ^ n).

theorem EquivMvZp.index_Γpow₁ {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Unique ι] (n : ℕ) : (↑(H.Γpow n).toOpenSubgroup).index = p ^ n

Γ ^ (p ^ n) is of index p ^ n.

theorem EquivMvZp.eq_Γpow_of_isOpen {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Unique ι] (O : Subgroup H.Γ) (h : IsOpen ↑O) : ∃ (n : ℕ), O = ↑(H.Γpow n).toOpenSubgroup

If O is an open subgroup of Γ, then it is equal to Γ ^ (p ^ n) for some n.

theorem EquivMvZp.eq_bot_or_Γpow_of_isClosed {G : Type u_1} [Group G] [TopologicalSpace G] {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_2} (H : EquivMvZp G p ι) [Unique ι] (O : Subgroup H.Γ) (h : IsClosed ↑O) : O = ⊥ ∨ ∃ (n : ℕ), O = ↑(H.Γpow n).toOpenSubgroup

If O is a closed subgroup of Γ, then it is equal to 0 or Γ ^ (p ^ n) for some n.