rings from subtype

Stream: new members

[Damiano Testa]

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

[Heather Macbeth]

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.

[Heather Macbeth]

Can you adjust your situation to fit this framework?

[Heather Macbeth]

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

[Damiano Testa]

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!

[Damiano Testa]

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

[Eric Wieser]

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

[Damiano Testa]

Indeed: this seems to work!

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

[Eric Wieser]

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

[Eric Wieser]

Or does it work on an arbitrary sub_semiring

[Eric Wieser]

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

[Damiano Testa]

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!

[Damiano Testa]

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

[Eric Wieser]

You should be stating that result for all subsemirings

[Eric Wieser]

Since it doesnt apply to all subtypes

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

Do we have docs#function.injective.ordered_semiring?

[Damiano Testa]

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

Thanks!

[Damiano Testa]

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

[Eric Wieser]

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

[Eric Wieser]

Hmm, also no

[Damiano Testa]

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

[Damiano Testa]

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 }

[Hanting Zhang]

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?

[Damiano Testa]

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?

[Damiano Testa]

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?

[Damiano Testa]

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.

[Eric Wieser]

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

[Eric Wieser]

That way lean will use the notation from the has_add argument

[Damiano Testa]

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 }

[Eric Wieser]

Does refl solve those goals?

[Eric Wieser]

Perhaps after using convert ... using 1

[Eric Wieser]

Or 2

[Damiano Testa]

refl does not work saying that it fails to unify

[Damiano Testa]

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.

[Damiano Testa]

convert abc using 2 gives the same goals as convert abc

[Damiano Testa]

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:

[Damiano Testa]

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

[Damiano Testa]

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 }

[Damiano Testa]

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 β :=
{ ... }

[Eric Wieser]

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

[Damiano Testa]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Damiano Testa]

Ok, good suggestion!

[Kevin Buzzard]

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

[Damiano Testa]

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

[Rémy Degenne]

docs#preorder.lift

[Damiano Testa]

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

[Damiano Testa]

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 β :=
{ ... }

[Eric Wieser]

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

[Eric Wieser]

Use library_search to find out?

[Damiano Testa]

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

[Eric Wieser]

Did it find partial_order.lift?

[Damiano Testa]

You raise a good point:

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

says

library_search failed.

[Eric Wieser]

Of course it does

[Eric Wieser]

docs#partial_order.lift requires injectivity

[Kevin Buzzard]

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

[Damiano Testa]

This also fails:

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

[Kevin Buzzard]

And a 1 and in the second one too

[Damiano Testa]

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

[Damiano Testa]

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!

[Eric Wieser]

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

[Eric Wieser]

At any rate, this is probably ready for PR comments

[Damiano Testa]

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?

[Damiano Testa]

PR #6489

[Rémy Degenne]

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

[Rémy Degenne]

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.

[Damiano Testa]

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!

[Mario Carneiro]

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

[Damiano Testa]

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

[Mario Carneiro]

perhaps partial_order.comap?

[Damiano Testa]

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!

[Mario Carneiro]

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

[Damiano Testa]

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!

[Mario Carneiro]

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

[Rémy Degenne]

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

[Damiano Testa]

The final PR only talks about ordered_stuff_ring/monoid.

[Mario Carneiro]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Rémy Degenne]

That looks good to me

[Mario Carneiro]

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

[Damiano Testa]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Damiano Testa]

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.

[Damiano Testa]

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

[Damiano Testa]

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

[Damiano Testa]

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

I would say not...

[Eric Wieser]

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

[Eric Wieser]

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?

[Johan Commelin]

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

[Johan Commelin]

Thanks for all your help!

[Eric Wieser]

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

[Damiano Testa]

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!

[Damiano Testa]

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

[Damiano Testa]

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

[Johan Commelin]

ring_hom.to_algebra already exists (with that name)

[Damiano Testa]

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

[Damiano Testa]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Johan Commelin]

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

[Damiano Testa]

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 ℝ

[Eric Wieser]

That last one looks dangerous to me

[Eric Wieser]

Oh sorry, didn't scroll down

[Eric Wieser]

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

[Damiano Testa]

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 } }

[Eric Wieser]

I thing docs#restrict_scalars might be related too

[Eric Wieser]

(deleted)

[Damiano Testa]

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

[Eric Wieser]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

Will inherit all module structures that R has

[Damiano Testa]

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.

[Eric Wieser]

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

[Eric Wieser]

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

[Damiano Testa]

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

[Eric Wieser]

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

[Damiano Testa]

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.

[Damiano Testa]

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

[Damiano Testa]

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.

[Damiano Testa]

(deleted)

[Eric Wieser]

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

[Eric Wieser]

That is, assume [semimodule ℝ≥0 N]

[Damiano Testa]

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

[Damiano Testa]

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!

[Damiano Testa]

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

[Eric Wieser]

The first of those three assumptions should be a global instance

[Eric Wieser]

You should indeed assume the other two

[Damiano Testa]

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

[Damiano Testa]

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.

[Eric Wieser]

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

[Damiano Testa]

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?

[Damiano Testa]

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

[Eric Wieser]

That instance definitely belongs in mathlib IMO

[Damiano Testa]

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

[Eric Wieser]

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

[Damiano Testa]

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!

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Damiano Testa]

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

[Damiano Testa]

PR #6560

[Eric Wieser]

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

[Damiano Testa]

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:

[Eric Wieser]

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

[Eric Wieser]

Attempted in #6562

[Damiano Testa]

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

[Eric Wieser]

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

[Eric Wieser]

Much to my surprise, CI passes already!

[Damiano Testa]

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.

[Eric Wieser]

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

[Eric Wieser]

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