Zulip Chat Archive

Stream: maths

Topic: bundled kernels for add_comm_groups?


view this post on Zulip Kevin Buzzard (Feb 06 2020 at 11:26):

Do we have bundled group homs, kernels etc? I only need them for add_comm_groups.

view this post on Zulip Kevin Buzzard (Feb 06 2020 at 11:27):

oh I found them

view this post on Zulip Johan Commelin (Feb 06 2020 at 11:27):

Oooh, I didn't know that we had those already.

view this post on Zulip Kevin Buzzard (Feb 06 2020 at 11:27):

They're not in group_theory, they're in algebra/group

view this post on Zulip Kevin Buzzard (Feb 06 2020 at 11:28):

Is there some logic to all of this?

view this post on Zulip Kevin Buzzard (Feb 06 2020 at 11:29):

hmm, maybe we have bundled group homs but not their kernels?

view this post on Zulip Johan Commelin (Feb 06 2020 at 11:34):

We don't have bundled subgroups at the moment, do we?

view this post on Zulip Johan Commelin (Feb 06 2020 at 11:34):

So for now the kernel is just a set

view this post on Zulip Kevin Buzzard (Feb 06 2020 at 11:34):

aah is that what's missing? I'll get a student on it :-)


Last updated: May 11 2021 at 16:22 UTC