Zulip Chat Archive

Stream: maths

Topic: has_sum_nat_add_iff for add_monoid?


view this post on Zulip Johan Commelin (Jan 12 2021 at 15:32):

If would like to apply the following lemma to nnreal, but it's proven only for topological additive groups.

lemma has_sum_nat_add_iff {f :   α} (k : ) {a : α} :
  has_sum (λ n, f (n + k)) a  has_sum f (a +  i in range k, f i) :=

I'm not really good at manipulating has_sum. Can someone tell me how to prove this for add_monoids?

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 16:04):

MWE?

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 16:12):

I haven't done it but here's the MWE. The proof in mathlib does only work for groups :-/

import tactic
import topology.algebra.infinite_sum

open_locale big_operators

variables (α : Type*) [topological_space α] [add_comm_monoid α]

open finset

lemma has_sum_nat_add_iff'' {f :   α} (k : ) {a : α} :
  has_sum (λ n, f (n + k)) a  has_sum f (a +  i in range k, f i) :=
begin
  sorry
end

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 16:24):

Oh! @Heather Macbeth this was the example I mentioned to you the other day! The extraordinary file topology.algebra.infinite_sum assumes that alpha is an add_comm_monoid and a topological_space, and for the first 214 lines it does not assume that there is any relation between these two structures. Continuity of addition appears on line 214. It's quite surprising what they prove without this assumption!

view this post on Zulip Heather Macbeth (Jan 12 2021 at 16:26):

There will be more -- @Alex J. Best gave me a preview of his linter's effect on topology.algebra.ordered, and it was quite drastic :)

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 16:29):

Johan, I suspect the lemma is not true for general add_comm_monoids. If a monoid has some saturating element then a + sum can lose information.

view this post on Zulip Sebastien Gouezel (Jan 12 2021 at 16:31):

But it will definitely be true for nnreal.

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 16:32):

It's easier to think of in terms of products, with the target a monoid with zero. If we have an infinite set S and a finite set F, then the product over S union F is the product of the product over S and the product over F, but if you know that the product over S union F is zero then you don't know which one caused it.

view this post on Zulip Mario Carneiro (Jan 12 2021 at 16:33):

I think it's true in general

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 16:34):

If you really need both directions then you'll need some extra assumption saying things cancel (which as Sebastien says is fine for nnreal); or do you only need the true way?

view this post on Zulip Mario Carneiro (Jan 12 2021 at 16:34):

You can always assume WLOG that the sum contains any chosen finite set of summands because that's how the filter works, so you can assume in this case that you are only dealing with partial sums that contain range k

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 16:36):

Mario, a counterexample for <- in the product version with target the reals (a topological monoid under multiplication) would be if f(0)=0 and k=1. Then RHS is true for any a because 0*a1*a2*a3*... is always 0 whatever the product of the a_i converges to.

view this post on Zulip Mario Carneiro (Jan 12 2021 at 16:37):

Ah, I see, we're cancelling in the <- direction

view this post on Zulip Mario Carneiro (Jan 12 2021 at 16:39):

But if the goal is just nnreal we can just add add_right_cancel as a hypothesis

view this post on Zulip Mario Carneiro (Jan 12 2021 at 16:40):

or use add_left_cancel_monoid or whatever it is called if it is a mixin

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 16:41):

Looks like add_cancel_comm_monoid is a thing (I think everything has to be commutative)

view this post on Zulip Mario Carneiro (Jan 12 2021 at 16:42):

We probably assume it but it's not strictly necessary for tsum stuff

view this post on Zulip Mario Carneiro (Jan 12 2021 at 16:42):

you only need things to be "eventually commutative"

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 16:42):

My guess is that this is provable:

import tactic
import topology.algebra.infinite_sum

open_locale big_operators

variables (α : Type*) [topological_space α] [add_cancel_comm_monoid α] [has_continuous_add α]

open finset

lemma has_sum_nat_add_iff'' {f :   α} (k : ) {a : α} :
  has_sum (λ n, f (n + k)) a  has_sum f (a +  i in range k, f i) :=
begin
  sorry
end

Edit: it is not!

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 16:43):

If I were doing this in class I would just say "because alpha is cancellative we can just work in its group of fractions and now we're obviously done"

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 16:47):

example : add_cancel_comm_monoid nnreal := by apply_instance -- fails :-(

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 16:51):

got it:

noncomputable example : add_left_cancel_monoid nnreal := by apply_instance -- works :-)
noncomputable example : add_right_cancel_monoid nnreal := by apply_instance -- fails :-)

view this post on Zulip Mario Carneiro (Jan 12 2021 at 16:57):

Oh, some new theorems pop up when you try the obvious thing. Is it true that if f + g ~> a + b and f ~> a then g ~> b (in a cancellative topological monoid)?

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 16:57):

Oh surely.

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 16:57):

wait stop

view this post on Zulip Mario Carneiro (Jan 12 2021 at 16:57):

I suspect you need some condition that plays a role analogous to "negation is continuous" in a group

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 16:57):

Yeah!

view this post on Zulip Mario Carneiro (Jan 12 2021 at 16:57):

like addition is an open map or something

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 16:58):

Yeah I am now less sure that my example is provable!

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 16:58):

For nnreal it's fine, but could one imagine a cancellative additive monoid where inverse is not continuous?

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 16:59):

Just to prove I'm not shirking, here's the fun I'm having:

import data.real.nnreal

/-
@[protect_proj, ancestor add_right_cancel_semigroup add_monoid]
class add_right_cancel_monoid (M : Type u) extends add_right_cancel_semigroup M, add_monoid M
-/

noncomputable example : add_right_cancel_semigroup nnreal := by apply_instance
noncomputable example : add_monoid nnreal := by apply_instance
noncomputable example : add_right_cancel_monoid nnreal := by apply_instance -- fails

view this post on Zulip Mario Carneiro (Jan 12 2021 at 16:59):

Seems like the same kind of thing as noncomputable inverses

view this post on Zulip Mario Carneiro (Jan 12 2021 at 17:00):

BTW re: your example, you don't get a class just because you have all the superclasses

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:01):

All we need is a topological space with a group structure such that multiplication is continuous and inverse isn't, and I know examples of these but they're quite pathological.

view this post on Zulip Mario Carneiro (Jan 12 2021 at 17:01):

you have to explicitly implement it, even if there are no fields

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:03):

OK I'll handle that. I suspect this example isn't going to help you but the adeles are the following topological subring of the product of the real numbers and the product over all p of the p-adic numbers: at all but finitely many of the p-adic places, the element must be an integer. This is a topological ring, and its units with the (bad) subspace topology are a topological monoid which is not a topological group because inverse is not continuous with the subspace topology.

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:03):

I like that my maths proof had this bug in :D

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:04):

I swear I could have delivered that line well enough to get it past anyone.

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:05):

I will stop worrying about instances and try to find a counterexample.

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:11):

OK so here's a pretty concrete example of negation not being continuous (translated down from my adelic example): if you give the integers the topology with basis [n,)[n,\infty) for nZn\in\mathbb{Z} then it seems to me that addition is continuous, because the pre-image of [n,)[n,\infty) is the union over x+y=nx+y=n of [x,)×[y,)[x,\infty)\times[y,\infty). But inverse is not continuous. I think.

view this post on Zulip Mario Carneiro (Jan 12 2021 at 17:12):

ah, you just beat me to it. I was going to suggest the basis {0}\{0\} for natural numbers under addition

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:13):

So now what do we want? We're still asking questions about infinite sums, or were you asking about sequences?

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:14):

I could imagine that an infinite sum converging upwards might have different behaviour to an infinite sum converging downwards with this topology

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:14):

Use the reals rather than the integers or naturals

view this post on Zulip Mario Carneiro (Jan 12 2021 at 17:14):

I'm confused by the question

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:14):

all this just to satisfy Alex's linter! ;-)

view this post on Zulip Mario Carneiro (Jan 12 2021 at 17:15):

infinite sums don't converge in any particular direction here

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:15):

I'm just checking I understand the question. Originally we were talking about has_sum. I'm just checking that we still are.

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:15):

i.e. that your comment about f + g ~> a + b was still a question about sums

view this post on Zulip Mario Carneiro (Jan 12 2021 at 17:15):

I think the has_sum question reduces to the question I posed about filter limits, which boils down to some continuity property

view this post on Zulip Mario Carneiro (Jan 12 2021 at 17:16):

It's not about sequences, because has_sum can handle more general convergent nets of partial sums

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:16):

Oh this topology isn't even Hausdorff! So probably 1+1+1+1+... tends to 37

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:17):

this is looking good

view this post on Zulip Eric Wieser (Jan 12 2021 at 17:17):

Kevin Buzzard said:

Just to prove I'm not shirking, here's the fun I'm having:
...

For some reason docs#ordered_cancel_comm_monoid.to_left_cancel_monoid exists but docs#ordered_cancel_comm_monoid.to_right_cancel_monoid doesn't!

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:18):

Yes I'd got this far :-) But now I've been distracted by pathological topological monoids

view this post on Zulip Reid Barton (Jan 12 2021 at 17:18):

how about an example like: take the nonnegative reals but make the topology discrete on [0, 1]

view this post on Zulip Mario Carneiro (Jan 12 2021 at 17:18):

But actually that property spells doom as a counterexample, because everything converges to everything

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:19):

No, because if you don't get far enough then you don't converge.

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:20):

0+0+0+0+... doesn't tend to 2 because it never makes it to [1,infty)

view this post on Zulip Mario Carneiro (Jan 12 2021 at 17:20):

true, but that happens iff the sequence converges in the usual sense to infinity, and taking a few elements off won't change that

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:20):

so I think that's it, right? 0+0+0+... doesn't tend to 2, but 1+1+1+... tends to 37 and the sum tends to 39.

view this post on Zulip Mario Carneiro (Jan 12 2021 at 17:21):

but that's not a counterexample

view this post on Zulip Mario Carneiro (Jan 12 2021 at 17:21):

you can only remove finitely many elements from the sequence

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:23):

Mario Carneiro said:

Oh, some new theorems pop up when you try the obvious thing. Is it true that if f + g ~> a + b and f ~> a then g ~> b (in a cancellative topological monoid)?

I don't know what this means, but I thought that I had given a counterexample to it.

view this post on Zulip Mario Carneiro (Jan 12 2021 at 17:24):

Ah, you were giving a counterexample to that

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:24):

I agree we don't have a counterexample to Johan's original question yet.

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:25):

But we have Reid's comment to fall back on if this one doesn't give us something.

view this post on Zulip Mario Carneiro (Jan 12 2021 at 17:26):

Actually a more accurate version of what you get by reducing Johan's question is if f + b ~> a + b then f ~> a

view this post on Zulip Mario Carneiro (Jan 12 2021 at 17:27):

Where the + b is acting on the convergents (partial sums), not the elements of the sum

view this post on Zulip Mario Carneiro (Jan 12 2021 at 17:28):

I think that's equivalent to saying that _+b\_ + b is an open map

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:30):

and in this example we're working with, right addition probably is an open map. So let's fall back on Reid's example because there it looks to me like it isn't.

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:31):

So put the usual topology on R\mathbb{R}, and then add a bunch more open sets -- any subset of [0,1][0,1] is open -- and there's a topology.

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:32):

But now addition is not continuous :-(

view this post on Zulip Reid Barton (Jan 12 2021 at 17:32):

Needs to be the nonnegative reals for that reason

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:32):

yeah I just went to re-check your comment :-)

view this post on Zulip Eric Wieser (Jan 12 2021 at 17:34):

Kevin Buzzard said:

Yes I'd got this far :-) But now I've been distracted by pathological topological monoids

Fixed in #5713, hopefully

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:34):

I see. So the pre-image of a usual open set is certainly open because usual addition is continuous for the usual topology, and the preimage of a weird open set is open because it's in this [0,1] chaos.

view this post on Zulip Mario Carneiro (Jan 12 2021 at 17:35):

Here's a formal rendering of the statement I gave above (with f in place of + b)

def property {α β} [topological_space α] [topological_space β] (f : α  β) :=
 (F : filter α) (a : α), F.map f  nhds (f a)  F  nhds a

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:35):

Thanks Eric! Does nnreal become an add_cancel_comm_monoid now?

view this post on Zulip Eric Wieser (Jan 12 2021 at 17:35):

Who knows, the universe has to rebuild first

view this post on Zulip Mario Carneiro (Jan 12 2021 at 17:36):

this looks like something that should have a straightforward topological rendering, but I'm not sure what

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:38):

I would guess it's "f is open"

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:51):

OK I think I've got everything straight.

So Reid's example gives us a cancellative add comm monoid with a topology for which addition is continuous but for which Johan's lemma fails, because 1/10+1/100+1/1000+... does _not_ tend to 0.11111111111...=1/9 because it never reaches the open set {1/9}. However 37+1/10+1/100+1/1000.. does tend to 37.1111... because over there the topology is sensible. Adding 37 isn't open. So this proves that my second attempt at a MWE is also not provable.

The idea of adding a cancellative assumption was that we seemed to be cancelling, but we need to cancel continuously. So there is some predicate on topological add monoids which is strictly stronger than algebraic cancellation, it says that not only is adding x injective (from cancellative) and continuous (from the top add monoid assumption), it is also open. Presumably this is precisely the condition which one needs in order to make the top add monoid a submonoid of a top add group (certainly for submonoids, with the subspace topology, of top add groups, addition will be continuous). So this would be the natural assumption to put on alpha to make Johan's lemma true.

My guess is that more generally if MM is a topological commutative monoid and SS is a subset then there might be random ways to put a topology on M[1/S]M[1/S] but the nicest theorems will only hold under the assumption that multiplication by sSs\in S is an open map (because then division by ss will be continuous). This seems like quite a neat project. In fact maybe M[1/S]M[1/S] won't be a topological monoid if you just put a random topology on it somehow coming from MM, without this extra hypothesis.

If Johan only needs the result for nnreal then I guess the most painless thing to do is to prove that adding a constant is an open map on nnreal, or alternatively trying to deduce the result on nnreal from the corresponding result for reals.

@Johan Commelin thanks for the interesting question!

view this post on Zulip Mario Carneiro (Jan 12 2021 at 17:51):

Kevin Buzzard said:

I would guess it's "f is open"

Confirmed, under the assumption that f is injective (which it is in our examples)

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:53):

Nice! So there is an argument for a "topologically cancellative" top monoid class.

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 17:55):

If you drop injectivity of ff then the lemma is probably false for other reasons (a1 + b = a2 + b and the infinite sum won't tend to both a1 and a2)

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 18:41):

@Mario Carneiro are these missing? Are you working on them?

import tactic
import topology.algebra.infinite_sum

open_locale big_operators

open finset

variables (M N : Type*) [topological_space M] [topological_space N]
  [add_comm_monoid M] [add_comm_monoid N]
  [has_continuous_add M] [has_continuous_add N] -- I have no idea whether we need these!

variable (ι : Type*)

lemma lemma1 (φ : M →+ N) ( : continuous φ) (f : ι  M) (m : M) (hm : has_sum f m) :
  has_sum (φ  f) (φ m) :=
begin
  sorry
end

open function

lemma lemma2 (φ : M →+ N) ( : continuous φ) (hφ2 : injective φ) (hφ3 : is_open_map φ)
  (f : ι  M) (m : M) (hm : has_sum (φ  f) (φ m)) : has_sum f m :=
begin
  sorry
end

view this post on Zulip Mario Carneiro (Jan 12 2021 at 18:41):

we should have the first one already, but I doubt we have the second

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 18:43):

In topology.algebra.infinite_sum I couldn't find a single lemma about changing the target monoid. Should I be looking somewhere else? I'll remark in passing that if we used math notation (M, N for the monoids, alpha, beta for the index types) it would be easier to look!

view this post on Zulip Johan Commelin (Jan 12 2021 at 19:06):

Hah, I see that you opened and closed some cans of worms while I put my kids in bed (-;

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 19:06):

I've nearly proved your lemma!

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 19:06):

Is this for the liquid stuff?

view this post on Zulip Johan Commelin (Jan 12 2021 at 19:14):

yup

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 19:17):

You led us up quite the garden path!

view this post on Zulip Johan Commelin (Jan 12 2021 at 19:17):

mi sori

view this post on Zulip Johan Commelin (Jan 12 2021 at 19:18):

But it should be possible to get a statement that works for both nnreal and nnrat (when we ever get around to defining that one).

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 19:18):

Oh it was great fun, I have loads of things to do today and it was a wonderful excuse not to do any of them. I've just got it compiling.

view this post on Zulip Johan Commelin (Jan 12 2021 at 19:18):

so what is the solution in the end? you're assuming that addition is open? I guess this should be a new typeclass... or did you already make it that?

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 19:20):

No, the new typeclass is a proper little project. I figured that you just wanted it for nnreal.

import topology.algebra.infinite_sum
import topology.instances.nnreal

open_locale big_operators

open nnreal

open finset

lemma has_sum_nat_add_iff'' {f :   nnreal} (k : ) {a : nnreal} :
  has_sum (λ n, f (n + k)) a  has_sum f (a +  i in range k, f i) :=
begin
  unfold has_sum,
  rw  tendsto_coe,
  rw  tendsto_coe,
  simp only [coe_sum],
  convert has_sum_nat_add_iff k,
  refl,
  classical,
  rw nnreal.coe_add,
  simp only [coe_sum],
  apply_instance,
end

I've not tidied it up yet.

view this post on Zulip Johan Commelin (Jan 12 2021 at 19:23):

ok, so this is the "cheaty" version that falls back to real (-;

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 19:29):

Here's what's going on. It's absolutely crucial that addition is an open map (otherwise the lemma is false). It's also crucial that the monoid is cancellative (otherwise the lemma is false). This should really be a new typeclass ("topologically cancellative monoids -- the top monoids which are submonoids of top groups). The correct localisation theory for topological add_monoids (you want a topology on the localisation too) is, I suspect, when the things you're inverting have the property that adding them is an open map (Patrick will probably tell us that all of this is in Bourbaki). If you do it this way then basically you're reducing the question from top monoids to top groups. But to actually do the reduction you need lemma1 and lemma2 above, to move between the monoid and the group (and the corollary that for a continuous injective open map, like nnreal -> real, sum = a iff coerced sum = a). This is the key thing:

lemma lemma1 (φ : M →+ N) ( : continuous φ) {f : ι  M} {m : M} (hm : has_sum f m) :
  has_sum (φ  f) (φ m) :=
begin
  sorry
end

open function

lemma lemma2 (φ : M →+ N) (hφ1 : injective φ) (hφ2 : is_open_map φ)
  {f : ι  M} {m : M} (hm : has_sum (φ  f) (φ m)) : has_sum f m :=
begin
  sorry
end

lemma corollary3 (φ : M →+ N) ( : continuous φ) (hφ2 : injective φ) (hφ3 : is_open_map φ)
  {f : ι  M} {m : M} : has_sum f m  has_sum (φ  f) (φ m) :=
lemma1 φ , lemma2 φ hφ2 hφ3

I'm not sure we have those lemmas either! Mario was optimistic about lemma 1 but I couldn't find it. So on the face of it, your lemma looks like a lot of work!

However Yury has already proved corollary 3 in the special case where the map is nnreal -> real, so if you just need it in the nnreal case you may as well use Yury's result, which is what I used (nnreal.tendsto_coe). I was rather hoping it would be a really slick one-liner, but unfortunately you have to commute the coercions with everything. Also, for some reason the first simp only (which is a rewrite under a binder) takes forever right now. I'll try to tidy.

view this post on Zulip Mario Carneiro (Jan 12 2021 at 19:35):

@Kevin Buzzard I'm looking at docs#has_sum.map for lemma1

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 19:38):

Nice! I missed it because the add_comm_monoid instance was put on the random type gamma. If it had been an N I would have been more likely to spot it! The lemma is before line 214 so indeed it does not assume that things are topological monoids! In particular my earlier comment [has_continuous_add M] [has_continuous_add N] -- I have no idea whether we need these! -- indeed we don't seem to!

view this post on Zulip Kevin Buzzard (Jan 12 2021 at 20:41):

I got it down to one line in the end! #5716


Last updated: May 09 2021 at 10:11 UTC