## Stream: maths

### Topic: nonarchimedean rings

#### Ashwin Iyengar (Feb 20 2021 at 12:55):

I've pushed a definition of nonarchimedean normed ring with the Gauss norm to the branch "nonarchimedean", but then realized that I could do the same definition for more general nonarchimedean topological ring. I'm just putting this here to see if anyone has any thoughts on whether increasing the level of generality seems sensible/desirable.

#### Eric Wieser (Feb 20 2021 at 13:12):

branch#nonarchimedean

#### Kevin Buzzard (Feb 20 2021 at 13:41):

Did you take a look at what we did in the perfectoid project? I think we developed a bunch of theory

#### Ashwin Iyengar (Feb 20 2021 at 13:47):

Havent looked at it too carefully, maybe I'll take a closer look

#### Kevin Buzzard (Feb 20 2021 at 16:42):

https://github.com/leanprover-community/lean-perfectoid-spaces/tree/master/src/for_mathlib/nonarchimedean

#### Kevin Buzzard (Feb 20 2021 at 16:50):

@Patrick Massot modulo tidying up proofs, is all this stuff PR-able or should there be some changes because of what has happened in mathlib since 2019?

#### Ashwin Iyengar (Feb 20 2021 at 18:19):

Ok yeah I found this, and put it in my copy of mathlib and there are errors, but they mostly seem minor. I'll get to work on fixing them up and push

#### Ashwin Iyengar (Feb 21 2021 at 15:17):

From a mathlib design perspective, which looks most sensible? I like the second class definition best, but the "def" definition is what was in the perfectoid project.

@[to_additive]
class nonarchimedean_topological_group (G : Type*)
[group G] [topological_space G] [topological_group G] :=
(is_nonarchimedean : ∀ U ∈ nhds (1 : G), ∃ V : open_subgroup G, (V : set G) ⊆ U)

class nonarchimedean_topological_group (G : Type*)
extends group G, topological_space G, topological_group G :=
(is_nonarchimedean : ∀ U ∈ nhds (1 : G), ∃ V : open_subgroup G, (V : set G) ⊆ U)

def topological_group.nonarchimedean (G : Type*)
[group G] [topological_space G] [topological_group G] : Prop :=
∀ U ∈ nhds (1 : G), ∃ V : open_subgroup G, (V : set G) ⊆ U


#### Eric Wieser (Feb 21 2021 at 15:38):

I'd propose either option 1, or a variant:

@[to_additive]
class nonarchimedean_topological_group (G : Type*)
[group G] [topological_space G] extends topological_group G :=
(is_nonarchimedean : ∀ U ∈ nhds (1 : G), ∃ V : open_subgroup G, (V : set G) ⊆ U)


since that matches the level of bundling of docs#topological_group

#### Kevin Buzzard (Feb 21 2021 at 15:40):

In 2018 there were various ideas about how we should be making things like this. We now know what we're doing a lot better, in the sense that we experimented with various design decisions and now have a much better understanding of what works.

#### Johan Commelin (Feb 22 2021 at 07:30):

I think Eric's suggestion is the best

#### Ashwin Iyengar (Feb 26 2021 at 00:52):

Some ramblings: given a nonarchimedean topological ring $R$, a set of indeterminates $(X_i)_{i \in I}$ for some indexing set $I$ and a finite set $T_i$ for each $i \in I$ (the $T_i$ must satisfy some topological hypothesis, which I'm ignoring for the moment), then a restricted power series is an expression $\sum_{\nu: I \to \mathbb{N} \text{ finitely supported}} c_\nu X^\nu$ such that for every open subgroup $U \subset R$, the set $\{ \nu | c_\nu \not \in T^\nu U \}$ is finite. Here $T^\nu = \prod_{i \in I} T_i^{\nu(i)}$. This suggests the definition (note I haven't specified the $T_i$ are finite in this definition, need to add this)

def mv_strict_power_series (σ R : Type*)
[comm_ring R] [topological_space R] [nonarchimedean_topological_ring R] (T : σ → set R) :=
{f : mv_power_series σ R //
{n | (coeff R n f) ∉ ((∏ s in n.support, (T s)^(n s)) * (U : set R))}.finite}


But on the other hand if you assume that for all $i \in I$ we have $T_i = \{a_i\}$ where $a_i \in R^\times$ (which is an important special case but isn't quite general enough to do everything you want), then you can sort of cheat and switch $c_\nu \in T^\nu U$ to $(a^\nu)^{-1} c_\nu \in U$. Here $a^\nu = \prod_{i \in I} a_i^{\nu(i)}$. Then you can write

def mv_strict_power_series (σ R : Type*)
[comm_ring R] [topological_space R] [nonarchimedean_topological_ring R] (T : σ → units R) :=
{f : mv_power_series σ R //
tendsto (λ n : σ →₀ ℕ, (∏ s in n.support, ((T s)⁻¹.val)^(n s)) * (coeff R n f)) cofinite (nhds 0)}


which gives you access to all of the filter machinery. But sadly I don't immediately see how to use the filter machinery outside of this special case: there's probably something clever that I'm not seeing yet.

#### Ashwin Iyengar (Mar 05 2021 at 00:50):

Does this look sensible? I'm getting errors later on about maximum class-instance depth reached, and I feel like it's because docs#topological_ring.to_topological_add_group already exists, but I want to say that whenever you have nonarchimedean_topological_ring R you also get nonarchimedean_topological_add_group R but my current approach seems to give rise to two different instances of topological_add_group R.

import topology.algebra.ring
import topology.algebra.open_subgroup
import data.set.basic
import group_theory.subgroup
import algebra.ring.prod

(is_nonarchimedean : ∀ U ∈ nhds (0 : G), ∃ V : open_add_subgroup G, (V : set G) ⊆ U)

/--A topological group is non-archimedean if every neighborhood of 1 contains an open subgroup.-/
class nonarchimedean_topological_group (G : Type*)
[group G] [topological_space G] extends topological_group G : Prop :=
(is_nonarchimedean : ∀ U ∈ nhds (1 : G), ∃ V : open_subgroup G, (V : set G) ⊆ U)

class nonarchimedean_topological_ring (R : Type*)
[ring R] [topological_space R] extends topological_ring R : Prop :=
(is_nonarchimedean : ∀ U ∈ nhds (0 : R), ∃ V : open_add_subgroup R, (V : set R) ⊆ U)

(R : Type*) [ring R] [topological_space R] [t: nonarchimedean_topological_ring R] :


#### Ashwin Iyengar (Mar 05 2021 at 00:56):

@[to_additive]
instance emb_of_na (f : G →* H) (emb : open_embedding f) : nonarchimedean_topological_group H :=
{ is_nonarchimedean := λ U hU, have h₁ : (f ⁻¹' U) ∈ nhds (1 : G), from
by {apply emb.continuous.tendsto, rwa is_group_hom.map_one f},
let ⟨V, hV⟩ := is_nonarchimedean (f ⁻¹' U) h₁ in
⟨{is_open' := emb.is_open_map _ V.is_open, ..subgroup.map f V},
set.image_subset_iff.2 hV⟩ }


which seems like a pretty bad idea

#### Johan Commelin (Mar 05 2021 at 04:25):

Right, that should be a lemma, not an instance (-;

Last updated: May 12 2021 at 08:14 UTC