# Documentation

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

• NonarchimedeanAddGroup: nonarchimedean additive group.
• NonarchimedeanGroup: nonarchimedean multiplicative group.
• NonarchimedeanRing: nonarchimedean ring.
class NonarchimedeanAddGroup (G : Type u_1) [] [] extends :

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

Instances
class NonarchimedeanGroup (G : Type u_1) [] [] extends :

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

Instances
class NonarchimedeanRing (R : Type u_1) [Ring R] [] extends :

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

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

Every nonarchimedean ring is naturally a nonarchimedean additive group.

theorem NonarchimedeanAddGroup.nonarchimedean_of_emb {G : Type u_1} [] [] {H : Type u_2} [] [] (f : G →+ H) (emb : ) :
abbrev NonarchimedeanAddGroup.nonarchimedean_of_emb.match_1 {G : Type u_1} [] [] {H : Type u_2} [] (f : G →+ H) (U : Set H) (motive : (V, V f ⁻¹' U) → Prop) :
(x : V, V f ⁻¹' U) → ((V : ) → (hV : V f ⁻¹' U) → motive (_ : V, V f ⁻¹' U)) → motive x
Instances For
theorem NonarchimedeanGroup.nonarchimedean_of_emb {G : Type u_1} [] [] {H : Type u_2} [] [] [] (f : G →* H) (emb : ) :

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

theorem NonarchimedeanAddGroup.prod_subset {G : Type u_1} [] [] {K : Type u_3} [] [] {U : Set (G × K)} (hU : U nhds 0) :
V W, 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_subset {G : Type u_1} [] [] {K : Type u_3} [] [] {U : Set (G × K)} (hU : U nhds 1) :
V W, 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_self_subset {G : Type u_1} [] [] {U : Set (G × G)} (hU : U nhds 0) :
V, 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.

abbrev NonarchimedeanAddGroup.prod_self_subset.match_1 {G : Type u_1} [] [] {U : Set (G × G)} (motive : (V W, V ×ˢ W U) → Prop) :
(x : V W, V ×ˢ W U) → ((V W : ) → (h : V ×ˢ W U) → motive (_ : V W, V ×ˢ W U)) → motive x
Instances For
theorem NonarchimedeanGroup.prod_self_subset {G : Type u_1} [] [] {U : Set (G × G)} (hU : U nhds 1) :
V, 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.

The cartesian product of two nonarchimedean groups is nonarchimedean.

abbrev NonarchimedeanAddGroup.instNonarchimedeanAddGroupSumInstAddGroupInstTopologicalSpaceSum.match_1 {G : Type u_1} [] [] {K : Type u_2} [] [] (U : Set (G × K)) (motive : (V W, V ×ˢ W U) → Prop) :
(x : V W, V ×ˢ W U) → ((V : ) → (W : ) → (h : V ×ˢ W U) → motive (_ : V W, V ×ˢ W U)) → motive x
Instances For

The cartesian product of two nonarchimedean groups is nonarchimedean.

The cartesian product of two nonarchimedean rings is nonarchimedean.

theorem NonarchimedeanRing.left_mul_subset {R : Type u_1} [Ring R] [] (U : ) (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 NonarchimedeanRing.mul_subset {R : Type u_1} [Ring R] [] (U : ) :
V, V * V U

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