Sylow Subgroup is preserved with respect to conjugation?

Stream: mathlib4

[张守信(Shouxin Zhang)]

How can we prove that if a subgroup H of group G has a Sylow p-subgroup Q, then g•Q is a Sylow p-subgroup of g•H? Here, • represents the conjugation action.

section muSylowConj
namespace muSylowConj

open Subgroup Sylow MulAut ConjAct Pointwise

variable (p : ℕ) {G : Type*} [Group G] {p : ℕ} [Fact p.Prime] (H : Subgroup G) (Q : Sylow p H) (g : G) (h : H)

instance Subgroup_subgroup [Group G] {H : Subgroup G} : CoeOut (Subgroup H) (Subgroup G) where
  coe := fun K => Subgroup.map H.subtype K

def Q' (Q : Subgroup G) (g : G) := (toConjAct g) • (Q : Subgroup G)
def H' := (toConjAct g) • H

def my_sylow_smul (g : G) (Q : Sylow p H) : Sylow p (H' H g) := by
  apply Sylow.mk
  let Q_ := Q' Q g
  . have is_p_group_Q_: IsPGroup p Q_ := by
      have : IsPGroup p Q := by
        exact IsPGroup.map Q.2 H.subtype
      show IsPGroup p (@HSMul.hSMul (ConjAct G) (Subgroup G) (Subgroup G) instHSMul (toConjAct g) (map H.subtype Q.toSubgroup) )
      exact IsPGroup.map this ((MulDistribMulAction.toMonoidEnd (ConjAct G) G) (toConjAct g))
    exact IsPGroup.comap_subtype is_p_group_Q_
  . sorry

end muSylowConj
end muSylowConj

Next, I need to prove the maximality of Q_. Mathematically, this is easy because Q is maximal among Sylow p-subgroups of H, and since the conjugation relation preserves subgroups, Q_ must also be maximal among Sylow p-subgroups of H_.

However, I've encountered problems in Lean because this involves many complex type conversions. Can someone help me with this?

[Kevin Buzzard]

I would first prove that if $\phi:G_1\to G_2$ is an isomorphism then it sends Sylow $p$-subgroups of $G_1$ to Sylow $p$-subgroups of $G_2$ (we might have this already?) and deduce it from that.

Another possibility, if you really want to switch between $H$ being a group and $H$ being a subgroup, is to define a new predicate which eats two subgroups $H$ and $Q$ of G and returns the statement "$Q\subseteq H$ and $Q$ is a Sylow $p$-subgroup of $H$ considered as a group" (it might even be simpler to work with "$Q\cap H$ is a Sylow $p$-subgroup of $H$" and forget about the inclusion) and develop some of the API there, and then work with eveyrthing being a subgroup of $G$.

[张守信(Shouxin Zhang)]

Kevin Buzzard said:

I would first prove that if $\phi:G_1\to G_2$ is an isomorphism then it sends Sylow $p$-subgroups of $G_1$ to Sylow $p$-subgroups of $G_2$ (we might have this already?) and deduce it from that.

Another possibility, if you really want to switch between $H$ being a group and $H$ being a subgroup, is to define a new predicate which eats two subgroups $H$ and $Q$ of G and returns the statement "$Q\subseteq H$ and $Q$ is a Sylow $p$-subgroup of $H$ considered as a group" (it might even be simpler to work with "$Q\cap H$ is a Sylow $p$-subgroup of $H$" and forget about the inclusion) and develop some of the API there, and then work with eveyrthing being a subgroup of $G$.

"Group isomorphisms preserve Sylow p-subgroups"

I searched through the mathlib4 library, but I couldn't find this magical theorem...

[Thomas Browning]

docs#Sylow.comapOfInjective lets you take the preimage of a Sylow subgroup

[Thomas Browning]

Paired with docs#Sylow.exists_comap_eq_of_injective should tell you that every Sylow subgroup of $G_1$ arises in this way.

[张守信(Shouxin Zhang)]

In the end, I wrote a mountain of bad code. This lengthy proof borrowed from the work of others. I'm certain that the task could be accomplished in less than 60 lines of code, but I don't know how to do it.

import Mathlib

section Exercise_1192
namespace Exercise_1192
set_option maxHeartbeats 0
open Subgroup CommGroup MulAut ConjAct Pointwise

variable {G : Type*} [Group G]
variable (p : ℕ) [Fact p.Prime]
variable (H : Subgroup G) (P : Sylow p H)

instance Subgroup_subgroup [Group G] {H : Subgroup G} : CoeOut (Subgroup H) (Subgroup G) where
  coe := fun K => Subgroup.map H.subtype K

def myconjSylow (g : G) :
  let H' := (toConjAct g) • (H : Subgroup G)
  Sylow p H' := by
  dsimp
  use ((toConjAct g) • (P : Subgroup G)).subgroupOf (toConjAct g • H)
  . refine IsPGroup.comap_subtype ?_
    refine IsPGroup.map ?_ ((MulDistribMulAction.toMonoidEnd (ConjAct G) G) (toConjAct g))
    exact IsPGroup.map P.isPGroup' H.subtype
  . intro P₀ h₁ h₂
    clear Q
    let myconjEquiv : H ≃* (@HSMul.hSMul (ConjAct G) (Subgroup G) (Subgroup G) instHSMul (toConjAct g) H ) := by
      exact {
        toFun := by
          intro y
          use (toConjAct g) • y.val
          simp only [smul_mem_pointwise_smul_iff, SetLike.coe_mem]
        invFun := by
          intro y
          use (toConjAct g⁻¹) • y.val
          simp only [map_inv]
          rcases y with ⟨y_val, y_h⟩
          simp only
          rcases y_h with ⟨z, hz₁, hz₂⟩
          rw [← hz₂]
          simp only [MulDistribMulAction.toMonoidEnd_apply, MulDistribMulAction.toMonoidHom_apply,
            inv_smul_smul]
          exact hz₁
        left_inv := by
          simp only [map_inv]
          unfold toConjAct
          unfold ofConjAct
          simp only [MulEquiv.symm_mk, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk, id_eq]
          intro y
          simp only [inv_smul_smul, Subtype.coe_eta]
        right_inv := by
          intro y
          simp only [map_inv, smul_inv_smul, Subtype.coe_eta]
        map_mul' := by
          intro x y
          simp only [Submonoid.coe_mul, coe_toSubmonoid, smul_mul', Submonoid.mk_mul_mk,
            pointwise_smul_toSubmonoid]
      }
    have this_1 : ↑P ≤ map myconjEquiv.symm.toMonoidHom P₀ := by
      rw [@SetLike.le_def]
      intro y hy
      apply mem_map_equiv.mpr
      simp only [MulEquiv.symm_symm]
      replace hy : myconjEquiv y ∈ (map myconjEquiv.toMonoidHom ↑P) := by
        refine mem_map_equiv.mpr ?_
        simp only [MulEquiv.symm_apply_apply, hy]
      have : (map myconjEquiv.toMonoidHom ↑P) ≤ (toConjAct g • map H.subtype ↑P).subgroupOf (toConjAct g • H) := by
        have : (map myconjEquiv.toMonoidHom ↑P) = (toConjAct g • map H.subtype ↑P) := by
          simp only [pointwise_smul_toSubmonoid, map_inv, myconjEquiv]
          refine Subgroup.ext ?_
          intro x
          constructor
          . intro hx
            simp only [mem_map, MulEquiv.coe_toMonoidHom, MulEquiv.coe_mk, Equiv.coe_fn_mk,
              Subtype.exists, coeSubtype, coe_pointwise_smul, Subtype.mk.injEq, exists_and_right,
              exists_and_left, exists_prop, exists_eq_right_right] at hx
            refine (mem_smul_pointwise_iff_exists x (toConjAct g) (map H.subtype ↑P)).mpr ?_
            rcases hx with ⟨a, ⟨ha1, ha2⟩⟩
            rw [ha2] at ha1
            clear a ha2
            rcases ha1 with ⟨ha21, ⟨a, ⟨ha22, ha23⟩⟩⟩
            use a
            constructor
            . refine mem_map.mpr ?_
              rcases ha22 with ⟨z, hz⟩
              use ⟨a, z⟩
              constructor
              . exact hz
              . simp only [coeSubtype]
            . exact ha23
          . intro hx
            simp only [mem_map, MulEquiv.coe_toMonoidHom, MulEquiv.coe_mk, Equiv.coe_fn_mk,
              Subtype.exists, coeSubtype, coe_pointwise_smul, Subtype.mk.injEq, exists_and_right,
              exists_and_left, exists_prop, exists_eq_right_right]
            use x
            constructor
            . constructor
              . refine (mem_smul_pointwise_iff_exists x (toConjAct g) H).mpr ?_
                rw [@mem_smul_pointwise_iff_exists] at hx
                rcases hx with ⟨s, ⟨hs1, hs2⟩⟩
                use s
                constructor
                . rw [← @zpowers_le] at hs1
                  rw [← @zpowers_le]
                  have : map H.subtype ↑P ≤ H := by
                    exact map_subtype_le (G := G) (H := H) ↑P
                  exact fun ⦃x⦄ a => this (hs1 a)
                . exact hs2
              . rw [@mem_smul_pointwise_iff_exists] at hx
                rcases hx with ⟨s, ⟨hs1, hs2⟩⟩
                use s
                constructor
                . rcases hs1 with ⟨t, ⟨ht1, ht2⟩⟩
                  simp only [SetLike.mem_coe] at ht1
                  rw [@coeSubtype] at ht2
                  rw [← ht2]
                  have : t.val ∈ H := by exact SetLike.coe_mem t
                  use this
                . exact hs2
            exact rfl
        rw [← this]
        refine map_subtype_le_map_subtype.mp ?_
        simp only [pointwise_smul_toSubmonoid, subgroupOf_map_subtype, le_inf_iff, le_refl,
          true_and]
        simp only [map_inv, myconjEquiv]
        apply map_subtype_le
      exact h₂ (this hy)
    have temp : map myconjEquiv.symm.toMonoidHom P₀ = P := by
      apply P.3
      . exact IsPGroup.map h₁ myconjEquiv.symm.toMonoidHom
      . exact this_1
    rw [← temp]
    refine Subgroup.ext ?_
    intro x
    have : @HSMul.hSMul (ConjAct G) (Subgroup G) (Subgroup G) instHSMul (toConjAct g) (map H.subtype (map myconjEquiv.symm.toMonoidHom P₀)) = map myconjEquiv.toMonoidHom (map myconjEquiv.symm.toMonoidHom P₀) := by
      refine Subgroup.ext ?_
      intro y
      constructor
      . intro hy
        simp only [pointwise_smul_toSubmonoid, map_inv, MulEquiv.symm_mk, myconjEquiv] at *
        simp only [mem_map, MulEquiv.coe_toMonoidHom, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk,
          Subtype.exists, Equiv.coe_fn_mk, Subtype.mk.injEq, exists_and_right, exists_and_left,
          exists_exists_and_eq_and, smul_inv_smul, coeSubtype, coe_pointwise_smul, exists_prop,
          exists_eq_right_right]
        use y
        rcases hy with ⟨z, hz1, hz2⟩
        simp only [coe_map, coeSubtype, MulEquiv.coe_toMonoidHom, MulEquiv.coe_mk,
          Equiv.coe_fn_symm_mk, Set.mem_image, SetLike.mem_coe, Subtype.exists, Subtype.mk.injEq,
          exists_and_right, exists_and_left, exists_prop, exists_eq_right_right] at hz1
        simp only [MulDistribMulAction.toMonoidEnd_apply, MulDistribMulAction.toMonoidHom_apply] at hz2
        rcases hz1 with ⟨a, ⟨ha1, ha2⟩⟩
        rw [ha2] at ha1
        clear a ha2
        rcases ha1 with ⟨ha21, ⟨a, ⟨ha22, ha23⟩⟩⟩
        have : a = y := by
          rw [← hz2]
          rw [@inv_smul_eq_iff] at ha23
          exact ha23
        rw [this] at ha22 ha23
        simp only [and_true]
        constructor
        . constructor
          . rw [← hz2]
            simp only [smul_mem_pointwise_smul_iff, ha21]
          . exact ha22
        . rw [ha23]
          exact ha21
      . intro hy
        apply (mem_smul_pointwise_iff_exists y (toConjAct g) (map H.subtype (map myconjEquiv.symm.toMonoidHom P₀))).mpr
        rw [@mem_map] at hy
        simp only [pointwise_smul_toSubmonoid, map_inv, MulEquiv.symm_mk, mem_map,
          MulEquiv.coe_toMonoidHom, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk, Subtype.exists,
          coeSubtype, Subtype.mk.injEq, exists_and_right, exists_and_left, exists_prop,
          exists_eq_right_right, myconjEquiv]
        simp only [pointwise_smul_toSubmonoid, map_inv, MulEquiv.symm_mk, mem_map,
          MulEquiv.coe_toMonoidHom, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk, Subtype.exists,
          Equiv.coe_fn_mk, Subtype.mk.injEq, exists_and_right, exists_and_left,
          exists_exists_and_eq_and, smul_inv_smul, coeSubtype, coe_pointwise_smul, exists_prop,
          exists_eq_right_right, myconjEquiv] at hy
        rcases hy with ⟨a, ⟨ha1, ha2⟩⟩
        rw [ha2] at ha1
        clear a ha2
        rcases ha1 with ⟨⟨ha111, ha112⟩, ha12⟩
        use ((toConjAct g)⁻¹ • y)
        simp only [exists_eq_right, smul_left_cancel_iff, smul_inv_smul, and_true]
        exact ⟨ha12, ha112⟩

    rw [this]
    constructor
    . simp only [pointwise_smul_toSubmonoid, map_inv, MulEquiv.symm_mk, myconjEquiv]
      intro hx
      refine mem_subgroupOf.mpr ?_
      simp only [coe_pointwise_smul, mem_map, MulEquiv.coe_toMonoidHom, MulEquiv.coe_mk,
        Equiv.coe_fn_symm_mk, Subtype.exists, Equiv.coe_fn_mk, Subtype.mk.injEq, exists_and_right,
        exists_and_left, exists_exists_and_eq_and, smul_inv_smul, coeSubtype, SetLike.coe_eq_coe,
        exists_eq_right]
      use x.val
      constructor
      . simp only [Subtype.coe_eta, SetLike.coe_mem, exists_const, hx]
      . simp only [Subtype.coe_eta, exists_prop, and_true]
        refine mem_pointwise_smul_iff_inv_smul_mem.mp ?_
        exact x.2
    . intro hx
      replace hx : x.val ∈ (map (toConjAct g • H).subtype (map myconjEquiv.toMonoidHom (map myconjEquiv.symm.toMonoidHom P₀))) := by
        exact hx
      simp only [pointwise_smul_toSubmonoid, map_inv, MulEquiv.symm_mk, mem_map,
        MulEquiv.coe_toMonoidHom, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk, Subtype.exists,
        Equiv.coe_fn_mk, Subtype.mk.injEq, exists_and_right, exists_and_left,
        exists_exists_and_eq_and, smul_inv_smul, coeSubtype, coe_pointwise_smul, SetLike.coe_eq_coe, exists_eq_right, myconjEquiv] at hx
      rcases hx with ⟨a, ⟨⟨ha11, ha12⟩, ⟨ha21, ha22⟩⟩⟩
      rw [ha22] at ha12
      exact ha12
end Exercise_1192
end Exercise_1192

[Thomas Browning]

Here's a way that uses isomorphisms.

import Mathlib.GroupTheory.Sylow

section Iso

variable {G G' : Type*} [Group G] [Group G']
variable {p : ℕ} [Fact p.Prime]
variable (ϕ : G ≃* G')

noncomputable def Sylow.congr : Sylow p G ≃ Sylow p G' :=
  (Equiv.ofBijective (fun P ↦ P.comapOfInjective ϕ ϕ.injective
    (le_top.trans_eq (MonoidHom.range_top_of_surjective ϕ ϕ.surjective).symm))
    ⟨fun _ _ h ↦ Sylow.ext (Subgroup.comap_injective ϕ.surjective (Sylow.ext_iff.mp h)),
    fun P ↦ let ⟨Q, h⟩ := P.exists_comap_eq_of_injective ϕ.injective; ⟨Q, Sylow.ext h⟩⟩).symm

end Iso

section Exercise_1192
namespace Exercise_1192

open Subgroup CommGroup MulAut ConjAct Pointwise

variable {G : Type*} [Group G]
variable (p : ℕ) [Fact p.Prime]
variable (H : Subgroup G) (P : Sylow p H)

noncomputable def myconjSylow (g : G) :
  let H' := (toConjAct g) • (H : Subgroup G)
  Sylow p H' := by
  let ϕ : H ≃* ((toConjAct g) • (H : Subgroup G) : Subgroup G) := H.equivSMul (toConjAct g)
  exact Sylow.congr ϕ P

end Exercise_1192
end Exercise_1192

[Thomas Browning]

You could probably make it computable if you manually showed that map preserves Sylow subgroups.

[张守信(Shouxin Zhang)]

Thomas Browning said:

You could probably make it computable if you manually showed that map preserves Sylow subgroups.

Seeing this code, I feel like a fighter jet swooping in for a low-altitude bombing run, then vanishing into the sky.:speechless:

[张守信(Shouxin Zhang)]

I managed to find a way to simplify the code based on the existing code. My estimation indeed correct.. And then, as expected, I realized I should definitely spend more time learning to use library functions \#_#

section Exercise_1192'
namespace Exercise_1192'
set_option maxHeartbeats 0
open Subgroup CommGroup MulAut ConjAct Pointwise

variable {G : Type*} [Group G]
variable (p : ℕ) [Fact p.Prime]
variable (H : Subgroup G) (P : Sylow p H)

instance Subgroup_subgroup [Group G] {H : Subgroup G} : CoeOut (Subgroup H) (Subgroup G) where
  coe := fun K => Subgroup.map H.subtype K

def myconjSylow (g : G) :
  let H' := (toConjAct g) • (H : Subgroup G)
  Sylow p H' := by
  dsimp
  let P' := (toConjAct g) • (P : Subgroup G)
  apply Sylow.mk
  . have is_p_group_P' : IsPGroup p P' := IsPGroup.map (IsPGroup.map P.2 H.subtype) ((MulDistribMulAction.toMonoidEnd (ConjAct G) G) (toConjAct g))
    exact IsPGroup.comap_subtype is_p_group_P'
  . intro Q hQ₁ hQ₂
    rw [comap_subtype] at hQ₂ ⊢
    ext x
    constructor
    . intro hx
      refine mem_subgroupOf.mpr ?_
      have h : toConjAct g⁻¹ • (Q : Subgroup G) = P.toSubgroup := by
        let z := toConjAct g⁻¹ • (Q : Subgroup G)
        have : IsPGroup p z := by
          simp only [toConjAct_inv, z]
          exact IsPGroup.map (IsPGroup.map hQ₁ (toConjAct g • H).subtype) ((MulDistribMulAction.toMonoidEnd (ConjAct G) G) (toConjAct g)⁻¹)
        have h₂_1 : z.subgroupOf H = P := by
          apply P.3 (IsPGroup.comap_subtype this)
          refine map_subtype_le_map_subtype.mp ?_
          simp only [map_inv, comap_subtype, subgroupOf_map_subtype, le_inf_iff, map_subtype_le (G := G) (H := H) ↑P, and_true]
          have : map (toConjAct g • H).subtype ((toConjAct g • map H.subtype ↑P).subgroupOf (toConjAct g • H)) = toConjAct g • map H.subtype ↑P := by
            simp only [subgroupOf_map_subtype, inf_eq_left, pointwise_smul_le_pointwise_smul_iff]
            exact map_subtype_le (G := G) (H := H) ↑P
          rw [← map_subtype_le_map_subtype, this] at hQ₂
          exact pointwise_smul_subset_iff.mp hQ₂
        simp only [map_inv, ← h₂_1, subgroupOf_map_subtype, left_eq_inf, ge_iff_le, z]
        exact subset_pointwise_smul_iff.mp (map_subtype_le Q)
      simp only [coe_pointwise_smul, P', ← h, map_inv, smul_inv_smul, mem_map, coeSubtype, coe_pointwise_smul, SetLike.coe_eq_coe, exists_eq_right, hx]
    . intro hx
      exact hQ₂ hx

end Exercise_1192'
end Exercise_1192'