group_with_zero morphisms with domain ℚ

Stream: Is there code for X?

[Julien Marquet]

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]

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]

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

[Johan Commelin]

I would just prove phi_1 = phi_2

[Johan Commelin]

I guess you can use this to golf the ext_rat result that Eric mentioned

[Johan Commelin]

Also, the name mention pnat, but I think the name should probably be monoid_with_zero_hom.ext_rat

[Julien Marquet]

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]

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]

Then you can tag it with @[ext]

[Johan Commelin]

@Eric Wieser but there isn't necessarily a unique monoid_with_zero_hom from int, right?

[Johan Commelin]

There isn't really a cast, because you don't assume has_add on the target.

[Eric Wieser]

Wait, then why did φ₁ n work?

[Johan Commelin]

That's coercing nat to rat

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Johan Commelin]

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

[Eric Wieser]

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

[Eric Wieser]

But I think the lemma is salvageable

[Julien Marquet]

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]

I would say that this one belongs in data.int.cast because then it is available "everywhere".

[Johan Commelin]

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

[Julien Marquet]

I don't plan on generalizing for now, so to data.int.cast it will go
Thanks

[Eric Wieser]

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

[Eric Wieser]

But please go ahead and make the PR :)

[Julien Marquet]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Julien Marquet]

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

[Julien Marquet]

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]

Can you PR the theorem that doesn't need primes first?

[Eric Wieser]

That one should work fine in data.rat.cast

[Eric Wieser]

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

[Julien Marquet]

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

monoid_with_zero_hom.congr_fun same_on_int I think

[Eric Wieser]

docs#monoid_with_zero_hom.congr_fun