Zulip Chat Archive

Stream: maths

Topic: univeral property of quotient abelian groups


view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:03):

I have a comm_group G and a subgroup N, which is the kernel of an is_group_hom f : G -> H. I'd like a quotient group G/N, and an injective group homomorphism from G/N to H. The quotient has been made for general groups (in group_theory.coset) but not the injective hom as far as I can see, and also for modules over an arbitrary ring (with the injective hom), so I can either build the injection for general groups or I can persuade Lean that an abelian group is the same as a Z-module. Have either of these been done? Neither should be hard, but which to do?

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:06):

Should there be an instance (add_comm_group G) -> module ℤ G? What about comm_group G -> module ℤ G? Do either of these cause problems?

view this post on Zulip Johan Commelin (Jul 19 2018 at 20:07):

Modules cause problems, in general. I would stay away of them for now.

view this post on Zulip Johan Commelin (Jul 19 2018 at 20:07):

I think it is best to prove a bit about the universal property of group quotients.

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:10):

I'm trying to define perfectoid spaces, I've just spent an hour worrying about constructing an object isomorphic to an object I already have but in a different universe, and now I'm doing quotient groups :-) Some things are just slow going, I guess!

view this post on Zulip Patrick Massot (Jul 19 2018 at 20:11):

I'm also having universe issues and type class inference issues at the moment

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:12):

It's good for the soul I guess...

view this post on Zulip Patrick Massot (Jul 19 2018 at 20:14):

I'm discovering new error messages

view this post on Zulip Patrick Massot (Jul 19 2018 at 20:14):

synthesized type class instance is not definitionally equal to expression inferred by typing rules

view this post on Zulip Mario Carneiro (Jul 19 2018 at 20:14):

I think an instance for add_comm_group G -> module ℤ G will not go awry

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:14):

Does that say "you have a diamond"?

view this post on Zulip Mario Carneiro (Jul 19 2018 at 20:15):

comm_group G -> module ℤ G doesn't make any sense

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:15):

I think an instance for add_comm_group G -> module ℤ G will not go awry

module might extend add_comm_group -- will there be an instance the other way?

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:16):

comm_group G -> module ℤ G doesn't make any sense

well that's a pain because my group laws are all * :-/

view this post on Zulip Mario Carneiro (Jul 19 2018 at 20:16):

ah, actually I think you are right

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:17):

I'm sticking to groups.

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:18):

I think it's about time we had a mathlib issue about modules, the chat about the problems is dispersed here and there in Zulip, I don't understand the problems myself, and they're stopping Patrick from doing stuff.

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:21):

instance [group α] (s : set α) [normal_subgroup s] : group (left_cosets s) := .... That's in section quotient_group. How do I find out the name of that instance?

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:22):

[all in group_theory/coset.lean]

view this post on Zulip Chris Hughes (Jul 19 2018 at 20:23):

left_cosets.group

view this post on Zulip Chris Hughes (Jul 19 2018 at 20:23):

Clue is in the statement.

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:24):

I remembered there was an algorithm but couldn't remember what it was. Thanks Chris.

view this post on Zulip Patrick Massot (Jul 19 2018 at 20:25):

you could also use that print_names command we did recently

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:26):

That's the other type of answer to this question. All that was way over my head, but I cut and pasted some stuff and it was pretty cool :-)

view this post on Zulip Chris Hughes (Jul 19 2018 at 20:27):

you could also use that print_names command we did recently

Is that in mathlib?

view this post on Zulip Kevin Buzzard (Jul 19 2018 at 20:29):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/full.20names

view this post on Zulip Johan Commelin (Jul 20 2018 at 10:52):

I think it's about time we had a mathlib issue about modules, the chat about the problems is dispersed here and there in Zulip, I don't understand the problems myself, and they're stopping Patrick from doing stuff.

I completely agree. They are also stopping me from doing stuff. (Both with simplicial homology and with Lie algebras...)

view this post on Zulip Patrick Massot (Jul 20 2018 at 10:55):

My hope here is that someone will fix my issue in the norms PR, and this will explain how to handle modules

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 10:58):

But you've been hoping that someone will fix modules for a long time now, and what I find I'm doing is: occasionally asking "what is the problem with modules again?", and someone answers, in some random thread, and I go "oh", and then the discussion degenerates into out_param stuff, and peters out, and then I forget everything, and it was a waste of everyone's time even talking about it. Making it an issue will at least give me a place where I can read about what the problem is and exactly what it is stopping people from doing.

view this post on Zulip Patrick Massot (Jul 20 2018 at 10:59):

The difference this time is I opened a PR for normed spaces. But feel free to open an issue

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 11:01):

If I open the issue it will just be a one-liner saying "something is wrong with modules and this issue is a place where we can talk about what it is and how to fix it".

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 11:01):

But I'm happy to do this.

view this post on Zulip Patrick Massot (Jul 20 2018 at 11:01):

The only ones who could write a much better description are Mario, Johannes and Sebastian

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 11:03):

Not you?


Last updated: May 12 2021 at 06:14 UTC