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

• continuous_add : Continuous fun (p : G × G) => p.1 + p.2
• continuous_neg : Continuous fun (a : G) => -a
• is_nonarchimedean : Unhds 0, ∃ (V : ), V U
Instances
theorem NonarchimedeanAddGroup.is_nonarchimedean {G : Type u_1} [] [] [self : ] (U : Set G) :
U nhds 0∃ (V : ), V U
class NonarchimedeanGroup (G : Type u_1) [] [] extends :

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

Instances
theorem NonarchimedeanGroup.is_nonarchimedean {G : Type u_1} [] [] [self : ] (U : Set G) :
U nhds 1∃ (V : ), V U
class NonarchimedeanRing (R : Type u_1) [Ring R] [] extends :

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

Instances
theorem NonarchimedeanRing.is_nonarchimedean {R : Type u_1} [Ring R] [] [self : ] (U : Set R) :
U nhds 0∃ (V : ), V U
@[instance 100]
instance NonarchimedeanRing.to_nonarchimedeanAddGroup (R : Type u_1) [Ring R] [] [t : ] :

Every nonarchimedean ring is naturally a nonarchimedean additive group.

Equations
• =
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 )motive x
Equations
• =
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 )motive x
Equations
• =
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.

instance NonarchimedeanAddGroup.instSum {G : Type u_1} [] [] {K : Type u_3} [] [] :

The cartesian product of two nonarchimedean groups is nonarchimedean.

Equations
• =
abbrev NonarchimedeanAddGroup.instSum.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 )motive x
Equations
• =
Instances For
instance NonarchimedeanGroup.instProd {G : Type u_1} [] [] {K : Type u_3} [] [] :

The cartesian product of two nonarchimedean groups is nonarchimedean.

Equations
• =
instance NonarchimedeanRing.instProd {R : Type u_1} {S : Type u_2} [Ring R] [] [Ring S] [] :

The cartesian product of two nonarchimedean rings is nonarchimedean.

Equations
• =
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.