# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Correct setting for positive shifts of intervals

#### Peter Nelson (Mar 09 2021 at 17:41):

There are many trivial lemmas in `data.set.intervals.image_preimage`

about images of intervals under various functions, in particular - adding a constant. However, they all require at least a group structure on the linear order, so none imply the obvious fact that adding a constant maps intervals to intervals in `nat`

. I've tried to look through the structures in mathlib that give the right setting for this fact, but they all seem either too weak or too strong. I'm trying to avoid having to deal with `nat`

as a special case.

Specifically, I want lemmas like :

```
lemma Ioc_add_bij (a b d : ℕ):
set.bij_on (+d) (Ioc a b) (Ioc (a+d) (b+d)) := sorry
```

I believe what is required is an `add_comm_monoid`

, with an ordering such that for all `0 \le a \le b`

, there exists `c`

with `a + c = b`

. Is there any instance or combination of instances that gives these properties?

#### Eric Wieser (Mar 09 2021 at 17:42):

Can you link to the statement you'd like to use that seems too restrictive to apply to `nat`

?

#### Eric Wieser (Mar 09 2021 at 17:44):

So docs#set.image_add_const_Ico?

#### Peter Nelson (Mar 09 2021 at 17:44):

Yes, exactly : https://leanprover-community.github.io/mathlib_docs/data/set/intervals/image_preimage.html#images-under-codex--a--xcode

#### Eric Wieser (Mar 09 2021 at 17:45):

(What a beautiful url anchor, thanks doc-gen)

#### Peter Nelson (Mar 09 2021 at 17:45):

(For what it's worth, I've written proofs for my example lemma and various related facts; it just feels a bit weird that I would have to do so).

#### Eric Wieser (Mar 09 2021 at 17:46):

I wonder if some of the lemmas in that file can be reduced to docs#ordered_add_comm_monoid or docs#ordered_cancel_add_comm_monoid

#### Peter Nelson (Mar 09 2021 at 17:47):

Yeah, I'm not sure. At least if you want bijections, I think that you do need a 'partial subtraction' of the type I described, and I don't know if that follows from a more general cancellative property

#### Eric Wieser (Mar 09 2021 at 18:01):

docs#canonically_linear_ordered_add_monoid is sufficient to prove `image_const_add_Ici`

for nat:

```
@[simp] lemma image_const_add_Ici {G : Type u} [canonically_linear_ordered_add_monoid G] (a b c : G) :
(λ x, a + x) '' Ici b = Ici (a + b) :=
begin
ext,
simp only [mem_image, mem_Ici],
split,
{ rintros ⟨c, hc, hc'⟩,
exact (add_le_add_left hc a).trans_eq hc', },
{ intro h,
obtain ⟨c, rfl⟩ := le_iff_exists_add.mp h,
refine ⟨b + c, self_le_add_right _ _, (add_assoc _ _ _).symm⟩, },
end
```

#### Bryan Gin-ge Chen (Mar 09 2021 at 18:02):

I don't think there's any deep reason why `nat`

(or more general) versions of these lemmas are missing. I suspect that @Yury G. Kudryashov just didn't need them in that generality when he made the PR. They'd certainly be welcome if someone were to PR them!

#### Peter Nelson (Mar 09 2021 at 18:04):

Eric -that's true, but that setting doesn't apply to `int`

, which fails this axiom

`le_iff_exists_add : ∀ (a b : α), a ≤ b ↔ ∃ (c_1 : α), b = a + c_1`

.

A one-sided version of that axiom, with only the forwards implication, is what's needed to apply to both `nat`

and (for example )`int`

.

#### Eric Wieser (Mar 09 2021 at 18:05):

Right, although the existing lemmas covers `int`

right?

#### Yury G. Kudryashov (Mar 09 2021 at 18:16):

Indeed, I added lemmas in the generality I needed. Feel free to generalize them and/or add `'`

versions that work for canonically ordered (add) comm monoids.

#### Eric Wieser (Mar 09 2021 at 18:18):

A one-sided version of that axiom, with only the forwards implication, is what's needed to apply to both nat and (for example )int.

I'd be loosely in favor of an ad-hoc typeclass in that file to avoid the need for separate primed and unprimed versions, containing the axiom you suggest and instantiated for `ordered_add_comm_monoid`

and `canonically_linear_ordered_add_monoid`

#### Kevin Buzzard (Mar 09 2021 at 22:50):

(deleted)

#### Peter Nelson (Mar 10 2021 at 06:20):

To get a bijection version (addition translates an interval bijectively) it is even more awkward. A `[canonically_linear_ordered_add_monoid]`

instance is not enough without some sort of cancellation law (otherwise it fails on singleton intervals).

Here is some code that gives the required lemma, proved using a bespoke typecless with (I think) the minimal required assumptions, and instances for both `nat`

and `ordered_add_comm_group`

.

```
class ordered_cancel_add_comm_exists_sub_monoid (α : Type u)
extends ordered_cancel_add_comm_monoid α :=
(exists_add_of_le : ∀ (a b : α), a ≤ b → ∃ (c : α), b = a + c)
instance ordered_add_comm_group.ordered_cancel_add_comm_exists_sub_monoid
(α : Type u)[ordered_add_comm_group α]:
ordered_cancel_add_comm_exists_sub_monoid α :=
{ exists_add_of_le := λ a b hab, ⟨b - a, (add_sub_cancel'_right a b).symm⟩}
instance nat.ordered_cancel_add_comm_exists_sub_monoid :
ordered_cancel_add_comm_exists_sub_monoid ℕ :=
{ exists_add_of_le := λ a b hab, ⟨_, (nat.add_sub_of_le hab).symm⟩}
open set ordered_cancel_add_comm_exists_sub_monoid
lemma Ioo_add_bij {α : Type}[ordered_cancel_add_comm_exists_sub_monoid α](a b d : α):
bij_on (+d) (Icc a b) (Icc (a+d) (b+d)) :=
begin
refine ⟨λ x h, _, λ x hx y hy h, _, λ x h, _⟩,
{ rw [mem_Icc] at ⊢ h,
exact ⟨add_le_add_right h.1 _, add_le_add_right h.2 _⟩},
{ apply add_right_cancel h, },
rw mem_image,
simp_rw mem_Icc at h ⊢,
cases h with h1 h2,
obtain ⟨c,rfl⟩ := exists_add_of_le _ _ h1,
rw [add_right_comm, add_le_add_iff_right] at h1 h2,
exact ⟨ a+c, ⟨h1,h2⟩, by rw add_right_comm⟩,
end
```

This would also work for `nnreal`

, but I don't know a good typeclass that encapsulates both `nnreal`

and `nat`

, because `canonically_linear_ordered_add_monoid`

is too weak. Thoughts on this would be welcome.

#### Kevin Buzzard (Mar 10 2021 at 06:43):

Can you give me an example of a canonically linear ordered add monoid for which a theorem you want to be true fails?

Johan asked a question about nnreal a few months ago which, after Mario and I discussed it here (I'm sorry I'm on mobile and the link is too fiddly to find) and we boiled the question down to "when is a topological monoid a submonoid of a topological group?". There is the usual algebraic obstruction -- the monoid needs to be cancellative, or else it doesn't embed into any group at all. However there is also a topological obstruction, as observed by Reid's example of nnreal with following topology: every subset which is open with the usual order topology is open, and also every subset of [0,1] is open. This is a topological monoid, but addition of a fixed element is not an open map in contrast to what happens in a topological group. Conversely adding this condition looked like it was precisely the right one to make the group localisation inherit a topological group structure.

What is the counterexample of a canonically ordered monoid which you have in mind which stops your lemmas being true?

#### Damiano Testa (Mar 10 2021 at 08:00):

I am not really sure if this would work, but I think that this might be a great addition to the `counterexamples`

branch, if it works! (This is somewhat shameless self-promotion of my branch :wink:)

In the branch, there is an example of a `canonically_ordered_comm_semiring`

in which multiplication by `2`

is not injective. The example is obtained from `ℕ × zmod 2`

, with the ring structure given by the usual componentwise addition and multiplication. The ordering is defined by declaring `(a,s) ≤ (b,t)`

if and only if

`a < b`

, or`(a,s) = (b,t)`

.

Thus, "far apart", the order ignores the `zmod 2`

components, but prevents `(a,0)`

and `(a,1)`

from being comparable. [This is actually formalized.]

It seems to me that, if you remove from the ring the "initial segment" of elements of the form `(a,1)`

, for `0 ≤ a ≤ 2`

you still have all the properties above and moreover, the interval `[0, 2]`

now has fewer elements than the interval `[2, 4]`

, since in the initial one, you are missing out on all the interesting `zmod 2`

elements.

[Note: there is a formalization that if you remove just `(0,1)`

, you still get a `canonically_ordered_comm_semiring`

, but I had not thought about removing more elements.]

I hope that this makes sense!

#### Damiano Testa (Mar 10 2021 at 08:04):

Also, the `cancellation`

that you want is on addition, right? This should hold for the example above, since it is a subsemiring of the `comm_ring`

`ℤ × zmod 2`

.

#### Damiano Testa (Mar 10 2021 at 08:10):

Ah, I see an issue with my approach: the identity of the semiring `ℕ × zmod 2`

is `(1,1)`

, so you cannot simply remove it. However, it might be possible to tweak this into an example showing that without your axiom, intervals are not "homogeneous".

#### Peter Nelson (Mar 10 2021 at 13:28):

Ah, it looks like canonically ordered monoids have cancellation after all - I was doing something wrong earlier and the instance wasn't firing. This makes me happier.

Potentially this, and some other small things related to intervals, could make my first PR. Can anyone suggest a good name for this typeclass?

```
/-- an add_comm_monoid with one-sided 'subtraction' in the sense that if a ≤ b,
there is some c for which a + c = b -/
class ordered_cancel_add_exists_add_monoid (α : Type u)
extends ordered_cancel_add_comm_monoid α :=
(exists_add_of_le : ∀ (a b : α), a ≤ b → ∃ (c : α), b = a + c)
instance ordered_add_comm_group.ordered_cancel_add_exists_add_monoid
(α : Type u)[ordered_add_comm_group α]:
ordered_cancel_add_exists_add_monoid α :=
{ exists_add_of_le := λ a b hab, ⟨b - a, (add_sub_cancel'_right a b).symm⟩}
instance canonically_ordered_comm_monoid.ordered_cancel_add_exists_add_monoid
(α : Type u)[canonically_ordered_add_monoid α]:
ordered_cancel_add_exists_add_monoid ℕ :=
{ exists_add_of_le := λ a b hab, le_iff_exists_add.mp hab}
open set ordered_cancel_add_exists_add_monoid
lemma Icc_add_bij {α : Type}[ordered_cancel_add_exists_add_monoid α](a b d : α):
bij_on (+d) (Icc a b) (set.Icc (a+d) (b+d)) :=
begin
refine ⟨λ x h, _, λ x hx y hy h, _, λ x h, _⟩,
{ rw [mem_Icc] at ⊢ h,
exact ⟨add_le_add_right h.1 _, add_le_add_right h.2 _⟩},
{ apply add_right_cancel h, },
rw mem_image,
simp_rw mem_Icc at h ⊢,
cases h with h1 h2,
obtain ⟨c,rfl⟩ := exists_add_of_le _ _ h1,
rw [add_right_comm, add_le_add_iff_right] at h1 h2,
exact ⟨ a+c, ⟨h1,h2⟩, by rw add_right_comm⟩,
end
```

#### Heather Macbeth (Mar 10 2021 at 17:15):

I think `cancel`

should not appear in the name, since in `cancel_monoid`

the statement like `b = a + c`

appears in the hypothesis rather than the goal. Maybe `ordered_has_sub_add_monoid`

?

Anyway, since these gadgets are remarkably hard to name, I suggest you open the PR and the discussion can continue there! :)

#### Peter Nelson (Mar 10 2021 at 18:31):

@Eric Wieser @Kevin Buzzard the plot thickens! There was a small but important typo in my code just above, where I forgot to change an `ℕ`

back into an `α`

. Changing it into an `α`

breaks the code, because canonically ordered additive monoids (even with a linear order) aren't cancellative.

In fact, re Kevin's question, there is a nice example to show this - take the usual ordering on `nat`

with the monoid where addition is (the usual) `max`

. This is a canonical linear ordered monoid (it satisfies all those axioms; in particular `a \le b`

iff there is some `c`

with `max a c = b`

) but it isn't cancellative, and it is also easy to see that adding a constant maps intervals to intervals, but not bijectively.

So it really seems that `ordered_cancel_add_comm_monoid`

together with `(exists_add_of_le : ∀ (a b : α), a ≤ b → ∃ (c : α), b = a + c)`

is the right set of assumptions; this happens to work for both `nat`

and `nnreal`

, but the only existing general class that obviously has an instance for this is `ordered_add_comm_group`

. Maybe the right abstraction is just that this should hold for either an ordered add_comm group, or the submonoid of nonnegative elements of such a group. If this is the answer, it feels unlikely to be worth formalizing.

#### Heather Macbeth (Mar 10 2021 at 18:35):

Well, there is also:

docs#multiset.le_iff_exists_add

docs#cardinal.le_iff_exists_add :)

#### Peter Nelson (Mar 10 2021 at 18:35):

good point!

#### Peter Nelson (Mar 10 2021 at 18:36):

also set union

#### Peter Nelson (Mar 10 2021 at 18:36):

(deleted)

#### Eric Wieser (Mar 10 2021 at 18:37):

I'd argue (perhaps controversially) that if the same lemma statement appears ≥3 times, it's worthy of a typeclass

#### Eric Wieser (Mar 10 2021 at 18:37):

That or one of the lemmas it uses is

#### Peter Nelson (Mar 10 2021 at 18:38):

So would the typeclass correspond to 'the nonnegative elements of some `ordered_add_comm_group`

' and have instances from `nat`

and `nnreal`

?

#### Eric Wieser (Mar 10 2021 at 18:41):

I was thinking you might just be able to get away with:

```
class has_exists_add_of_le [ordered_cancel_add_comm_monoid α] :=
(exists_add_of_le : ∀ (a b : α), a ≤ b → ∃ (c : α), b = a + c)
```

#### Eric Wieser (Mar 10 2021 at 18:42):

Then your lemma becomes

```
lemma Icc_add_bij {α : Type} [ordered_cancel_add_comm_monoid α] [has_exists_add_of_le α] (a b d : α):
bij_on (+d) (Icc a b) (set.Icc (a+d) (b+d)) :=
begin
```

#### Peter Nelson (Mar 10 2021 at 18:43):

ok, that seems nicer than the way I was writing it using `extends`

.

#### Eric Wieser (Mar 10 2021 at 18:43):

Heather Macbeth said:

Well, there is also:

docs#multiset.le_iff_exists_add

docs#cardinal.le_iff_exists_add :)

Well, `cardinal`

is an instance of `canonically_linear_ordered_add_monoid`

already, and multiset is a `canonically_ordered_add_monoid`

#### Eric Wieser (Mar 10 2021 at 18:45):

But I echo Heather's comment that this would be easier to discuss in a PR

#### Peter Nelson (Mar 10 2021 at 18:45):

that'll happen in the next few hours. Thanks everyone!

#### Peter Nelson (Mar 10 2021 at 20:27):

Last updated: May 07 2021 at 21:10 UTC