Zulip Chat Archive

Stream: maths

Topic: Maps between zmod


view this post on Zulip Adam Topaz (Sep 01 2020 at 21:06):

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

view this post on Zulip Mario Carneiro (Sep 01 2020 at 21:06):

Isn't there a cast?

view this post on Zulip Kevin Buzzard (Sep 01 2020 at 21:07):

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

view this post on Zulip Adam Topaz (Sep 01 2020 at 21:08):

Ah, yes, it's cast_hom thanks :)

view this post on Zulip Mario Carneiro (Sep 01 2020 at 21:08):

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

view this post on Zulip Adam Topaz (Sep 01 2020 at 21:13):

Oof src#zmod.cast is indeed a scandal.

view this post on Zulip Kevin Buzzard (Sep 01 2020 at 21:20):

Mathematically random and really hard to prove anything about!

view this post on Zulip Adam Topaz (Sep 01 2020 at 21:41):

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) _

view this post on Zulip Adam Topaz (Sep 01 2020 at 21:41):

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

view this post on Zulip Kyle Miller (Sep 01 2020 at 21:43):

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

view this post on Zulip Adam Topaz (Sep 01 2020 at 22:01):

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

view this post on Zulip Mario Carneiro (Sep 01 2020 at 22:03):

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

view this post on Zulip Adam Topaz (Sep 01 2020 at 22:04):

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

view this post on Zulip Mario Carneiro (Sep 01 2020 at 22:05):

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

view this post on Zulip Mario Carneiro (Sep 01 2020 at 22:05):

basically fact is opt in

view this post on Zulip Adam Topaz (Sep 01 2020 at 22:09):

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

Last updated: May 11 2021 at 16:22 UTC