Inverse to sylow.card_eq_multiplicity

Stream: new members

[Bernhard Reinke]

Hello, I am trying to show that a subgroup of a finite group is a p-Sylow group if it has the right cardinality, so in some sense an inverse to sylow.card_eq_multiplicity. Here is my current attempt:

import group_theory.sylow

open fintype

variables {G : Type*} [group G]

def card_eq_multiplicity_to_sylow [fintype G] {p : ℕ} [hp : fact (nat.prime p)]
  (H : subgroup G) [fintype H]
  (eq_card: card H = p ^ nat.factorization (card G) p) : sylow p G :=
{
  to_subgroup := H,
  is_p_group' := is_p_group.of_card eq_card,
  is_maximal' := begin
    intros Q is_p_Q hHQ,
    obtain ⟨P, hQP⟩ := is_p_group.exists_le_sylow is_p_Q,
    have hHP : H ≤ ↑P := le_trans hHQ hQP,
    have hHsubP_fintype: fintype ↥(H.subgroup_of ↑P) := begin
      apply fintype.of_equiv H,
      symmetry,
      apply (subgroup.subgroup_of_equiv_of_le hHP).to_equiv,
    end,
    have eq_HP : H.subgroup_of ↑P = ⊤ := begin
      have eq_card_P := sylow.card_eq_multiplicity P,
      resetI,
      apply subgroup.eq_top_of_card_eq, --fails
    end,
    sorry,
  end,
}

My idea is in order to show that H is a maximal p-subgroup is the following: every bigger p-subgroup Q has to be contained in a p-Sylow subgroup P, but H and P have the same cardinality, so they all have to be equal.

I get the following error message

135:7: invalid apply tactic, failed to synthesize type class instance for
  fintype ↥↑P
state:
G : Type u_1,
_inst_1 : group G,
_inst_2 : fintype G,
p : ℕ,
hp : fact (prime p),
H : subgroup G,
_inst_3 : fintype ↥H,
eq_card : card ↥H = p ^ ⇑((card G).factorization) p,
Q : subgroup G,
is_p_Q : is_p_group p ↥Q,
hHQ : H ≤ Q,
P : sylow p G,
hQP : Q ≤ ↑P,
hHP : H ≤ ↑P,
hHsubP_fintype : fintype ↥(H.subgroup_of ↑P),
eq_card_P : card ↥P = p ^ ⇑((card G).factorization) p
⊢ H.subgroup_of ↑P = ⊤

so there seems to be a typeclass coercion problem, but I have no idea how to address it. If this is fixed, would this be an interesting addition to mathlib?

[Kevin Buzzard]

It would be great if you could make your question a #mwe . Right now we're missing imports so the code as it stands doesn't compile in a new lean session. [Edit: thanks Alex for doing this for me ;-) ]

[Alex J. Best]

You need to add tactic#classical so you get

import group_theory.sylow
open fintype

variables {G : Type*} [group G]

def card_eq_multiplicity_to_sylow [fintype G] {p : ℕ} [hp : fact (nat.prime p)]
  (H : subgroup G) [fintype H]
  (eq_card: card H = p ^ nat.factorization (card G) p) : sylow p G :=
{
  to_subgroup := H,
  is_p_group' := is_p_group.of_card eq_card,
  is_maximal' := begin
    intros Q is_p_Q hHQ,
    classical,
    obtain ⟨P, hQP⟩ := is_p_group.exists_le_sylow is_p_Q,
    have hHP : H ≤ ↑P := le_trans hHQ hQP,
    have hHsubP_fintype: fintype ↥(H.subgroup_of ↑P) := begin
      apply fintype.of_equiv H,
      symmetry,
      apply (subgroup.subgroup_of_equiv_of_le hHP).to_equiv,
    end,
    have eq_HP : H.subgroup_of ↑P = ⊤ := begin
      have eq_card_P := sylow.card_eq_multiplicity P,
      resetI,
      apply subgroup.eq_top_of_card_eq, --fails
    end,
    sorry,
  end,
}

to find this I noticed that the goal is trying to show a subgroup is a fintype, and when I search for these things in the docs I found https://leanprover-community.github.io/mathlib_docs/group_theory/subgroup/finite.html#subgroup.fintype. This has a decidable equality argument which is why it doesn't fire, using classical means that you can ignore such arguments (doing classical mathematics).

[Bernhard Reinke]

Thanks a lot!

[Bernhard Reinke]

I am now here (I hope this should be a mwe):

import group_theory.sylow
import tactic

open fintype

variables {G : Type*} [group G]

def card_eq_multiplicity_to_sylow [fintype G] {p : ℕ} [hp : fact (nat.prime p)]
  (H : subgroup G) [fintype H]
  (eq_card: card H = p ^ nat.factorization (card G) p) : sylow p G :=
{
  to_subgroup := H,
  is_p_group' := is_p_group.of_card eq_card,
  is_maximal' := begin
    intros Q is_p_Q hHQ,
    obtain ⟨P, hQP⟩ := is_p_group.exists_le_sylow is_p_Q,
    have hHP : H ≤ ↑P := le_trans hHQ hQP,
    have hHsubP_fintype: fintype ↥(H.subgroup_of ↑P) := begin
      apply fintype.of_equiv H,
      symmetry,
      apply (subgroup.subgroup_of_equiv_of_le hHP).to_equiv,
    end,
    have eq_HP : H.subgroup_of ↑P = ⊤ := begin
      have eq_card_P := sylow.card_eq_multiplicity P,
      classical,
      resetI,
      apply subgroup.eq_top_of_card_eq,
      rw ← of_equiv_card ((subgroup.subgroup_of_equiv_of_le hHP).to_equiv),
      have coe_assoc : ↥↑ P ≃ ↥ P, by sorry,
      rw ← of_equiv_card coe_assoc,
      -- rw eq_card_P, --fails
      -- rw eq_card, --fails
      sorry,
    end,
    rw subgroup.subgroup_of_eq_top at eq_HP,
    apply le_antisymm,
    exact le_trans hQP eq_HP,
    exact hHQ,
  end,
}

I think I am still confused about coercions. I have no idea how to show coe_assoc. Since the rewrites rw eq_card_Pand rw eq_cardfail, I guess ↥P means different things in eq_card_Pand in the goal. How can I find out what I'm casting to?

[Bernhard Reinke]

I found coe_sort_coe_trans which seems to be the lemma for the assertion I called coe_assoc, so I tried the following (again MWE):

import group_theory.sylow
import tactic

open fintype

variables {G : Type*} [group G]

def card_eq_multiplicity_to_sylow [fintype G] {p : ℕ} [hp : fact (nat.prime p)]
  (H : subgroup G) [fintype H]
  (eq_card: card H = p ^ nat.factorization (card G) p) : sylow p G :=
{
  to_subgroup := H,
  is_p_group' := is_p_group.of_card eq_card,
  is_maximal' := begin
    intros Q is_p_Q hHQ,
    obtain ⟨P, hQP⟩ := is_p_group.exists_le_sylow is_p_Q,
    have hHP : H ≤ ↑P := le_trans hHQ hQP,
    have hHsubP_fintype: fintype ↥(H.subgroup_of ↑P) := begin
      apply fintype.of_equiv H,
      symmetry,
      apply (subgroup.subgroup_of_equiv_of_le hHP).to_equiv,
    end,
    have eq_HP : H.subgroup_of ↑P = ⊤ := begin
      have eq_card_P := sylow.card_eq_multiplicity P,
      classical,
      resetI,
      apply subgroup.eq_top_of_card_eq,
      rw ← of_equiv_card ((subgroup.subgroup_of_equiv_of_le hHP).to_equiv),
      have coe_eq : ↥ P = ↥↑ P := coe_sort_coe_trans P,
      apply eq_trans,
      rw eq_card,
      -- rw eq_card_P, --fails
      -- rw eq_card, --fails
      sorry,
    end,
    rw subgroup.subgroup_of_eq_top at eq_HP,
    apply le_antisymm,
    exact le_trans hQP eq_HP,
    exact hHQ,
  end,
}

but I get the following error for my definition of coe_eq:

invalid type ascription, term has type
  @eq ?m_1
    (@coe_sort (@sylow p G _inst_1) ?m_1
       (@coe_sort_trans (@sylow p G _inst_1) ?m_2 ?m_1 (@coe_sort_trans ?m_2 ?m_3 ?m_1 ?m_4 ?m_5)
          (@coe_base_aux (@sylow p G _inst_1) ?m_2 ?m_6))
       P)
    (@coe_sort ?m_2 ?m_1 (@coe_sort_trans ?m_2 ?m_3 ?m_1 ?m_4 ?m_5)
       (@coe (@sylow p G _inst_1) ?m_2
          (@coe_to_lift (@sylow p G _inst_1) ?m_2 (@coe_base (@sylow p G _inst_1) ?m_2 ?m_6))
          P))
but is expected to have type
  @eq (Type u_1)
    (@coe_sort (@sylow p G _inst_1) (Type u_1)
       (@set_like.has_coe_to_sort (@sylow p G _inst_1) G (@sylow.set_like p G _inst_1))
       P)
    (@coe_sort ?m_1 (Type u_1) ?m_2 (@coe (@sylow p G _inst_1) ?m_1 ?m_3 P))

I don't understand the error yet, I will try to add more type information get a better understanding of what happens

[Bernhard Reinke]

I am now also using

set_option pp.implicit true
set_option pp.coercions true

with this I hope I can figure this out myself.

[Bernhard Reinke]

I think I already understood the key issue: I was using fintype.of_equiv_card instead of fintype.card_congr. With this I constructed new fintype instance as I moved along, resulting competing fintype instances on the same types

[Bernhard Reinke]

I managed to finish it :) here is the whole thing (a little bit golfed)

import group_theory.sylow
import tactic

open fintype

variables {G : Type*} [group G]

def card_eq_multiplicity_to_sylow [fintype G] {p : ℕ} [hp : fact (nat.prime p)]
  (H : subgroup G) [fintype H]
  (eq_card: card H = p ^ nat.factorization (card G) p) : sylow p G :=
{
  to_subgroup := H,
  is_p_group' := is_p_group.of_card eq_card,
  is_maximal' := begin
    intros Q is_p_Q hHQ,
    obtain ⟨P, hQP⟩ := is_p_group.exists_le_sylow is_p_Q,
    have eq_HP : H.subgroup_of ↑P = ⊤ := begin
      classical,
      apply subgroup.eq_top_of_card_eq,
      rw card_congr ((subgroup.subgroup_of_equiv_of_le (le_trans hHQ hQP)).to_equiv),
      rw eq_card,
      have coe_eq : ↥(↑ P : subgroup G) = ↥ P  := begin
        rw ← sylow.to_subgroup_eq_coe,
        refl,
      end,
      rw card_congr (equiv.cast coe_eq),
      symmetry,
      exact (sylow.card_eq_multiplicity P),
    end,
    rw subgroup.subgroup_of_eq_top at eq_HP,
    exact le_antisymm (le_trans hQP eq_HP) hHQ,
  end,
}

@[simp]
lemma card_eq_multiplicity_to_sylow_coe [fintype G] {p : ℕ} [hp : fact (nat.prime p)]
  (H : subgroup G) [fintype H]
  (eq_card: card H = p ^ nat.factorization (card G) p) : ↑(card_eq_multiplicity_to_sylow H eq_card) = H := rfl

Does it make sense to polish it and try to open a PR to add it to sylow? What do the current authors of sylow @Chris Hughes @Thomas Browning think?

[Michael Stoll]

Is the [fintype H] assumption really necessary? Mathematically, a subgroup of a finite group has to be finite...

[Yakov Pechersky]

It's not necessary, but it's good to have it -- there might be several ways one forms a [fintype H], one of which is the subgroup.fintype or whatever, or by some other method.

[Yakov Pechersky]

And including [fintype H] in the arguments is more general -- it means "it doesn't matter which fintype instance one uses for this proof", unlike if you didn't include it, which would mean "this proof _might_ only work if one uses the fintype instance that relies on the fintype G". That's my understanding at least

[Thomas Browning]

@Bernhard Reinke Yes, this converse seems like a great addition to sylow.lean. Here's a golf, with a helpful lemma extracted:

-- can weaken h2
lemma lem {H K : subgroup G} [fintype H] [fintype K] (h1 : K ≤ H) (h2 : card H = card K) :
  H = K :=
begin
  refine le_antisymm (relindex_eq_one.mp _) h1,
  rwa [←mul_right_inj', mul_one, relindex_mul_relindex ⊥ K H bot_le h1,
    relindex_bot_left_eq_card, relindex_bot_left_eq_card],
  exact index_ne_zero_of_finite,
end

def card_eq_multiplicity_to_sylow [fintype G] {p : ℕ} [hp : fact p.prime]
  (H : subgroup G) [fintype H]
  (card_eq: card H = p ^ (card G).factorization p) : sylow p G :=
{ to_subgroup := H,
  is_p_group' := is_p_group.of_card card_eq,
  is_maximal' := begin
    obtain ⟨P, hHP⟩ := (is_p_group.of_card card_eq).exists_le_sylow,
    exact (lem hHP (P.card_eq_multiplicity.trans card_eq.symm)) ▸ λ _, P.3,
  end }

[Bernhard Reinke]

I tried to generalize your lemma, it seems it is possible to reduce it to set.eq_of_subset_of_card_le. Here is my adjustment of your golf:

import data.set.finite
import data.set_like.basic

import group_theory.subgroup.basic
import group_theory.sylow

theorem set_like.eq_of_subset_of_card_le {A : Type*} {B : Type*}
[i : set_like A B] {s t : A} [fintype ↥s] [fintype ↥t]
(hsub : s ≤ t) (hcard : fintype.card ↥t ≤ fintype.card ↥s) : s = t :=
begin
  rw ← set_like.coe_set_eq,
  apply set.eq_of_subset_of_card_le hsub hcard,
end

open fintype


variables {G : Type*} [group G]

def card_eq_multiplicity_to_sylow [fintype G] {p : ℕ} [hp : fact p.prime]
  (H : subgroup G) [fintype H]
  (card_eq: card H = p ^ (card G).factorization p) : sylow p G :=
{ to_subgroup := H,
  is_p_group' := is_p_group.of_card card_eq,
  is_maximal' := begin
    classical,
    obtain ⟨P, hHP⟩ := (is_p_group.of_card card_eq).exists_le_sylow,
    exact (set_like.eq_of_subset_of_card_le hHP (P.card_eq_multiplicity.trans card_eq.symm).le).symm ▸ λ _, P.3,
  end }

[Bernhard Reinke]

Does it make sense to also add the first lemma to mathlib? What would be good place for it? data.set_like.fintype?

[Bernhard Reinke]

Also, I had to include classical in my proof again, is there a reason why you could omit it?

[Parivash]

(deleted)

[Kevin Buzzard]

This is not true (for x=1). What are the types of your objects? (the reals, complexes? An arbitrary ring?) You are also writing a question in someone else's thread (this is a thread about Sylow subgroups). Can you move your question to a new thread and if possible write it as a #mwe with Lean code rather than in LaTeX? Questions written in fully compiling Lean are much easier to answer definitively.

[Thomas Browning]

Bernhard Reinke said:

Does it make sense to also add the first lemma to mathlib? What would be good place for it? data.set_like.fintype?

Yeah, that seems like a good idea. Also, you should be able to get rid of the arrows and golf:

theorem set_like.eq_of_subset_of_card_le {A B : Type*} [i : set_like A B] {s t : A}
  [fintype s] [fintype t] (hsub : s ≤ t) (hcard : fintype.card t ≤ fintype.card s) :
  s = t :=
set_like.ext' (set.eq_of_subset_of_card_le hsub hcard)

[Thomas Browning]

Bernhard Reinke said:

Also, I had to include classical in my proof again, is there a reason why you could omit it?

Not sure. Perhaps it was because I was writing my proof inside sylow.lean (since that is where it would go eventually)?

[Junyan Xu]

Either you have open_locale classical in that file or it's this leakage problem.