Zulip Chat Archive

Stream: general

Topic: subgroup.fintype_range


Anatole Dedecker (Jun 18 2021 at 22:58):

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 (Jun 19 2021 at 16:09):

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 (Jun 19 2021 at 16:26):

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

Anne Baanen (Jun 19 2021 at 20:38):

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


Last updated: Dec 20 2023 at 11:08 UTC