## Stream: new members

### Topic: rings from subtype

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


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

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

#### 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!

#### 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,
rintros x y (x0 : 0 ≤ x) (y0 : 0 ≤ y),
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) :=
rintros a ⟨b, b0 : 0 ≤ b⟩ ⟨c, c0 : 0 ≤ c⟩ bc,
injection bc with hbc,
simpa using hbc,
end,
rintros ⟨a, a0 : 0 ≤ a⟩ b ⟨c, c0 : 0 ≤ c⟩ ac,
injection ac with hac,
simpa using hac,
end,
rintros ⟨a, a0 : 0 ≤ a⟩ ⟨b, b0 : 0 ≤ b⟩ (ab : a ≤ b) ⟨c, c0 : 0 ≤ c⟩,
end,
rintros ⟨a, a0 : 0 ≤ a⟩ ⟨b, b0 : 0 ≤ b⟩ ⟨c, c0 : 0 ≤ c⟩ (hbc : a + b ≤ a + c),
change b ≤ c,
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 (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.

#### Damiano Testa (Feb 28 2021 at 17:56):

Indeed: this seems to work!

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


#### Eric Wieser (Feb 28 2021 at 18:29):

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

#### Eric Wieser (Feb 28 2021 at 18:29):

Or does it work on an arbitrary sub_semiring

#### 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!

#### 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!

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

#### Eric Wieser (Feb 28 2021 at 19:08):

You should be stating that result for all subsemirings

#### Eric Wieser (Feb 28 2021 at 19:08):

Since it doesnt apply to all subtypes

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

#### Eric Wieser (Feb 28 2021 at 19:10):

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

#### Eric Wieser (Feb 28 2021 at 19:10):

Do we have docs#function.injective.ordered_semiring?

#### 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!

#### Damiano Testa (Feb 28 2021 at 19:11):

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

#### Eric Wieser (Feb 28 2021 at 19:15):

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

Hmm, also no

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


#### 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 β :=
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,
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 (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?

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

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

#### 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' := _,


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 (Mar 01 2021 at 06:44):

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

#### Eric Wieser (Mar 01 2021 at 06:45):

That way lean will use the notation from the has_add argument

#### 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 β :=
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,
sorry,
sorry,
end,
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 (Mar 01 2021 at 07:33):

Does refl solve those goals?

#### Eric Wieser (Mar 01 2021 at 07:34):

Perhaps after using convert ... using 1

Or 2

#### Damiano Testa (Mar 01 2021 at 07:38):

refl does not work saying that it fails to unify

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

#### Damiano Testa (Mar 01 2021 at 07:39):

convert abc using 2 gives the same goals as convert abc

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

#### 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,
-- [still to finish]
}


#### 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 β :=
change f (c + a) ≤ f (c + b),
end,
le_of_add_le_add_left := λ a b c (ab : f (a + b) ≤ f (a + c)), begin
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.semiring f zero one add mul }


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

[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) :
{ ... }

[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) :
{ ... }

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 (Mar 01 2021 at 09:07):

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

#### Damiano Testa (Mar 01 2021 at 09:08):

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

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

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

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

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

#### Damiano Testa (Mar 01 2021 at 09:10):

Ok, good suggestion!

#### Kevin Buzzard (Mar 01 2021 at 09:16):

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

#### 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!

#### Rémy Degenne (Mar 01 2021 at 09:19):

docs#preorder.lift

#### Damiano Testa (Mar 01 2021 at 09:22):

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

#### 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) :
{ ... }

[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) :
{ ... }

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 (Mar 01 2021 at 09:25):

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

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

Use library_search to find out?

#### Damiano Testa (Mar 01 2021 at 09:26):

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

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

Did it find partial_order.lift?

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

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

Of course it does

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

docs#partial_order.lift requires injectivity

#### Kevin Buzzard (Mar 01 2021 at 09:30):

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

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


#### Kevin Buzzard (Mar 01 2021 at 09:31):

And a 1 and in the second one too

#### Damiano Testa (Mar 01 2021 at 09:32):

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

#### 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. -/
(f : β → α) (hf : injective f) (zero : f 0 = 0)
(add : ∀ x y, f (x + y) = f x + f y) :
show f (c + a) ≤ f (c + b), by simp [add, add_le_add_left ab (f c)],
..partial_order.lift f hf,

/-- Pullback an ordered_cancel_add_comm_monoid under an injective map. -/
(f : β → α) (hf : injective f) (zero : f 0 = 0)
(add : ∀ x y, f (x + y) = f x + f y) :
{ le_of_add_le_add_left := λ a b c (ab : f (a + b) ≤ f (a + c)),

/-- 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.semiring f zero one add mul }

#lint


lint is happy!

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

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

PR #6489

#### Rémy Degenne (Mar 01 2021 at 11:15):

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

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

#### 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!

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

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

#### Mario Carneiro (Mar 01 2021 at 11:52):

perhaps partial_order.comap?

#### 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!

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

#### 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!

#### Mario Carneiro (Mar 01 2021 at 11:54):

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

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

#### Damiano Testa (Mar 01 2021 at 11:54):

The final PR only talks about ordered_stuff_ring/monoid.

#### Mario Carneiro (Mar 01 2021 at 11:55):

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

#### Damiano Testa (Mar 01 2021 at 11:55):

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

#### Damiano Testa (Mar 01 2021 at 11:56):

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

#### Rémy Degenne (Mar 01 2021 at 11:57):

That looks good to me

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

#### 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_[...].

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

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

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

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

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

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

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

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

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

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

#### 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!

#### 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!

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

#### Johan Commelin (Mar 05 2021 at 17:31):

ring_hom.to_algebra already exists (with that name)

#### Damiano Testa (Mar 05 2021 at 17:36):

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

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


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

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

#### Johan Commelin (Mar 05 2021 at 19:28):

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

#### 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 ℝ


#### Eric Wieser (Mar 05 2021 at 19:36):

That last one looks dangerous to me

#### Eric Wieser (Mar 05 2021 at 19:37):

Oh sorry, didn't scroll down

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

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


#### Eric Wieser (Mar 05 2021 at 19:41):

I thing docs#restrict_scalars might be related too

(deleted)

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

#### Eric Wieser (Mar 05 2021 at 19:47):

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

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

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

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

#### Eric Wieser (Mar 05 2021 at 19:57):

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

#### Eric Wieser (Mar 05 2021 at 19:58):

Will inherit all module structures that R has

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

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

#### Eric Wieser (Mar 05 2021 at 20:01):

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

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


#### Eric Wieser (Mar 05 2021 at 20:02):

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

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

#### Damiano Testa (Mar 05 2021 at 20:03):

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

#### Damiano Testa (Mar 05 2021 at 20:06):

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

(deleted)

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

#### Eric Wieser (Mar 05 2021 at 20:45):

That is, assume [semimodule ℝ≥0 N]

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

#### 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!

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

#### Eric Wieser (Mar 05 2021 at 21:04):

The first of those three assumptions should be a global instance

#### Eric Wieser (Mar 05 2021 at 21:04):

You should indeed assume the other two

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


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

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

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

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


#### Eric Wieser (Mar 05 2021 at 21:17):

That instance definitely belongs in mathlib IMO

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

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

#### 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!

#### Eric Wieser (Mar 05 2021 at 23:33):

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

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

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

#### 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!

PR #6560

#### Eric Wieser (Mar 06 2021 at 08:10):

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

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

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

#### Eric Wieser (Mar 06 2021 at 10:47):

Attempted in #6562

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

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

#### Eric Wieser (Mar 06 2021 at 11:45):

Much to my surprise, CI passes already!

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

#### Eric Wieser (Mar 06 2021 at 12:18):

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

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