Maps between zmod

Stream: maths

[Adam Topaz]

What's the idiomatic way to write down the ring hom from zmod a to zmod b given a proof that b divides a?

[Mario Carneiro]

Isn't there a cast?

[Kevin Buzzard]

Yes there's a cast which is a ring hom somewhere

[Adam Topaz]

Ah, yes, it's cast_hom thanks :)

[Mario Carneiro]

it was recently involved in a scandal, but it's a good citizen if you know b divides a

[Adam Topaz]

Oof src#zmod.cast is indeed a scandal.

[Kevin Buzzard]

Mathematically random and really hard to prove anything about!

[Adam Topaz]

Would it be crazy to do something like this?

import data.zmod.basic

variables (n N : ℕ)

class divides (n N : ℕ) := (cond : n ∣ N)

def proj [divides n N] : zmod N →+* zmod n := zmod.cast_hom (divides.cond : n ∣ N) _

[Adam Topaz]

I don't want to feed in divisibility proofs all the time.

[Kyle Miller]

I think [fact (n ∣ N)] covers this sort of thing. It seems hard to know when it's appropriate to use it!

[Adam Topaz]

Cool. Although I'm surprised that mathlib doesn't have something like this:

example {a b c : ℕ} [fact (b ≤ c)] : fact (a^b  ∣ a^c) := sorry

[Mario Carneiro]

fact is exclusively for lightweight local typeclass inference. Global fact instances are banned because you could put literally anything in a fact and lean has to search through all instances in a very stupid way

[Adam Topaz]

I see. I'll just abuse the typeclass search in my own project then.

[Mario Carneiro]

You can use localized to set up largeish fact problems across several files

[Mario Carneiro]

basically fact is opt in

[Adam Topaz]

I've never made a localized thing before. Is this the right syntax?

def foo {a b c : ℕ} [fact (b ≤ c)] : fact (a^b ∣ a^c) := sorry
localized "attribute [instance] foo" in bar