Improve mapping out of a generated subgroup

[Alizter]

I noticed that functor_subgroup_generated can be proven using a simpler result where the target is any subgroup rather than another generated one.

This isn't the most general way to map out of a generated subgroup however. I have some up coming work on commutators where I need a different eliminator. In that case f being a homomoprhism is weakened to a "homomorphism upto conjugation of one factor" and the target subgroup being normal takes care of the conjugation. This doesn't fall into the way of eliminating subgroups as stated here but we can discuss that when its ready.

[jdchristensen]

This result is really a combination of two things. First, consider the special case when f is the identity map. Then it says that subgroup_generated X is the smallest subgroup containing the generating set. I think this is something worth recording on its own.

And then this result follows from that special case, since S o f is again a subgroup of G (by subgroup_preimage).

I think separating this out into those two pieces would be useful and a bit shorter (since the current approach redoes subgroup_preimage).

[Alizter]

I simplified the lemma like you suggested and added a comment. I'll add the preimage version back in if it becomes useful.

[jdchristensen]

Sounds good. Do you think subgroup_generated_rec should be renamed to something like subgroup_generated_minimal?

[jdchristensen]

Did you see the previous comment?

[Alizter]

I missed that. Whats wrong with subgroup_generated_rec?

[jdchristensen]

What the result is saying is that every subgroup containing the generators contains the generated subgroup, so the generated subgroup is the minimal subgroup containing the generators. So I thought a name in that direction might make more sense. subgroup_generated_rec would seem more appropriate for something that defines a function from the generated subgroup to an arbitrary group (or even an arbitrary type).

[Alizter]

That's a good point. I think I'll hold off on that for now. At some point I should go around and start using inclusions like we do in Ideal.v for subgroups, that way it would make sense to call this a sg_incl or something to that effect.

[Alizter]

This worked out much nicer this way. My funny elimination principle I alluded to earlier became a special case by choosing a certain subgroup. It turns out you can precompose commutators with normal subgroups to get another subgroup. I have no idea what this is called, but it allowed for my later arguments to go through.