subgroups of direct products

[Alizter]

Here was some miscellaneous stuff about subgroups of products that I didn't end up using.

[jdchristensen]

This definition of the induced subgroup of G x H is concise, but in some ways is more complicated than necessary. First, subgroup_image is defined in terms of grp_image, which adds a truncation, but because grp_prod_inl is an embedding, the truncation is not needed. So maybe we should have a subgroup_image_embedding that uses grp_image_embedding, and then use that here?

Second, grp_image_embedding adds a sigma type (via hfiber), but in this case even that is not necessary. The predicate for the induced subgroup can be defined to send (g, h) to K g * (h = 1). But then we'd have to prove that this does define a subgroup, which probably makes it not worthwhile.

Neither of these are very important, but I thought I'd mention them.

[jdchristensen]

What is pred_eq? Is this referring to something we discussed earlier?

[Alizter]

Predicate equality which is introduced in #2121 addressing #2202.

[jdchristensen]

Ah, great. I'll try to get to 2121 soon.

[jdchristensen]

Another way to state the conclusion is

forall x, subgroup_product
            (subgroup_grp_prod_l (maximal_subgroup G))
            (subgroup_grp_prod_r (maximal_subgroup H)) x.

but maybe your way is better?

Independently, the two groups on the right can be simplified to (grp_image_embedding grp_prod_inl) and (grp_image_embedding grp_prod_inr), which avoids mentioning maximal groups, avoids subgroup_grp_prod_l and _r, and avoids the truncations. If your goal was this result, then using these versions of these groups would be a shorter way to get here.