Correct setting for positive shifts of intervals

Stream: Is there code for X?

[Peter Nelson]

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]

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

[Eric Wieser]

So docs#set.image_add_const_Ico?

[Peter Nelson]

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

[Eric Wieser]

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

[Peter Nelson]

(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]

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]

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]

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]

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]

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]

Right, although the existing lemmas covers int right?

[Yury G. Kudryashov]

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]

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]

(deleted)

[Peter Nelson]

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]

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]

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 ≤ 2you 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]

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]

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]

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]

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]

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

Well, there is also:
docs#multiset.le_iff_exists_add
docs#cardinal.le_iff_exists_add :)

[Peter Nelson]

good point!

[Peter Nelson]

also set union

[Peter Nelson]

(deleted)

[Eric Wieser]

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

[Eric Wieser]

That or one of the lemmas it uses is

[Peter Nelson]

So would the typeclass correspond to 'the nonnegative elements of some ordered_add_comm_group' and have instances from nat and nnreal?

[Eric Wieser]

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]

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]

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

[Eric Wieser]

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]

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

[Peter Nelson]

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

[Peter Nelson]

#6629