Fintype of subgroup

Stream: new members

[Jiang Jiedong]

Hi everyone!
I was trying to write some abstract algebra exercises into lean4. A first exercise I choose is "Let p, q be distinct primes. Let G be a finite group of order p * q, then G is not a simple group". I met the problem of showing the Fintype { x // x ∈ Q } for some Sylow q subgroup Q.
Here is what I have written with infoview:

import Mathlib.Tactic
import Mathlib.GroupTheory.Sylow

lemma group_order_pq_not_simple' {p : ℕ} {q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (hpq : p < q) {G : Type _} [Group G] [Fintype G] (h : Fintype.card G = p * q) : ¬ IsSimpleGroup G := by
  -- denote a Sylow `q` subgroup by `Q`
  cases' IsPGroup.exists_le_sylow (IsPGroup.of_bot (p := q) (G := G)) with Q triv
  let N := Subgroup.normalizer (Q : Subgroup G)
  -- `Q` has `q` elements so `Q ≠ ⊥`
  have nontriv₁ : (Q : Subgroup G) ≠ ⊥ := by
    by_contra contra
    rw [← Subgroup.card_eq_one] at contra
    have hQ := Sylow.card_eq_multiplicity Q
    rw [h] at hQ
    /-
    p q : ℕ
    hp : Fact (Nat.Prime p)
    hq : Fact (Nat.Prime q)
    hpq : p < q
    G : Type u_1
    inst✝¹ : Group G
    inst✝ : Fintype G
    h : Fintype.card G = p * q
    Q : Sylow q G
    triv : ⊥ ≤ ↑Q
    N : Subgroup G := Subgroup.normalizer ↑Q
    contra : Nat.card { x // x ∈ ↑Q } = 1
    hQ : Fintype.card { x // x ∈ ↑Q } = q ^ ↑(Nat.factorization (p * q)) q
    ⊢ False
    -/

From here, I was trying to use contra and hQ to get 1 = q ^ ↑(Nat.factorization (p * q)) q then a contradiction.

But when I tried to write
rw [← Nat.card_eq_fintype_card] at hQ
to turn Nat.card into Fintype.card, error happens. Lean says
**failed to synthesize instance
Fintype { x // x ∈ ↑Q }**

If I write

    have hQ' := Fintype.ofFinite { x // x ∈ Q }
    rw [← Nat.card_eq_fintype_card] at hQ

Lean still raises error, saying
**synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
hQ'
inferred
Subgroup.instFintypeSubtypeMemSubgroupInstMembershipInstSetLikeSubgroup ↑Q**

What is the correct way to get the Fintype { x // x ∈ ↑Q } or avoid this problem?
Why is there no written instance of Fintype { x // x ∈ H } with H : Subgroup G and Fintype G?
If possible, could you please explain what is happening here and what is the relation between Finite and Fintype here? (Fintype.ofFinite has info Noncomputably get a Fintype instance from a Finite instance. ) Questions about Fintype keep disturbing me.

Thanks in advance!

[Eric Wieser]

But when I tried to use Nat.card_eq_fintype_card to turn Nat.card into Fintype.card, error happens.

Please can you include this in the #mwe? The #mwe should include the thing that causes the problem, not just the code that leads up to it

[Eric Wieser]

(please also add the imports that are needed to run your code)

[Jiang Jiedong]

Eric Wieser said:

(please also add the imports that are needed to run your code)

I'm very sorry. I've add imports so that the code can work after pasting into an empty file. But it's quite hard for me to judge which detail is not necessary. :exhausted:

[Riccardo Brasca]

Don't worry! The idea is that we can just copy/paste your code and see what happens. So "working" is more important than "minimal" (but "small enough" is still important)

[Eric Wieser]

This works:

    classical
    rw [← Nat.card_eq_fintype_card] at hQ

[Eric Wieser]

As G is finite, lean can find Fintype { x // x ∈ ↑Q } by itself by brute force once you tell it the algorithm to check whether each x is in Q (the algorithm is "cheat using the axiom of choice")

[Jiang Jiedong]

Eric Wieser said:

As G is finite, lean can find Fintype { x // x ∈ ↑Q } by itself by brute force once you tell it the algorithm to check whether each x is in Q (the algorithm is "cheat using the axiom of choice")

Thank you very much! May I ask that do you know there is some material to read or learn that can makes me understand classical(and all of the "noncomputable, axiom of choice, decidable, excluded middle") better? For now, classical is very like a magic spell to me. :mage:

[Kevin Buzzard]

If you do not believe in classical axioms then probably there are situations where you can't prove that a subset of a finite set is finite (because constructive finiteness implies you know how many elements it has). If you are doing regular mathematics and are not interested in foundations then this is not a situation you want to be in. So switch on classical and everything is fine. There are now two concepts of eg the size of a finite set but there's a theorem saying they're equal.

[Jiang Jiedong]

Kevin Buzzard said:

If you do not believe in classical axioms then probably there are situations where you can't prove that a subset of a finite set is finite (because constructive finiteness implies you know how many elements it has). If you are doing regular mathematics and are not interested in foundations then this is not a situation you want to be in. So switch on classical and everything is fine. There are now two concepts of eg the size of a finite set but there's a theorem saying they're equal.

Thank you, Kevin! I think due to the same reason as "a subset of a finite set is finite cannot be proved without classical axioms" , one cannot get "a subgroup of a finite group is finite" without classical axioms. So there is no such instance in mathlib. As far as I am concerned, I will just stick to classical.

[Eric Wieser]

one cannot get "a subgroup of a finite group is finite" without classical axioms.

One can get this in some but not all cases; indeed, this result is precisely docs#Subgroup.instFintypeSubtypeMemSubgroupInstMembershipInstSetLikeSubgroup which does not use any classical axioms

[Eric Wieser]

The DecidablePred fun x => x ∈ K argument is the relevant one here; some places where this is true without classical axioms include:

• When K = \bot
• When K is MonoidHom.range f for some f with a finite group as its domain, and where the is some algorithm to detect duplicates in the codomain

Some places where it's not true without classical axioms are:

• When K is defined with a carrier of something like {z : Units Int | x = 1 \or continuum_hypothesis_is_true}
• When K is a subgroup of something like the units of the real numbers, as you cannot decide if two real numbers are equal without these axioms.