set of subgroups and set of underlying set equiv

Stream: new members

[Alex Brodbelt]

Hi,

I am trying to prove that set of subgroups of a finite group with some properties is finite but I am struggling to take define an equivalence between Set (Subgroup L) to Set (Set L) which just maps the subgroups to their underlying set. I can see I might be in a pickle as going from set to subgroup seems impossible considering all the subgroup structure is lost - maybe some useful functor is lying around? but this seems too complicated for what I am trying to do.

I suspect the definition of some of properties are irrelevant but I provide them in case they are

import Mathlib

open Subgroup MatrixGroups

def IsMaximalAbelian {L : Type*} [Group L] (G : Subgroup L) : Prop := Maximal (IsCommutative) G

def MaximalAbelianSubgroups { L : Type*} [Group L] (G : Subgroup L) : Set (Subgroup L) :=
  { K : Subgroup L | IsMaximalAbelian (K.subgroupOf G) ∧ K ≤ G}

lemma finite_MaximalAbelianSubgroups {F : Type*} [Field F] (G : Subgroup SL(2,F)) [Finite G] : Finite (MaximalAbelianSubgroups G) := by
  apply Set.Finite.subset (s := {K | (K : Subgroup SL(2,F)) ≤ G})
  ·  sorry
  · intro M hM
    simp
    exact hM.right

Here the skeleton for the Equiv - I couldn't get set builder notation to work for the RHS so I thought I would just do the image of the following set through the forgetful functor(ish).

def subgroup_equiv_set {L : Type*} [Group L] {G : Subgroup L} :
  {K | (K : Subgroup L) ≤ G} ≃ (fun (K : Subgroup L) => K.carrier) '' {K | (K : Subgroup L) ≤ G} where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

[Scott Carnahan]

The map from Set (Subgroup L) to Set (Set L) taking a subgroup to its underlying set is not an equivalence, because there are subsets of L that are not subgroups (in particular, the empty subset). On the other hand, it sounds like you really just want an Injective map from Subgroup Lto Set L to get finiteness of Subgroup L, and then any subset of that is still finite.

[Alex Brodbelt]

Ah yes, of course - do you mean surjective? But yes that makes sense - thank you

[Scott Carnahan]

I'm pretty sure I mean injective. If you want to prove that Subgroup L is finite, one way is to construct an injective map from Subgroup L to a finite set.

[Alex Brodbelt]

Ah yes yes

[Kevin Buzzard]

#loogle "powerset", "finite"

[Kevin Buzzard]

@loogle "powerset", "finite"

[loogle]

:search: Set.Finite.powerset

[Alex Brodbelt]

Found the right mathlib theorem!

instance finite_MaximalAbelianSubgroups {F : Type*} [Field F] (G : Subgroup SL(2,F))
  [hG : Finite G] : Set.Finite (MaximalAbelianSubgroups G) := by
  apply Set.Finite.subset (s := {K | (K : Subgroup SL(2,F)) ≤ G})
  · apply @Finite.of_injective _ _ ?set_finite _ (Injective_subroup_to_subset G)
    exact Set.Finite.finite_subsets hG
  · intro M hM
    exact hM.right

this problem has been solved - I'll close it

[Kevin Buzzard]

don't bother closing it, it just adds noise