# Zulip Chat Archive

## Stream: general

### Topic: subgroup map comap lemmas

#### Adrián Doña Mateo (Mar 31 2021 at 12:06):

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 (Mar 31 2021 at 12:15):

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 (Mar 31 2021 at 12:21):

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 (Mar 31 2021 at 12:22):

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

#### Eric Wieser (Mar 31 2021 at 12:27):

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 (Mar 31 2021 at 12:29):

~~Ah, that's easy by adding a ~~`copy`

member to setlike

#### Eric Wieser (Mar 31 2021 at 12:32):

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 (Mar 31 2021 at 12:45):

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 (Mar 31 2021 at 12:48):

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 (Mar 31 2021 at 13:12):

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 (Mar 31 2021 at 13:13):

The names I gave to these are meant to mirror the `set`

lemmas.

#### Eric Wieser (Mar 31 2021 at 13:15):

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

#### Eric Wieser (Mar 31 2021 at 13:17):

Since `q ≤ f.range`

is less strict than `function.surjective f`

unless `q = ⊤`

(docs#linear_map.range_eq_top)

#### Adrián Doña Mateo (Mar 31 2021 at 13:19):

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

#### Eric Wieser (Mar 31 2021 at 13:24):

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

#### Adrián Doña Mateo (Mar 31 2021 at 13:42):

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.

Last updated: May 11 2021 at 12:15 UTC