fix(library/theories/group_theory): group_theory
This commit is contained in:
parent
0eec984485
commit
ffbb2be6ac
3 changed files with 16 additions and 13 deletions
|
@ -48,7 +48,7 @@ lemma pow_madd {a : A} {n : nat} {i j : fin (succ n)} :
|
|||
a^(succ n) = 1 → a^(val (i + j)) = a^i * a^j :=
|
||||
assume Pe, calc
|
||||
a^(val (i + j)) = a^((i + j) mod (succ n)) : rfl
|
||||
... = a^(i + j) : by rewrite [-pow_mod Pe]
|
||||
... = a^(val i + val j) : by rewrite [-pow_mod Pe]
|
||||
... = a^i * a^j : by rewrite pow_add
|
||||
|
||||
lemma mk_pow_mod {a : A} {n m : nat} : a ^ (succ m) = 1 → a ^ n = a ^ (mk_mod m n) :=
|
||||
|
@ -87,7 +87,7 @@ definition cyc (a : A) : finset A := {x ∈ univ | bex (succ (card A)) (λ n, a
|
|||
|
||||
definition order (a : A) := card (cyc a)
|
||||
|
||||
definition pow_fin (a : A) (n : nat) (i : fin (order a)) := pow a (i + n)
|
||||
definition pow_fin (a : A) (n : nat) (i : fin (order a)) := a ^ (i + n)
|
||||
|
||||
definition cyc_pow_fin (a : A) (n : nat) : finset A := image (pow_fin a n) univ
|
||||
|
||||
|
@ -143,7 +143,7 @@ lemma mem_cyc (a : A) : ∀ {n : nat}, a^n ∈ cyc a
|
|||
begin rewrite pow_succ', apply cyc_mul_closed a, exact mem_cyc, apply self_mem_cyc end
|
||||
|
||||
lemma order_le {a : A} {n : nat} : a^(succ n) = 1 → order a ≤ succ n :=
|
||||
assume Pe, let s := image (pow a) (upto (succ n)) in
|
||||
assume Pe, let s := image (pow_nat a) (upto (succ n)) in
|
||||
assert Psub: cyc a ⊆ s, from subset_of_forall
|
||||
(take g, assume Pgin, obtain i Pilt Pig, from of_mem_sep Pgin, begin
|
||||
rewrite [-Pig, pow_mod Pe],
|
||||
|
@ -155,14 +155,14 @@ assert Psub: cyc a ⊆ s, from subset_of_forall
|
|||
... = succ n : card_upto (succ n)
|
||||
|
||||
lemma pow_ne_of_lt_order {a : A} {n : nat} : succ n < order a → a^(succ n) ≠ 1 :=
|
||||
assume Plt, not_imp_not_of_imp order_le (nat.not_le_of_gt Plt)
|
||||
assume Plt, not_imp_not_of_imp order_le (not_le_of_gt Plt)
|
||||
|
||||
lemma eq_zero_of_pow_eq_one {a : A} : ∀ {n : nat}, a^n = 1 → n < order a → n = 0
|
||||
| 0 := assume Pe Plt, rfl
|
||||
| (succ n) := assume Pe Plt, absurd Pe (pow_ne_of_lt_order Plt)
|
||||
|
||||
lemma pow_fin_inj (a : A) (n : nat) : injective (pow_fin a n) :=
|
||||
take i j,
|
||||
take i j : fin (order a),
|
||||
suppose a^(i + n) = a^(j + n),
|
||||
have a^(dist i j) = 1, begin apply !dist_add_add_right ▸ (pow_dist_eq_one_of_pow_eq this) end,
|
||||
have dist i j = 0, from
|
||||
|
@ -214,12 +214,12 @@ is_finsubg.mk (cyc_has_one a) (cyc_mul_closed a) (cyc_has_inv a)
|
|||
lemma order_dvd_group_order (a : A) : order a ∣ card A :=
|
||||
dvd.intro (eq.symm (!mul.comm ▸ lagrange_theorem (subset_univ (cyc a))))
|
||||
|
||||
definition pow_fin' (a : A) (i : fin (succ (pred (order a)))) := pow a i
|
||||
definition pow_fin' (a : A) (i : fin (succ (pred (order a)))) := pow_nat a i
|
||||
|
||||
local attribute group_of_add_group [instance]
|
||||
|
||||
lemma pow_fin_hom (a : A) : homomorphic (pow_fin' a) :=
|
||||
take i j,
|
||||
take i j : fin (succ (pred (order a))),
|
||||
begin
|
||||
rewrite [↑pow_fin'],
|
||||
apply pow_madd,
|
||||
|
@ -239,7 +239,6 @@ open fin fintype list
|
|||
|
||||
section
|
||||
local attribute group_of_add_group [instance]
|
||||
local infix ^ := algebra.pow
|
||||
lemma pow_eq_mul {n : nat} {i : fin (succ n)} : ∀ {k : nat}, i^k = mk_mod n (i*k)
|
||||
| 0 := by rewrite [pow_zero]
|
||||
| (succ k) := begin
|
||||
|
@ -290,7 +289,7 @@ lemma rotl_rotr : ∀ {n : nat} (m : nat), (@rotl n m) ∘ (rotr m) = id
|
|||
| (nat.succ n) := take m, funext take i, calc (mk_mod n (n*m)) + (-(mk_mod n (n*m)) + i) = i : add_neg_cancel_left
|
||||
|
||||
lemma rotl_succ {n : nat} : (rotl 1) ∘ (@succ n) = lift_succ :=
|
||||
funext (take i, eq_of_veq (begin rewrite [↑compose, ↑rotl, ↑madd, mul_one n, ↑mk_mod, mod_add_mod, ↑lift_succ, val_succ, -succ_add_eq_succ_add, add_mod_self_left, mod_eq_of_lt (lt.trans (is_lt i) !lt_succ_self), -val_lift] end))
|
||||
funext (take i, eq_of_veq (begin krewrite [↑compose, ↑rotl, ↑madd, mul_one n, ↑mk_mod, mod_add_mod, ↑lift_succ, val_succ, -succ_add_eq_succ_add, add_mod_self_left, mod_eq_of_lt (lt.trans (is_lt i) !lt_succ_self), -val_lift] end))
|
||||
|
||||
definition list.rotl {A : Type} : ∀ l : list A, list A
|
||||
| [] := []
|
||||
|
|
|
@ -139,6 +139,9 @@ lemma fin_lcoset_subset {S : finset A} (Psub : S ⊆ H) : ∀ x, x ∈ H → fin
|
|||
lemma finsubg_lcoset_id {a : A} : a ∈ H → fin_lcoset H a = H :=
|
||||
by rewrite [eq_eq_to_set_eq, fin_lcoset_eq, mem_eq_mem_to_set]; apply subgroup_lcoset_id
|
||||
|
||||
set_option pp.notation false
|
||||
set_option pp.full_names true
|
||||
|
||||
lemma finsubg_inv_lcoset_eq_rcoset {a : A} :
|
||||
fin_inv (fin_lcoset H a) = fin_rcoset H a⁻¹ :=
|
||||
begin
|
||||
|
|
|
@ -320,10 +320,12 @@ lemma generator_of_prime_of_dvd_order {p : nat}
|
|||
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,
|
||||
assert 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 (pow_nat (card A) pp) mod spp = (card (fixed_points (rotl_perm_ps A pp) univ)) mod spp,
|
||||
by rewrite -card_peo_seq; apply card_mod_eq_of_action_by_psubg Ppsubg,
|
||||
have Pcardmod : (pow_nat (card A) pp) mod p = (card (fixed_points (rotl_perm_ps A pp) univ)) mod p,
|
||||
from Peq ▸ this,
|
||||
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,
|
||||
|
@ -345,7 +347,6 @@ decidable.by_cases
|
|||
(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 :=
|
||||
|
|
Loading…
Reference in a new issue