mathlib3 documentation

topology.algebra.nonarchimedean.basic

Nonarchimedean Topology #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source
@[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
source
@[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
source
@[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
source
@[protected, instance]
def nonarchimedean_ring.to_nonarchimedean_add_group (R : Type u_1) [ring R] [topological_space R] [t : nonarchimedean_ring R] :
nonarchimedean_add_group R

Every nonarchimedean ring is naturally a nonarchimedean additive group.

source
theorem nonarchimedean_add_group.nonarchimedean_of_emb {G : Type u_1} [add_group G] [topological_space G] [nonarchimedean_add_group G] {H : Type u_2} [add_group H] [topological_space H] [topological_add_group H] (f : G →+ H) (emb : open_embedding ⇑f) :
nonarchimedean_add_group H

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

source
theorem nonarchimedean_group.nonarchimedean_of_emb {G : Type u_1} [group G] [topological_space G] [nonarchimedean_group G] {H : Type u_2} [group H] [topological_space H] [topological_group H] (f : G →* H) (emb : open_embedding ⇑f) :
nonarchimedean_group H

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

source
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) :
∃ (V : open_add_subgroup G) (W : open_add_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.

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

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

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

source
@[protected, instance]
def nonarchimedean_add_group.prod.nonarchimedean_add_group {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] :
nonarchimedean_add_group (G × K)

The cartesian product of two nonarchimedean groups is nonarchimedean.

source
@[protected, instance]
def nonarchimedean_group.prod.nonarchimedean_group {G : Type u_1} [group G] [topological_space G] [nonarchimedean_group G] {K : Type u_3} [group K] [topological_space K] [nonarchimedean_group K] :
nonarchimedean_group (G × K)

The cartesian product of two nonarchimedean groups is nonarchimedean.

source
@[protected, instance]
def nonarchimedean_ring.prod.nonarchimedean_ring {R : Type u_1} {S : Type u_2} [ring R] [topological_space R] [nonarchimedean_ring R] [ring S] [topological_space S] [nonarchimedean_ring S] :
nonarchimedean_ring (R × S)

The cartesian product of two nonarchimedean rings is nonarchimedean.

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

source
theorem nonarchimedean_ring.mul_subset {R : Type u_1} [ring R] [topological_space R] [nonarchimedean_ring R] (U : open_add_subgroup R) :
∃ (V : open_add_subgroup R), ↑V * ↑V ⊆ ↑U

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