isomorphism between subgroups

Stream: new members

[Edward van de Meent]

i'd like to prove that there exists an isomorphism between the stabiliser of n in the alternating group on n characters, and the alternating group of n-1 characters...
To do that, i believe i need to write a function of approximate type Subgroup a → Subgroup b, which means i get some x : Subgroup a and need to return some y:Subgroup b. i think i know how to do something similar, but for that i need something of the form x ∈ Subgroup a.
How do i convert between these? is that at all possible?

import Mathlib.GroupTheory.SpecificGroups.Alternating
import Mathlib.GroupTheory.Subgroup.Simple

open alternatingGroup
open Subgroup

theorem stabiliser_of_elem_is_alternator (n : ℕ) :
  MulAction.stabilizer (alternatingGroup (Fin (n+1))) (n: Fin (n+1)) ≃* alternatingGroup (Fin n) where
    toFun := _ -- has type alternatingGroup (Fin (n+1)) →  alternatingGroup (Fin n)
    invFun := _
    left_inv := _
    right_inv := _
    map_mul' := _

[Matt Diamond]

i think i know how to do something similar, but for that i need something of the form x ∈ Subgroup a

what similar thing are you referring to? like mapping individual elements?

[Edward van de Meent]

Well, I think that having statements like that would probably be useful, as most of the theorems for Subgroups and stabilisers seem to use the set notation... Although it might be the case that I haven't looked enough, or that my lack of experience with lean is giving me tunnel vision

[Matt Diamond]

oh wait, I think I know what you're asking about... converting terms of a type to members of a Subgroup? you can use docs#Subtype.prop and docs#Subtype.property to get the proof of membership (Edit: See below, there's a better way to do this by destructuring the function argument)

[Matt Diamond]

(deleted)

[Matt Diamond]

I was confused at first because you wrote Subgroup a → Subgroup b and I misread that as "a function that takes a Subgroup and returns a Subgroup" but that's not what you're trying to do... rather, you're trying to provide [a specific Subgroup] → [a specific Subgroup], where the Subgroups are coerced to types via Subtypes

[Matt Diamond]

So you can do something like this:

import Mathlib.GroupTheory.SpecificGroups.Alternating
import Mathlib.GroupTheory.Subgroup.Simple

open alternatingGroup
open Subgroup

theorem stabiliser_of_elem_is_alternator (n : ℕ) :
  MulAction.stabilizer (alternatingGroup (Fin (n+1))) (n: Fin (n+1)) ≃* alternatingGroup (Fin n) where
    toFun := fun x => by
      have hx := x.property -- proof that x.val is a member of the subgroup
      let y : Equiv.Perm (Fin n) := sorry
      have hy : y ∈ alternatingGroup (Fin n) := sorry
      exact ⟨y, hy⟩
    invFun := sorry
    left_inv := sorry
    right_inv := sorry
    map_mul' := sorry

[Matt Diamond]

actually, an even better solution is to destructure the Subtype up front by writing fun ⟨x, hx⟩ => ...

[Matt Diamond]

then x is the member of the Subgroup and hx is the proof of membership... clean and simple

[Johan Commelin]

Edward van de Meent said:

To do that, i believe i need to write a function of approximate type Subgroup a → Subgroup b, which means i get some x : Subgroup a and need to return some y:Subgroup b.

Your code block looks fine. But I want to briefly point out that Subgroup a → Subgroup b means "a is a group, b is a group, and this is the type of functions that turn all subgroups of a into subgroups of b".

Similarly x : Subgroup a means "x is a subgroup of the group a". It does not mean "x is an element of some subgroup". For that reason x ∈ Subgroup a doesn't really make sense. What you can write is

variable
  (G : Type*)
  [Group G]
  (H : Subgroup G)
  (x : G)
  (y : H)

#check x ∈ H : Prop
#check y.1 : G
#check y.2 : y.1 ∈ H

[Johan Commelin]

At y : H a bit of magic happens, because H is not a type at face value. But a bit of Lean code explains the elaborator how to treat H as a type anyways: namely as the type of pairs x : G, x ∈ H.

[Johan Commelin]

Concerning your isomorphism: do we already have it for permutation groups? It might be easier to do that first, and then restrict it to alternating groups in a second step.