lean2/library/theories/group_theory/pgroup.lean

391 lines
15 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/-
Copyright (c) 2015 Haitao Zhang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author : Haitao Zhang
-/
import theories.number_theory.primes data algebra.group algebra.group_power algebra.group_bigops .cyclic .finsubg .hom .perm .action
open nat fin list algebra function subtype
namespace group
section pgroup
open finset fintype
variables {G S : Type} [ambientG : group G] [deceqG : decidable_eq G] [finS : fintype S] [deceqS : decidable_eq S]
include ambientG
definition psubg (H : finset G) (p m : nat) : Prop := prime p ∧ card H = p^m
include deceqG finS deceqS
variables {H : finset G} [subgH : is_finsubg H]
include subgH
variables {hom : G → perm S} [Hom : is_hom_class hom]
include Hom
open finset.partition
lemma card_mod_eq_of_action_by_psubg {p : nat} :
∀ {m : nat}, psubg H p m → (card S) mod p = (card (fixed_points hom H)) mod p
| 0 := by rewrite [↑psubg, pow_zero]; intro Psubg;
rewrite [finsubg_eq_singleton_one_of_card_one (and.right Psubg), fixed_points_of_one]
| (succ m) := take Ppsubg, begin
rewrite [@orbit_class_equation' G S ambientG finS deceqS hom Hom H subgH],
apply add_mod_eq_of_dvd, apply dvd_Sum_of_dvd,
intro s Psin,
rewrite mem_sep_iff at Psin,
cases Psin with Psinorbs Pcardne,
esimp [orbits, equiv_classes, orbit_partition] at Psinorbs,
rewrite mem_image_iff at Psinorbs,
cases Psinorbs with a Pa,
cases Pa with Pain Porb,
substvars,
cases Ppsubg with Pprime PcardH,
assert Pdvd : card (orbit hom H a) p ^ (succ m),
rewrite -PcardH,
apply dvd_of_eq_mul (finset.card (stab hom H a)),
apply orbit_stabilizer_theorem,
apply or.elim (eq_one_or_dvd_of_dvd_prime_pow Pprime Pdvd),
intro Pcardeq, contradiction,
intro Ppdvd, exact Ppdvd
end
end pgroup
section psubg_cosets
open finset fintype
variables {G : Type} [ambientG : group G] [finG : fintype G] [deceqG : decidable_eq G]
include ambientG deceqG finG
variables {H : finset G} [finsubgH : is_finsubg H]
include finsubgH
lemma card_psubg_cosets_mod_eq {p : nat} {m : nat} :
psubg H p m → (card (lcoset_type univ H)) mod p = card (lcoset_type (normalizer H) H) mod p :=
assume Psubg, by rewrite [-card_aol_fixed_points_eq_card_cosets]; exact card_mod_eq_of_action_by_psubg Psubg
end psubg_cosets
section cauchy
lemma prodl_rotl_eq_one_of_prodl_eq_one {A B : Type} [gB : group B] {f : A → B} :
∀ {l : list A}, Prodl l f = 1 → Prodl (list.rotl l) f = 1
| nil := assume Peq, rfl
| (a::l) := begin
rewrite [rotl_cons, Prodl_cons f, Prodl_append _ _ f, Prodl_singleton],
exact mul_eq_one_of_mul_eq_one
end
section rotl_peo
variables {A : Type} [ambA : group A]
include ambA
variable [finA : fintype A]
include finA
variable (A)
definition all_prodl_eq_one (n : nat) : list (list A) :=
map (λ l, cons (Prodl l id)⁻¹ l) (all_lists_of_len n)
variable {A}
lemma prodl_eq_one_of_mem_all_prodl_eq_one {n : nat} {l : list A} : l ∈ all_prodl_eq_one A n → Prodl l id = 1 :=
assume Plin, obtain l' Pl' Pl, from exists_of_mem_map Plin,
by substvars; rewrite [Prodl_cons id _ l', mul.left_inv]
lemma length_of_mem_all_prodl_eq_one {n : nat} {l : list A} : l ∈ all_prodl_eq_one A n → length l = succ n :=
assume Plin, obtain l' Pl' Pl, from exists_of_mem_map Plin,
begin substvars, rewrite [length_cons, length_mem_all_lists Pl'] end
lemma nodup_all_prodl_eq_one {n : nat} : nodup (all_prodl_eq_one A n) :=
nodup_map (take l₁ l₂ Peq, tail_eq_of_cons_eq Peq) nodup_all_lists
lemma all_prodl_eq_one_complete {n : nat} : ∀ {l : list A}, length l = succ n → Prodl l id = 1 → l ∈ all_prodl_eq_one A n
| nil := assume Pleq, by contradiction
| (a::l) := assume Pleq Pprod,
begin
rewrite length_cons at Pleq,
rewrite (Prodl_cons id a l) at Pprod,
rewrite [eq_inv_of_mul_eq_one Pprod],
apply mem_map, apply mem_all_lists, apply succ.inj Pleq
end
open fintype
lemma length_all_prodl_eq_one {n : nat} : length (@all_prodl_eq_one A _ _ n) = (card A)^n :=
eq.trans !length_map length_all_lists
open fin
definition prodseq {n : nat} (s : seq A n) : A := Prodl (upto n) s
definition peo [reducible] {n : nat} (s : seq A n) := prodseq s = 1
definition constseq {n : nat} (s : seq A (succ n)) := ∀ i, s i = s !zero
lemma prodseq_eq {n :nat} {s : seq A n} : prodseq s = Prodl (fun_to_list s) id :=
Prodl_map
lemma prodseq_eq_pow_of_constseq {n : nat} (s : seq A (succ n)) :
constseq s → prodseq s = (s !zero) ^ succ n :=
assume Pc, assert Pcl : ∀ i, i ∈ upto (succ n) → s i = s !zero,
from take i, assume Pin, Pc i,
by rewrite [↑prodseq, Prodl_eq_pow_of_const _ Pcl, fin.length_upto]
lemma seq_eq_of_constseq_of_eq {n : nat} {s₁ s₂ : seq A (succ n)} :
constseq s₁ → constseq s₂ → s₁ !zero = s₂ !zero → s₁ = s₂ :=
assume Pc₁ Pc₂ Peq, funext take i, by rewrite [Pc₁ i, Pc₂ i, Peq]
lemma peo_const_one : ∀ {n : nat}, peo (λ i : fin n, (1 : A))
| 0 := rfl
| (succ n) := let s := λ i : fin (succ n), (1 : A) in
assert Pconst : constseq s, from take i, rfl,
calc prodseq s = (s !zero) ^ succ n : prodseq_eq_pow_of_constseq s Pconst
... = (1 : A) ^ succ n : rfl
... = 1 : algebra.one_pow
variable [deceqA : decidable_eq A]
include deceqA
variable (A)
definition peo_seq [reducible] (n : nat) := {s : seq A (succ n) | peo s}
definition peo_seq_one (n : nat) : peo_seq A n :=
tag (λ i : fin (succ n), (1 : A)) peo_const_one
definition all_prodseq_eq_one (n : nat) : list (seq A (succ n)) :=
dmap (λ l, length l = card (fin (succ n))) list_to_fun (all_prodl_eq_one A n)
definition all_peo_seqs (n : nat) : list (peo_seq A n) :=
dmap peo tag (all_prodseq_eq_one A n)
variable {A}
lemma prodseq_eq_one_of_mem_all_prodseq_eq_one {n : nat} {s : seq A (succ n)} :
s ∈ all_prodseq_eq_one A n → prodseq s = 1 :=
assume Psin, obtain l Pex, from exists_of_mem_dmap Psin,
obtain leq Pin Peq, from Pex,
by rewrite [prodseq_eq, Peq, list_to_fun_to_list, prodl_eq_one_of_mem_all_prodl_eq_one Pin]
lemma all_prodseq_eq_one_complete {n : nat} {s : seq A (succ n)} :
prodseq s = 1 → s ∈ all_prodseq_eq_one A n :=
assume Peq,
assert Plin : map s (elems (fin (succ n))) ∈ all_prodl_eq_one A n,
from begin
apply all_prodl_eq_one_complete,
rewrite [length_map], exact length_upto (succ n),
rewrite prodseq_eq at Peq, exact Peq
end,
assert Psin : list_to_fun (map s (elems (fin (succ n)))) (length_map_of_fintype s) ∈ all_prodseq_eq_one A n,
from mem_dmap _ Plin,
by rewrite [fun_eq_list_to_fun_map s (length_map_of_fintype s)]; apply Psin
lemma nodup_all_prodseq_eq_one {n : nat} : nodup (all_prodseq_eq_one A n) :=
dmap_nodup_of_dinj dinj_list_to_fun nodup_all_prodl_eq_one
lemma rotl1_peo_of_peo {n : nat} {s : seq A n} : peo s → peo (rotl_fun 1 s) :=
begin rewrite [↑peo, *prodseq_eq, seq_rotl_eq_list_rotl], apply prodl_rotl_eq_one_of_prodl_eq_one end
section
local attribute perm.f [coercion]
lemma rotl_perm_peo_of_peo {n : nat} : ∀ {m} {s : seq A n}, peo s → peo (rotl_perm A n m s)
| 0 := begin rewrite [↑rotl_perm, rotl_seq_zero], intros, assumption end
| (succ m) := take s,
assert Pmul : rotl_perm A n (m + 1) s = rotl_fun 1 (rotl_perm A n m s), from
calc s ∘ (rotl (m + 1)) = s ∘ ((rotl m) ∘ (rotl 1)) : rotl_compose
... = s ∘ (rotl m) ∘ (rotl 1) : compose.assoc,
begin
rewrite [-add_one, Pmul], intro P,
exact rotl1_peo_of_peo (rotl_perm_peo_of_peo P)
end
end
lemma nodup_all_peo_seqs {n : nat} : nodup (all_peo_seqs A n) :=
dmap_nodup_of_dinj (dinj_tag peo) nodup_all_prodseq_eq_one
lemma all_peo_seqs_complete {n : nat} : ∀ s : peo_seq A n, s ∈ all_peo_seqs A n :=
take ps, subtype.destruct ps (take s, assume Ps,
assert Pin : s ∈ all_prodseq_eq_one A n, from all_prodseq_eq_one_complete Ps,
mem_dmap Ps Pin)
lemma length_all_peo_seqs {n : nat} : length (all_peo_seqs A n) = (card A)^n :=
eq.trans (eq.trans
(show length (all_peo_seqs A n) = length (all_prodseq_eq_one A n), from
assert Pmap : map elt_of (all_peo_seqs A n) = all_prodseq_eq_one A n,
from map_dmap_of_inv_of_pos (λ s P, rfl)
(λ s, prodseq_eq_one_of_mem_all_prodseq_eq_one),
by rewrite [-Pmap, length_map])
(show length (all_prodseq_eq_one A n) = length (all_prodl_eq_one A n), from
assert Pmap : map fun_to_list (all_prodseq_eq_one A n) = all_prodl_eq_one A n,
from map_dmap_of_inv_of_pos list_to_fun_to_list
(λ l Pin, by rewrite [length_of_mem_all_prodl_eq_one Pin, card_fin]),
by rewrite [-Pmap, length_map]))
length_all_prodl_eq_one
definition peo_seq_is_fintype [instance] {n : nat} : fintype (peo_seq A n) :=
fintype.mk (all_peo_seqs A n) nodup_all_peo_seqs all_peo_seqs_complete
lemma card_peo_seq {n : nat} : card (peo_seq A n) = (card A)^n :=
length_all_peo_seqs
section
variable (A)
local attribute perm.f [coercion]
definition rotl_peo_seq (n : nat) (m : nat) (s : peo_seq A n) : peo_seq A n :=
tag (rotl_perm A (succ n) m (elt_of s)) (rotl_perm_peo_of_peo (has_property s))
variable {A}
end
lemma rotl_peo_seq_zero {n : nat} : rotl_peo_seq A n 0 = id :=
funext take s, subtype.eq begin rewrite [↑rotl_peo_seq, ↑rotl_perm, rotl_seq_zero] end
lemma rotl_peo_seq_id {n : nat} : rotl_peo_seq A n (succ n) = id :=
funext take s, subtype.eq begin rewrite [↑rotl_peo_seq, -rotl_perm_pow_eq, rotl_perm_pow_eq_one] end
lemma rotl_peo_seq_compose {n i j : nat} :
(rotl_peo_seq A n i) ∘ (rotl_peo_seq A n j) = rotl_peo_seq A n (j + i) :=
funext take s, subtype.eq begin rewrite [↑rotl_peo_seq, ↑rotl_perm, ↑rotl_fun, compose.assoc, rotl_compose] end
lemma rotl_peo_seq_mod {n i : nat} : rotl_peo_seq A n i = rotl_peo_seq A n (i mod succ n) :=
funext take s, subtype.eq begin rewrite [↑rotl_peo_seq, rotl_perm_mod] end
lemma rotl_peo_seq_inj {n m : nat} : injective (rotl_peo_seq A n m) :=
take ps₁ ps₂, subtype.destruct ps₁ (λ s₁ P₁, subtype.destruct ps₂ (λ s₂ P₂,
assume Peq, tag_eq (rotl_fun_inj (dinj_tag peo _ _ Peq))))
variable (A)
definition rotl_perm_ps [reducible] (n : nat) (m : fin (succ n)) : perm (peo_seq A n) :=
perm.mk (rotl_peo_seq A n m) rotl_peo_seq_inj
variable {A}
variable {n : nat}
lemma rotl_perm_ps_eq {m : fin (succ n)} {s : peo_seq A n} : elt_of (perm.f (rotl_perm_ps A n m) s) = perm.f (rotl_perm A (succ n) m) (elt_of s) := rfl
lemma rotl_perm_ps_eq_of_rotl_perm_eq {i j : fin (succ n)} :
(rotl_perm A (succ n) i) = (rotl_perm A (succ n) j) → (rotl_perm_ps A n i) = (rotl_perm_ps A n j) :=
assume Peq, eq_of_feq (funext take s, subtype.eq (by rewrite [*rotl_perm_ps_eq, Peq]))
lemma rotl_perm_ps_hom (i j : fin (succ n)) :
rotl_perm_ps A n (i+j) = (rotl_perm_ps A n i) * (rotl_perm_ps A n j) :=
eq_of_feq (begin rewrite [↑rotl_perm_ps, {val (i+j)}val_madd, add.comm, -rotl_peo_seq_mod, -rotl_peo_seq_compose] end)
section
local attribute group_of_add_group [instance]
definition rotl_perm_ps_is_hom [instance] : is_hom_class (rotl_perm_ps A n) :=
is_hom_class.mk rotl_perm_ps_hom
open finset
lemma const_of_is_fixed_point {s : peo_seq A n} :
is_fixed_point (rotl_perm_ps A n) univ s → constseq (elt_of s) :=
assume Pfp, take i, begin
rewrite [-(Pfp i !mem_univ) at {1}, rotl_perm_ps_eq, ↑rotl_perm, ↑rotl_fun, {i}mk_mod_eq at {2}, rotl_to_zero]
end
lemma const_of_rotl_fixed_point {s : peo_seq A n} :
s ∈ fixed_points (rotl_perm_ps A n) univ → constseq (elt_of s) :=
assume Psin, take i, begin
apply const_of_is_fixed_point, exact is_fixed_point_of_mem_fixed_points Psin
end
lemma pow_eq_one_of_mem_fixed_points {s : peo_seq A n} :
s ∈ fixed_points (rotl_perm_ps A n) univ → (elt_of s !zero)^(succ n) = 1 :=
assume Psin, eq.trans
(eq.symm (prodseq_eq_pow_of_constseq (elt_of s) (const_of_rotl_fixed_point Psin)))
(has_property s)
lemma peo_seq_one_is_fixed_point : is_fixed_point (rotl_perm_ps A n) univ (peo_seq_one A n) :=
take h, assume Pin, by esimp [rotl_perm_ps]
lemma peo_seq_one_mem_fixed_points : peo_seq_one A n ∈ fixed_points (rotl_perm_ps A n) univ :=
mem_fixed_points_of_exists_of_is_fixed_point (exists.intro !zero !mem_univ) peo_seq_one_is_fixed_point
lemma generator_of_prime_of_dvd_order {p : nat}
: prime p → p card A → ∃ g : A, g ≠ 1 ∧ g^p = 1 :=
assume Pprime Pdvd,
let pp := nat.pred p, spp := nat.succ pp in
assert Peq : spp = p, from succ_pred_prime Pprime,
have Ppsubg : psubg (@univ (fin spp) _) spp 1,
from and.intro (eq.symm Peq ▸ Pprime) (by rewrite [Peq, card_fin, pow_one]),
have Pcardmod : (nat.pow (card A) pp) mod p = (card (fixed_points (rotl_perm_ps A pp) univ)) mod p,
from Peq ▸ card_peo_seq ▸ card_mod_eq_of_action_by_psubg Ppsubg,
have Pfpcardmod : (card (fixed_points (rotl_perm_ps A pp) univ)) mod p = 0,
from eq.trans (eq.symm Pcardmod) (mod_eq_zero_of_dvd (dvd_pow_of_dvd_of_pos Pdvd (pred_prime_pos Pprime))),
have Pfpcardpos : card (fixed_points (rotl_perm_ps A pp) univ) > 0,
from card_pos_of_mem peo_seq_one_mem_fixed_points,
have Pfpcardgt1 : card (fixed_points (rotl_perm_ps A pp) univ) > 1,
from gt_one_of_pos_of_prime_dvd Pprime Pfpcardpos Pfpcardmod,
obtain s₁ s₂ Pin₁ Pin₂ Psnes, from exists_two_of_card_gt_one Pfpcardgt1,
decidable.by_cases
(λ Pe₁ : elt_of s₁ !zero = 1,
assert Pne₂ : elt_of s₂ !zero ≠ 1,
from assume Pe₂,
absurd
(subtype.eq (seq_eq_of_constseq_of_eq
(const_of_rotl_fixed_point Pin₁)
(const_of_rotl_fixed_point Pin₂)
(eq.trans Pe₁ (eq.symm Pe₂))))
Psnes,
exists.intro (elt_of s₂ !zero)
(and.intro Pne₂ (Peq ▸ pow_eq_one_of_mem_fixed_points Pin₂)))
(λ Pne, exists.intro (elt_of s₁ !zero)
(and.intro Pne (Peq ▸ pow_eq_one_of_mem_fixed_points Pin₁)))
end
theorem cauchy_theorem {p : nat} : prime p → p card A → ∃ g : A, order g = p :=
assume Pprime Pdvd,
obtain g Pne Pgpow, from generator_of_prime_of_dvd_order Pprime Pdvd,
assert Porder : order g p, from order_dvd_of_pow_eq_one Pgpow,
or.elim (eq_one_or_eq_self_of_prime_of_dvd Pprime Porder)
(λ Pe, absurd (eq_one_of_order_eq_one Pe) Pne)
(λ Porderp, exists.intro g Porderp)
end rotl_peo
end cauchy
section sylow
open finset fintype
variables {G : Type} [ambientG : group G] [finG : fintype G] [deceqG : decidable_eq G]
include ambientG deceqG finG
theorem first_sylow_theorem {p : nat} (Pp : prime p) :
∀ n, p^n card G → ∃ (H : finset G) (finsubgH : is_finsubg H), card H = p^n
| 0 := assume Pdvd, exists.intro (singleton 1)
(exists.intro one_is_finsubg
(by rewrite [card_singleton, pow_zero]))
| (succ n) := assume Pdvd,
obtain H PfinsubgH PcardH, from first_sylow_theorem n (pow_dvd_of_pow_succ_dvd Pdvd),
assert Ppsubg : psubg H p n, from and.intro Pp PcardH,
assert Ppowsucc : p^(succ n) (card (lcoset_type univ H) * p^n),
by rewrite [-PcardH, -(lagrange_theorem' !subset_univ)]; exact Pdvd,
assert Ppdvd : p card (lcoset_type (normalizer H) H), from
dvd_of_mod_eq_zero
(by rewrite [-(card_psubg_cosets_mod_eq Ppsubg), -dvd_iff_mod_eq_zero];
exact dvd_of_pow_succ_dvd_mul_pow (pos_of_prime Pp) Ppowsucc),
obtain J PJ, from cauchy_theorem Pp Ppdvd,
exists.intro (fin_coset_Union (cyc J))
(exists.intro _
(by rewrite [pow_succ', -PcardH, -PJ]; apply card_Union_lcosets))
end sylow
end group