Nonarchimedean Topology

In this file we set up the theory of nonarchimedean topological groups and rings.

A nonarchimedean group is a topological group whose topology admits a basis of open neighborhoods of the identity element in the group consisting of open subgroups. A nonarchimedean ring is a topological ring whose underlying topological (additive) group is nonarchimedean.

Definitions

• NonarchimedeanAddGroup: nonarchimedean additive group.
• NonarchimedeanGroup: nonarchimedean multiplicative group.
• NonarchimedeanRing: nonarchimedean ring.

class NonarchimedeanAddGroup (G : Type u_1) [AddGroup G] [TopologicalSpace G] extends TopologicalAddGroup G : Prop

A topological additive group is nonarchimedean if every neighborhood of 0 contains an open subgroup.

• continuous_add : Continuous fun (p : G × G) => p.1 + p.2
• continuous_neg : Continuous fun (a : G) => -a
• is_nonarchimedean (U : Set G) : U ∈ nhds 0 → ∃ (V : OpenAddSubgroup G), ↑V ⊆ U

class NonarchimedeanGroup (G : Type u_1) [Group G] [TopologicalSpace G] extends TopologicalGroup G : Prop

A topological group is nonarchimedean if every neighborhood of 1 contains an open subgroup.

• continuous_mul : Continuous fun (p : G × G) => p.1 * p.2
• continuous_inv : Continuous fun (a : G) => a⁻¹
• is_nonarchimedean (U : Set G) : U ∈ nhds 1 → ∃ (V : OpenSubgroup G), ↑V ⊆ U

class NonarchimedeanRing (R : Type u_1) [Ring R] [TopologicalSpace R] extends TopologicalRing R : Prop

A topological ring is nonarchimedean if its underlying topological additive group is nonarchimedean.

• continuous_add : Continuous fun (p : R × R) => p.1 + p.2
• continuous_mul : Continuous fun (p : R × R) => p.1 * p.2
• continuous_neg : Continuous fun (a : R) => -a
• is_nonarchimedean (U : Set R) : U ∈ nhds 0 → ∃ (V : OpenAddSubgroup R), ↑V ⊆ U

@[instance 100]

instance NonarchimedeanRing.to_nonarchimedeanAddGroup (R : Type u_1) [Ring R] [TopologicalSpace R] [t : NonarchimedeanRing R] : NonarchimedeanAddGroup R

Every nonarchimedean ring is naturally a nonarchimedean additive group.

theorem NonarchimedeanGroup.nonarchimedean_of_emb {G : Type u_1} [Group G] [TopologicalSpace G] [NonarchimedeanGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [TopologicalGroup H] (f : G →* H) (emb : Topology.IsOpenEmbedding ⇑f) : NonarchimedeanGroup H

If a topological group embeds into a nonarchimedean group, then it is nonarchimedean.

theorem NonarchimedeanAddGroup.nonarchimedean_of_emb {G : Type u_1} [AddGroup G] [TopologicalSpace G] [NonarchimedeanAddGroup G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] [TopologicalAddGroup H] (f : G →+ H) (emb : Topology.IsOpenEmbedding ⇑f) : NonarchimedeanAddGroup H

theorem NonarchimedeanGroup.prod_subset {G : Type u_1} [Group G] [TopologicalSpace G] [NonarchimedeanGroup G] {K : Type u_3} [Group K] [TopologicalSpace K] [NonarchimedeanGroup K] {U : Set (G × K)} (hU : U ∈ nhds 1) : ∃ (V : OpenSubgroup G) (W : OpenSubgroup K), ↑V ×ˢ ↑W ⊆ U

An open neighborhood of the identity in the cartesian product of two nonarchimedean groups contains the cartesian product of an open neighborhood in each group.

theorem NonarchimedeanAddGroup.prod_subset {G : Type u_1} [AddGroup G] [TopologicalSpace G] [NonarchimedeanAddGroup G] {K : Type u_3} [AddGroup K] [TopologicalSpace K] [NonarchimedeanAddGroup K] {U : Set (G × K)} (hU : U ∈ nhds 0) : ∃ (V : OpenAddSubgroup G) (W : OpenAddSubgroup K), ↑V ×ˢ ↑W ⊆ U

An open neighborhood of the identity in the cartesian product of two nonarchimedean groups contains the cartesian product of an open neighborhood in each group.

theorem NonarchimedeanGroup.prod_self_subset {G : Type u_1} [Group G] [TopologicalSpace G] [NonarchimedeanGroup G] {U : Set (G × G)} (hU : U ∈ nhds 1) : ∃ (V : OpenSubgroup G), ↑V ×ˢ ↑V ⊆ U

An open neighborhood of the identity in the cartesian square of a nonarchimedean group contains the cartesian square of an open neighborhood in the group.

theorem NonarchimedeanAddGroup.prod_self_subset {G : Type u_1} [AddGroup G] [TopologicalSpace G] [NonarchimedeanAddGroup G] {U : Set (G × G)} (hU : U ∈ nhds 0) : ∃ (V : OpenAddSubgroup G), ↑V ×ˢ ↑V ⊆ U

An open neighborhood of the identity in the cartesian square of a nonarchimedean group contains the cartesian square of an open neighborhood in the group.

instance NonarchimedeanGroup.instProd {G : Type u_1} [Group G] [TopologicalSpace G] [NonarchimedeanGroup G] {K : Type u_3} [Group K] [TopologicalSpace K] [NonarchimedeanGroup K] : NonarchimedeanGroup (G × K)

The cartesian product of two nonarchimedean groups is nonarchimedean.

instance NonarchimedeanAddGroup.instSum {G : Type u_1} [AddGroup G] [TopologicalSpace G] [NonarchimedeanAddGroup G] {K : Type u_3} [AddGroup K] [TopologicalSpace K] [NonarchimedeanAddGroup K] : NonarchimedeanAddGroup (G × K)

The cartesian product of two nonarchimedean groups is nonarchimedean.

instance NonarchimedeanRing.instProd {R : Type u_1} {S : Type u_2} [Ring R] [TopologicalSpace R] [NonarchimedeanRing R] [Ring S] [TopologicalSpace S] [NonarchimedeanRing S] : NonarchimedeanRing (R × S)

The cartesian product of two nonarchimedean rings is nonarchimedean.

theorem NonarchimedeanRing.left_mul_subset {R : Type u_1} [Ring R] [TopologicalSpace R] [NonarchimedeanRing R] (U : OpenAddSubgroup R) (r : R) : ∃ (V : OpenAddSubgroup R), r • ↑V ⊆ ↑U

Given an open subgroup U and an element r of a nonarchimedean ring, there is an open subgroup V such that r • V is contained in U.

theorem NonarchimedeanRing.mul_subset {R : Type u_1} [Ring R] [TopologicalSpace R] [NonarchimedeanRing R] (U : OpenAddSubgroup R) : ∃ (V : OpenAddSubgroup R), ↑V * ↑V ⊆ ↑U

An open subgroup of a nonarchimedean ring contains the square of another one.