## 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

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]

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