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) [AddGroup G] [TopologicalSpace G] extends TopologicalAddGroup : Prop

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 : ∀ U ∈ nhds 0, ∃ (V : OpenAddSubgroup G), ↑V ⊆ U

class NonarchimedeanGroup (G : Type u_1) [Group G] [TopologicalSpace G] extends TopologicalGroup : Prop

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

• continuous_mul : Continuous fun (p : G × G) => p.1 * p.2
• continuous_inv : Continuous fun (a : G) => a⁻¹
• is_nonarchimedean : ∀ U ∈ nhds 1, ∃ (V : OpenSubgroup G), ↑V ⊆ U

class NonarchimedeanRing (R : Type u_1) [Ring R] [TopologicalSpace R] extends TopologicalRing : Prop

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

• continuous_add : Continuous fun (p : R × R) => p.1 + p.2
• continuous_mul : Continuous fun (p : R × R) => p.1 * p.2
• continuous_neg : Continuous fun (a : R) => -a
• is_nonarchimedean : ∀ U ∈ nhds 0, ∃ (V : OpenAddSubgroup R), ↑V ⊆ U

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

Every nonarchimedean ring is naturally a nonarchimedean additive group.

Equations

• (_ : NonarchimedeanAddGroup R) = (_ : NonarchimedeanAddGroup R)

theorem NonarchimedeanAddGroup.nonarchimedean_of_emb {G : Type u_1} [AddGroup G] [TopologicalSpace G] [NonarchimedeanAddGroup G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] [TopologicalAddGroup H] (f : G →+ H) (emb : OpenEmbedding ⇑f) : NonarchimedeanAddGroup H

abbrev NonarchimedeanAddGroup.nonarchimedean_of_emb.match_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] {H : Type u_2} [AddGroup H] (f : G →+ H) (U : Set H) (motive : (∃ (V : OpenAddSubgroup G), ↑V ⊆ ⇑f ⁻¹' U) → Prop) : ∀ (x : ∃ (V : OpenAddSubgroup G), ↑V ⊆ ⇑f ⁻¹' U), (∀ (V : OpenAddSubgroup G) (hV : ↑V ⊆ ⇑f ⁻¹' U), motive (_ : ∃ (V : OpenAddSubgroup G), ↑V ⊆ ⇑f ⁻¹' U)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

theorem NonarchimedeanGroup.nonarchimedean_of_emb {G : Type u_1} [Group G] [TopologicalSpace G] [NonarchimedeanGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [TopologicalGroup H] (f : G →* H) (emb : OpenEmbedding ⇑f) : NonarchimedeanGroup H

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

theorem NonarchimedeanAddGroup.prod_subset {G : Type u_1} [AddGroup G] [TopologicalSpace G] [NonarchimedeanAddGroup G] {K : Type u_3} [AddGroup K] [TopologicalSpace K] [NonarchimedeanAddGroup K] {U : Set (G × K)} (hU : U ∈ nhds 0) : ∃ (V : OpenAddSubgroup G) (W : OpenAddSubgroup 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 NonarchimedeanGroup.prod_subset {G : Type u_1} [Group G] [TopologicalSpace G] [NonarchimedeanGroup G] {K : Type u_3} [Group K] [TopologicalSpace K] [NonarchimedeanGroup K] {U : Set (G × K)} (hU : U ∈ nhds 1) : ∃ (V : OpenSubgroup G) (W : OpenSubgroup 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 NonarchimedeanAddGroup.prod_self_subset {G : Type u_1} [AddGroup G] [TopologicalSpace G] [NonarchimedeanAddGroup G] {U : Set (G × G)} (hU : U ∈ nhds 0) : ∃ (V : OpenAddSubgroup 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.

abbrev NonarchimedeanAddGroup.prod_self_subset.match_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : Set (G × G)} (motive : (∃ (V : OpenAddSubgroup G) (W : OpenAddSubgroup G), ↑V ×ˢ ↑W ⊆ U) → Prop) : ∀ (x : ∃ (V : OpenAddSubgroup G) (W : OpenAddSubgroup G), ↑V ×ˢ ↑W ⊆ U), (∀ (V W : OpenAddSubgroup G) (h : ↑V ×ˢ ↑W ⊆ U), motive (_ : ∃ (V : OpenAddSubgroup G) (W : OpenAddSubgroup G), ↑V ×ˢ ↑W ⊆ U)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

theorem NonarchimedeanGroup.prod_self_subset {G : Type u_1} [Group G] [TopologicalSpace G] [NonarchimedeanGroup G] {U : Set (G × G)} (hU : U ∈ nhds 1) : ∃ (V : OpenSubgroup 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.

abbrev NonarchimedeanAddGroup.instNonarchimedeanAddGroupSumInstAddGroupInstTopologicalSpaceSum.match_1 {G : Type u_1} [AddGroup G] [TopologicalSpace G] {K : Type u_2} [AddGroup K] [TopologicalSpace K] (U : Set (G × K)) (motive : (∃ (V : OpenAddSubgroup G) (W : OpenAddSubgroup K), ↑V ×ˢ ↑W ⊆ U) → Prop) : ∀ (x : ∃ (V : OpenAddSubgroup G) (W : OpenAddSubgroup K), ↑V ×ˢ ↑W ⊆ U), (∀ (V : OpenAddSubgroup G) (W : OpenAddSubgroup K) (h : ↑V ×ˢ ↑W ⊆ U), motive (_ : ∃ (V : OpenAddSubgroup G) (W : OpenAddSubgroup K), ↑V ×ˢ ↑W ⊆ U)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

instance NonarchimedeanAddGroup.instNonarchimedeanAddGroupSumInstAddGroupInstTopologicalSpaceSum {G : Type u_1} [AddGroup G] [TopologicalSpace G] [NonarchimedeanAddGroup G] {K : Type u_3} [AddGroup K] [TopologicalSpace K] [NonarchimedeanAddGroup K] : NonarchimedeanAddGroup (G × K)

The cartesian product of two nonarchimedean groups is nonarchimedean.

Equations

• (_ : NonarchimedeanAddGroup (G × K)) = (_ : NonarchimedeanAddGroup (G × K))

instance NonarchimedeanGroup.instNonarchimedeanGroupProdInstGroupInstTopologicalSpaceProd {G : Type u_1} [Group G] [TopologicalSpace G] [NonarchimedeanGroup G] {K : Type u_3} [Group K] [TopologicalSpace K] [NonarchimedeanGroup K] : NonarchimedeanGroup (G × K)

The cartesian product of two nonarchimedean groups is nonarchimedean.

Equations

• (_ : NonarchimedeanGroup (G × K)) = (_ : NonarchimedeanGroup (G × K))

instance NonarchimedeanRing.instNonarchimedeanRingProdInstRingInstTopologicalSpaceProd {R : Type u_1} {S : Type u_2} [Ring R] [TopologicalSpace R] [NonarchimedeanRing R] [Ring S] [TopologicalSpace S] [NonarchimedeanRing S] : NonarchimedeanRing (R × S)

The cartesian product of two nonarchimedean rings is nonarchimedean.

Equations

• (_ : NonarchimedeanRing (R × S)) = (_ : NonarchimedeanRing (R × S))

theorem NonarchimedeanRing.left_mul_subset {R : Type u_1} [Ring R] [TopologicalSpace R] [NonarchimedeanRing R] (U : OpenAddSubgroup R) (r : R) : ∃ (V : OpenAddSubgroup 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.

theorem NonarchimedeanRing.mul_subset {R : Type u_1} [Ring R] [TopologicalSpace R] [NonarchimedeanRing R] (U : OpenAddSubgroup R) : ∃ (V : OpenAddSubgroup R), ↑V * ↑V ⊆ ↑U

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