Theory Sn_Composition_Factors
section ‹Composition factors of the symmetric and alternating groups›
theory Sn_Composition_Factors
imports Composition_Factors_Solvable Sym_Not_Solvable Symmetric_Generation
begin
text ‹These are ∗‹consistency› checks, not new mathematics. The composition-series material of
‹Composition_Factors_Solvable› was contributed as a large block and merged on
structural evidence (it builds, contains no ‹sorry›, and cites the existing solvability lemmas).
The checks below test its ∗‹content› against results proved independently elsewhere in this
development, on the principle that a vacuous or too-weak definition would let a false statement
through.
The sharpest available cross-check is @{thm [source] Sn_not_solvable}: this development already
proves, by an argument that knows nothing of composition series, that ‹S⇩n› is not solvable for
‹n ≥ 5›. The new criterion says solvability is equivalent to all composition factors being
abelian. The two must agree, and forcing them to agree pins down real content: if
@{const composition_series.abelian_factors} were vacuously true --- say because
@{text series_factor} returned something degenerate --- then ‹S⇩5› would come out solvable and
contradict a theorem already in the library.›
subsection ‹A finite group has a composition series, and ‹S⇩5› in particular›
text ‹First that the existence theorem applies at all to a concrete group of interest.›
lemma Sn_has_composition_series:
"∃H m. composition_series (Sn n) (∘) id H m"
proof (rule finite_group_has_composition_series_ex)
show "Group (Sn n) (∘) id" by (rule Group_Sn)
show "finite (Sn n)" by (rule finite_Sn)
qed
subsection ‹The criterion is consistent with ‹S⇩n› being unsolvable›
text ‹❙‹The main cross-check.› Every composition series of ‹S⇩n› (‹n ≥ 5›) has a factor that is
∗‹not› abelian. This is not proved by exhibiting one --- it is forced, by combining the new
criterion with the independently proved unsolvability of ‹S⇩n›. It therefore fails if the new
criterion is too weak in either direction.›
theorem Sn_composition_factors_not_all_abelian:
assumes n5: "5 ≤ n" and series: "composition_series (Sn n) (∘) id H m"
shows "¬ composition_series.abelian_factors (∘) id H m"
proof
interpret S: composition_series "Sn n" "(∘)" id H m by (rule series)
assume "S.abelian_factors"
then have "Group.solvable (Sn n) (∘) id" using S.solvable_iff_abelian_factors by blast
with Sn_not_solvable[OF n5] show False by simp
qed
text ‹The same for the alternating groups, via @{thm [source] An_not_solvable}.›
theorem An_composition_factors_not_all_abelian:
assumes n5: "5 ≤ n" and series: "composition_series (An n) (∘) id H m"
shows "¬ composition_series.abelian_factors (∘) id H m"
proof
interpret A: composition_series "An n" "(∘)" id H m by (rule series)
assume "A.abelian_factors"
then have "Group.solvable (An n) (∘) id" using A.solvable_iff_abelian_factors by blast
with An_not_solvable[OF n5] show False by simp
qed
text ‹And the existence and criterion theorems combine: some composition series of ‹S⇩5› exists, and
every one of them has a non-abelian factor. If @{const composition_series} were unsatisfiable
these two would not sit together --- the first would be vacuous.›
corollary S5_has_series_with_a_nonabelian_factor:
"∃H m. composition_series (Sn 5) (∘) id H m
∧ ¬ composition_series.abelian_factors (∘) id H m"
proof -
obtain H m where series: "composition_series (Sn 5) (∘) id H m"
using Sn_has_composition_series[of 5] by blast
then have "¬ composition_series.abelian_factors (∘) id H m"
by (rule Sn_composition_factors_not_all_abelian[OF order_refl])
with series show ?thesis by blast
qed
end