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

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

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