mathlib sprint

Stream: condensed mathematics

[Johan Commelin]

Scott suggested that we do a mathlib sprint before continuing with the col_exact part of the proof. I think he has a very good point.

[Johan Commelin]

jmc@atarrimbo:~/data/math/lean-liquid$ wc -l src/for_mathlib/*.lean
    18 src/for_mathlib/additive_functor.lean
    93 src/for_mathlib/add_monoid_hom.lean
    89 src/for_mathlib/arrow.lean
    16 src/for_mathlib/big_operators_basic.lean
    30 src/for_mathlib/category.lean
     9 src/for_mathlib/curry.lean
    42 src/for_mathlib/dfinsupp.lean
    55 src/for_mathlib/equalizers.lean
    31 src/for_mathlib/extend_from_nat.lean
    36 src/for_mathlib/filter_at_top_bot.lean
    44 src/for_mathlib/finsupp.lean
   400 src/for_mathlib/free_abelian_group.lean
   135 src/for_mathlib/Gordan.lean
   100 src/for_mathlib/grading_examples.lean
   544 src/for_mathlib/grading.lean
    54 src/for_mathlib/grading_monoid_algebra.lean
   165 src/for_mathlib/grading_zero_subring.lean
    58 src/for_mathlib/int_grading_lemma.lean
    90 src/for_mathlib/kronecker.lean
    70 src/for_mathlib/linear_algebra.lean
    35 src/for_mathlib/nnreal.lean
    99 src/for_mathlib/normed_group_hom_bound_by.lean
   175 src/for_mathlib/normed_group_hom_completion.lean
    96 src/for_mathlib/normed_group_hom_equalizer.lean
    72 src/for_mathlib/normed_group_hom.lean
   167 src/for_mathlib/normed_group.lean
   360 src/for_mathlib/normed_group_quotient.lean
    26 src/for_mathlib/order_basic.lean
    14 src/for_mathlib/pi_nat_apply.lean
    74 src/for_mathlib/preadditive_category.lean
    21 src/for_mathlib/Profinite.lean
    34 src/for_mathlib/pseudo_metric.lean
    26 src/for_mathlib/quotient_group.lean
    26 src/for_mathlib/real_Inf.lean
    72 src/for_mathlib/specific_limit.lean
    34 src/for_mathlib/tsum.lean
    37 src/for_mathlib/uniform_space_cauchy.lean
  3447 total

[Kevin Buzzard]

The biggest file there is grading.lean and I was hoping to leave it there until the proof of Gordan's lemma is done -- basically Gordan will be the proof that Eric and I have got gradings right

[Johan Commelin]

Sure, we can leave the Gordan files there for now.

[Johan Commelin]

But there is enough other stuff that can be moved to mathlib already :grinning:

[Johan Commelin]

Some easy progress:

    75 src/for_mathlib/add_monoid_hom.lean
    86 src/for_mathlib/arrow.lean -- PR exists
    16 src/for_mathlib/big_operators_basic.lean
    32 src/for_mathlib/category.lean -- PR exists
    11 src/for_mathlib/curry.lean -- PR exists
    42 src/for_mathlib/dfinsupp.lean
    55 src/for_mathlib/equalizers.lean
    36 src/for_mathlib/filter_at_top_bot.lean
    44 src/for_mathlib/finsupp.lean
   400 src/for_mathlib/free_abelian_group.lean
   135 src/for_mathlib/Gordan.lean
   100 src/for_mathlib/grading_examples.lean
   544 src/for_mathlib/grading.lean
    54 src/for_mathlib/grading_monoid_algebra.lean
   165 src/for_mathlib/grading_zero_subring.lean
    58 src/for_mathlib/int_grading_lemma.lean
    90 src/for_mathlib/kronecker.lean
    70 src/for_mathlib/linear_algebra.lean
    35 src/for_mathlib/nnreal.lean
    99 src/for_mathlib/normed_group_hom_bound_by.lean
   175 src/for_mathlib/normed_group_hom_completion.lean
    96 src/for_mathlib/normed_group_hom_equalizer.lean
    72 src/for_mathlib/normed_group_hom.lean
   167 src/for_mathlib/normed_group.lean
   360 src/for_mathlib/normed_group_quotient.lean
    26 src/for_mathlib/order_basic.lean
    14 src/for_mathlib/pi_nat_apply.lean
    74 src/for_mathlib/preadditive_category.lean
    21 src/for_mathlib/Profinite.lean
    34 src/for_mathlib/pseudo_metric.lean
    26 src/for_mathlib/quotient_group.lean
    26 src/for_mathlib/real_Inf.lean
    72 src/for_mathlib/specific_limit.lean
    34 src/for_mathlib/tsum.lean
    37 src/for_mathlib/uniform_space_cauchy.lean
  3381 total

[Patrick Massot]

I'll open topology PRs

[Johan Commelin]

Merci!

[Riccardo Brasca]

I will do some normed_group stuff.

[Riccardo Brasca]

You mentioned that the quotient has causes some diamond, right?

[Johan Commelin]

But with pseudo_normed_group which isn't moving to mathlib anytime soon, I think

[Johan Commelin]

Ooh, I think you are refering to another issue.

[Johan Commelin]

Yes, I don't fully understand it.

[Johan Commelin]

https://github.com/leanprover-community/lean-liquid/blob/master/src/polyhedral_lattice/cech.lean#L156 is quite evil

[Riccardo Brasca]

My concern was much more basic: the quotient is a topological space in two ways, I don't if this is going to be a problem

[Johan Commelin]

It might very well be the problem that I was hitting

[Johan Commelin]

And it certainly will start causing problems at some point.

[Johan Commelin]

But this can be fixed by not using of_core

[Johan Commelin]

If you manually fill in all the fields the you can give it the quotient topology and prove that this is equal to the norm topology.

[Eric Wieser]

Kevin Buzzard said:

The biggest file there is grading.lean and I was hoping to leave it there until the proof of Gordan's lemma is done -- basically Gordan will be the proof that Eric and I have got gradings right

I've got a few mathlib PRs open for grading-related things already; (#7380, #7420, #7422)

[Kevin Buzzard]

These are all "external grading" PR's -- grading.lean is the "internal grading" version. I've been trying to make sure that our ideas glue together with one another.

[Johan Commelin]

The first two of Eric's PRs are now on the queue. Nr3 depends on nr2, so has to wait a bit.

[Johan Commelin]

@Eric Wieser was this stuff that is also in for_mathlib?

[Kevin Buzzard]

No I don't think so

[Kevin Buzzard]

The grading file in for_mathlib can be split up into two pieces: there are unfortunately four stories here, or possibly even six if you do it properly. There's gradings of an add_comm_monoid by add_submonoids indexed by a type, gradings of an add_comm_group by add_subgroups indexed by a type (the types submonoid G and subgroup G are not defeq, and it seems to be practical just to do everything twice :-( ), and then there are gradings of a semiring and a ring by add_submonoids and add_subgroups respectively, indexed by both a monoid and an add_monoid (and goodness knows whether to_additive will work). In collaboration with Eric I've developed a bunch of the theory, but now it's getting to the point where I just want to get Gordan out of the way so I've started focussing on the case we're interested in, namely gradings of a ring by add_subgroups indexed by an add_monoid.

[Eric Wieser]

Yes, sorry, I should have made the fact it was external clear. I kept trying to do internal ones and ending up finding the external version easier to prove

[Kevin Buzzard]

Right now things are fine because I'm still tinkering with the API for internal stuff, and if it starts going into mathlib then this will add to the confusion.

[Johan Commelin]

Ooops! My wc -l was too naive...

[Johan Commelin]

jmc@atarrimbo:~/data/math/lean-liquid$ git ls-files | grep for_mathlib | xargs wc -l
    26 src/for_mathlib/Fintype/basic.lean
   135 src/for_mathlib/Gordan.lean
    30 src/for_mathlib/Profinite.lean
  1029 src/for_mathlib/Profinite/functorial_limit.lean
    46 src/for_mathlib/Profinite/limits.lean
    69 src/for_mathlib/Profinite/locally_constant.lean
    67 src/for_mathlib/Profinite/nhds.lean
    34 src/for_mathlib/Top/limits.lean
    86 src/for_mathlib/arrow.lean
    16 src/for_mathlib/big_operators_basic.lean
    32 src/for_mathlib/category.lean
    11 src/for_mathlib/curry.lean
    42 src/for_mathlib/dfinsupp.lean
    55 src/for_mathlib/equalizers.lean
    36 src/for_mathlib/filter_at_top_bot.lean
    44 src/for_mathlib/finsupp.lean
   400 src/for_mathlib/free_abelian_group.lean
   544 src/for_mathlib/grading.lean
   100 src/for_mathlib/grading_examples.lean
    54 src/for_mathlib/grading_monoid_algebra.lean
   165 src/for_mathlib/grading_zero_subring.lean
    58 src/for_mathlib/int_grading_lemma.lean
    90 src/for_mathlib/kronecker.lean
    70 src/for_mathlib/linear_algebra.lean
    35 src/for_mathlib/nnreal.lean
   167 src/for_mathlib/normed_group.lean
    72 src/for_mathlib/normed_group_hom.lean
    99 src/for_mathlib/normed_group_hom_bound_by.lean
   175 src/for_mathlib/normed_group_hom_completion.lean
    96 src/for_mathlib/normed_group_hom_equalizer.lean
   360 src/for_mathlib/normed_group_quotient.lean
    26 src/for_mathlib/order_basic.lean
    14 src/for_mathlib/pi_nat_apply.lean
    74 src/for_mathlib/preadditive_category.lean
    34 src/for_mathlib/pseudo_metric.lean
    26 src/for_mathlib/quotient_group.lean
    26 src/for_mathlib/real_Inf.lean
    81 src/for_mathlib/simplicial/augmented.lean
   158 src/for_mathlib/simplicial/complex.lean
    72 src/for_mathlib/specific_limit.lean
    34 src/for_mathlib/tsum.lean
    37 src/for_mathlib/uniform_space_cauchy.lean
  4825 total

[Johan Commelin]

Moving all of this to mathlib is going to cut the de Bruijn constant of the project by 30%

[Patrick Massot]

I PRed filter_at_top_bot.lean and order_basic.lean

[Patrick Massot]

and big_operators_basic.lean

[Patrick Massot]

I opened a PR for nnreal.lean and created a temporary wiki page at https://github.com/leanprover-community/lean-liquid/wiki

[Johan Commelin]

Thanks for creating that wiki page

[Patrick Massot]

I didn't add PR numbers unless it was very quick to find the number with certainty

[Patrick Massot]

Do we want to create dependent PRs or wait a bit for a first wave of merge? I think I'll be quickly stuck until #7469 is merged.

[Patrick Massot]

It would be nice if @Sebastien Gouezel could have a look at #7469 soon, it should be pretty quick, unless I missed existing lemmas or golfing opportunities.

[Johan Commelin]

I think dependent PRs are fine, if you think the PR it depends on is completely straightforward, or if you don't mind backporting updates from the dependency to the depending PR

[Patrick Massot]

Riccardo Brasca said:

I will do some normed_group stuff.

Do you mean the pseudo normed stuff or also my work?

[Johan Commelin]

I think he meant quotients of (semi) normed groups

[Johan Commelin]

Which are currently in the normed_group_hom namespace. (@Riccardo Brasca they should probably move out of that...)

[Riccardo Brasca]

Yes, I meant quotient of seminormed groups. I am currently PRing for_mathlib/normed_group_hom.lean, that is easy

[Patrick Massot]

This particular file is part of my work. I don't mind at all (although I would slightly prefer to PR my non-trivial stuff myself), I mostly want to avoid duplicating PRs.

[Riccardo Brasca]

Ah sorry, I saw that the lemma were easy enough to PR them quite quickly. In any case I will do normed_group_quotient.lean next.

[Sebastien Gouezel]

Patrick Massot said:

It would be nice if Sebastien Gouezel could have a look at #7469 soon, it should be pretty quick, unless I missed existing lemmas or golfing opportunities.

Done.

[Kevin Buzzard]

I put a bunch of sorried statements into polyhedral_lattice.basic a few weeks ago, and I've now moved them out into their own for_mathlib.finite_free file. In case anyone decides to sprint towards them -- I'm sitting on these sorrys because Anne is bundling is_basis so all the proofs will break. All but one should be trivial, but one (kernel of a non-zero map from $\Z^n$ to $\Z$ is finite free of rank one less than where you started) might be difficulr. @Anne Baanen should I PR some of these (and then they become your problem) or sit on them until you've refactored?

[Anne Baanen]

I was hoping to create the final bundled basis PR today after I fix the last lint errors, though merging might take a bit longer since I still have to check for any style issues. I could make a WIP pull request right now, to allow you to base your additions on top of it.

[Johan Commelin]

I think we can wait for a couple of days (-;

[Johan Commelin]

There is so much in flux right now that I don't think we should depend on a PR instead of mathlib master

[Patrick Massot]

Thanks Sébastien!

[Adam Topaz]

Just catching up here... a mathlib sprint is a great idea! I opened #7448 yesterday which takes care of for_mathlib/***/limits.lean where *** = Top, Profinite. I updated the wiki as well.

[Patrick Massot]

Did we already reached that 200 open PR score before?

[Kevin Buzzard]

Surely not.

[Patrick Massot]

Johan, why did you add check boxes to the wiki page? When to you want to tick off an item? When the PR is merged?

[Johan Commelin]

For some reason the ticks didn't seem to work... but my idea was that we could tick off an item when a PR was made, and then remove the item when the PR is merged. But it's not very important.

[Adam Topaz]

For Fintype/basic.lean we should decide whether to add instance {A : Fintype} : topological_space A := ⊥ as a global instance ;)

[Riccardo Brasca]

It works if one writes [x].

[Johan Commelin]

Right, but you can't just click on the checkbox. You need to edit. Well, I guess we need to edit anyway, to add PR numbers.

[Johan Commelin]

Adam Topaz said:

For Fintype/basic.lean we should decide whether to add instance {A : Fintype} : topological_space A := ⊥ as a global instance ;)

I vote for def, and then make it a local instance when needed.

[Adam Topaz]

#7491

[Johan Commelin]

We're doing something wrong:

    26 src/for_mathlib/Fintype/basic.lean
   135 src/for_mathlib/Gordan.lean
    30 src/for_mathlib/Profinite.lean
  1029 src/for_mathlib/Profinite/functorial_limit.lean
    46 src/for_mathlib/Profinite/limits.lean
    69 src/for_mathlib/Profinite/locally_constant.lean
    67 src/for_mathlib/Profinite/nhds.lean
    34 src/for_mathlib/Top/limits.lean
    86 src/for_mathlib/arrow.lean
    16 src/for_mathlib/big_operators_basic.lean
    32 src/for_mathlib/category.lean
    11 src/for_mathlib/curry.lean
    42 src/for_mathlib/dfinsupp.lean
    55 src/for_mathlib/equalizers.lean
    36 src/for_mathlib/filter_at_top_bot.lean
   133 src/for_mathlib/finite_free.lean
    44 src/for_mathlib/finsupp.lean
   390 src/for_mathlib/free_abelian_group.lean
   630 src/for_mathlib/grading.lean
   104 src/for_mathlib/grading_examples.lean
    54 src/for_mathlib/grading_monoid_algebra.lean
   281 src/for_mathlib/grading_zero_subring.lean
    58 src/for_mathlib/int_grading_lemma.lean
    90 src/for_mathlib/kronecker.lean
    70 src/for_mathlib/linear_algebra.lean
    35 src/for_mathlib/nnreal.lean
   167 src/for_mathlib/normed_group.lean
    80 src/for_mathlib/normed_group_hom.lean
    99 src/for_mathlib/normed_group_hom_bound_by.lean
   175 src/for_mathlib/normed_group_hom_completion.lean
    96 src/for_mathlib/normed_group_hom_equalizer.lean
   360 src/for_mathlib/normed_group_quotient.lean
    26 src/for_mathlib/order_basic.lean
    14 src/for_mathlib/pi_nat_apply.lean
    74 src/for_mathlib/preadditive_category.lean
    34 src/for_mathlib/pseudo_metric.lean
    26 src/for_mathlib/quotient_group.lean
    26 src/for_mathlib/real_Inf.lean
    76 src/for_mathlib/simplicial/augmented.lean
   165 src/for_mathlib/simplicial/complex.lean
    72 src/for_mathlib/specific_limit.lean
    34 src/for_mathlib/tsum.lean
    37 src/for_mathlib/uniform_space_cauchy.lean
  5164 total

[Johan Commelin]

Total number of lines in for_mathlib is going up instead of down :thinking: :cold_sweat:

[Adam Topaz]

Sorry... I think my changes to for_mathlib/simplicial/* added a net of 2 lines.

[Johan Commelin]

Probably a bunch of grading stuff was added (-;

[Yaël Dillies]

Oh, you're doing simplicial stuff. Does that overlap in any way with the stuff Bhavik and I are doing to prove Sperner's Lemma? We define a simplicial complex as a set of finsets closed by inclusion and gluing nicely. From skimming through the files, I wouldn't say so, but I may be lacking insight.

[Johan Commelin]

No, we're not doing anything with that kind of simplicial complexes

[Johan Commelin]

I guess there is a bit of clash in terminology there

[Peter Scholze]

All this terminology with simplicial objects vs simplicial complexes is a bit of a mess...

[Yaël Dillies]

Yeah okay, that's what I was suspecting :)

[Riccardo Brasca]

I am going to start working on normed_group_quotient.lean. Since there a little bit of work to do here and I am not very experienced with diamonds, I would to know if the following is the good strategy. The problem is that if M is a semi_normed_group and S : add_subgroup M, then quotient S is automatically a uniform_space, but equipping quotient S with a seminorm will equip it with another uniform_space structure. My idea is the following.

• Equip quotient S with a seminorm, providing has_norm (quotient S).
• Equip quotient S with a pseudodistance, providing has_dist (quotient S): dist x y will be defined as ∥x - y∥.
• Prove all the relevant properties of ∥ ∥ (this is already done) and deduce the relevant properties of dist.
• Providing pseudo_metric_space (quotient S):
  * dist_self dist_comm dist_triangle are already proven.
  * edist and edist_dist can be ignored.
  * to_uniform_space : uniform_space (quotient S) here I guess that by apply_instance should work, but in any case it is the one already there.
• uniformity_dist: this is the main point that should be proven by hand.
• Redo everything for normed_group and a closed S.

[Johan Commelin]

That looks good to me.

[Johan Commelin]

Note that "Redo everything" shouldn't be a lot of work, because you can probably reuse the uniformity_dist proof.

[Adam Topaz]

Another option could be to make a type alias sub_semi_normed_group defined as add_subgroup and derive whatever you don't want to replicate

[Riccardo Brasca]

Sure! It's funny, this is not a Lean problem, uniformity_dist is a real mathematical theorem, whose standard proof is "it's called quotient, so it has the quotient topology".

[Johan Commelin]

That's exactly the trick that "forgetful inheritance" plays. You prove this theorem once and for all, and you never have to mention it again.

[Johan Commelin]

$ git commit -am "bump mathlib"
[master 465cbd5] bump mathlib
 10 files changed, 3 insertions(+), 104 deletions(-)
 delete mode 100644 src/for_mathlib/big_operators_basic.lean
 delete mode 100644 src/for_mathlib/category.lean
 delete mode 100644 src/for_mathlib/filter_at_top_bot.lean

[Riccardo Brasca]

I need some to solve the diamond about semi_normed_group quotient. I am really inexperienced in working with uniformity and stuff like that, so this can very well be not difficult but I don't know how to attack it. The specific lemma I need is here:
https://github.com/leanprover-community/lean-liquid/blob/61025a2661fac60cee1adc200681a31196ba584f/src/for_mathlib/normed_group_quotient.lean#L224
The second sorry is mathematically trivial, right? The identity from the space with the quotient topology to the same space with the topology induced by the metric is continuous since the composition with the projection (that is of course again the projection) is continuous. But I have no idea where to start
I don't mind doing the dirty work with the epsilon and so on, but I would appreciate some indication from some uniform_space guru.

[Patrick Massot]

is this on a special branch?

[Riccardo Brasca]

Yes, it is my branch riccardobrasca, we decided that for the LTE we could just ignore the diamond and so use normed_group.of_core

[Riccardo Brasca]

I started the work to PR it to mathlib so I did some modifications to the whole file that are irrelevant for this problem, the quickest way to show it was to add this instance to LTE (but not in master of course)

[Patrick Massot]

It's too late now, but I'll have a look tomorrow evening, don't worry.

[Riccardo Brasca]

Thank's! If I make some progress I will push it to the same branch

[Riccardo Brasca]

Note that I am not 100% sure this is the statement we want. The problem I want to solve is the following. If M is a semi_normed_group and S : add_subgroup M, then quotient S is automatically a topological_space, but equipping quotient S with a seminorm will equip it with another topological_space structure. We want these to be the same. The proposed solution is to first of all provide the pseudo_metric_space instance (via the norm of course, but by hand), using topological_add_group.to_uniform_space (quotient S) as uniformity, so we need to prove uniformity_dist for this uniformity.

[Johan Commelin]

Hmm, I don't think that is the uniformity you want to use. Is there already something for quotients of pseudo_metric_spaces?

[Riccardo Brasca]

We don't have anything about quotient of metric spaces. Indeed in general there is no hope to make it a metric space, but it's possible to make it a pseudometric space. But the compatibility with the quotient topology seems to be a subtle question, see for example here: https://mathoverflow.net/questions/195611/quotient-of-metric-spaces
In our case, quotient S is automatically a topological space (meaning that apply_instance works). There is no instance of uniform_space on it, but the doc for topological_add_group.to_uniform_space says "The right uniformity on a topological group", so I decided to work with it.

lemma test (S : add_subgroup M) :
  (topological_add_group.to_uniform_space (quotient S)).to_topological_space =
  quotient.topological_space := rfl

works, so I think we are good here.

[Johan Commelin]

Hmm, but topological_add_group.to_uniform_space is somewhat non-canonical. It just chooses the right uniformity (why not the left). I would be surprised if that's the best thing to do here. But it might be the best way to avoid crazy headaches.
Let me read that MO thread.

[Riccardo Brasca]

It's possible that there is no canonical uniformity on the quotient (although here the group commutative, so left and right should be the same). I mean, of course there is one, since there is a norm. But the (canonical) topological space structure comes from free, without using the norm, I don't know if the same is true for the uniformity

[Johan Commelin]

Does mathlib have quotients of topological groups?

[Johan Commelin]

src/topology/algebra/group.lean:instance topological_group_quotient [N.normal] : topological_group (quotient N) :=

looks good

[Johan Commelin]

Let's see what they do there

[Riccardo Brasca]

Yes, there is docs#topological_add_group_quotient

[Riccardo Brasca]

But it's only a topological space, not a uniform space

[Johan Commelin]

Right, it avoids the whole issue :sad:

[Riccardo Brasca]

For the topology everything is clear, but in mathlib a metric space is a metric that is compatible with a uniformity, not with a topology

[Johan Commelin]

We need to define the uniformity on the quotient in terms of the uniformity upstairs.

[Johan Commelin]

And maybe this is hard in general, but I think that for group quotients it should be easier

[Johan Commelin]

On the other hand, if there are no other ways of putting a uniformity on a quotient, this cannot lead to a diamond

[Johan Commelin]

So maybe it is fine to use topological_add_group.to_uniform_space on the quotient group.

[Riccardo Brasca]

But the diamond would appear for the topological_space structure, right?

[Johan Commelin]

But that is solved by what you are doing.

[Johan Commelin]

It appeared when using normed_group.of_core. Because then the topology wouldn't be the quotient topology.

[Johan Commelin]

I am far from an expert on uniformities, but isn't there something like a push-forward uniformity?

[Riccardo Brasca]

I have no idea :sweat_smile:

[Johan Commelin]

It looks like there is only a comap in general.

[Riccardo Brasca]

Wait! "The right uniformity on a topological group." means "The good uniformity on a topological group." or "The not left uniformity on a topological group."??

[Kevin Buzzard]

It means the not left one

[Johan Commelin]

The "not left" uniformity

[Johan Commelin]

But given that we are in the commutative setting, it doesn't matter up to defeq issues.

[Johan Commelin]

And of course defeq is exactly what we care about now :expressionless:

[Johan Commelin]

https://core.ac.uk/download/pdf/82205121.pdf Thm 11 suggests that {pi(U) | U is an entourage upstairs} should be a uniformity on the quotient. (Here pi is the quotient map to the quotient group.)

[Kevin Buzzard]

A uniformity is informally a way of saying "a is as close to b as c is to d". In a metric space we can say this as d(a,b)=d(c,d). In a topological space we can't say this because there is no way of comparing neighbourhoods of a to neighbourhoods of c. In a topological group however there are two ways of doing this -- left multiplication by c/a or right multiplication by a\c.

[Kevin Buzzard]

The first line of that paper seems to indicate that pushing forward a uniform structure along a quotient map is a problematic issue in general (which would explain the non-existence of map for uniform structures)

[Patrick Massot]

I'm on my phone and won't get to a computer in the next 8 hours. But I promise I'll handle this tonight. Indeed there is no pushfoward uniformity in general.

[Riccardo Brasca]

BTW I just bumped mathlib, removingsrc/for_mathlib/real_Inf.lean

[Johan Commelin]

Bunch of mathlib PRs merged. I'll do another bump

[Riccardo Brasca]

normed_group_hom.ker_eq_preimage has become normed_group_hom.coe_ker

[Johan Commelin]

The mathlib bump was intterupted by a trip to Kindergarten to pick up my daughter. But now it's done.

[Kevin Buzzard]

Thank you as ever!

Grading -- I see no problems with pushing this stuff through, however I have just had around 10 days of solid marking dumped on my desk so I might be less active than usual for the next week or two. My two worries are that (a) we're going to need that the kernel of a nonzero map $\Z^n\to\Z$ has rank $n-1$ and (b) the is_basis refactor will break a bunch of stuff (but it will be easy to fix). Everything else, I can see the light at the end of the tunnel.

[Johan Commelin]

Good luck... grading rings is sooo much more fun than grading exams.

[Riccardo Brasca]

How far are we from the following proof? Given $f \colon \mathbf{Z}^n \to \mathbf{Z}$, we know (even mathlib knows) that $\mathrm{im}(f)$ is free, so $0 \to \ker (f) \to \mathbf{Z}^n \to \mathrm{im}(f) \to 0$ splits and $\mathbf{Z}^n \cong \ker(f) \oplus \mathrm{im}(f)$ implies $\mathrm{rk} \ker(f) = n -1$.

[Johan Commelin]

We know that the rank is unique. So I think it's mostly the splitting that's needed.

[Riccardo Brasca]

I don't know the situation of the direct sum, but the section is given by docs#is_basis.constr

[Riccardo Brasca]

Now that #7523 is merged we can remove quotient_group.lean with the next bump. I don't have time this afternoon to look at it, but note that mk'_eq_mk'_iff has become quotient_add_group.eq_iff_sub_mem and it uses ↑ instead of mk'

[Johan Commelin]

thanks for the warning (-;

[Johan Commelin]

src/for_mathlib/grading_examples.lean is now broken, because polynomials are irreducible. I'm commenting it out for now. We can fix it after the mathlib bump.

[Johan Commelin]

Mathlib is bumped again.

[Kevin Buzzard]

Yes, we don't need that file in the proof.

[Patrick Massot]

I'm back to my computer and I have time to work on Riccardo's issue, but I fail to understand the issue. Why do you want to provide the uniform structure here?

[Patrick Massot]

I thought you had a diamond issue, but I don't see any diamond here.

[Sebastien Gouezel]

You have a topology on the quotient, which is the quotient topology. If you endow the quotient with a norm using of_core, this creates a second topology, which is not definitionally equal to the former.

[Patrick Massot]

I see. I was confused because they were talking about uniform structures, but the issue is already with the topology.

[Patrick Massot]

I got distracted and I have to stop, but at least I can tell you this uniform structure equality is true and this has some mathematical content. I'll type the Lean proof tomorrow.

[Patrick Massot]

I can also tell you it reduces to a statement that features no uniform structure. You need to prove that neighborhoods of zero in the quotient topology are exactly sets containing an open ball with positive radius around 0 for the norm we defined on the quotient.

[Riccardo Brasca]

Sorry for the late answer: indeed the diamond is at level of topological_space structure. My idea was to use the uniformity since pseudo_metric_space is set up that way.

lemma test (S : add_subgroup M) :
  (topological_add_group.to_uniform_space (quotient S)).to_topological_space =
  quotient.topological_space := rfl

works, so I think my strategy would solve the diamond.

[Johan Commelin]

I've started another mathlib bump on bump-08-may. This one needs a bit of care. A bunch of limit stuff for profinite sets has moved to mathlib. @Adam Topaz if you have time, could you take a look please?

[Patrick Massot]

I finished to prove quotient normed group have the correct uniformity, but I still don't know where I should push this since I don't know what is Riccardo's branch.

[Patrick Massot]

Presumably I should simply start writing mathlib PRs with all this.

[Patrick Massot]

@Riccardo Brasca, if you are curious, you can diff your version with https://gist.github.com/PatrickMassot/a499393c0affc16281e6b66f9506a781

[Patrick Massot]

You'll see I had to add a number of lemmas about groups that should be somewhere already. I'd be interested to know if you find them in mathlib

[Patrick Massot]

For everybody, I mean:

section
open quotient_group
variables {G : Type*} [group G]

@[to_additive]
lemma monoid_hom.eq_iff {H : Type*} [group H] (f : G →* H) {x y : G} : f x = f y ↔ y⁻¹*x ∈ f.ker :=
begin
  rw [f.mem_ker, f.map_mul, f.map_inv],
  split,
  { intro h,
    rw h,
    exact inv_mul_self (f y) },
  { intro h,
    convert congr_arg (λ z : H, (f y)*z) h ; simp }
end

variables (N : subgroup G) [N.normal]

@[to_additive]
lemma quotient_group.mk'_eq_iff {x y : G} : mk' N x = mk' N y ↔ y⁻¹*x ∈ N :=
by rw [(mk' N).eq_iff, quotient_group.ker_mk]

@[to_additive, simp]
lemma quotient_group.mk'_eq_one {x : G} (h : x ∈ N): mk' N x = 1 :=
by rwa [← monoid_hom.mem_ker, quotient_group.ker_mk]


@[to_additive]
lemma quotient_group.preimage_image {s : set G} :
  (mk' N) ⁻¹' ((mk' N) '' s) = ⋃ n : N, (λ x : G, (x*n : G)) ⁻¹' s :=
begin
  ext x,
  simp,
  split,
  { rintro ⟨g, g_in, h⟩,
    rw quotient_group.mk'_eq_iff at h,
    use ⟨_, h⟩,
    simpa using g_in },
  { rintro ⟨⟨g, g_in⟩, (h : x*g ∈ s)⟩,
    refine ⟨x*g, h, _⟩,
    rw (mk' N).map_mul,
    simp [g_in] },
end

end

[Eric Wieser]

Isn't mk'_eq_iff docs#quotient_group.eq?

[Riccardo Brasca]

Thank you!! I don't have time this weekend to work on it, if you want to PR feel free to do it!
My plan was to PR the whole normed_group_quotient.lean file, and this was needed to replace

instance semi_normed_group_quotient (S : add_subgroup M) :
  semi_normed_group (quotient S) :=
semi_normed_group.of_core (quotient S) (quotient.is_semi_normed_group.core S)

[Eric Wieser]

mk'_eq_one is a weaker version of docs#quotient_group.eq_one_iff

[Riccardo Brasca]

I think mk'_eq_one was exactly quotient_group.eq_one_iff before I PRed it and Eric improved it

[Riccardo Brasca]

In #7523

[Eric Wieser]

I don't know if we have monoid_hom.eq_iff

[Patrick Massot]

I knew I already wrote this!

[Patrick Massot]

I even wrote docs#quotient_group.preimage_image_coe, probably during the perfectoid project. But I used a direct image at that time, silly young me.

[Patrick Massot]

Eric Wieser said:

Isn't mk'_eq_iff docs#quotient_group.eq?

This is true only up to defeq, which is annoying for rewriting.

[Eric Wieser]

I get the feeling that mk' is not intended to be the simp-normal form

[Eric Wieser]

In the same way that docs#submonoid.subtype has few lemmas as coe is simp-normal

[Eric Wieser]

Perhaps we're missing a quotient_group.mk'_apply : mk' N x = (x : quotient_group N) or even quotient_group.coe_mk' : ⇑(mk' N) = coe simp lemma

[Patrick Massot]

This is not about simp normal forms. This is about explicit argument vs type class arguments.

[Patrick Massot]

Your quotient_group.mk'_apply : mk' N x = (x : quotient_group N) doesn't make sense because mk' N is used only when there is no instance allowing to make sense of (x : quotient_group N)

[Eric Wieser]

What instance / typeclass argument are you referring to?

[Eric Wieser]

This works fine for me:

import group_theory.quotient_group

namespace quotient_group

@[simp]
lemma coe_mk' {G : Type*} [group G] (N : subgroup G) [N.normal] :
  ⇑(mk' N) = coe := rfl

@[simp]
lemma mk'_apply {G : Type*} [group G] (N : subgroup G) [N.normal] (x : G) :
  mk' N x = x := rfl

end quotient_group

[Patrick Massot]

Sorry, I read too quickly what that file was doing.

[Eric Wieser]

I think you have your point backwards - it is docs#quotient_group.mk' that requires the extra N.normal instance argument, not coe (aka docs#quotient_group.quotient.has_coe_t)

[Eric Wieser]

To make matters worse, there's a third way to spell this, docs#quotient_group.mk

[Patrick Massot]

Yes, this whole area is a bit messy

[Adam Topaz]

Johan Commelin said:

I've started another mathlib bump on bump-08-may. This one needs a bit of care. A bunch of limit stuff for profinite sets has moved to mathlib. Adam Topaz if you have time, could you take a look please?

I'll take care of the profinite stuff this morning

[Adam Topaz]

Adam Topaz said:

Johan Commelin said:

I've started another mathlib bump on bump-08-may. This one needs a bit of care. A bunch of limit stuff for profinite sets has moved to mathlib. Adam Topaz if you have time, could you take a look please?

I'll take care of the profinite stuff this morning

Done! @Johan Commelin I think this makes up for the 2 lines I added to for_mathlib a few days ago:
https://github.com/leanprover-community/lean-liquid/compare/20019f38e734170b5574079bd268b8d3fdcbc653...009816d18fe288043abdc8980fb6a5a83e424e7e

[Johan Commelin]

Merci!

[Adam Topaz]

C'est rien

[Adam Topaz]

BTW, I also have an open PR about the Cech nerve: #7547 (it depends on #7546) in case anyone wants to take a look

[Johan Commelin]

did you merge and push to master?

[Adam Topaz]

No it's still in the brancch

[Adam Topaz]

I mean I pushed to the branch

[Adam Topaz]

Bah, I forgot about the other two files in profinite. I'll fix those now.

[Adam Topaz]

Okay, it should be fixed I think. I pushed to the branch again to see if CI is happy, then I'll merge to master

[Johan Commelin]

Thanks a lot

[Adam Topaz]

Okay, it's now updated on master

[Johan Commelin]

:tada:

[Patrick Massot]

@Riccardo Brasca I pushed a mathlib branch at https://github.com/leanprover-community/mathlib/tree/group-stuff. I still need to write a module docstring and maybe see if I can polish a bit, but you can already have a look and tell whether this looks good to you.

[Riccardo Brasca]

I will have a look at it this evening or tomorrow, thank's!

[Patrick Massot]

Note that one thing to discuss in particular is naming, especially the famous "namespace normed_group_hom -- probably needs to change" from here. I put those things in the add_subgroup namespace instead so that the normed group homomorphism from $M$ to $M/S$ is S.normed_mk. I think having access to this dot notation is nice, but I'm open to any other name for normed_mk. It cannot be mk because add_subgroup.mk is already the constructor for add_subgroup.

[Patrick Massot]

Maybe S.proj would be nicer but that sounds rather more like the algebraic version (ie. it should replace the ugly mk' S). We could look for a subscript or superscript evoking topology or norm, like the subscript l we use for linear maps.

[Eric Wieser]

For reference, the submodule version of docs#quotient_add_group.mk' is docs#submodule.mkq

[Eric Wieser]

And docs#quotient_add_group is analogous to docs#submodule.quotient. If renaming is on people's minds right now, it might make sense to rename the two to be more similar.

[Patrick Massot]

It would be nice to be consistent here. I'd be willing to implement any renaming if people tell me what they would like to see.

[Patrick Massot]

I'll be able to bump in about one hour.

[Johan Commelin]

@Patrick Massot ooh, I just pushed a bump...

[Johan Commelin]

Everything compiles, but maybe you had more cleanup in mind...

[Patrick Massot]

Yes there will be more cleanup.

[Johan Commelin]

I pushed a bunch of changes to #7473 (Scott's homology redesign). When that lands, some of the non-for-mathlib files of LTE can even be removed!

[Johan Commelin]

@Adam Topaz Can you take a look at this please?

[Johan Commelin]

It's going to be interesting, because when #7473 lands we probably also want to have redesigned homotopies. So maybe we shouldn't try to bump mathlib in between those PRs

[Patrick Massot]

@Riccardo Brasca and Johan, could you have a look at https://github.com/leanprover-community/lean-liquid/commit/e96a6d19b273083864d4f79269f1a41909ef531a? The commit message explains what happens.

[Johan Commelin]

Thanks a lot! This is good progress!

[Patrick Massot]

In the previous commit I also removed two files that had been PRed but were still in the repo

[Patrick Massot]

Now for_mathlib/normed_group_quotient.lean is almost ready for PR as it is, there is one tiny lemma which belongs to normed_group/basic.lean. But I'll wait for Riccardo's opinion before opening the mathlib PR.

[Patrick Massot]

In the mean time we'll get #7459 and #7474 which will unlock a lot of other stuff to PR.

[Riccardo Brasca]

Sorry, I've been very busy in the last days. Having a look at it now

[Sebastien Gouezel]

Can you get rid of the code duplication in add_subgroup.normed_group_quotient by using .. add_subgroup.semi_normed_group_quotient?

[Johan Commelin]

I'm afraid not, because they are new structures that don't extend each other.

[Sebastien Gouezel]

Yes but they have common ancestors like has_dist or uniform_space, so there could be some magic that unifies the fields. Does it really not work at all?

[Riccardo Brasca]

@Patrick Massot I think it's very good! We should just add a docstring missing at the beginning and probably structure is_quotient is useless for mathlib, but the rest is excellent

[Riccardo Brasca]

And I agree with Johan that the code duplication is difficult to avoid. I don't remember the reasons at the end, but we discussed about having normed_group extending semi_normed_group and we decided to go the other way

[Sebastien Gouezel]

I just checked, and

/-- The quotient in the category of normed groups. -/
noncomputable
instance add_subgroup.normed_group_quotient (S : add_subgroup M) [hS : is_closed (S : set M)] :
  normed_group (quotient S) :=
{ eq_of_dist_eq_zero :=
  begin
    rintros ⟨m⟩ ⟨m'⟩ (h : ∥mk' S m - mk' S m'∥ = 0),
    erw [← (mk' S).map_sub, quotient_norm_eq_zero_iff, hS.closure_eq,
         ← quotient_add_group.eq_iff_sub_mem] at h,
    exact h
  end,
  .. add_subgroup.semi_normed_group_quotient S }

seems to work fine.

[Sebastien Gouezel]

(I understand the .. foo as: try to find in foo stuff that will fill some of the missing fields. No need that bar extends foo for this).

[Riccardo Brasca]

Oh, wow!!

[Sebastien Gouezel]

I've just pushed directly to master. I hope it's allowed in LTE, otherwise don't hesitate to revert.

[Kevin Buzzard]

I push all sorts of crap directly to master :-/

[Sebastien Gouezel]

Perfect! :-)

[Riccardo Brasca]

I added some docstring

[Johan Commelin]

Sebastien Gouezel said:

I've just pushed directly to master. I hope it's allowed in LTE, otherwise don't hesitate to revert.

I wish you pushed more often :stuck_out_tongue_wink: :stuck_out_tongue_wink:

[Johan Commelin]

The basis refactor is in mathlib! Thanks a lot @Anne Baanen!

[Johan Commelin]

Time for another mathlib bump :rofl:

[Johan Commelin]

Concerning mathlib bumps: as I alluded to a little bit in some post above, we have to coordinate the "normal" mathlib PRs coming from LTE with the big homological algebra redesign from Scott.

[Johan Commelin]

Because we are relying on hand-rolled cochain complexes and homotopies in LTE. So that's going to need refactoring.

[Johan Commelin]

And we probably don't want to mix that refactor with "ordinary" mathlib bumps.

[Riccardo Brasca]

#7459 is merged, so subgroup.mem_map_of_mem can be removed from normed_group_hom.lean. I think no modification is needed

[Johan Commelin]

I'm trying to bump it right now :smiley:

[Johan Commelin]

mathlib bump is done.

[Riccardo Brasca]

I just noticed that the results in for_mathlib/nnreal.lean are never used in the project. We can maybe remove the file and the author (I think @Damiano Testa ) can open a PR if he wants to. Unless the results are there to be used somewhere in the future

[Kevin Buzzard]

I have just finished marking for the day and could work on the inevitable breakage in the Gordan stuff in about 1 hour

[Johan Commelin]

@Riccardo Brasca maybe there is even a PR already? There is a PR about nnreal stuff

[Riccardo Brasca]

Ah yes, sorry! I didn't see it somehow in the wiki

[Kevin Buzzard]

@Johan Commelin is there a branch with new mathlib and broken is_basis stuff?

After Gordan is done and I'm finished with marking I could take on the job of bumping LTE to use the new homology stuff by making a new branch which has Scott's mathlib branch as a dependency and then tries to fix everything up. This is worthwhile because Scott's ideas could be tested this way

[Johan Commelin]

@Kevin Buzzard there is no broken is_basis stuff anymore. I fixed the breakage.

[Kevin Buzzard]

Oh thanks! I was about to start on Lean -- I'll go back to Gordan!

[Johan Commelin]

Good luck! Bhavik claimed on the toric thread that he and Yael might have a topological proof done by the end of today (-;

[Kevin Buzzard]

It was never clear to me that he was claiming that he'd prove what we're calling Gordan's Lemma. The other job I need to do is to start porting grading stuff into mathlib, parts of it are working well now although we still need to think about names.

[Johan Commelin]

I would worry about PRing to mathlib after Gordan is done

[Bhavik Mehta]

Kevin Buzzard said:

It was never clear to me that he was claiming that he'd prove what we're calling Gordan's Lemma. The other job I need to do is to start porting grading stuff into mathlib, parts of it are working well now although we still need to think about names.

I am claiming this :)

[Johan Commelin]

The game is on!

[Kevin Buzzard]

Oh I'm sure he will win easily! I still have a bunch of stuff to do and I am very limited in my lean time for the next two weeks. But I will keep trying in order to force him to see this through :D

[Bhavik Mehta]

The only difference in my version is that https://github.com/leanprover-community/lean-liquid/blob/1c9a0dd21297646b88b31cea4e36f2adc0f19d3f/src/for_mathlib/Gordan.lean#L129 is changed from

lemma explicit_gordan [module ℤ Λ] (hΛ : finite_free Λ) [fintype ι] (l : ι → Λ) :

to

lemma explicit_gordan (hΛ : finite_free Λ) [fintype ι] (l : ι → Λ) :

since there's a clash between the module instance given there and from line 14 - I'm presuming this is an oversight in master rather than anything fundamental?

[Johan Commelin]

That module instance should have been deleted after the int_smul refactor

[Bhavik Mehta]

In that case would a better temporary fix for me to be to locally disable that instance so that when the refactor goes through it doesn't break?

[Johan Commelin]

Which refactor?

[Bhavik Mehta]

The int_smul refactor

[Johan Commelin]

That was done weeks ago.

[Johan Commelin]

We just didn't carefully delete all the module instances.

[Johan Commelin]

Check master again (-;

[Johan Commelin]

@Bhavik Mehta where are you writing up your approach to Gordan?

[Johan Commelin]

Some mathlib branch?

[Bhavik Mehta]

A branch of LTE, I haven't pushed yet

[Yaël Dillies]

Johan Commelin said:

Good luck! Bhavik claimed on the toric thread that he and Yael might have a topological proof done by the end of today (-;

By the way, I'm not claiming to do anything, because Bhavik told me I'm supposed to do past papers :upside_down:

[Yaël Dillies]

Do you still need Krein-Milman? What's stuck right now is that I want to polish exposed faces, and Bhavik wants to polish Hahn-Banach.

[Kevin Buzzard]

We need the thing we're calling Gordan's Lemma and I think that you guys have done enough for Bhavik to convince himself that he can get there quickly

[Yaël Dillies]

Exactly, I want to show that exposed faces form a complete lattice (in finite dimension), and even maybe a graded lattice (basically section 2 of the paper you sent). But I'm missing some framework, most crucially I can't seem to show transivity without the H-representation.

[Johan Commelin]

mathlib bumped again

[Damiano Testa]

Dear All,

I am back from my holiday and I see lots of great activity around Gordan: I am really pleased!

Kevin / Bhavik-Yaël -- This feels like the saying on building a tunnel: start simultaneously from both ends. You either finish in half the time or you have a two-lanes tunnel!

Riccardo: my temporary fix had been to split the lemmas for mathlib, but I may not have actually used them in the project, since it was easy enough to simply replace them with their short proofs. Also, when I started moving them to mathlib I decided to finally try to refactor the ordered hierarchy, since at the moment it is very limiting. I am almost done with a first serious attempt at this.

[Johan Commelin]

Where is my tunnel emoji?

[Riccardo Brasca]

@Patrick Massot Do you prefer to PR normed_group_quotient.lean yourself? I think you wrote the most delicate parts so I don't want to steal it, but otherwise I can do it today (mentioning you as co-author of course)

[Patrick Massot]

Yes I'll do it tonight

[Adam Topaz]

Now that Scott's new complexes PR is merged, what's the plan with the next mathlib bump?

[Kevin Buzzard]

I think this project provides a perfect place to test his ideas

[Johan Commelin]

I think we should wait till homotopies are merged before we refactor LTE to the new complexes

[Adam Topaz]

Which PR defines homotopies?

[Adam Topaz]

Got it #7483

[Adam Topaz]

In the meantime, I made another mathlib bump to include the Cech nerve, and I adapted the work I did previously obtaining the contracting homotopy needed for 8.19. This is now in the branch bump-2021-05-11. I wasn't sure whether there was anything else that should have been changed with the recent mathlib update, so please take a look at the diff
https://github.com/leanprover-community/lean-liquid/compare/bump-2021-05-11

[Johan Commelin]

@Adam Topaz does it build? If so, just merge into master

[Johan Commelin]

others can then clean up on top of that

[Johan Commelin]

I'm doing a bump on top of yours. Will merge it into master soon

[Johan Commelin]

merged

[Patrick Massot]

@Riccardo Brasca #7603

[Riccardo Brasca]

Very nice! It seems very good to me, I will have a closer look tomorrow

[Johan Commelin]

I bumped mathlib again, but there might be some cleanup that I missed

[Scott Morrison]

#7614 dualizes the existing material on simplicial_object in mathlib, and incorporates Adam's for_mathlib/simplicial/augmented.lean.

[Scott Morrison]

@Adam Topaz, what is the change_cone stuff in for_mathlib/Profinite/functorial_limit.lean needed for? The bottom half of the file seems happy without it, and it isn't used elsewhere.

[Adam Topaz]

Thanks for opening #7614 @Scott Morrison !

I added the change_cone stuff just in case we ever need to use the functorial properties of the Profinite.as_limit construction, but you're right, it's not used anywhere yet. I don't think we should delete it just yet, in case we do end up using it for 8.19.

[Scott Morrison]

Would it be reasonable to rename NormedGroup to SemiNormedGroup, since that's what it is?

[Johan Commelin]

@Scott Morrison yes, it's been somewhere on my todo list for a while

[Johan Commelin]

While you are in cleaning-up-mode. locally_constant/Vhat.lean is a huge mess, it's doing everything and is only marginally related to what it's name suggests.

[Johan Commelin]

Lots of stuff is more generally about SemiNormedGroup

[Scott Morrison]

Presumably in documentation it's fine to still just talk about normed groups, even when the constructions/theorems work for seminormed groups.

[Scott Morrison]

Or would it be better to be precise, so it's clear what works for seminormed vs normed groups?

[Johan Commelin]

I guess since we're mathlib we want to be precise (-;

[Scott Morrison]

Is it okay to still use the phrase "normed group hom", or should that also be "seminormed group hom"?

[Kevin Buzzard]

We call semiring homs ring homs...

[Scott Morrison]

Exactly.

[Johan Commelin]

@Scott Morrison yes, there I wouldn't make a distinction, also because a normed group hom is really just a semi normed group hom

[Scott Morrison]

Some doc-strings refer to LCC_Mbar_pow, but it doesn't exist. Is this future or past? :-)

[Scott Morrison]

Or just named differently?

[Johan Commelin]

ouch... that must be really old

[Johan Commelin]

It's called CLCFP these days...

[Johan Commelin]

aka "CompletionLocallyConstantFiltrationPow"... :head_bandage:

[Johan Commelin]

but that is so long that I decided to abbreviate

[Scott Morrison]

Okay, I did the renaming NormedGroup to SemiNormedGroup, and hopefully (semi?)normalized the doc-strings. :-)

[Scott Morrison]

Would SemiNormedGroupNormNoninc really be the preferred name? Couldn't we just use a prime or something?

[Johan Commelin]

I don't have a strong opinion. A ' also seems reasonable to me

[Johan Commelin]

Or maybe a subscript 1?

[Adam Topaz]

I vote for '

[Adam Topaz]

If only we could write $\mathcal{O}_{\mathrm{SemiNormedGroup}}$

[Scott Morrison]

?

[Adam Topaz]

Sorry, maybe that joke is way too obscure... This is the "unit ball" of SemiNormedGroup and $\mathcal{O}_v$ is the unit ball of a Krull valuation v