subgroup.fintype_range

Stream: general

[Anatole Dedecker]

Would these instances cause any problem ? I'm considering adding them because they allow to do with bundled subgroups what is already possible with (deprecated) unbundled subgroups : when working with unbundled subgroups everything is set.range anyway, so typeclass inference finds docs#set.finite_image and docs#set.finite_range

import group_theory.subgroup

instance subgroup.fintype_comap {G H : Type*} [group G] [group H] [decidable_eq H] (S : subgroup G)
  [fintype S] (f : G →* H) : fintype (S.map f) :=
set.fintype_image S.carrier f

instance subgroup.fintype_range {G H : Type*} [group G] [group H] [decidable_eq H] [fintype G]
  (f : G →* H) : fintype f.range :=
set.fintype_range f

[Anne Baanen]

We'll definitely need a lemma saying S = T implies finset.univ (S.map f) = finset.univ (T.map f). I can't think of any other important considerations. (They do not appear fragile since there's no dependence on a specific choice of f, and the specific choice of S is not too bad since there are more typeclasses for specific subgroups.)

[Jasmin Blanchette]

Anne, isn't your lemma just an instance of eq.subst?

[Anne Baanen]

You are completely right, not quite sure what I was thinking there :P