# 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.

source
class NonarchimedeanAddGroup (G : Type u_1) [AddGroup G] [TopologicalSpace G] extends IsTopologicalAddGroup 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

Instances

source
class NonarchimedeanGroup (G : Type u_1) [Group G] [TopologicalSpace G] extends IsTopologicalGroup 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

Instances

source
class NonarchimedeanRing (R : Type u_1) [Ring R] [TopologicalSpace R] extends IsTopologicalRing 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

Instances

source
@[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.

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

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

source
theorem NonarchimedeanAddGroup.nonarchimedean_of_emb {G : Type u_1} [AddGroup G] [TopologicalSpace G] [NonarchimedeanAddGroup G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] [IsTopologicalAddGroup H] (f : G →+ H) (emb : Topology.IsOpenEmbedding ⇑f) :
NonarchimedeanAddGroup H
source
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.

source
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.

source
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.

source
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.

source
instance NonarchimedeanGroup.Prod.instNonarchimedeanGroup {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.

source
instance NonarchimedeanAddGroup.Prod.instNonarchimedeanAddGroup {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.

source
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.

source
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`.

source
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.