# mathlibdocumentation

topology.algebra.nonarchimedean.basic

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

• nonarchimedean_add_group: nonarchimedean additive group.
• nonarchimedean_group: nonarchimedean multiplicative group.
• nonarchimedean_ring: nonarchimedean ring.
@[class]
Prop
• is_nonarchimedean : ∀ (U : set G), U 𝓝 0(∃ (V : , V U)

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

Instances
@[class]
structure nonarchimedean_group (G : Type u_1) [group G]  :
Prop
• to_topological_group :
• is_nonarchimedean : ∀ (U : set G), U 𝓝 1(∃ (V : , V U)

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

Instances
@[class]
structure nonarchimedean_ring (R : Type u_1) [ring R]  :
Prop
• to_topological_ring :
• is_nonarchimedean : ∀ (U : set R), U 𝓝 0(∃ (V : , V U)

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

Instances
@[instance]

Every nonarchimedean ring is naturally a nonarchimedean additive group.

theorem nonarchimedean_add_group.nonarchimedean_of_emb {G : Type u_1} [add_group G] {H : Type u_2} [add_group H] (f : G →+ H) (emb : open_embedding f) :
theorem nonarchimedean_group.nonarchimedean_of_emb {G : Type u_1} [group G] {H : Type u_2} [group H] (f : G →* H) (emb : open_embedding f) :

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

theorem nonarchimedean_add_group.prod_subset {G : Type u_1} [add_group G] {K : Type u_3} [add_group K] {U : set (G × K)} (hU : U 𝓝 0) :
∃ (V : (W : , V.prod W U
theorem nonarchimedean_group.prod_subset {G : Type u_1} [group G] {K : Type u_3} [group K] {U : set (G × K)} (hU : U 𝓝 1) :
∃ (V : (W : , V.prod 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 nonarchimedean_add_group.prod_self_subset {G : Type u_1} [add_group G] {U : set (G × G)} (hU : U 𝓝 0) :
∃ (V : , V.prod V U
theorem nonarchimedean_group.prod_self_subset {G : Type u_1} [group G] {U : set (G × G)} (hU : U 𝓝 1) :
∃ (V : , V.prod 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]
@[instance]
def nonarchimedean_group.prod.nonarchimedean_group {G : Type u_1} [group G] {K : Type u_3} [group K]  :

The cartesian product of two nonarchimedean groups is nonarchimedean.

@[instance]
def nonarchimedean_ring.prod.nonarchimedean_ring {R : Type u_1} {S : Type u_2} [ring R] [ring S]  :

The cartesian product of two nonarchimedean rings is nonarchimedean.

theorem nonarchimedean_ring.left_mul_subset {R : Type u_1} [ring R] (U : open_add_subgroup R) (r : R) :
∃ (V : , 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 nonarchimedean_ring.mul_subset {R : Type u_1} [ring R] (U : open_add_subgroup R) :
∃ (V : , (V) * V U

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