# Zulip Chat Archive

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

Can you adjust your situation to fit this framework?

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

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

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 β :=
{ 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 (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' := _,
map_add' := _ },
```

I run into the issue, I think, that Lean now has two `1`

s 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 β :=
{ 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 (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`

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

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,
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 (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 }
```

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

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

#### 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) :
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 (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. -/
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 (Mar 01 2021 at 09:54):

Can you generate `function.injective.ordered_add_comm_monoid`

from `to_additive`

and `function.injective.ordered_comm_monoid`

?

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

At any rate, this is probably ready for PR comments

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

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

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

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

#### Johan Commelin (Mar 05 2021 at 10:03):

Thanks for all your help!

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

s 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

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

(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 `\R`

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

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

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

!

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

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