feat(GroupTheory/SpecificGroups/Alternating/Simple): simplicity of the alternating groups

[AntoineChambert-Loir]

This is the conclusion of the story of the proof of simplicity of the alternating group using the
Iwasawa criterion.

• Equiv.Perm.iwasawaStructure_two:
  the natural IwasawaStructure of Equiv.Perm α acting on Nat.Combination α 2
  Its commutative subgroups consist of the permutations with support
  in a given element of Nat.Combination α 2.
  They are cyclic of order 2.

• alternatingGroup_of_le_of_normal:
  If α has at least 5 elements, then a nontrivial normal subgroup
  of Equiv.Perm α contains the alternating group.

• alternatingGroup.iwasawaStructure_three:
  the natural IwasawaStructure of alternatingGroup α acting on Nat.Combination α 3

  Its commutative subgroups consist of the permutations with support
  in a given element of Nat.Combination α 2.
  They are cyclic of order 3.

• alternatingGroup.iwasawaStructure_three:
  the natural IwasawaStructure of alternatingGroup α acting on Nat.Combination α 4

  Its commutative subgroups consist of the permutations of
  cycleType (2, 2) with support in a given element of Nat.Combination α 2.
  They have order 4 and exponent 2 (IsKleinFour).

• alternatingGroup.normal_subgroup_eq_bot_or_eq_top:
  If α has at least 5 elements, then a nontrivial normal subgroup of alternatingGroup is ⊤.

• alternatingGroup.isSimpleGroup:
  If α has at least 5 elements, then alternatingGroup α
  is a simple group.

---

• depends on: [Merged by Bors] - feat(GroupTheory/SpecificGroups/Alternating/Simple): the alternating group on at least 5 letters is simple. #33082
• depends on: [Merged by Bors] - chore(GroupTheory/SpecificGroups/Cyclic/Basic): refactor #36983
• depends on: [Merged by Bors] - feat(Data/Nat/Perm): add two lemmas #37026

[AntoineChambert-Loir]

I resolved the issues above to make the page clearer, but there is one problem with t
Equiv.Perm.isCyclic_of_card_le_two and Equiv.Perm.isMulCommutative_of_card_le_two for which I can't find a good place.

The problem is that docs#Nat.card_perm is in a file that requires that Field doesn't exist, while docs#IsCyclic use it ultimately.

[tb65536]

Do you need to be changes these variables?

[AntoineChambert-Loir]

This is probably a consequence of missed merges.

[AntoineChambert-Loir]

Actually, you know what? — obtain ⟨φ⟩ := hxy doesn't work anymore (unexpected token error), while obtain ⟨φ⟩ := hxy does.

[AntoineChambert-Loir]

At this point, some stuff is opened and φ represents Euler's totient function.

[tb65536]

I'm still a bit confused as to how the file can break here given that nothing above changed?

[tb65536]

I resolved the issues above to make the page clearer, but there is one problem with t Equiv.Perm.isCyclic_of_card_le_two and Equiv.Perm.isMulCommutative_of_card_le_two for which I can't find a good place.

The problem is that docs#Nat.card_perm is in a file that requires that Field doesn't exist, while docs#IsCyclic use it ultimately.

Hmmm, not sure what is best. Maybe add a small Perm/Cyclic file or something?

[AntoineChambert-Loir]

On short term, it would be the easiest thing to do. On a longer term, it is very bizarre that Nat.card_perm is in a file that prohibits Field, but that SpecificGroups.Cyclic uses the full strength of fields because of its use of Euler's totient function from Totient (to analyse the generators of a cyclic group). Maybe one should try splitting that file in two parts.

[AntoineChambert-Loir]

See #36983 for an attempt to split Mathlib.GroupTheory.SpecificGroups.Cyclic into one part that imports less files (Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic) and the rest (kept in Mathlib.GroupTheory.SpecificGroups.Cyclic, which allows to modify no import in the rest of Mathlib)

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(GroupTheory/SpecificGroups/Alternating/Simple): the alternating group on at least 5 letters is simple. #33082
• [Merged by Bors] - chore(GroupTheory/SpecificGroups/Cyclic/Basic): refactor #36983
• [Merged by Bors] - feat(Data/Nat/Perm): add two lemmas #37026
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.