# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: group_with_zero morphisms with domain ℚ

#### Julien Marquet (Mar 20 2021 at 17:17):

I proved this :

```
theorem ext_hom_pnat {α} [group_with_zero α] (φ₁ φ₂: monoid_with_zero_hom ℚ α)
(same_on_neg_one: φ₁ (-1) = φ₂ (-1)) (same_on_nat: ∀ n: ℕ, φ₁ n = φ₂ n): (φ₁: ℚ → α) = φ₂
```

I wanted to make a PR to mathlib for it but I can't tell if it would be relevant

PROS :

- This states is closely related to the fact that ℚ is the fraction field of ℤ
- Mathlib seems open to such results (ring_theory.int.basic collects results in this vein for instance)

CONS :

- This result might be too specific to be actually useful (it may not be "mathlib-worthy" unless generalized)

One other possibility is to generalize this to fraction field and to provide this result as a particular case

The other reason why I didn't PR mathlib is that I didn't know in which file to put this result

So are some of you interested by this ?

#### Eric Wieser (Mar 20 2021 at 17:20):

This looks like it would belong next to src#ring_hom.ext_rat as `monoid_with_zero_hom.ext_rat`

, and could probably be used to shorten the proof of that lemma

#### Johan Commelin (Mar 20 2021 at 17:20):

@Julien Marquet Why do you coerce to function in the conclusion?

#### Johan Commelin (Mar 20 2021 at 17:20):

I would just prove `phi_1 = phi_2`

#### Johan Commelin (Mar 20 2021 at 17:22):

I guess you can use this to golf the `ext_rat`

result that Eric mentioned

#### Johan Commelin (Mar 20 2021 at 17:22):

Also, the name mention `pnat`

, but I think the name should probably be `monoid_with_zero_hom.ext_rat`

#### Julien Marquet (Mar 20 2021 at 17:23):

Johan Commelin said:

Julien Marquet Why do you coerce to function in the conclusion?

(It made sense in the context of the proof, but not here)

#### Eric Wieser (Mar 20 2021 at 17:28):

I think it would be even better to define a `int.cast_monoid_with_zero_hom`

(like docs#int.cast_ring_hom), and then state your lemma as

```
theorem ext_rat {α} [group_with_zero α] (φ₁ φ₂ : monoid_with_zero_hom ℚ α) (h : φ₁.comp (int.cast_monoid_with_zero_hom) = φ₂.comp (cast_monoid_with_zero_hom)) : φ = φ₂
```

#### Eric Wieser (Mar 20 2021 at 17:28):

Then you can tag it with `@[ext]`

#### Johan Commelin (Mar 20 2021 at 17:30):

@Eric Wieser but there isn't necessarily a unique `monoid_with_zero_hom`

from `int`

, right?

#### Johan Commelin (Mar 20 2021 at 17:30):

There isn't really a `cast`

, because you don't assume `has_add`

on the target.

#### Eric Wieser (Mar 20 2021 at 17:31):

Wait, then why did `φ₁ n`

work?

#### Johan Commelin (Mar 20 2021 at 17:32):

That's coercing `nat`

to `rat`

#### Eric Wieser (Mar 20 2021 at 17:32):

Right, and in my lemma the cast is from int to rat

#### Eric Wieser (Mar 20 2021 at 17:32):

But I see your point, there's no general cast

#### Eric Wieser (Mar 20 2021 at 17:33):

So `φ₁.comp (int.cast_ring_hom.to_monoid_with_zero_hom)`

?

#### Johan Commelin (Mar 20 2021 at 17:33):

Ooh, sorry, then I misunderstood the type of your proposed `int.cast_monoid_with_zero_hom`

.

#### Eric Wieser (Mar 20 2021 at 17:33):

My proposed function was stupid, you called me out on that

#### Eric Wieser (Mar 20 2021 at 17:33):

But I think the lemma is salvageable

#### Julien Marquet (Mar 20 2021 at 18:21):

Eric Wieser said:

This looks like it would belong next to src#ring_hom.ext_rat as

`monoid_with_zero_hom.ext_rat`

, and could probably be used to shorten the proof of that lemma

Should it really be put in this file ?

I am actually very tempted to add that :

- If two monoid_with_zero_hom are equal on $\mathbb{Z}$, then they are equal on $\mathbb{Q}$
- If two monoid_with_zero_hom are equal on all primes and all invertibles, then they are equal everywhere

(the second theorem can even be generalized to fraction fields, as I said earlier)

It seems to me that these three lemmas should be kept together, and that they don' belong in `data.int.cast`

...

#### Johan Commelin (Mar 20 2021 at 18:31):

I would say that this one belongs in `data.int.cast`

because then it is available "everywhere".

#### Johan Commelin (Mar 20 2021 at 18:32):

But if you prove something general for localisations, then that should of course go in the file on localisations

#### Julien Marquet (Mar 20 2021 at 18:35):

I don't plan on generalizing for now, so to `data.int.cast`

it will go

Thanks

#### Eric Wieser (Mar 20 2021 at 18:36):

Your first bullet is a weaker version of what I was suggesting you prove

#### Eric Wieser (Mar 20 2021 at 18:36):

But please go ahead and make the PR :)

#### Julien Marquet (Mar 20 2021 at 18:55):

Eric Wieser said:

Your first bullet is a weaker version of what I was suggesting you prove

Oh I see

I guess that what we would really want is to show that the inection $\mathbb{Z} \to \mathbb{Q}$ is epi (in monoids with zero) ?

(And the other lemmas also look like saying that some arrows are epi)

#### Julien Marquet (Mar 20 2021 at 18:56):

At least I thought about showing that but I'm not sure I want to dive into these details now :sweat_smile:

#### Johan Commelin (Mar 20 2021 at 18:57):

I think that the way you phrased it originally is quite suitable for mathlib

#### Johan Commelin (Mar 20 2021 at 18:57):

@Julien Marquet do you already have write access to mathlib?

#### Julien Marquet (Mar 20 2021 at 18:58):

Yes (I'm thejohncrafter on github), thanks :)

#### Julien Marquet (Mar 20 2021 at 19:12):

I just encountered a problem when trying to add this to mathlib :/

I tried to add everything to `data.rat.cast`

, but or the theorem `ext_hom_primes`

, I need to have `nat.prime`

in scope, which lies in `data.nat.prime`

, but `data.nat.prime`

depends on `tactic.norm_num`

which depends back on `data.rat.cast`

, and I can't remove the dependency on `tactic.norm_num`

.

Is there a way to work around this ?

#### Eric Wieser (Mar 20 2021 at 19:48):

Can you PR the theorem that doesn't need `primes`

first?

#### Eric Wieser (Mar 20 2021 at 19:48):

That one should work fine in `data.rat.cast`

#### Eric Wieser (Mar 20 2021 at 19:53):

But as you remark, the other one will need to go somewhere else

#### Julien Marquet (Mar 21 2021 at 21:05):

@Eric Wieser I was trying to prove what you suggested

```
theorem ext_hom_int {α} [group_with_zero α] (φ₁ φ₂ : monoid_with_zero_hom ℚ α)
(same_on_int : φ₁.comp (int.cast_ring_hom ℚ).to_monoid_with_zero_hom =
φ₂.comp (int.cast_ring_hom ℚ).to_monoid_with_zero_hom) : φ₁ = φ₂ :=
begin
have same_on_int' : ∀ k : ℤ, φ₁ k = φ₂ k,
{ sorry },
sorry -- The rest is done
end
```

but I am stuck at the first sorry because I can't find the right lemmas to go grom `same_on_int`

to `same_on_int'`

#### Eric Wieser (Mar 21 2021 at 21:33):

`monoid_with_zero_hom.congr_fun same_on_int`

I think

#### Eric Wieser (Mar 21 2021 at 21:36):

docs#monoid_with_zero_hom.congr_fun

Last updated: May 17 2021 at 15:13 UTC