Ring hom ℤ/nℤ → ℤ/mℤ?

Stream: Is there code for X?

[Michael Stoll]

Do we have the canonical ring homomorphism ℤ/nℤ → ℤ/mℤ when m divides n?

example (m n : ℕ) (h : m ∣ n) : (zmod n) →+* (zmod m) := by suggest

comes up with only

Try this: refine ring_equiv.to_ring_hom _
Try this: refine ring_hom.mk' _ _
Try this: refine ring_hom.copy _ _ _
Try this: refine {to_fun := _, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

[Eric Wieser]

docs#zmod.lift

[Michael Stoll]

That says

 def zmod.lift (n : ℕ) {A : Type u_2} [add_group A] :
{f // ⇑f ↑n = 0} ≃ (zmod n →+ A)

The map from zmod n induced by f : ℤ →+ A that maps n to 0.

which does not seem to be what I want.

[Michael Stoll]

It is only about maps preserving addition, not ring homomorphisms.

[Adam Topaz]

is there a zmod.lift_ring_hom or something?

[Eric Wieser]

docs#zmod.cast_hom

[Michael Stoll]

OK, that looks better!

[Michael Stoll]

I wonder why suggest did not pick this up?

[Eric Wieser]

Does library_search?

[Michael Stoll]

No (with or without !). But

example (m n : ℕ) (h : m ∣ n) : (zmod n) →+* (zmod m) := zmod.cast_hom h _

works...

[Jireh Loreaux]

I wonder if propose works in mathlib4?

[Jireh Loreaux]

But I'm surprised library_search didn't get it.

[Scott Morrison]

The reason library_search is not getting this is:

example (m n : ℕ) (h : m ∣ n) : (ZMod n) →+* (ZMod m) := by
  apply ZMod.castHom

fails with

failed to synthesize
  CharP (ZMod m) ?m

[Scott Morrison]

It never gets to the stage of using h : m ∣ n because the apply fails, because at that point it doesn't know which characteristic ?m to expect.

[Scott Morrison]

Sad, but I'm not sure there is a systematic way to improve this.

[Scott Morrison]

library_search wants to try this lemma: with the current heuristics, it is in fact the very first lemma it tries!

[Eric Wieser]

Is this the apply bug?

[Eric Wieser]

Could library_search learn to use refine instead?

[Scott Morrison]

I guess there is something systematic you could do:

• While applying the lemmas, postpone any typeclass goals that involve metavariables.
• Then try to solve these during the solveByElim stage.

[Scott Morrison]

Oh! Sure, can you point me to the discussion on this?

[Eric Wieser]

That was mostly a joke; @Kevin Buzzard always complains about "the apply bug" in Lean 3, which I think is usually just complaining that apply foo fails when refine foo _ _ _ with apropriately many _s works

[Eric Wieser]

I have no data indicating whether this sort of thing happens in Lean4 other than your post above

[Scott Morrison]

I don't think I know how to modify apply to return typeclass args with metavariables rather than failing on them. If anyone is interested in thinking about that, I would love to hear any outcome.

[Eric Wieser]

I guess we could also solve this by making char_p use an out_param

[Eric Wieser]

But I think there's some annoying defeq reason about char_p R (ring_char R) that makes this a bad idea, and it's been discussed before.

[Johan Commelin]

I claim char_p R (ring_char R) is an unfriendly citizen anyways. Very locally, you can use it. But if you have a lot of rings floating around that should have the same characteristic, then it's a lot better to have an abstract p once and for all.

[Alex J. Best]

Maybe then we could have a typeclass CanonicalCharP with an out param that provides an instance of CharP. Rather than modifying CharP itself and dealing with that. The idea would be the truly nice CharP instances like CharP (ZMod m) m or CharZero K to CharP K 0 can be upgraded to CanonicalCharP.