Zulip Chat Archive

Stream: Is there code for X?

Topic: group_with_zero morphisms with domain ℚ


view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 20 2021 at 17:20):

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

view this post on Zulip Johan Commelin (Mar 20 2021 at 17:20):

I would just prove phi_1 = phi_2

view this post on Zulip Johan Commelin (Mar 20 2021 at 17:22):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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)) : φ = φ₂

view this post on Zulip Eric Wieser (Mar 20 2021 at 17:28):

Then you can tag it with @[ext]

view this post on Zulip Johan Commelin (Mar 20 2021 at 17:30):

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

view this post on Zulip Johan Commelin (Mar 20 2021 at 17:30):

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

view this post on Zulip Eric Wieser (Mar 20 2021 at 17:31):

Wait, then why did φ₁ n work?

view this post on Zulip Johan Commelin (Mar 20 2021 at 17:32):

That's coercing nat to rat

view this post on Zulip Eric Wieser (Mar 20 2021 at 17:32):

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

view this post on Zulip Eric Wieser (Mar 20 2021 at 17:32):

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

view this post on Zulip Eric Wieser (Mar 20 2021 at 17:33):

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

view this post on Zulip Johan Commelin (Mar 20 2021 at 17:33):

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

view this post on Zulip Eric Wieser (Mar 20 2021 at 17:33):

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

view this post on Zulip Eric Wieser (Mar 20 2021 at 17:33):

But I think the lemma is salvageable

view this post on Zulip 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 Z \mathbb{Z} , then they are equal on Q \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...

view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 20 2021 at 18:36):

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

view this post on Zulip Eric Wieser (Mar 20 2021 at 18:36):

But please go ahead and make the PR :)

view this post on Zulip 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 ZQ \mathbb{Z} \to \mathbb{Q} is epi (in monoids with zero) ?
(And the other lemmas also look like saying that some arrows are epi)

view this post on Zulip 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:

view this post on Zulip Johan Commelin (Mar 20 2021 at 18:57):

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

view this post on Zulip Johan Commelin (Mar 20 2021 at 18:57):

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

view this post on Zulip Julien Marquet (Mar 20 2021 at 18:58):

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

view this post on Zulip 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 ?

view this post on Zulip Eric Wieser (Mar 20 2021 at 19:48):

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

view this post on Zulip Eric Wieser (Mar 20 2021 at 19:48):

That one should work fine in data.rat.cast

view this post on Zulip Eric Wieser (Mar 20 2021 at 19:53):

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

view this post on Zulip 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'

view this post on Zulip Eric Wieser (Mar 21 2021 at 21:33):

monoid_with_zero_hom.congr_fun same_on_int I think

view this post on Zulip Eric Wieser (Mar 21 2021 at 21:36):

docs#monoid_with_zero_hom.congr_fun


Last updated: May 17 2021 at 15:13 UTC