has_sum_nat_add_iff for add_monoid?

Stream: maths

[Johan Commelin]

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?

[Kevin Buzzard]

MWE?

[Kevin Buzzard]

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

[Kevin Buzzard]

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!

[Heather Macbeth]

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 :)

[Kevin Buzzard]

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.

[Sebastien Gouezel]

But it will definitely be true for nnreal.

[Kevin Buzzard]

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.

[Mario Carneiro]

I think it's true in general

[Kevin Buzzard]

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?

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

you only need things to be "eventually commutative"

[Kevin Buzzard]

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!

[Kevin Buzzard]

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"

[Kevin Buzzard]

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

[Kevin Buzzard]

got it:

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

[Mario Carneiro]

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)?

[Kevin Buzzard]

Oh surely.

[Kevin Buzzard]

wait stop

[Mario Carneiro]

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

[Kevin Buzzard]

Yeah!

[Mario Carneiro]

like addition is an open map or something

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

Seems like the same kind of thing as noncomputable inverses

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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,\infty)$ for $n\in\mathbb{Z}$ then it seems to me that addition is continuous, because the pre-image of $[n,\infty)$ is the union over $x+y=n$ of $[x,\infty)\times[y,\infty)$. But inverse is not continuous. I think.

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Use the reals rather than the integers or naturals

[Mario Carneiro]

I'm confused by the question

[Kevin Buzzard]

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

[Mario Carneiro]

infinite sums don't converge in any particular direction here

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

this is looking good

[Eric Wieser]

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!

[Kevin Buzzard]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Mario Carneiro]

but that's not a counterexample

[Mario Carneiro]

you can only remove finitely many elements from the sequence

[Kevin Buzzard]

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.

[Mario Carneiro]

Ah, you were giving a counterexample to that

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

But now addition is not continuous :-(

[Reid Barton]

Needs to be the nonnegative reals for that reason

[Kevin Buzzard]

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

[Eric Wieser]

Kevin Buzzard said:

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

Fixed in #5713, hopefully

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Kevin Buzzard]

Thanks Eric! Does nnreal become an add_cancel_comm_monoid now?

[Eric Wieser]

Who knows, the universe has to rebuild first

[Mario Carneiro]

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

[Kevin Buzzard]

I would guess it's "f is open"

[Kevin Buzzard]

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 $M$ is a topological commutative monoid and $S$ is a subset then there might be random ways to put a topology on $M[1/S]$ but the nicest theorems will only hold under the assumption that multiplication by $s\in S$ is an open map (because then division by $s$ will be continuous). This seems like quite a neat project. In fact maybe $M[1/S]$ won't be a topological monoid if you just put a random topology on it somehow coming from $M$, 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!

[Mario Carneiro]

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)

[Kevin Buzzard]

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

[Kevin Buzzard]

If you drop injectivity of $f$ 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)

[Kevin Buzzard]

@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) (hφ : continuous φ) (f : ι → M) (m : M) (hm : has_sum f m) :
  has_sum (φ ∘ f) (φ m) :=
begin
  sorry
end

open function

lemma lemma2 (φ : M →+ N) (hφ : 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

[Mario Carneiro]

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

[Kevin Buzzard]

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!

[Johan Commelin]

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

[Kevin Buzzard]

I've nearly proved your lemma!

[Kevin Buzzard]

Is this for the liquid stuff?

[Johan Commelin]

yup

[Kevin Buzzard]

You led us up quite the garden path!

[Johan Commelin]

mi sori

[Johan Commelin]

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).

[Kevin Buzzard]

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.

[Johan Commelin]

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?

[Kevin Buzzard]

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.

[Johan Commelin]

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

[Kevin Buzzard]

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) (hφ : 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) (hφ : continuous φ) (hφ2 : injective φ) (hφ3 : is_open_map φ)
  {f : ι → M} {m : M} : has_sum f m ↔ has_sum (φ ∘ f) (φ m) :=
⟨lemma1 φ hφ, 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.

[Mario Carneiro]

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

[Kevin Buzzard]

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!

[Kevin Buzzard]

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