Zulip Chat Archive

Stream: maths

Topic: nonarchimedean rings


view this post on Zulip 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.

view this post on Zulip Eric Wieser (Feb 20 2021 at 13:12):

branch#nonarchimedean

view this post on Zulip 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

view this post on Zulip Ashwin Iyengar (Feb 20 2021 at 13:47):

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

view this post on Zulip Kevin Buzzard (Feb 20 2021 at 16:42):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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)

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 22 2021 at 07:30):

I think Eric's suggestion is the best

view this post on Zulip Ashwin Iyengar (Feb 26 2021 at 00:52):

Some ramblings: given a nonarchimedean topological ring RR, a set of indeterminates (Xi)iI(X_i)_{i \in I} for some indexing set II and a finite set TiT_i for each iIi \in I (the TiT_i must satisfy some topological hypothesis, which I'm ignoring for the moment), then a restricted power series is an expression ν:IN finitely supportedcνXν\sum_{\nu: I \to \mathbb{N} \text{ finitely supported}} c_\nu X^\nu such that for every open subgroup URU \subset R, the set {νcν∉TνU}\{ \nu | c_\nu \not \in T^\nu U \} is finite. Here Tν=iITiν(i)T^\nu = \prod_{i \in I} T_i^{\nu(i)}. This suggests the definition (note I haven't specified the TiT_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 iIi \in I we have Ti={ai}T_i = \{a_i\} where aiR×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νTνUc_\nu \in T^\nu U to (aν)1cνU(a^\nu)^{-1} c_\nu \in U. Here aν=iIaiν(i)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.

view this post on Zulip 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

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}

view this post on Zulip Ashwin Iyengar (Mar 05 2021 at 00:56):

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

view this post on Zulip 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