Zulip Chat Archive

Stream: maths

Topic: univeral property of quotient abelian groups

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?

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?

Johan Commelin (Jul 19 2018 at 20:07):

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

Johan Commelin (Jul 19 2018 at 20:07):

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

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!

Patrick Massot (Jul 19 2018 at 20:11):

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

Kevin Buzzard (Jul 19 2018 at 20:12):

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

Patrick Massot (Jul 19 2018 at 20:14):

I'm discovering new error messages

Patrick Massot (Jul 19 2018 at 20:14):

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

Mario Carneiro (Jul 19 2018 at 20:14):

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

Kevin Buzzard (Jul 19 2018 at 20:14):

Does that say "you have a diamond"?

Mario Carneiro (Jul 19 2018 at 20:15):

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

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?

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 * :-/

Mario Carneiro (Jul 19 2018 at 20:16):

ah, actually I think you are right

Kevin Buzzard (Jul 19 2018 at 20:17):

I'm sticking to groups.

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.

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?

Kevin Buzzard (Jul 19 2018 at 20:22):

[all in group_theory/coset.lean]

Chris Hughes (Jul 19 2018 at 20:23):

left_cosets.group

Chris Hughes (Jul 19 2018 at 20:23):

Clue is in the statement.

Kevin Buzzard (Jul 19 2018 at 20:24):

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

Patrick Massot (Jul 19 2018 at 20:25):

you could also use that print_names command we did recently

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

Chris Hughes (Jul 19 2018 at 20:27):

you could also use that print_names command we did recently

Is that in mathlib?

Kevin Buzzard (Jul 19 2018 at 20:29):

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

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

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

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.

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

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".

Kevin Buzzard (Jul 20 2018 at 11:01):

But I'm happy to do this.

Patrick Massot (Jul 20 2018 at 11:01):

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

Kevin Buzzard (Jul 20 2018 at 11:03):

Not you?

Last updated: Dec 20 2023 at 11:08 UTC