Equiv.Perm.isThreeCycle_sq_of_three_mem_cycleType_five
theorem Equiv.Perm.isThreeCycle_sq_of_three_mem_cycleType_five :
∀ {g : Equiv.Perm (Fin 5)}, 3 ∈ g.cycleType → (g * g).IsThreeCycle
This theorem is a part of the proof that the alternating group $A_5$ is simple. It demonstrates that if any permutation `g` of a 5-element set has a 3-cycle in its cycle type, then the square of that permutation, `g * g`, is itself a 3-cycle. This result implies that the normal closure of the original permutation `g` must be the entire alternating group $A_5$.
More concisely: If a permutation in the alternating group A5 has a 3-cycle in its cycle decomposition, then the square of that permutation is also a 3-cycle.
|
Equiv.Perm.mem_alternatingGroup
theorem Equiv.Perm.mem_alternatingGroup :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {f : Equiv.Perm α},
f ∈ alternatingGroup α ↔ Equiv.Perm.sign f = 1
This theorem states that for any finite type `α` with decidable equality and any permutation `f` of the set `α`, `f` belongs to the alternating group of `α` if and only if the signature or parity of the permutation `f` is `1`. The alternating group of a set `α` consists of permutations that can be represented as an even number of transpositions (i.e., pairwise swaps), and these permutations are considered "even" and have a signature of `1`. Therefore, this theorem connects the concept of a permutation being in the alternating group with its signature being `1`.
More concisely: A finite type `α` with decidable equality's permutations belong to its alternating group if and only if they have signature 1.
|
alternatingGroup.normalClosure_swap_mul_swap_five
theorem alternatingGroup.normalClosure_swap_mul_swap_five :
Subgroup.normalClosure {⟨Equiv.swap 0 4 * Equiv.swap 1 3, ⋯⟩} = ⊤
This theorem states that the normal closure of the permutation that swaps `0` with `4` and `1` with `3` within the alternating group $A_5$ is the entire group itself. This result will later be used to demonstrate that the normal closure of any permutation having a cycle type of $(2, 2)$ (that is, a permutation that can be decomposed into two 2-cycles) is the whole group. The normal closure of a set is the smallest normal subgroup that contains that set, and in this case, it turns out to encompass the entire group $A_5$.
More concisely: The normal closure of the transposition ((0 4) (1 3)) in the alternating group A5 equals A5.
|
alternatingGroup.isConj_swap_mul_swap_of_cycleType_two
theorem alternatingGroup.isConj_swap_mul_swap_of_cycleType_two :
∀ {g : Equiv.Perm (Fin 5)},
g ∈ alternatingGroup (Fin 5) → g ≠ 1 → (∀ n ∈ g.cycleType, n = 2) → IsConj (Equiv.swap 0 4 * Equiv.swap 1 3) g
This theorem states that any non-identity element of the alternating group $A_5$, whose cycle decomposition consists only of swaps (i.e., permutations that swap only two elements), is conjugate to the permutation formed by swapping 0 with 4 and 1 with 3. Conjugacy in this context means that there exists a permutation that can transform the given permutation into the permutation formed by the said swaps. This theorem is instrumental in showing that any such permutation, when included in $A_5$, does not change the group, i.e., the normal closure of the permutation in $A_5$ is still $A_5$.
More concisely: Any non-identity element in the alternating group A5 with cycle decomposition consisting only of swaps is conjugate to (0 4)(1 3).
|
Equiv.Perm.IsThreeCycle.alternating_normalClosure
theorem Equiv.Perm.IsThreeCycle.alternating_normalClosure :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α],
5 ≤ Fintype.card α → ∀ {f : Equiv.Perm α} (hf : f.IsThreeCycle), Subgroup.normalClosure {⟨f, ⋯⟩} = ⊤
This theorem states that for any type `α` which is a finite type with decidable equality, if the cardinality of `α` is at least 5, then for any bijective function `f` from `α` to itself that forms a 3-cycle, the smallest normal subgroup (the normal closure) containing `f` is the entire group. This is a key lemma used to prove that the alternating group of degree 5 (denoted as $A_5$) is simple, meaning it has no nontrivial normal subgroups.
More concisely: If `α` is a finite type with decidable equality and cardinality at least 5, then any bijective 3-cycle `f` in the symmetries of `α` has the entire symmetries group as its normal subgroup.
|
alternatingGroup.normalClosure_finRotate_five
theorem alternatingGroup.normalClosure_finRotate_five : Subgroup.normalClosure {⟨finRotate 5, ⋯⟩} = ⊤
The theorem `alternatingGroup.normalClosure_finRotate_five` states that the normal closure of the 5-cycle defined by the function `finRotate 5` within the Alternating Group $A_5$ is the whole group itself. In other words, the smallest normal subgroup of $A_5$ that contains the 5-cycle is $A_5$ itself. This theorem is a stepping stone towards showing that the normal closure of any 5-cycle within $A_5$ is the whole group.
More concisely: The normal subgroup generated by the 5-cycle in the Alternating Group A5 is equal to A5 itself.
|