Finite type, finite set, lack of an instance

Stream: new members

[Nick_adfor]

I was trying to write code to construct A_4 with tetrahedron. I cannot give a mwe as it is all connected. The whole code is at the end.

But I have notice that Fintype.card ↥G and Fintype.card G are all wrong.

failed to synthesize
  Fintype ↥G
Additional diagnostic information may be available using the `set_option diagnostics true` command.

ChatGPT tells me that I have defined G as a Subgroup, not a Finset, so I need an instance (I don't know why.) It also try to fix it like this

lemma G_finite : Set.Finite (↑G : Set (Perm (Fin 4))) :=
  Set.Finite.subset (fintype.isFinite _) G_subgroup_A4

noncomputable instance fintypeG : Fintype ↥G :=
  Fintype.ofFiniteSubtype G

But it cannot work on lean. ChatGPT often tell me something wrong, even some lean3 code, although I've told it I was writing lean4. And also, just copy the wrong messages from Lean Infoview cannot be of any help, as the wrong messages in Lean Infoview is often of no help (The only help is to tell me that the code has something wrong. As for what thing wrong, it never helps.)

Even from the line 12 = generators ≤ card G (G is defined as closure of generators) ≤ card A₄ = 12 and generators in A₄ to prove G=A₄ is easy for maths, but hard for lean.

import Mathlib

open Equiv Perm

def IsDoubleTransposition (σ : Perm (Fin 4)) : Prop :=
  ∃ (a b c d : Fin 4), a ≠ b ∧ c ≠ d ∧
  Disjoint (support (swap a b)) (support (swap c d)) ∧
  σ = swap a b * swap c d

def doubleTranspositions : List (Perm (Fin 4)) :=
  [swap 0 1 * swap 2 3,
   swap 0 2 * swap 1 3,
   swap 0 3 * swap 1 2]

lemma mem_doubleTranspositions_iff {σ : Perm (Fin 4)} :
  σ ∈ doubleTranspositions ↔ IsDoubleTransposition σ := by
  revert σ
  simp only [doubleTranspositions, IsDoubleTransposition]
  decide

lemma doubleTranspositions_mem_A4 :
    ∀ σ ∈ doubleTranspositions, σ ∈ alternatingGroup (Fin 4) := by
  simp only [Equiv.Perm.mem_alternatingGroup, Equiv.Perm.sign_mul, Equiv.Perm.IsSwap.sign_eq]
  decide

def ThreeCycles : List (Perm (Fin 4)) :=
  [swap 0 1 * swap 0 2,  -- (0 1 2)
   swap 0 2 * swap 0 1,  -- (0 2 1)
   swap 0 1 * swap 0 3,  -- (0 1 3)
   swap 0 3 * swap 0 1,  -- (0 3 1)
   swap 0 2 * swap 0 3,  -- (0 2 3)
   swap 0 3 * swap 0 2,  -- (0 3 2)
   swap 1 2 * swap 1 3,  -- (1 2 3)
   swap 1 3 * swap 1 2]  -- (1 3 2)
--lean does not have a good way to deFine a list of all 3-cycles, so I use swap products.

lemma mem_allThreeCycles_iff {σ : Perm (Fin 4)} :
    σ ∈ ThreeCycles ↔ σ.IsThreeCycle := by
  revert σ
  simp only [ThreeCycles, ← card_support_eq_three_iff]
  decide

lemma ThreeCycles_mem_A4 :
    ∀ σ ∈ ThreeCycles, σ ∈ alternatingGroup (Fin 4) := by
  simp only [Equiv.Perm.mem_alternatingGroup, Equiv.Perm.sign_mul, Equiv.Perm.IsSwap.sign_eq]
  decide

lemma one_mem_A4 : (1 : Perm (Fin 4)) ∈ alternatingGroup (Fin 4) := by
  simp only [Equiv.Perm.mem_alternatingGroup, Perm.sign_one]

def generators : List (Perm (Fin 4)) :=
  (1 : Perm (Fin 4)) :: (ThreeCycles ++ doubleTranspositions)

lemma generators_subset_A4 : ∀ σ ∈ generators, σ ∈ alternatingGroup (Fin 4) := by
  intros σ hσ
  simp only [generators] at hσ
  cases hσ
  · -- σ = 1
    exact one_mem_A4
  · -- σ ∈ ThreeCycles ++ doubleTranspositions
    rename_i h
    change σ ∈ ThreeCycles ++ doubleTranspositions at h
    simp only [List.mem_append] at h
    cases h
    · rename_i h'
      exact ThreeCycles_mem_A4 σ h'
    · rename_i h'
      exact doubleTranspositions_mem_A4 σ h'

def G : Subgroup (Perm (Fin 4)) := Subgroup.closure generators.toFinset

lemma G_subgroup_A4 : G ≤ alternatingGroup (Fin 4) := by
  dsimp [G]
  rw [Subgroup.closure_le]
  intros σ hσ
  have h_mem := List.mem_toFinset.mp hσ
  exact generators_subset_A4 σ h_mem

lemma card_A4 : Fintype.card (alternatingGroup (Fin 4)) = 12 := by
  have h1 := @Fintype.card_perm (Fin 4) _ _
  have h2 := @two_mul_card_alternatingGroup (Fin 4) _ _ _
  rw [h1] at h2
  norm_num at h2
  exact (Nat.eq_of_mul_eq_mul_left zero_lt_two h2).symm

def set_of_generators := generators.toFinset

lemma generators_card : Finset.card set_of_generators = 12 := by
  decide

lemma G_finite : Set.Finite (↑G : Set (Perm (Fin 4))) :=
    Set.Finite.subset (Fintype.finite (alternatingGroup (Fin 4))) G_subgroup_A4

noncomputable instance fintypeG : Fintype ↥G :=
    Set.Finite.fintype G_finite

theorem G_eq_A4 : G = alternatingGroup (Fin 4) := by
  -- Step 1: Show that the generators are all contained in G by construction
  -- Since G is defined as the subgroup generated by `generators`, every element of `generators` lies in G
  have gens_subset_G : set_of_generators.toSet ⊆ ↑G := Subgroup.subset_closure

  -- Step 2: Therefore, the cardinality of the generators set is less than or equal to the cardinality of G
  have h1 : Finset.card set_of_generators ≤ Fintype.card ↥G := by
    -- Use Nat.card_eq_fintype_card to rewrite the RHS
    rw [← Nat.card_eq_fintype_card]
    -- Convert generators.toFinset into a subtype of itself
    exact Nat.card_le_of_subset gens_subset_G



  -- Step 3: From the lemma `G_subgroup_A4`, we know G is a subgroup of A₄, so card G ≤ card A₄

  have h2 : Fintype.card G ≤ Fintype.card (alternatingGroup (Fin 4)) :=
    Fintype.card_le_of_injective
      (fun x : ↥G => ⟨(x : Perm (Fin 4)), G_subgroup_A4 x.2⟩) -- embedding G into A₄
      (by
        intros x y h
        cases x; cases y
        simp only at h
        congr -- since underlying values are equal, subtypes are equal
      )

  -- Step 4: From earlier lemmas we know that A₄ has cardinality 12 and so does the generator set
  have hA4 : Fintype.card (alternatingGroup (Fin 4)) = 12 := card_A4
  have hGens : Finset.card set_of_generators = 12 := generators_card

  -- So combining the three inequalities: 12 = generators_card ≤ card G ≤ card A₄ = 12
  -- Therefore, all the inequalities must be equalities, so card G = 12 = card A₄
  have h_card_eq : Fintype.card G = 12 := by
    apply Nat.le_antisymm
    · exact h2.trans_eq hA4
    · rw [←hGens]
      exact h1

  -- Step 5: Since G ⊆ A₄ and they have the same cardinality, we conclude G = A₄
  exact?

[Jz Pan]

Nick_adfor said:

But I have notice that Fintype.card ↥G and Fintype.card G are all wrong.

failed to synthesize
  Fintype ↥G
Additional diagnostic information may be available using the `set_option diagnostics true` co

Looks like you need DecidablePred or something on G. To make G a Fintype, you need to know how to determine whether an element is contained in G, i.e. it must be decidable. That's what Fintype means. Otherwise I think you should use Finite and Nat.card instead of Fintype and Fintype.card.

BTW, my personal suggestions:

1. before writing anything Lean, try to plan you proof in pen and paper.
2. Don't rely on CharGPT. Lean and think by yourself by trial and error, asking questions here, and reading manuals. And it's important to take notes by yourself.

[Nick_adfor]

Thanks for your help! In fact the plan of my proof is in the note of the theorem, maybe my lean code doesn't realize it well, and when I have no way to fix it, I try to seek help from ChatGPT, but surely it will give me some code in lean3 or some wrong theorems (these wrong theorems are not in mathlib)

I am reading Finite now to try to organize my proof in the last theorem, very thanks!

  -- Step 1: Show that the generators are all contained in G by construction
  -- Since G is defined as the subgroup generated by `generators`, every element of `generators` lies in G

  -- Step 2: Therefore, the cardinality of the generators set is less than or equal to the cardinality of G

  -- Step 3: From the lemma `G_subgroup_A4`, we know G is a subgroup of A₄, so card G ≤ card A₄

  -- Step 4: From earlier lemmas we know that A₄ has cardinality 12 and so does the generator set

  -- So combining the three inequalities: 12 = generators_card ≤ card G ≤ card A₄ = 12

  -- Step 5: Since G ⊆ A₄ and they have the same cardinality, we conclude G = A₄

[Jz Pan]

My suggestion is try to simplify your pen and paper proof. You uses 12 generators which obviously too many. Do you do some background research before writing your proof? A simple search on Internet reveals that $A_n$ could have much fewer generators:

https://math.stackexchange.com/questions/1358030/set-of-generators-for-a-n-the-alternating-group

https://math.stackexchange.com/questions/3478685/the-alternating-group-a-n-is-generated-by-langle1-2-dots-n-123-rangle

So in your question, (123) and (124) suffices. I don't know if these two results are in mathlib, but they are mathematically correct, and are much more interesting than your original question.

[Nick_adfor]

Jz Pan said:

Looks like you need DecidablePred or something on G. To make G a Fintype, you need to know how to determine whether an element is contained in G, i.e. it must be decidable. That's what Fintype means. Otherwise I think you should use Finite and Nat.card instead of Fintype and Fintype.card.

Using exact? the noncomputable instance is corrected as follows:

noncomputable instance fintypeG : Fintype ↥G := by
  exact Fintype.ofFinite ↥G

[Nick_adfor]

If write lemma G_finite not automatically (by exact in noncomputable instance), it should be like this:

  lemma G_finite : Set.Finite (G : Set (Perm (Fin 4))) := by
    exact Set.toFinite (G : Set (Perm (Fin 4)))

  noncomputable instance fintypeG : Fintype ↥G :=
    Set.Finite.fintype G_finite

The origin one isSet.Finite.subset (Fintype.finite (alternatingGroup (Fin 4))), but Set.Finite.subset may need somthing like Fintype a rather than alternatingGroup (Fin 4)

[Nick_adfor]

I'm not so familiar with Finite type or Set, so maybe an automatical method is fine. But later I may need to read the origin code in Mathlib.

[Nick_adfor]

Jz Pan said:

So in your question, (123) and (124) suffices. I don't know if these two results are in mathlib, but they are mathematically correct, and are much more interesting than your original question.

It is that I try to give my generators a geometry meaning on the regular tetrahedron. But it is obvious that the geometry meaning makes the whole proof terrible.