subgroup map comap lemmas

Stream: general

[Adrián Doña Mateo]

Should these lemmas be included in group_theory/subgroup? Similar ones are true for submonoids, so maybe there's a way of proving it only once for one of the two. Also, I wonder if the new set_like could be used to transport lemmas like these about functions to lemmas about morphisms.

import group_theory.subgroup

namespace subgroup

variables {G H K : Type*} [group G] [group H] [group K]

open monoid_hom

@[to_additive]
lemma range_comp (f : G →* H) (g : H →* K) : (g.comp f).range = map g f.range :=
ext' $ set.range_comp g f

variables {f : G →* H}

@[to_additive]
lemma map_comap_eq (hf : function.surjective f) (K : subgroup H) :
  map f (comap f K) = K :=
ext' $ by rw [coe_map, coe_comap, set.image_preimage_eq ↑K hf]

@[to_additive]
lemma comap_map_eq (hf : function.injective f) (K : subgroup G) :
  comap f (map f K) = K :=
ext' $ by rw [coe_comap, coe_map, set.preimage_image_eq ↑K hf]

@[to_additive]
lemma map_eq_comap_of_inverse {g : H →* G} (hl : function.left_inverse g f)
  (hr : function.right_inverse g f) (K : subgroup G) : map f K = comap g K :=
ext' $ by rw [coe_map, coe_comap, set.image_eq_preimage_of_inverse hl hr]

end subgroup

[Eric Wieser]

I agree that seems like an obvious target for generalizing over subobjects. I don't think docs#set_like will help much here, but it might work as a template to build what you're suggesting

[Anne Baanen]

I was just thinking how to interface set_like nicely with the morphism typeclass proposal. I think we might end up with a has_map_comap F S typeclass which relates the "fun_like" F and the "set_like" S.

[Anne Baanen]

We'd have to be careful not to reimplement the subobject part of the category theory library though :)

[Eric Wieser]

It would be nice if there were some way to enforce that (map f s : set _) be defeq to f '' (s : set _), but I can't think of a neat way to do that right now

[Eric Wieser]

Ah, that's easy by adding a copy member to setlike

[Eric Wieser]

Ok, that doesn't work either - I don't think it's possible to generalize docs#submonoid.copy while enforcing it actually be defeq

[Adrián Doña Mateo]

Would it be worth adding them for the time being? I can think of a way of golfing docs#is_simple_group_of_surjective using map_comap_eq.

[Eric Wieser]

I think the lemmas are definitely worth having - can you check if we have them already for submodule, and if so match the names?

[Adrián Doña Mateo]

There are linear_map.map_comap_eq and linear_map.comap_map_eq but they are different. They don't assume injectivity or surjectivity. The closest is perhaps linear_map.map_comap_eq_self and linear_map.comap_map_eq_self. I don't think there's an analog to the inverse one in the linear algebra section.

[Adrián Doña Mateo]

The names I gave to these are meant to mirror the set lemmas.

[Eric Wieser]

docs#linear_map.map_comap_eq_self makes a stronger statement than the one you're proposing, right?

[Eric Wieser]

Since q ≤ f.range is less strict than function.surjective f unless q = ⊤ (docs#linear_map.range_eq_top)

[Adrián Doña Mateo]

Yes. But I don't think the stronger statement is true for groups.

[Eric Wieser]

I think it probably is; it's even true for sets!

[Adrián Doña Mateo]

Oh right, sorry. I was thinking of docs#linear_map.comap_map_eq_self. On second thought, I think even that one is true for groups.