Klein's Vierergruppe, and conjugacy classes

Stream: maths

[Antoine Chambert-Loir]

Let α be a fintype with four elements. Klein's Vierergruppe is the subgroup of equiv.perm α consisting of the identity and of the 3 double transpositions, those permutations of cycle type (2,2). When I wished to tell that to Lean, I didn't know how to do it in the same way that we do in class, namely “one check!”, so I invented a more complicated proof, see below. Everything is finite, this should be a mere computation that could be automated.
So my challenge here is that somebody fills the following sorry in a simple way:

variables (α : Type*) [decidable_eq α] [fintype α]

def V4  : subgroup (alternating_group α) :=
  subgroup.closure { g : alternating_group α | (g : equiv.perm α).cycle_type = {2,2} }

lemma V4_carrier (hα4 : fintype.card α = 4) : (V4 α).carrier = {g : alternating_group α | (g : equiv.perm α).cycle_type = 0 ∨ (g : equiv.perm α).cycle_type = {2, 2} } := sorry

My proof followed a different logic. I proved successively that (I change here the proof to sorry, to make the code shorter — see https://github.com/leanprover-community/mathlib/blob/b040b0da501d47615382a16319754c52cf9527b0/acl-sandbox/group_theory/jordan/V4.lean) :

lemma mem_V4_of_order_two_pow (hα4 : fintype.card α = 4)
  (g : equiv.perm α) (hg0 : g ∈ alternating_group α) (n : ℕ) (hg : order_of g ∣ 2 ^ n) :
  g.cycle_type = {} ∨ g.cycle_type = {2,2} := sorry

lemma A4_sylow_carrier (hα4 : fintype.card α = 4) (S : sylow 2 (alternating_group α)) :
  S.carrier = {g : alternating_group α | (g : equiv.perm α).cycle_type = 0 ∨ (g : equiv.perm α).cycle_type = {2, 2} } := sorry

lemma V4_is_unique_sylow (hα4 : fintype.card α = 4) (S : sylow 2 (alternating_group α)) :
  V4 α = S := sorry

Moreover, the proof that the carrier of Sylow subgroup is what I write (A4_sylow_carrier) requires to know that there are exactly three double transpositions. For this, I formalized the whole computation of the cardinality classes in the symmetric and alternating groups, see https://github.com/leanprover-community/mathlib/blob/b040b0da501d47615382a16319754c52cf9527b0/acl-sandbox/group_theory/jordan/conj_class_count.lean

/-- Cardinality of a conjugacy class in `equiv.perm α` of a given `cycle_type` -/
theorem equiv.perm.conj_class_card (g : equiv.perm α) (m : multiset ℕ)
  (hg : g.cycle_type = m) :
  fintype.card ({ h : equiv.perm α | is_conj g h}) =
    (fintype.card α).factorial
    / ((fintype.card α - m.sum).factorial
      * m.prod
      * (m.dedup.map (λ (n : ℕ), (m.count n).factorial)).prod) := sorry

I believe this is of independent interest, but the way I did it was not easy neither.

At the end, I actually like this whole proof, but as I said above, an immediate computational proof would have been nice too.

[Johan Commelin]

I assume cycle_type is computable?

[Johan Commelin]

Is membership of subgroup.closure decidable?

[Johan Commelin]

Could you write something like

def V4  : subgroup (alternating_group α) :=
{ carrier := {g : alternating_group α | (g : equiv.perm α).cycle_type = 0 ∨ (g : equiv.perm α).cycle_type = {2, 2} },
  one_mem' := dec_trivial,
  mul_mem' := dec_trivial,
  inv_mem' := dec_trivial, }

[Johan Commelin]

I didn't test this... some decidability instances might be missing. But I feel like this way is slightly closer to "what we do in class". Because we don't actually use subgroup.closure

[Antoine Chambert-Loir]

This would definitely be "what we do in class", but I get the following error message

exact tactic failed, type mismatch, given expression has type
  true
but is expected to have type
  as_true
    (∀ {x : ↥(alternating_group α)},
       x ∈ {g : ↥(alternating_group α) | ↑g.cycle_type = 0 ∨ ↑g.cycle_type = {2, 2}} →
       x⁻¹ ∈ {g : ↥(alternating_group α) | ↑g.cycle_type = 0 ∨ ↑g.cycle_type = {2, 2}})

The subgroup.closure was a trick suggested by @Floris van Doorn to obtain a subgroup before I even prove that it is the correct one.

[Johan Commelin]

Yes, it is a good trick. But I'm not sure it meshes well with "finite computation".

[Johan Commelin]

So the dec_trivial works fine for one_mem and mul_mem?

[Antoine Chambert-Loir]

No it fails as well, with a similar error message.

[Johan Commelin]

Aah, too bad.

[Antoine Chambert-Loir]

Your suggestion is something I wouldn't even know how to start.

[Johan Commelin]

Ooh, wait. I just realized that Lean doesn't know that α has 4 elements.

[Johan Commelin]

So it has no chance of knowing how finite the computation is.

[Antoine Chambert-Loir]

(I had told it so!)

[Johan Commelin]

Hmmm, I'm not enough of a computation-guy to know how to make this work smoothly.

[Antoine Chambert-Loir]

On the other hand, I just tried the following, and it indicates that Lean does not really understand that this V4 is finite.

variables (α : Type*) [decidable_eq α] [fintype α] (hα4 : fintype.card α = 4)

include hα4

def V4 := { g : alternating_group α | (g : equiv.perm α).cycle_type = 0 ∨ (g : equiv.perm α).cycle_type = {2, 2} }

#check fintype (V4 α hα4)

example : fintype (V4 α hα4) := fintype.of_finite ↥(V4 α hα4)

requiring a noncomputable (and library_searchdoes not find any other way of proving finiteness…)

[Yakov Pechersky]

You can think of dec_trivial as a "brute force" tactic. In this context, the brute force would have to realize you have a hypothesis that you only have 4 possible alpha, then try all 4^3 multiplication definitions, keep only the ones that satisfy the axioms of a group, then make sure the set you have satisfies the properties you asserted about it.

[Jireh Loreaux]

There's docs#set_fintype, which should be what you want, but you need the membership predicate to be decidable.

[Yakov Pechersky]

Johan's definition won't work with dec_trivial because it can't conjure up elements of an arbitrary alpha type.

[Yakov Pechersky]

fintype is more than just the assertion that a type is finite, it's a witness carrying all the elements of the type and no more. So even though I can come up with a lem provable finite set {0,1} if RH else {0}, I can't construct the fintype instance for this set computably because I can't prove that my witness enumerated all the possible elements and no more than that.

[Johan Commelin]

@Yakov Pechersky but that doesn't apply in this case right? Because we don't have RH here: everything is decidable.

[Yakov Pechersky]

fintype (V4 alpha ha4) isn't smart enough to know exactly which of the 4 alpha satisfy V4

[Yakov Pechersky]

Or, at least, fintype.of_finite isn't by default iiuc

[Johan Commelin]

Hmm, so the fintype instance for alternating_group is not good enough?

[Johan Commelin]

I agree that fintype.of_finite is bad in this context.

[Yakov Pechersky]

One can try fintype by filtering the finset.univ by "mem V4"

[Yakov Pechersky]

The mwe for this would be, imo, does there exist a binop on fin 4, such that exists an "identity" for that binop

[Yakov Pechersky]

Where the proof is "by brute force". If we can't do that, then we can't say much about an arbitrary alpha with an arbitrary mul just knowing that alpha is dec_eq

[Reid Barton]

Yeah the dec_trivial proof can only work for a concrete type (and instances)

[Yakov Pechersky]

Here's what I meant about my MWE:

import group_theory.specific_groups.alternating
import group_theory.perm.cycle.concrete

set_option profiler true

example : ∃ (op : fin 4 → fin 4 → fin 4), ∃ e : fin 4, ∀ i : fin 4, op e i = i :=
begin
  dec_trivial
end
-- 560 ms

example : ∃ (op : fin 4 → fin 4 → fin 4), ∃ e : fin 4, ∀ i : fin 4, op i e = i :=
begin
  dec_trivial
end
-- deterministic time out

[Yakov Pechersky]

Restricting it to an (op : fin 4 → fin 4 ≃ fin 4) speeds up the first example to 156 ms, but the second still times out

[Reid Barton]

I'm not sure what this has to do with the original question though--alternating_group (fin 4) is a known group and it should be within reason (depending on the details of implementation) to check that the elements of certain cycle types are closed under multiplication

[Yakov Pechersky]

I meant the mwe to imply something like this for an "arbitrary" type:

import group_theory.specific_groups.alternating
import group_theory.perm.cycle.concrete

set_option profiler true

example {α : Type*} [decidable_eq α] [fintype α] (e4 : α ≃ fin 4) :
  ∃ (op : α → α ≃ α), ∃ e : α, ∀ i : α, op e i = i :=
begin
  obtain ⟨op, e, he⟩ : ∃ (op : fin 4 → fin 4 ≃ fin 4), ∃ e : fin 4, ∀ i : fin 4, op e i = i,
  { dec_trivial },
  refine ⟨λ x, (e4.trans (op (e4 x))).trans e4.symm, e4.symm e, _⟩,
  simp [he],
end