The alternating group is simple!

Stream: maths

[Antoine Chambert-Loir]

Finally, Lean know that the alternating group (in 5 letters or more) is simple !
This will be my Christmas gift to y'all!

The proof is contained in the branch named an-very-simple, (https://github.com/leanprover-community/mathlib/tree/an-very-simple). It is basically the proof contained in James Milne's booklet Group theory (4.34-4.36), with some simplifications explained in a blog post on Freedom Math Dance.

Presumably, a lot of simplifications and golfing will be possible.

I have 5 files :

• an-very-simple.lean: the main proof
• basic_lemma.lean: an auxiliary lemma that selects some cycle types of permutations satisfying relevant properties. This is done in an ad hoc manner, and I expect that tactic reasoning could provide an automatic enumeration/selection process.
• ad_sub_mul_actions.lean: some definitions of mul_action on various other structures (set, finset, list)
• multiset_pigeonhole.lean: some basic inequalities on multisets which are used in the basic_lemma.
• pairs.lean: essentially useless API to work on pairs, was used at some point, and could probably be deleted.

[Antoine Chambert-Loir]

Thanks to all of you who helped me in this adventure. Especially to @Yaël Dillies!

[Antoine Chambert-Loir]

(I will now go prepare the Christmas dinner and won't probably work until next monday.)

[Yaël Dillies]

Congratulations! We've already talked about it in private, but I think mathlib could have strict_sym a version of sym for finsets. It comes up here, and many other places. For example, the n-th braid group is the fundamental group of strict_sym ℂ n.

[Antoine Chambert-Loir]

This remark makes me wish that Lean had HOTT, then one could prove something like this at the type level!

[Kevin Buzzard]

Yeah but then would we be able to prove all the other stuff or would a change in the definition of equality break everything or make it much much harder to write code? Nobody knows

[Eric Rodriguez]

non-serious: https://github.com/gebner/hott3 ;b

[Eric Rodriguez]

it is incompatible with the type theory of lean in a way that seems minor, as well

[Eric Rodriguez]

(but is not as it can prove false)

[Adam Topaz]

I'm not sure I understand @Yaël Dillies what is strict_sym supposed to do?

[Riccardo Brasca]

Félicitations Antoine !

[Yaël Dillies]

sym α n is {s : multiset α // s.card = n}. strict_sym α n would be {s : finset α // s.card = n}

[Adam Topaz]

Ok I see... But to get the topology on this you would still want to represent the configuration space as a quotient of the product minus the pairwise diagonals.

[Yaël Dillies]

But this type is neat and simple, so I was thinking that instead we could get its topology from lifting rather than quotienting.

[Adam Topaz]

The space of ordered n-tuples on a space also shows up in math, and the relation between these two is pretty important.

[Adam Topaz]

E.g. $\mathcal{M}_{0,n+3}$ :wink:

[Yaël Dillies]

Ordered tuples are just a pi type, though?

[Adam Topaz]

import topology.constructions

variables (X : Type*) [topological_space X] (α : Type*) [fintype α]

@[derive topological_space]
def foo := {f : α → X // function.injective f}

def bar_setoid : setoid (foo X α) :=
{ r := λ f g, ∃ σ : α ≃ α, f.1 = g.1 ∘ ⇑σ,
  iseqv := sorry }

@[derive topological_space]
def bar := quotient (bar_setoid X α)

[Adam Topaz]

now go compute $\pi_1(bar)$ ;)

[Yaël Dillies]

Well, I just summon Shing!

[Adam Topaz]

Yaël Dillies said:

Ordered tuples are just a pi type, though?

I should have said ordered $n$-tuples of distinct points.

[Yakov Pechersky]

Subtype of pi types such that it is injective?

[Adam Topaz]

@Yakov Pechersky see code above

[Eric Rodriguez]

btw foo is embedding :)

[David Wärn]

Plain HoTT is actually not enough to talk about the fundamental group of this space (strict_sym will just be an hSet). You would need to add some real-cohesion axioms (and take the "shape" of strict_sym)

[Kevin Buzzard]

wait what really? Does "add some...axioms" really mean add new axioms to the system?

[Kevin Buzzard]

You could make a topological space and look at continuous maps from the topological [0,1] in and make it that way, right? You just wouldn't be able to use synthetic pi_1?

[Antoine Chambert-Loir]

Well, the homotopy groups of strict_sym C n and strict_sym R ndiffer, so certainly some assumption has to be added to understand what is meant. But I had the idea of the type of a sphere in mind. Probably strict_sym (S^k) n could be studied by plain HoTT.

[David Wärn]

It's not that simple. If you use the higher-inductive type $S_k$, then you can't say what it means for a configuration $[n] \to S_k$ to consist of distinct points, since this isn't a homotopy-invariant notion. On the other hand if you use the 'topological' sphere $\mathbb S_k \coloneqq \{ v \in \mathbb R^{k+1} \mid \lVert v \rVert = 1 \}$, then you won't be able to reason synthetically about fundamental groups, since $\mathbb S_k$ is an hSet (equality in $\mathbb S_k$ is just the usual, non-homotopical equality). You can still reason analytically as in Lean of course. Or you can use real-cohesive HoTT, which adds some axioms to the theory so that you can relate $\mathbb S_k$ and $S_k$ and reason synthetically about this fundamental group.

[Patrick Massot]

@Antoine Chambert-Loir : https://github.com/leanprover-community/mathlib/commit/ec538300461b62a5c386257009848292f3b55d83

[Patrick Massot]

I've written a principled proof of the main lemma, including a block in the middle that should be put in a tactic. There is a mystery in this block, clear refusing to do its job in a all_goals { try {clear H } } whereas it works if you do it by hand. The block is also a bit stupid because it enumerates possible multisets without taking into account the permutation action. In the case at had, we have a multiset of natural number with cardinal at most 2 and each element is between 2 and 5. With the naive algorithm implemented here, it generates 4^0 + 4^1 + 4^2 = 21 cases.

import tactic
import data.multiset.basic

lemma all_cycle_types_le_5 {m : multiset ℕ} (hm : ∀ {n : ℕ}, n ∈ m → 2 ≤ n)
  (hs : m.sum ≤ 5) (hm0 : m ≠ 0) :
  m = {5} ∨ m = {4} ∨ m = {3} ∨ m = {2} ∨ m = {3,2} ∨ m = {2,2} :=
begin
  have hcard : m.card ≤ 2,
  { by_contra h,
    push_neg at h,
    replace h : 3 ≤ m.card := nat.succ_le_iff.mpr h,
    have : m.card * 2 ≤ 5 := (multiset.card_nsmul_le_sum (λ n, hm)).trans hs,
    linarith  },
  have hm' : ∀ n ∈ m, n ≤ 5 := λ n hn, (multiset.le_sum_of_mem hn).trans hs,

  /- BEGIN should be put in a tactic with input m, hcard, hm, hm' -/
  induction m using multiset.induction with a₁ m H,
  work_on_goal 1 {
    have hm₁ : 2 ≤ a₁ := by simp only [hm, multiset.mem_cons, true_or, eq_self_iff_true, or_true],
    have hm₁' : a₁ ≤ 5 := by simp only [hm', multiset.mem_cons, true_or, eq_self_iff_true, or_true],
    induction m using multiset.induction with a₂ m H,
    work_on_goal 1 {
      have hm₂ : 2 ≤ a₂ := by simp only [hm, multiset.mem_cons, true_or, eq_self_iff_true, or_true],
      have hm₂' : a₂ ≤ 5 := by simp only [hm', multiset.mem_cons, true_or, eq_self_iff_true, or_true],
      obtain rfl : m = 0,
      { simp at hcard,
        change m.card + 2 ≤ 2 at hcard,
        exact multiset.card_eq_zero.mp (nat.le_zero_iff.mp $ add_le_iff_nonpos_left.mp hcard) } } },
  all_goals { clear hcard },

  all_goals { try {interval_cases a₁} },
  all_goals { try {interval_cases a₂} },
  all_goals { clear hm hm', try { clear hm₁ hm₁' }, try { clear hm₂ hm₂' } },
  all_goals { try {clear H} }, -- This line doesn't work, no idea why
  /- END should be put in a tactic -/

  all_goals { norm_num at hs ; dec_trivial },
end

[Patrick Massot]

Tactic writers should feel free to take the code above and turn it into something useful. Note this is a completely self-contained snippet, it includes no group theory at all. @Rob Lewis @Mario Carneiro @Gabriel Ebner