Zulip Chat Archive

Stream: general

Topic: no_zero_smul_divisors

Eric Rodriguez (Dec 26 2021 at 04:08):

we have a fair few theorems stating that some algebra map is injective. we also have docs#no_zero_smul_divisors, which is essentially that fact but made available to TC; can we start adding instances such as no_zero_smul_divisors A K for is_fraction_ring A K? (docs#is_fraction_ring.injective)? If so, should we also _remove_ these explicit algebra_map_injectives and use docs#no_zero_smul_divisors.algebra_map_injective? In that case, should we even rename this to algebra_map_injective, and then basically have it documented that if you want injective(algebra_map), you should basically try this magic incantation? Or is that too noob-unfriendly

Eric Rodriguez (Dec 26 2021 at 04:09):

I'm very happy with any solution, but I'd quite like the instances... I'll put a poll up too

Eric Rodriguez (Dec 26 2021 at 04:10):

/poll What to do with injective algebra_maps?
Move everything to no_smul_zero_divisors + rename no_smul_zero_divisors.algebra_map_injective
Move everything to no_smul_zero_divisors without the rename
Leave both options available
Don't move anything to no_smul_zero_divisors

Andrew Yang (Dec 26 2021 at 04:16):

Why didn't we make function.injective a class in the first place?

Eric Rodriguez (Dec 26 2021 at 04:28):

My fuzzy memory tells me it used to be, then issues came up; maybe this is sort of what Anne's fun_like things are building up to (the "correct" approach to turning things like this into classes)

Reid Barton (Dec 26 2021 at 04:49):

I mean, in general you don't want things to be classes by default because classes are a pain

Andrew Yang (Dec 26 2021 at 04:50):

Why so? I've not yet been bitten by a Prop valued class.

Reid Barton (Dec 26 2021 at 04:51):

They make it harder to just prove stuff

Andrew Yang (Dec 26 2021 at 04:57):

Its probably because of my lack of experience that I have not yet ran into any problems, but I think the category theory part of mathlib uses classes quite extensively and yet it is quite easy to use?

Eric Rodriguez (Dec 27 2021 at 14:27):

I just wanna bump this before I start a refactor and then find out people have opinions on how this should be done

Eric Rodriguez (Dec 27 2021 at 14:27):

(although maybe this is inadvisable considering how many problems I'm having with this specific class in FLT-regular, c.f. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/TC.20hell.20in.20FLT-regular)

Last updated: Aug 03 2023 at 10:10 UTC