Zulip Chat Archive

Stream: new members

Topic: rings from subtype


view this post on Zulip Damiano Testa (Feb 28 2021 at 08:00):

Is something along the lines of the code below available?

import algebra.ring.basic

variables {R : Type*} [comm_semiring R]

variables {p : R  Prop} (p0 : p 0) (p1 : p 1)
  (padd :  {a b : R}, p a  p b  p (a + b))
  (pmul :  {a b : R}, p a  p b  p (a * b))

section pR

variable (p)

def pR : Type* := {r : R // p r}

end pR

instance comm_semiring : comm_semiring (pR p) := sorry

view this post on Zulip Heather Macbeth (Feb 28 2021 at 08:06):

You know, what you've written is basically the constructor for a subring: docs#subring. Then we know that a subring of a commutative ring is itself a commutative ring: docs#subring.to_comm_ring.

view this post on Zulip Heather Macbeth (Feb 28 2021 at 08:08):

Can you adjust your situation to fit this framework?

view this post on Zulip Heather Macbeth (Feb 28 2021 at 08:09):

Oh, I see, you want the semiring version, but that exists too: docs#subsemiring.to_comm_semiring

view this post on Zulip Damiano Testa (Feb 28 2021 at 08:10):

Ah, Heather, thank you very much! I did not know about any of these!

I will take a look: the semi issue may not be too relevant for me, I was just creating a template, to fit it later to what I exactly needed!
Already the comm_ring one is a great start!

Thanks!

view this post on Zulip Damiano Testa (Feb 28 2021 at 17:49):

Continuing this conversation, what I would like is to talk about the subsemiring of non-negative elements of an ordered ring R. The exact assumptions on the initial ordered rings are possibly flexible, but I would certainly like this to work when R is a comm_ring with a compatible order, possibly with no zero divisors. The most basic setup would be and , but I would like something that works simultaneously also for and ℚ≥0 and and ℝ≥0.

Hence, is what's below already in mathlib? Is there a simpler way to get Lean to realize all the repetitions in the statements/proofs?

Thanks!

import ring_theory.subring

section Rnnoneg

variables (R : Type*) [ordered_semiring R]

/--  The subtype of non-negative elements of `R`. -/
def pR : subsemiring R :=
{ carrier := {r : R | 0  r},
  one_mem' := by simp only [set.mem_set_of_eq, zero_le_one],
  mul_mem' := begin
    rintros x y (x0 : 0  x) (y0 : 0  y),
    exact mul_nonneg x0 y0,
  end,
  zero_mem' := rfl.le,
  add_mem' := begin
    rintros x y (x0 : 0  x) (y0 : 0  y),
    exact add_nonneg x0 y0,
  end }

/--  The non-negative elements come with a partial order. -/
def popR : partial_order (pR R) :=
{ le := (),
  lt := (<),
  le_refl := λ _, le_rfl,
  le_trans := λ _ _ _, le_trans,
  lt_iff_le_not_le := λ _ _, lt_iff_le_not_le,
  le_antisymm := λ _ _, le_antisymm }

/--  ... and they form an ordered semiring. -/
instance : ordered_semiring (pR R) :=
{ add_left_cancel := begin
    rintros a b, b0 : 0  b c, c0 : 0  c bc,
    injection bc with hbc,
    simpa using hbc,
  end,
  add_right_cancel := begin
    rintros a, a0 : 0  a b c, c0 : 0  c ac,
    injection ac with hac,
    simpa using hac,
  end,
  add_le_add_left := begin
    rintros a, a0 : 0  a b, b0 : 0  b (ab : a  b) c, c0 : 0  c⟩,
    apply add_le_add_left ab,
  end,
  le_of_add_le_add_left := begin
    rintros a, a0 : 0  a b, b0 : 0  b c, c0 : 0  c (hbc : a + b  a + c),
    change b  c,
    exact le_of_add_le_add_left hbc,
  end,
  zero_le_one := zero_le_one,
  mul_lt_mul_of_pos_left := λ _ _ _, mul_lt_mul_of_pos_left,
  mul_lt_mul_of_pos_right := λ _ _ _, mul_lt_mul_of_pos_right,
  ..(infer_instance : semiring (pR R)),
  ..(infer_instance : partial_order (pR R)) }

end Rnnoneg

view this post on Zulip Eric Wieser (Feb 28 2021 at 17:55):

I'd expect an instance like docs#subtype.partial_order or something that you could use for at least some of these.

view this post on Zulip Damiano Testa (Feb 28 2021 at 17:56):

Indeed: this seems to work!

def popR : partial_order (pR R) := by apply_instance

view this post on Zulip Eric Wieser (Feb 28 2021 at 18:29):

Does your ordered_semiring instance actually use any properties of the subsemiring you chose?

view this post on Zulip Eric Wieser (Feb 28 2021 at 18:29):

Or does it work on an arbitrary sub_semiring

view this post on Zulip Eric Wieser (Feb 28 2021 at 18:29):

If the latter, then mathlib ought to have provided it for you, and you should PR it!

view this post on Zulip Damiano Testa (Feb 28 2021 at 18:33):

I will take a look at this. most of these properties are simply checked on a subset of the choices, so they should hold no matter what. I will check later that there are no hidden issues.

Thanks for the comments! As usual, I always learn a lot!

view this post on Zulip Damiano Testa (Feb 28 2021 at 19:07):

Eric, glancing at the lemmas, you are right that the properties in the ordered_semiring instance above are true since they are true for any subtype of an ordered_semiring: you simply apply the property of the bigger type to the terms of the smaller one.

How does one go about "saying this in Lean"?

view this post on Zulip Eric Wieser (Feb 28 2021 at 19:08):

You should be stating that result for all subsemirings

view this post on Zulip Eric Wieser (Feb 28 2021 at 19:08):

Since it doesnt apply to all subtypes

view this post on Zulip Eric Wieser (Feb 28 2021 at 19:09):

Note that sometimes properties of the bigger one can't always be transferred to the smaller one

view this post on Zulip Eric Wieser (Feb 28 2021 at 19:10):

But when they can, a common approach is to define things like docs#function.injective.semiring

view this post on Zulip Eric Wieser (Feb 28 2021 at 19:10):

Do we have docs#function.injective.ordered_semiring?

view this post on Zulip Damiano Testa (Feb 28 2021 at 19:10):

Ok, this seems like it would take some time: I will take a look at this function.injective.semiring, but probably tomorrow!

Thanks!

view this post on Zulip Damiano Testa (Feb 28 2021 at 19:11):

The link docs#function.injective.ordered_semiring does not work, so probably not!

view this post on Zulip Eric Wieser (Feb 28 2021 at 19:15):

I assume we have docs#function.injective.preorder?

view this post on Zulip Eric Wieser (Feb 28 2021 at 19:15):

Hmm, also no

view this post on Zulip Damiano Testa (Mar 01 2021 at 04:30):

I am trying to understand how this works. Is the code below what you had in mind, in the case of a partial order?

def function.injective.partial_order [partial_order α] (f : β  α) (hf : injective f) :
  partial_order β :=
{ le := λ x y, f x  f y,
  lt := λ x y, f x < f y,
  le_refl := λ x, rfl.le,
  le_trans := λ a b c, le_trans,
  lt_iff_le_not_le := λ a b, lt_iff_le_not_le,
  le_antisymm := λ a b ab ba, hf (le_antisymm ab ba) }

view this post on Zulip Damiano Testa (Mar 01 2021 at 04:59):

I tried to extend this, but I am getting stuck: why does the proof below not work?

def function.injective.ordered_semiring [ordered_semiring α]
  [has_zero β] [has_one β] [has_add β] [has_mul β]
  (f : β  α) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
  (add :  x y, f (x + y) = f x + f y) (mul :  x y, f (x * y) = f x * f y) :
  ordered_semiring β :=
{ add_left_cancel := begin
    intros a b c bc,
    refine hf ((add_right_inj (f a)).mp _),
    have abc : f a + f b = f a + f c := (add a b).symm.trans ((congr_arg f bc).trans (add a c)),
    convert abc,
-- produces two goals.  My understanding is that Lean is not picking up what the various `+` symbols mean
-- but I am not sure whether this is really the case, nor how to fix it!
    sorry,
  end,
  add_right_cancel := sorry,
  add_le_add_left := sorry,
  le_of_add_le_add_left := sorry,
  zero_le_one := sorry,
  mul_lt_mul_of_pos_left := sorry,
  mul_lt_mul_of_pos_right := sorry,
  .. hf.partial_order f,
  .. hf.semiring f zero one add mul }

view this post on Zulip Hanting Zhang (Mar 01 2021 at 05:18):

I don't know what's going on exactly but most of the hypotheses can be bundled into docs#ring_hom. Why aren't you using semi_ring \b?

view this post on Zulip Damiano Testa (Mar 01 2021 at 06:30):

It seems to me that semiring_hom requires \b to already be a semiring, whereas I would like to prove that \b is an ordered semiring using this result. Am I misunderstanding your suggestion?

view this post on Zulip Damiano Testa (Mar 01 2021 at 06:33):

Actually, Lean seems to already know that \b is a semiring, since the last row of the proof above works. Maybe I should focus on trying to get lean to work out the semiring assumption on \b explicitly?

view this post on Zulip Damiano Testa (Mar 01 2021 at 06:39):

If I try

add_left_cancel := begin
    haveI : semiring β := hf.semiring f zero one add mul,
    let fr : ring_hom β α :=
    { to_fun := f,
      map_one' := begin
        convert one,
        _,
      end,
      map_mul' := _,
      map_zero' := _,
      map_add' := _ },

I run into the issue, I think, that Lean now has two 1s on β, one from the assumption has_one and one from the instance semiring β and I do not know how to convince it that they are the same.

view this post on Zulip Eric Wieser (Mar 01 2021 at 06:44):

Try adding add := (+) etc to your original version

view this post on Zulip Eric Wieser (Mar 01 2021 at 06:45):

That way lean will use the notation from the has_add argument

view this post on Zulip Damiano Testa (Mar 01 2021 at 07:12):

Hmm, it gets me to the same stage:

def function.injective.ordered_semiring [ordered_semiring α]
  [has_zero β] [has_one β] [has_add β] [has_mul β]
  (f : β  α) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
  (add :  x y, f (x + y) = f x + f y) (mul :  x y, f (x * y) = f x * f y) :
  ordered_semiring β :=
{ add := (+),
  add_left_cancel := begin
    intros a b c bc,
    refine hf ((add_right_inj (f a)).mp _),
    have abc : f a + f b = f a + f c := (add a b).symm.trans ((congr_arg f bc).trans (add a c)),
    convert abc,
-- two goals: add_semigroup.to_has_add α = distrib.to_has_add α
-- and: add_semigroup.to_has_add α = distrib.to_has_add α
    sorry,
    sorry,
  end,
  add_right_cancel := sorry,
  add_le_add_left := sorry,
  le_of_add_le_add_left := sorry,
  zero_le_one := sorry,
  mul_lt_mul_of_pos_left := sorry,
  mul_lt_mul_of_pos_right := sorry,
  .. hf.partial_order f,
  .. hf.semiring f zero one add mul }

view this post on Zulip Eric Wieser (Mar 01 2021 at 07:33):

Does refl solve those goals?

view this post on Zulip Eric Wieser (Mar 01 2021 at 07:34):

Perhaps after using convert ... using 1

view this post on Zulip Eric Wieser (Mar 01 2021 at 07:34):

Or 2

view this post on Zulip Damiano Testa (Mar 01 2021 at 07:38):

refl does not work saying that it fails to unify

view this post on Zulip Damiano Testa (Mar 01 2021 at 07:39):

convert abc using 1 produces

 f a + f b = f a + f b

and

f a + f c = f a + f c

as subgoals, but again refl fails to unify them.

view this post on Zulip Damiano Testa (Mar 01 2021 at 07:39):

convert abc using 2 gives the same goals as convert abc

view this post on Zulip Damiano Testa (Mar 01 2021 at 07:47):

I am really sorry about the confusion: I had a variables {α β : Type*} [semiring α] floating around, so the two add instances had been artificially introduced by me.
:face_palm:

view this post on Zulip Damiano Testa (Mar 01 2021 at 07:49):

Indeed, this now works:

def function.injective.ordered_semiring [ordered_semiring α]
  [has_zero β] [has_one β] [has_add β] [has_mul β]
  (f : β  α) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
  (add :  x y, f (x + y) = f x + f y) (mul :  x y, f (x * y) = f x * f y) :
  ordered_semiring β :=
{ add_left_cancel := λ a b c bc,
    hf ((add_right_inj (f a)).mp ((add a b).symm.trans ((congr_arg f bc).trans (add a c)))),
-- [still to finish]
}

view this post on Zulip Damiano Testa (Mar 01 2021 at 08:18):

Finally, this works!

def function.injective.ordered_semiring [ordered_semiring α]
  [has_zero β] [has_one β] [has_add β] [has_mul β]
  (f : β  α) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
  (add :  x y, f (x + y) = f x + f y) (mul :  x y, f (x * y) = f x * f y) :
  ordered_semiring β :=
{ add_le_add_left := λ a b ab c, begin
    change f (c + a)  f (c + b),
    rw [add, add],
    exact add_le_add_left ab (f c),
  end,
  le_of_add_le_add_left := λ a b c (ab : f (a + b)  f (a + c)), begin
    rw [add, add] at ab,
    exact le_of_add_le_add_left ab,
  end,
  zero_le_one := begin
    change f 0  f 1,
    rw [zero, one],
    exact zero_le_one,
  end,
  mul_lt_mul_of_pos_left := begin
    intros a b c ab c0,
    change f (c * a) < f (c * b),
    rw [mul, mul],
    apply mul_lt_mul_of_pos_left ab _,
    rwa  zero,
  end,
  mul_lt_mul_of_pos_right := begin
    intros a b c ab c0,
    change f (a * c) < f (b * c),
    rw [mul, mul],
    apply mul_lt_mul_of_pos_right ab _,
    rwa  zero,
  end,
  .. hf.partial_order f,
  .. hf.add_left_cancel_semigroup f add,
  .. hf.add_right_cancel_semigroup f add,
  .. hf.semiring f zero one add mul }

view this post on Zulip Damiano Testa (Mar 01 2021 at 09:05):

I now have a bunch of proofs for the results below. Are people interested in having them in mathlib?

def function.injective.preorder [preorder α] (f : β  α) (hf : injective f) :
  preorder β :=
{ ... }

lemma function.injective.preorder.mono [preorder α] (f : β  α) (hf : injective f) :
  @monotone β α (hf.preorder f) _ f :=
λ a b ab, ab

def function.injective.partial_order [partial_order α] (f : β  α) (hf : injective f) :
  partial_order β :=
{ ... }

def function.injective.ordered_add_comm_monoid [ordered_add_comm_monoid α]
  [has_zero β] [has_one β] [has_add β] [has_mul β]
  (f : β  α) (hf : injective f) (zero : f 0 = 0)
  (add :  x y, f (x + y) = f x + f y) :
  ordered_add_comm_monoid β :=
{ ... }

def function.injective.ordered_cancel_add_comm_monoid [ordered_cancel_add_comm_monoid α]
  [has_zero β] [has_one β] [has_add β] [has_mul β]
  (f : β  α) (hf : injective f) (zero : f 0 = 0)
  (add :  x y, f (x + y) = f x + f y) :
  ordered_cancel_add_comm_monoid β :=
{ ... }

def function.injective.ordered_semiring [ordered_semiring α]
  [has_zero β] [has_one β] [has_add β] [has_mul β]
  (f : β  α) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
  (add :  x y, f (x + y) = f x + f y) (mul :  x y, f (x * y) = f x * f y) :
  ordered_semiring β :=
{ ... }

view this post on Zulip Eric Wieser (Mar 01 2021 at 09:07):

I can't see why not, we have a precedent for those definitions for other typeclasses

view this post on Zulip Damiano Testa (Mar 01 2021 at 09:08):

Ok, and should they all go in the same file? Probably algebra.ring.basic?

view this post on Zulip Eric Wieser (Mar 01 2021 at 09:08):

They can't go there, because the ordering classes don't exist yet

view this post on Zulip Eric Wieser (Mar 01 2021 at 09:09):

Try to put each in the same file as the typeclass they implement is defined

view this post on Zulip Damiano Testa (Mar 01 2021 at 09:10):

Ok, good suggestion!

view this post on Zulip Kevin Buzzard (Mar 01 2021 at 09:16):

You don't need injectivity to pull back a preorder and the pullback is already there

view this post on Zulip Damiano Testa (Mar 01 2021 at 09:18):

Kevin, thanks! I had split the preorder from the partial_order and did not think back about the assumptions!

view this post on Zulip Rémy Degenne (Mar 01 2021 at 09:19):

docs#preorder.lift

view this post on Zulip Damiano Testa (Mar 01 2021 at 09:22):

Thanks Rémy! I see that also partial_order.lift exists: great!

view this post on Zulip Damiano Testa (Mar 01 2021 at 09:24):

I am down to what is below. Anything else that is already in mathlib?

def function.injective.ordered_add_comm_monoid [ordered_add_comm_monoid α]
  [has_zero β] [has_one β] [has_add β] [has_mul β]
  (f : β  α) (hf : injective f) (zero : f 0 = 0)
  (add :  x y, f (x + y) = f x + f y) :
  ordered_add_comm_monoid β :=
{ ... }

def function.injective.ordered_cancel_add_comm_monoid [ordered_cancel_add_comm_monoid α]
  [has_zero β] [has_one β] [has_add β] [has_mul β]
  (f : β  α) (hf : injective f) (zero : f 0 = 0)
  (add :  x y, f (x + y) = f x + f y) :
  ordered_cancel_add_comm_monoid β :=
{ ... }

def function.injective.ordered_semiring [ordered_semiring α]
  [has_zero β] [has_one β] [has_add β] [has_mul β]
  (f : β  α) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
  (add :  x y, f (x + y) = f x + f y) (mul :  x y, f (x * y) = f x * f y) :
  ordered_semiring β :=
{ ... }

view this post on Zulip Eric Wieser (Mar 01 2021 at 09:25):

It's annoying that the naming convention is different between partial_order.lift and function. Injective.semiring

view this post on Zulip Eric Wieser (Mar 01 2021 at 09:25):

Use library_search to find out?

view this post on Zulip Damiano Testa (Mar 01 2021 at 09:26):

library_search is often my first attempt, but I could not find any of these...

view this post on Zulip Eric Wieser (Mar 01 2021 at 09:27):

Did it find partial_order.lift?

view this post on Zulip Damiano Testa (Mar 01 2021 at 09:29):

You raise a good point:

def function.injective.partial_order [partial_order α] (f : β  α) :
  partial_order β :=
by library_search

says

library_search failed.

view this post on Zulip Eric Wieser (Mar 01 2021 at 09:30):

Of course it does

view this post on Zulip Eric Wieser (Mar 01 2021 at 09:30):

docs#partial_order.lift requires injectivity

view this post on Zulip Kevin Buzzard (Mar 01 2021 at 09:30):

For ordered add comm monoid you have an unneeded mul on beta

view this post on Zulip Damiano Testa (Mar 01 2021 at 09:30):

This also fails:

def function.injective.partial_order [partial_order α] (f : β  α) (hf : injective f):
  partial_order β :=
by library_search

view this post on Zulip Kevin Buzzard (Mar 01 2021 at 09:31):

And a 1 and in the second one too

view this post on Zulip Damiano Testa (Mar 01 2021 at 09:32):

Thanks for the linting! I cleared unnecessary hypotheses: now only the doc-strings are missing!

view this post on Zulip Damiano Testa (Mar 01 2021 at 09:33):

import ring_theory.subring

variables {α β : Type*}

open function

/-- Pullback an `ordered_add_comm_monoid` under an injective map. -/
def function.injective.ordered_add_comm_monoid [ordered_add_comm_monoid α]
  [has_zero β] [has_add β]
  (f : β  α) (hf : injective f) (zero : f 0 = 0)
  (add :  x y, f (x + y) = f x + f y) :
  ordered_add_comm_monoid β :=
{ add_le_add_left := λ a b ab c,
    show f (c + a)  f (c + b), by simp [add, add_le_add_left ab (f c)],
  lt_of_add_lt_add_left :=
    λ a b c bc, @lt_of_add_lt_add_left _ _ (f a) _ _ (by rwa [ add,  add]),
  ..partial_order.lift f hf,
  ..hf.add_comm_monoid f zero add }

/-- Pullback an `ordered_cancel_add_comm_monoid` under an injective map. -/
def function.injective.ordered_cancel_add_comm_monoid [ordered_cancel_add_comm_monoid α]
  [has_zero β] [has_add β]
  (f : β  α) (hf : injective f) (zero : f 0 = 0)
  (add :  x y, f (x + y) = f x + f y) :
  ordered_cancel_add_comm_monoid β :=
{ le_of_add_le_add_left := λ a b c (ab : f (a + b)  f (a + c)),
    (by { rw [add, add] at ab, exact le_of_add_le_add_left ab }),
  ..hf.add_left_cancel_semigroup f add,
  ..hf.add_right_cancel_semigroup f add,
  ..hf.ordered_add_comm_monoid f zero add }

/-- Pullback an `ordered_semiring` under an injective map. -/
def function.injective.ordered_semiring [ordered_semiring α]
  [has_zero β] [has_one β] [has_add β] [has_mul β]
  (f : β  α) (hf : injective f) (zero : f 0 = 0) (one : f 1 = 1)
  (add :  x y, f (x + y) = f x + f y) (mul :  x y, f (x * y) = f x * f y) :
  ordered_semiring β :=
{ zero_le_one := show f 0  f 1, by  simp [zero, one, zero_le_one],
  mul_lt_mul_of_pos_left := λ  a b c ab c0, show f (c * a) < f (c * b),
    begin
      rw [mul, mul],
      refine mul_lt_mul_of_pos_left ab _,
      rwa  zero,
    end,
  mul_lt_mul_of_pos_right := λ a b c ab c0, show f (a * c) < f (b * c),
    begin
      rw [mul, mul],
      refine mul_lt_mul_of_pos_right ab _,
      rwa  zero,
    end,
  ..hf.ordered_cancel_add_comm_monoid f zero add,
  ..hf.semiring f zero one add mul }

#lint

lint is happy!

view this post on Zulip Eric Wieser (Mar 01 2021 at 09:54):

Can you generate function.injective.ordered_add_comm_monoid from to_additive and function.injective.ordered_comm_monoid?

view this post on Zulip Eric Wieser (Mar 01 2021 at 09:54):

At any rate, this is probably ready for PR comments

view this post on Zulip Damiano Testa (Mar 01 2021 at 11:03):

I think that I managed to get lean to produce the additive version with the proof of the multiplicative ones. I have the issue now that lint complains about the doc-strings missing from the two automatically generated definitions.

How do I provide doc-strings for the [to_additive] stuff?

view this post on Zulip Damiano Testa (Mar 01 2021 at 11:07):

PR #6489

view this post on Zulip Rémy Degenne (Mar 01 2021 at 11:15):

Like that: [to_additive name_for_to_additive_version "Docstring for to_additive version"]

view this post on Zulip Rémy Degenne (Mar 01 2021 at 11:15):

and the name can most often be omitted. The linter will tell you to remove it if it is the same as the automatically generated one.

view this post on Zulip Damiano Testa (Mar 01 2021 at 11:19):

Rémy, thank you very much! I will update the PR. I will wait to see if the linter complains about the autogenerated name, although I imagine that I would want the autogenerated name anyway!

view this post on Zulip Mario Carneiro (Mar 01 2021 at 11:50):

I don't think that naming these after function.injective is a good idea if you want consistency, because it's not always a requirement

view this post on Zulip Damiano Testa (Mar 01 2021 at 11:51):

I am happy to give them a different name. I was simply minimizing the changes from

https://leanprover-community.github.io/mathlib_docs/algebra/ring/basic.html#function.injective.semiring

since I was trying to learn at the same time what this all meant

view this post on Zulip Mario Carneiro (Mar 01 2021 at 11:52):

perhaps partial_order.comap?

view this post on Zulip Damiano Testa (Mar 01 2021 at 11:52):

What seems to work well with this name is that you can eat the function.injective part with the assumption that the function is injective. This may not seem like a great deal to you, but I am still not entirely accustomed to dot-notation!

view this post on Zulip Mario Carneiro (Mar 01 2021 at 11:53):

No I see that, but like I said you won't get consistent naming that way unless you want function.injective.preorder even though that one doesn't take a function.injective argument

view this post on Zulip Damiano Testa (Mar 01 2021 at 11:54):

Ah, sorry, I think that the part of the thread that talked about partial_orders ended when I was told that partial_order.lift was already a thing!

view this post on Zulip Mario Carneiro (Mar 01 2021 at 11:54):

since Eric Wieser's original complaint was about lack of consistency in the naming

view this post on Zulip Rémy Degenne (Mar 01 2021 at 11:54):

The partial order one exists already and is partial_order.lift. There is also preorder.lift, linear_order.lift. I suggest keeping those names because they describe well what those lemmas do and using class_name.lift

view this post on Zulip Damiano Testa (Mar 01 2021 at 11:54):

The final PR only talks about ordered_stuff_ring/monoid.

view this post on Zulip Mario Carneiro (Mar 01 2021 at 11:55):

Those came later, and apparently were written without knowing about the *.lift lemmas

view this post on Zulip Damiano Testa (Mar 01 2021 at 11:55):

So, should the new ones that I PRed contain lift in them?

view this post on Zulip Damiano Testa (Mar 01 2021 at 11:56):

e.g. ordered_comm_monoid.lift, instead of function.injective.ordered_comm_monoid?

view this post on Zulip Rémy Degenne (Mar 01 2021 at 11:57):

That looks good to me

view this post on Zulip Mario Carneiro (Mar 01 2021 at 11:57):

Looking at the new lemmas, they seem to differ from the *.lift family in that they already expect the domain to have a one and mul

view this post on Zulip Damiano Testa (Mar 01 2021 at 11:58):

I can certainly change the three names (+2) to be of this form: class_name.lift where class_name is going to be ordered_[...].

view this post on Zulip Mario Carneiro (Mar 01 2021 at 11:59):

The point of partial_order.lift for example is to define a <= induced by the <= on the codomain, so we don't assume any structure on the domain a priori

view this post on Zulip Mario Carneiro (Mar 01 2021 at 12:00):

When there are more operations, I suppose it becomes a question of which operations you want to pull back and which you expect to already exist

view this post on Zulip Damiano Testa (Mar 01 2021 at 12:03):

In this case there is the issue that I would not want to say that the 0 ring is a subring of any other ring, since for me a ring map needs to take 1 to 0 1 (what a lapsus!)... so I would not be happy to define 1 and 0 from the map.

view this post on Zulip Damiano Testa (Mar 01 2021 at 12:05):

As far as "algebraic structures" go, though assuming add, mul, 0 and 1 seems pretty basic. In fact, you might even get away with not assuming 0, maybe...

view this post on Zulip Damiano Testa (Mar 01 2021 at 12:06):

Ah, except that it is there because of autogeneration from the assumption of 1, right? So, to remove 0 you would need to not use to_additive (which is what I was going to do anyway, until Eric suggested that I could take advantage of to_additive).

view this post on Zulip Damiano Testa (Mar 01 2021 at 12:11):

Hmm, not so sure about not needing 0: should pnat be an ordered_subsemiring of nat?

I would say not...

view this post on Zulip Eric Wieser (Mar 01 2021 at 12:47):

Mario Carneiro said:

I don't think that naming these after function.injective is a good idea if you want consistency, because it's not always a requirement

I agree, but I think that @Damiano Testa should continue to use function.injective.ordered_cancel_comm_monoid in their PR, and then someone can rename all of them at once later

view this post on Zulip Eric Wieser (Mar 05 2021 at 10:02):

So the conclusion of this thread is that you can now do:

section Rnnoneg

variables (R : Type*) [ordered_semiring R]

/--  The subtype of non-negative elements of `R`. -/
def pR : subsemiring R :=
{ carrier := {r : R | 0  r},
  one_mem' := zero_le_one,
  mul_mem' := λ x y, mul_nonneg,
  zero_mem' := rfl.le,
  add_mem' := λ x y (x0 : 0  x) y0, add_nonneg x0 y0, }

/--  ... and they form an ordered semiring. -/
instance : ordered_semiring (pR R) := infer_instance

end Rnnoneg

right?

view this post on Zulip Johan Commelin (Mar 05 2021 at 10:03):

Yes, I think we tested this on the toric branch of LTE this morning, and it works

view this post on Zulip Johan Commelin (Mar 05 2021 at 10:03):

Thanks for all your help!

view this post on Zulip Eric Wieser (Mar 05 2021 at 10:15):

You better use all the other ordering classes too to make the scope creep of the PR worthwhile :laughing:

view this post on Zulip Damiano Testa (Mar 05 2021 at 11:12):

I will try to use as many of these as possible! If needed, I will artificially prove lemmas about ordered_semi_canonical_monoids, just to use the appropriate typeclass!

view this post on Zulip Damiano Testa (Mar 05 2021 at 11:14):

In any case, I confirm that one of the new instances is already in use in the toric branch!

view this post on Zulip Damiano Testa (Mar 05 2021 at 17:09):

Continuing with the instance galore, are the instances below in mathlib?

The proofs are straightforward, but I was wondering if I have simply been unable to find them, or whether there are reasons why having them would cause issues.

Thanks!

instance ring_hom.to_algebra {R S : Type*} [comm_semiring R] [comm_semiring S] (f : R →+* S) :
  algebra R S :=

instance : algebra 0  := nnreal.to_real_hom.to_algebra

instance : semimodule 0  := by apply_instance

instance {R S : Type*} [comm_semiring R] [comm_semiring S] [algebra R S] [semimodule S M] :
  semimodule R M :=

(In case you are wondering, the apply_instance in the third line above is a consequence of the previous ones, otherwise I could not find it in mathlib.)

view this post on Zulip Johan Commelin (Mar 05 2021 at 17:31):

ring_hom.to_algebra already exists (with that name)

view this post on Zulip Damiano Testa (Mar 05 2021 at 17:36):

Good on the naming front, not so good on the search front!

view this post on Zulip Damiano Testa (Mar 05 2021 at 19:18):

Ok, so does it make sense to PR the instances below?

instance : algebra 0  := nnreal.to_real_hom.to_algebra

instance : semimodule 0  := by apply_instance

instance {R S : Type*} [comm_semiring R] [semiring S] [algebra R S] [semimodule S M] :
  semimodule R M :=
{ smul := λ a b, algebra_map R S a  b,
  one_smul := λ a, by simp only [one_smul, ring_hom.map_one],
  mul_smul := λ x y m, by simp [(), mul_smul ((algebra_map R S) x) ((algebra_map R S) y) m],
  smul_add := λ r m n, smul_add ((algebra_map R S) r) m n,
  smul_zero := λ r, smul_zero ((algebra_map R S) r),
  add_smul := λ a b m, by simp [(), add_smul ((algebra_map R S) a) ((algebra_map R S) b) m],
  zero_smul := λ m, by simp only [ring_hom.map_zero, zero_smul]}

instance pro [module  M] : semimodule 0 M := by apply_instance

view this post on Zulip Johan Commelin (Mar 05 2021 at 19:26):

Nr 1 looks good, nr 2 is by apply_instance so it is redundant, nr 3 should be a def, because the type class search can not determine S from the goal, so it will go crazy; nr 4 looks good (but the proof will have to change to use the def from nr 3).

view this post on Zulip Damiano Testa (Mar 05 2021 at 19:27):

nr 2 is by apply_instance only after nr 1 is in: that does not matter, right?

view this post on Zulip Johan Commelin (Mar 05 2021 at 19:28):

Right, as soon as nr 1 is in mathlib, nr 2 is redundant

view this post on Zulip Damiano Testa (Mar 05 2021 at 19:30):

Better?

instance : algebra 0  := nnreal.to_real_hom.to_algebra

variables {N : Type*} [add_comm_monoid N]

def semimodule.of_algebra (R S : Type*) [comm_semiring R] [semiring S] [algebra R S]
  [semimodule S N] :
  semimodule R N :=
{ smul := λ a b, algebra_map R S a  b,
  one_smul := λ a, by simp only [one_smul, ring_hom.map_one],
  mul_smul := λ x y m, by simp [(), mul_smul ((algebra_map R S) x) ((algebra_map R S) y) m],
  smul_add := λ r m n, smul_add ((algebra_map R S) r) m n,
  smul_zero := λ r, smul_zero ((algebra_map R S) r),
  add_smul := λ a b m, by simp [(), add_smul ((algebra_map R S) a) ((algebra_map R S) b) m],
  zero_smul := λ m, by simp only [ring_hom.map_zero, zero_smul]}

instance [semimodule  N] : semimodule 0 N := semimodule.of_algebra 0 

view this post on Zulip Eric Wieser (Mar 05 2021 at 19:36):

That last one looks dangerous to me

view this post on Zulip Eric Wieser (Mar 05 2021 at 19:37):

Oh sorry, didn't scroll down

view this post on Zulip Eric Wieser (Mar 05 2021 at 19:38):

I don't think semimodule.of_algebra is a great idea, that looks like something docs#is_scalar_tower is intended to solve

view this post on Zulip Damiano Testa (Mar 05 2021 at 19:39):

I would also like to have

instance ist [semimodule  N] : is_scalar_tower 0  N :=
{ smul_assoc := λ a b c, show (a.val  b)  c = a  b  c, by { rw smul_assoc a.val b c, congr } }

view this post on Zulip Eric Wieser (Mar 05 2021 at 19:41):

I thing docs#restrict_scalars might be related too

view this post on Zulip Eric Wieser (Mar 05 2021 at 19:42):

(deleted)

view this post on Zulip Damiano Testa (Mar 05 2021 at 19:44):

Eric, I am looking at your suggestions: they do look very close to what I want. (Although so far I have not been able to make them work "as is".)

view this post on Zulip Eric Wieser (Mar 05 2021 at 19:47):

Can you give two concrete examples for N for your last instance?

view this post on Zulip Damiano Testa (Mar 05 2021 at 19:48):

You mean two ℝ-modules N? Like some actual real vector spaces? Or am I misunderstanding what you are asking?

view this post on Zulip Damiano Testa (Mar 05 2021 at 19:49):

In toric I am trying to convert all the time between a vector space and a cone inside it, so I like to take "non-negative" multiples of vectors. This is the reason why I would like to have this instance.

(I just added a proof of the is_scalar_tower instance.)

view this post on Zulip Eric Wieser (Mar 05 2021 at 19:57):

My claim is that the semimodule instance should appear automatically if you define the scalar_tower one

view this post on Zulip Eric Wieser (Mar 05 2021 at 19:57):

Eg, docs#pi.semimodule for the module fin 3-> R

view this post on Zulip Eric Wieser (Mar 05 2021 at 19:58):

Will inherit all module structures that R has

view this post on Zulip Damiano Testa (Mar 05 2021 at 19:59):

If I understand you correctly, and I swap the last two like this:

instance ist [semimodule  N] : is_scalar_tower 0  N :=
{ smul_assoc := λ a b c, show (a.val  b)  c = a  b  c, by { rw smul_assoc a.val b c, congr } }

instance [semimodule  N] : semimodule 0 N := semimodule.of_algebra 0 

then, is_scalar_tower wants a has_scalar ℝ≥0 N assumption that it can't find.

view this post on Zulip Eric Wieser (Mar 05 2021 at 20:00):

I think my claim is that all concrete N you care about should be providing that is_scalar_tower instance

view this post on Zulip Eric Wieser (Mar 05 2021 at 20:01):

So in abstract situations you should just have it as a typeclass assumption

view this post on Zulip Damiano Testa (Mar 05 2021 at 20:01):

so, in the toric branch, this is a lemma that does not work without that instance and does with it:

lemma pointed_of_nnreal {ι : Type*} [module  M] {v : ι  M} (bv : is_basis  v) :
  pointed  (submodule.span 0 (set.range v)) :=
pointed_of_is_basis_is_inj (is_inj_nonneg.pR_ocr ) bv

view this post on Zulip Eric Wieser (Mar 05 2021 at 20:02):

I might take a look later. Can you give a github line permalink?

view this post on Zulip Damiano Testa (Mar 05 2021 at 20:02):

It is probably a little cryptic, but you can see the \Rmodule assumption on M which does not automatically get a nnreal is_scalar_tower.

view this post on Zulip Damiano Testa (Mar 05 2021 at 20:03):

would telling you where to find it in lean-liquid be ok?

view this post on Zulip Damiano Testa (Mar 05 2021 at 20:06):

https://github.com/leanprover-community/lean-liquid/blob/55f017b4c2238f7d5891d19b0adcc7c94bc8aa5c/src/toric_2021_02_19/toric.lean#L576

The lemma begins on line 575, the instances are before it.

view this post on Zulip Damiano Testa (Mar 05 2021 at 20:07):

(deleted)

view this post on Zulip Eric Wieser (Mar 05 2021 at 20:41):

Lines 559 to 573 should be removed, and replaced with hypotheses for the lemma on line 575

view this post on Zulip Eric Wieser (Mar 05 2021 at 20:45):

That is, assume [semimodule ℝ≥0 N]

view this post on Zulip Damiano Testa (Mar 05 2021 at 20:47):

I can certainly assume those instances, instead of proving them in general, but the situation with ℕ and ℤ is that those instances are there automatically (e.g. the lemmas on 537 and 543).

view this post on Zulip Damiano Testa (Mar 05 2021 at 20:51):

I think that Lean also wants me to assume

[algebra 0 ]
[semimodule 0 M]
[is_scalar_tower 0  M]

and then says that it cannot prove the result. Although, it is getting late, so I may be doing something silly!

view this post on Zulip Damiano Testa (Mar 05 2021 at 21:02):

It seems that making these assumptions creates new instances for what should already be there and then Lean gets stuck on using them and does not find a compatibility among them. Or maybe, this is what I think at the moment...

view this post on Zulip Eric Wieser (Mar 05 2021 at 21:04):

The first of those three assumptions should be a global instance

view this post on Zulip Eric Wieser (Mar 05 2021 at 21:04):

You should indeed assume the other two

view this post on Zulip Damiano Testa (Mar 05 2021 at 21:06):

Indeed, what is below works!

instance : algebra 0  := nnreal.to_real_hom.to_algebra

lemma pointed_of_nnreal {ι : Type*} [module  M] [semimodule 0 M] [is_scalar_tower 0  M]
  {v : ι  M} (bv : is_basis  v) :
  pointed  (submodule.span 0 (set.range v)) :=
pointed_of_is_basis_is_inj (is_inj_nonneg.pR_ocr ) bv

view this post on Zulip Damiano Testa (Mar 05 2021 at 21:07):

Why do you think that algebra => semimodule and then the nnreal instances are not good? I am not objecting, I am just trying to understand what goes wrong.

view this post on Zulip Eric Wieser (Mar 05 2021 at 21:09):

I think the key observation is that instead of trying to construct the second module structure to be consistent with the first, you just assume that someone else constructed them in a suitable way

view this post on Zulip Damiano Testa (Mar 05 2021 at 21:12):

Ok, to me, this seems a different convention than what happens with ℕ and ℤ. However, I can see that maybe ℕ gets treated differently than ℝ. Is this the case?

view this post on Zulip Damiano Testa (Mar 05 2021 at 21:15):

In any case, if you think that the instance below should go into mathlib, I can PR it (or feel free to do it yourself!), although I am going to bed now, so it will be at some other point!

instance : algebra 0  := nnreal.to_real_hom.to_algebra

view this post on Zulip Eric Wieser (Mar 05 2021 at 21:17):

That instance definitely belongs in mathlib IMO

view this post on Zulip Damiano Testa (Mar 05 2021 at 21:24):

I would put it in data/real/nnreal, but there is no import algebra.algebra.basis: it seems too much to import a file simply to use algebra for this instance, though...

view this post on Zulip Eric Wieser (Mar 05 2021 at 21:31):

N, Z, and Q are special because there are typeclasses for which every instance has an associated algebra - semiring, ring, and division_ring

view this post on Zulip Damiano Testa (Mar 05 2021 at 21:37):

I can see that, although in the case of division ring, you should also assume char_zero. Anyway, being the initial object of a "natural" category seems like a good place to draw the line!

view this post on Zulip Eric Wieser (Mar 05 2021 at 23:33):

But all three of those algebra (and semimodule) instances cause nasty non-defeq typeclass diamonds

view this post on Zulip Eric Wieser (Mar 05 2021 at 23:34):

Eg, a prod of two add_comm_monoids is a nat-module in two ways; by distributing the smul to the components, and by repeated addition

view this post on Zulip Eric Wieser (Mar 05 2021 at 23:38):

And it only gets worse, a product (M x N) x (P x Q) has 5 nat-module structures, all pairwise non-defeq

view this post on Zulip Damiano Testa (Mar 06 2021 at 05:16):

Eric, thank you for taking the time to explain the arguments in favour and against these instances!

view this post on Zulip Damiano Testa (Mar 06 2021 at 05:24):

PR #6560

view this post on Zulip Eric Wieser (Mar 06 2021 at 08:10):

Now, I guess you'll want \C to inherit that structure too...

view this post on Zulip Damiano Testa (Mar 06 2021 at 08:19):

Well, I have been working with ordered things, so I will let \C be for the moment... even though Scott was adding orders on \C! :upside_down:

view this post on Zulip Eric Wieser (Mar 06 2021 at 08:23):

I think docs#complex.algebra_over_reals should be changed to copy across any algebra structure on R, not just R itself

view this post on Zulip Eric Wieser (Mar 06 2021 at 10:47):

Attempted in #6562

view this post on Zulip Damiano Testa (Mar 06 2021 at 11:41):

Oooh, I see that this PR is also spraling... I hope that it will be easier than the other instance explosion.

view this post on Zulip Eric Wieser (Mar 06 2021 at 11:42):

But your observation that and are treated specially is salient, as that's where most of the pain in that PR is coming from

view this post on Zulip Eric Wieser (Mar 06 2021 at 11:45):

Much to my surprise, CI passes already!

view this post on Zulip Damiano Testa (Mar 06 2021 at 12:00):

I really find these conversations very useful! Thank you for explaining the "Lean translation" of "initial objects in a category".

And I am happy that this is also helpful for the development of the API that you are carrying forward!

Of course, in maths I am also used to making any ring R special/initial, by considering the category of all R-algebras. I can accept that this may not have the status of a "global" instance in Lean.

view this post on Zulip Eric Wieser (Mar 06 2021 at 12:18):

And thank you for teaching me some category theory words to describe the lean!

view this post on Zulip Eric Wieser (Mar 11 2021 at 01:05):

Eric Wieser said:

Now, I guess you'll want \C to inherit that structure too...

As of just now, you should find an algebra ℝ≥0 ℂ instance


Last updated: May 15 2021 at 23:13 UTC