filtering a (finite) group to a subgroup

Stream: Is there code for X?

[Stuart Presnell]

Given a (finite) group G, do we already have a standard way of picking out "the subgroup of elements satisfying predicate P" (in the case where this does indeed form a subgroup)?

def filtered_group (G : Type*) [group G] [fintype G] (P : G → Prop) [decidable_pred P]
  (h_mul : ∀ a b : G, P a → P b → P (a * b))
  (h_one : P 1)
  (h_inv : ∀ a : G, P a → P a⁻¹) : subgroup G :=
{ carrier  := filter P univ,
  mul_mem' := by { simpa using h_mul },
  one_mem' := by { simpa using h_one },
  inv_mem' := by { simpa using h_inv } }

[Yakov Pechersky]

Why does it have to be [fintype G]?

[Stuart Presnell]

That was just so I could use filter P to produce the carrier.

[Stuart Presnell]

Ah, but I could use {x : G | P x} instead.

[Yakov Pechersky]

import group_theory.subgroup.basic

def filtered_group {G : Type*} [group G] (P : G → Prop)
  (h_mul : ∀ a b : G, P a → P b → P (a * b))
  (h_one : P 1)
  (h_inv : ∀ a : G, P a → P a⁻¹) : subgroup G :=
subgroup.mk (set_of P) h_mul h_one h_inv

example {G : Type*} [group G] [fintype G] (P : G → Prop) [decidable_pred P]
  (h_mul) (h_one) (h_inv) :
  ((finset.univ.filter P) : set G) = filtered_group P h_mul h_one h_inv :=
by ext; simp [filtered_group]

[Yakov Pechersky]

So filtered_group is just subgroup.mk with a set_of

[Stuart Presnell]

Thanks! Is it worth PRing this with some associated API? Or is subgroup.mk (set_of P) already a nice enough (and mathliby enough) way of spelling this?

[Ruben Van de Velde]

Do you already have two places where you'd use it?

[Stuart Presnell]

I'll try using subgroup.mk (set_of P) in the work where the problem originally arose and see how I get on.

[Eric Wieser]

Mathlib is full of { carrier := {x | p x}, ..} constructions

[Eric Wieser]

(recall that that's notation for set_of)

[Eric Wieser]

So I think the convention is to just use subgroup.mk, but almost always via {} notation