Zulip Chat Archive

Stream: maths

Topic: normalizers


view this post on Zulip Kevin Buzzard (Jul 24 2020 at 08:35):

subgroup.normalizer (src) is the normalizer of a subgoup. This definition works fine for sets too. I changed it to sets, and the same definition still works fine (it never uses that H is a subgroup), but then in the applications I have a gazillion errors because Lean can't figure out the coercion from subgroup G to set ??. Basically, normalizers work for sets, and are occasionally useful for sets, however in pretty much all applications they're used on subgroups. What is the best way to solve this? I'd like to have access to the set normalizer function.

view this post on Zulip Scott Morrison (Jul 24 2020 at 08:38):

Can we write normalizer just in terms of set, and then have a subgroup.normalizer as essentially a forward that that normalizer, that includes the coercion explicitly.

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 08:53):

Which namespace does normalizer : set G -> subgroup G go in? I'm not very good at namespaces

view this post on Zulip Jalex Stark (Jul 24 2020 at 12:09):

group?

view this post on Zulip Jalex Stark (Jul 24 2020 at 12:11):

I'm imagining I've done open group. If I have a set s I can say normalizer s and if I have a subgroup H I can say H.normalizer


Last updated: May 19 2021 at 02:10 UTC