nonarchimedean rings

Stream: maths

[Ashwin Iyengar]

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]

branch#nonarchimedean

[Kevin Buzzard]

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

[Ashwin Iyengar]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

@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]

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]

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)

@[to_additive]
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)

@[to_additive]
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]

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]

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]

I think Eric's suggestion is the best

[Ashwin Iyengar]

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 //
  ∀ U : open_add_subgroup 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]

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

class nonarchimedean_topological_add_group (G : Type*)
  [add_group G] [topological_space G] extends topological_add_group G : Prop :=
(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.-/
@[to_additive]
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)

instance nonarchimedean_topological_ring.to_nonarchimedean_topological_add_group
  (R : Type*) [ring R] [topological_space R] [t: nonarchimedean_topological_ring R] :
nonarchimedean_topological_add_group R := {..t}

[Ashwin Iyengar]

Nevermind, the issue was that I had added

@[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]

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