mathlib documentation

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 #

@[class]
structure nonarchimedean_add_group (G : Type u_1) [add_group G] [topological_space G] :
Prop

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

Instances of this typeclass
@[class]
structure nonarchimedean_group (G : Type u_1) [group G] [topological_space G] :
Prop

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

Instances of this typeclass
@[class]
structure nonarchimedean_ring (R : Type u_1) [ring R] [topological_space R] :
Prop

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

Instances of this typeclass
@[protected, instance]

Every nonarchimedean ring is naturally a nonarchimedean additive group.

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

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] [topological_space G] [nonarchimedean_add_group G] {K : Type u_3} [add_group K] [topological_space K] [nonarchimedean_add_group K] {U : set (G × K)} (hU : U nhds 0) :

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_group.prod_subset {G : Type u_1} [group G] [topological_space G] [nonarchimedean_group G] {K : Type u_3} [group K] [topological_space K] [nonarchimedean_group K] {U : set (G × K)} (hU : U nhds 1) :
∃ (V : open_subgroup G) (W : open_subgroup 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 nonarchimedean_add_group.prod_self_subset {G : Type u_1} [add_group G] [topological_space G] [nonarchimedean_add_group G] {U : set (G × G)} (hU : U nhds 0) :
∃ (V : open_add_subgroup 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 nonarchimedean_group.prod_self_subset {G : Type u_1} [group G] [topological_space G] [nonarchimedean_group G] {U : set (G × G)} (hU : U nhds 1) :
∃ (V : open_subgroup 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.

@[protected, instance]

The cartesian product of two nonarchimedean groups is nonarchimedean.

@[protected, instance]

The cartesian product of two nonarchimedean groups is nonarchimedean.

@[protected, instance]

The cartesian product of two nonarchimedean rings is nonarchimedean.

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

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