## Stream: new members

### Topic: Inverse to sylow.card_eq_multiplicity

#### Bernhard Reinke (Jan 23 2023 at 09:45):

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 (Jan 23 2023 at 09:58):

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 (Jan 23 2023 at 09:58):

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).

Thanks a lot!

#### Bernhard Reinke (Jan 23 2023 at 12:12):

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 (Jan 23 2023 at 14:46):

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 (Jan 23 2023 at 15:29):

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 (Jan 23 2023 at 15:46):

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 (Jan 23 2023 at 16:22):

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 (Jan 23 2023 at 16:24):

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

#### Yakov Pechersky (Jan 23 2023 at 16:28):

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 (Jan 23 2023 at 16:29):

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 (Jan 23 2023 at 19:20):

@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 (Jan 24 2023 at 14:10):

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 (Jan 24 2023 at 14:13):

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 (Jan 24 2023 at 14:16):

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

(deleted)

#### Kevin Buzzard (Jan 24 2023 at 16:19):

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 (Jan 24 2023 at 18:58):

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 (Jan 24 2023 at 19:01):

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 (Jan 24 2023 at 19:08):

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

Last updated: Dec 20 2023 at 11:08 UTC