lean2/library/theories/group_theory/pgroup.lean

392 lines
15 KiB
Text
Raw Normal View History

/-
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