feat(library/theories/group_theory): Group and finite group theories

subgroup.lean : general subgroup theories, quotient group using quot
finsubg.lean : finite subgroups (finset and fintype), Lagrange theorem,
  finite cosets and lcoset_type, normalizer for finite groups, coset product
  and quotient group based on lcoset_type, semidirect product
hom.lean : homomorphism and isomorphism, kernel, first isomorphism theorem
perm.lean : permutation group
cyclic.lean : cyclic subgroup, finite generator, order of generator, sequence and rotation
action.lean : fixed point, action, stabilizer, orbit stabilizer theorem, orbit partition,
  Cayley theorem, action on lcoset, cardinality of permutation group
pgroup.lean : subgroup with order of prime power, Cauchy theorem, first Sylow theorem

library/theories/group_theory/action.lean

@@ -0,0 +1,578 @@
+/-
+Copyright (c) 2015 Haitao Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author : Haitao Zhang
+-/
+import algebra.group data .hom .perm .finsubg
+
+namespace group
+open finset algebra function
+
+local attribute perm.f [coercion]
+
+private lemma and_left_true {a b : Prop} (Pa : a) : a ∧ b ↔ b :=
+by rewrite [iff_true_intro Pa, true_and]
+
+section def
+variables {G S : Type} [ambientG : group G] [finS : fintype S] [deceqS : decidable_eq S]
+include ambientG finS
+
+definition is_fixed_point (hom : G → perm S) (H : finset G) (a : S) : Prop :=
+∀ h, h ∈ H → hom h a = a
+
+include deceqS
+
+definition orbit (hom : G → perm S) (H : finset G) (a : S) : finset S :=
+           image (move_by a) (image hom H)
+
+definition fixed_points [reducible] (hom : G → perm S) (H : finset G) : finset S :=
+{a ∈ univ | orbit hom H a = singleton a}
+
+variable [deceqG : decidable_eq G]
+include deceqG -- required by {x ∈ H |p x} filtering
+
+definition moverset (hom : G → perm S) (H : finset G) (a b : S) : finset G :=
+           {f ∈ H | hom f a = b}
+
+definition stab (hom : G → perm S) (H : finset G) (a : S) : finset G :=
+           {f ∈ H | hom f a = a}
+
+end def
+
+section orbit_stabilizer
+
+variables {G S : Type}
+variable [ambientG : group G]
+include ambientG
+variable [finS : fintype S]
+include finS
+variable [deceqS : decidable_eq S]
+include deceqS
+
+section
+
+variables {hom : G → perm S} {H : finset G} {a : S} [Hom : is_hom_class hom]
+include Hom
+
+lemma exists_of_orbit {b : S} : b ∈ orbit hom H a → ∃ h, h ∈ H ∧ hom h a = b :=
+      assume Pb,
+      obtain p (Pp₁ : p ∈ image hom H) (Pp₂ : move_by a p = b), from exists_of_mem_image Pb,
+      obtain h (Ph₁ : h ∈ H) (Ph₂ : hom h = p), from exists_of_mem_image Pp₁,
+      assert Phab : hom h a = b, from calc
+        hom h a = p a : Ph₂
+            ... = b   : Pp₂,
+      exists.intro h (and.intro Ph₁ Phab)
+
+lemma orbit_of_exists {b : S} : (∃ h, h ∈ H ∧ hom h a = b) → b ∈ orbit hom H a :=
+assume Pex, obtain h PinH Phab, from Pex,
+mem_image_of_mem_of_eq (mem_image_of_mem hom PinH) Phab
+
+lemma is_fixed_point_of_mem_fixed_points :
+  a ∈ fixed_points hom H → is_fixed_point hom H a :=
+assume Pain, take h, assume Phin,
+  eq_of_mem_singleton
+    (of_mem_filter Pain ▸ orbit_of_exists (exists.intro h (and.intro Phin rfl)))
+
+lemma mem_fixed_points_of_exists_of_is_fixed_point :
+  (∃ h, h ∈ H) → is_fixed_point hom H a → a ∈ fixed_points hom H :=
+assume Pex Pfp, mem_filter_of_mem !mem_univ
+  (ext take x, iff.intro
+    (assume Porb, obtain h Phin Pha, from exists_of_orbit Porb,
+      by rewrite [mem_singleton_eq, -Pha, Pfp h Phin])
+    (obtain h Phin, from Pex,
+      by rewrite mem_singleton_eq;
+         intro Peq; rewrite Peq;
+         apply orbit_of_exists;
+         existsi h; apply and.intro Phin (Pfp h Phin)))
+
+lemma is_fixed_point_iff_mem_fixed_points_of_exists :
+  (∃ h, h ∈ H) → (a ∈ fixed_points hom H ↔ is_fixed_point hom H a) :=
+assume Pex, iff.intro is_fixed_point_of_mem_fixed_points (mem_fixed_points_of_exists_of_is_fixed_point Pex)
+
+lemma is_fixed_point_iff_mem_fixed_points [finsubgH : is_finsubg H] :
+  a ∈ fixed_points hom H ↔ is_fixed_point hom H a :=
+is_fixed_point_iff_mem_fixed_points_of_exists (exists.intro 1 !finsubg_has_one)
+
+lemma is_fixed_point_of_one : is_fixed_point hom (singleton 1) a :=
+take h, assume Ph, by rewrite [eq_of_mem_singleton Ph, hom_map_one]
+
+lemma fixed_points_of_one : fixed_points hom (singleton 1) = univ :=
+ext take s, iff.intro (assume Pl, mem_univ s)
+  (assume Pr, mem_fixed_points_of_exists_of_is_fixed_point
+    (exists.intro 1 !mem_singleton) is_fixed_point_of_one)
+
+open fintype
+lemma card_fixed_points_of_one : card (fixed_points hom (singleton 1)) = card S :=
+by rewrite [fixed_points_of_one]
+
+end
+
+variable [deceqG : decidable_eq G]
+include deceqG
+
+-- these are already specified by stab hom H a
+variables {hom : G → perm S} {H : finset G} {a : S}
+
+variable [Hom : is_hom_class hom]
+include Hom
+
+lemma stab_lmul {f g : G} : g ∈ stab hom H a → hom (f*g) a = hom f a :=
+      assume Pgstab,
+      assert Pg : hom g a = a, from of_mem_filter Pgstab, calc
+        hom (f*g) a = perm.f ((hom f) * (hom g)) a : is_hom hom
+                ... = ((hom f) ∘ (hom g)) a        : rfl
+                ... = (hom f) a                    : Pg
+
+lemma stab_subset : stab hom H a ⊆ H :=
+      begin
+        apply subset_of_forall, intro f Pfstab, apply mem_of_mem_filter Pfstab
+      end
+
+lemma reverse_move {h g : G} : g ∈ moverset hom H a (hom h a) → hom (h⁻¹*g) a = a :=
+      assume Pg,
+      assert Pga : hom g a = hom h a, from of_mem_filter Pg, calc
+      hom (h⁻¹*g) a = perm.f ((hom h⁻¹) * (hom g)) a : is_hom hom
+      ... = ((hom h⁻¹) ∘ hom g) a        : rfl
+      ... = ((hom h⁻¹) ∘ hom h) a        : {Pga}
+      ... = perm.f ((hom h⁻¹) * hom h) a : rfl
+      ... = perm.f ((hom h)⁻¹ * hom h) a : hom_map_inv hom h
+      ... = (1 : perm S) a               : mul.left_inv (hom h)
+      ... = a                            : rfl
+
+lemma moverset_inj_on_orbit : set.inj_on (moverset hom H a) (ts (orbit hom H a)) :=
+      take b1 b2,
+      assume Pb1, obtain h1 Ph1₁ Ph1₂, from exists_of_orbit Pb1,
+      assert Ph1b1 : h1 ∈ moverset hom H a b1,
+        from mem_filter_of_mem Ph1₁ Ph1₂,
+      assume Psetb2 Pmeq, begin
+        subst b1,
+        rewrite Pmeq at Ph1b1,
+        apply of_mem_filter Ph1b1
+      end
+
+variable [subgH : is_finsubg H]
+include subgH
+
+lemma subg_stab_of_move {h g : G} :
+      h ∈ H → g ∈ moverset hom H a (hom h a) → h⁻¹*g ∈ stab hom H a :=
+      assume Ph Pg,
+      assert Phinvg : h⁻¹*g ∈ H, from begin
+        apply finsubg_mul_closed H,
+          apply finsubg_has_inv H, assumption,
+          apply mem_of_mem_filter Pg
+        end,
+      mem_filter_of_mem Phinvg (reverse_move Pg)
+
+lemma subg_stab_closed : finset_mul_closed_on (stab hom H a) :=
+      take f g, assume Pfstab, assert Pf : hom f a = a, from of_mem_filter Pfstab,
+      assume Pgstab,
+      assert Pfg : hom (f*g) a = a, from calc
+        hom (f*g) a = (hom f) a : stab_lmul Pgstab
+        ... = a : Pf,
+      assert PfginH : (f*g) ∈ H,
+        from finsubg_mul_closed H (mem_of_mem_filter Pfstab) (mem_of_mem_filter Pgstab),
+      mem_filter_of_mem PfginH Pfg
+
+lemma subg_stab_has_one : 1 ∈ stab hom H a :=
+      assert P : hom 1 a = a, from calc
+        hom 1 a = (1 : perm S) a : {hom_map_one hom}
+        ... = a : rfl,
+      assert PoneinH : 1 ∈ H, from finsubg_has_one H,
+      mem_filter_of_mem PoneinH P
+
+lemma subg_stab_has_inv : finset_has_inv (stab hom H a) :=
+      take f, assume Pfstab, assert Pf : hom f a = a, from of_mem_filter Pfstab,
+      assert Pfinv : hom f⁻¹ a = a, from calc
+        hom f⁻¹ a = hom f⁻¹ ((hom f) a) : Pf
+        ... = perm.f ((hom f⁻¹) * (hom f)) a : rfl
+        ... = hom (f⁻¹ * f) a                : is_hom hom
+        ... = hom 1 a                        : mul.left_inv
+        ... = (1 : perm S) a : hom_map_one hom,
+      assert PfinvinH : f⁻¹ ∈ H, from finsubg_has_inv H (mem_of_mem_filter Pfstab),
+      mem_filter_of_mem PfinvinH Pfinv
+
+definition subg_stab_is_finsubg [instance] :
+           is_finsubg (stab hom H a) :=
+           is_finsubg.mk subg_stab_has_one subg_stab_closed subg_stab_has_inv
+
+lemma subg_lcoset_eq_moverset {h : G} :
+      h ∈ H → fin_lcoset (stab hom H a) h = moverset hom H a (hom h a) :=
+      assume Ph, ext (take g, iff.intro
+      (assume Pl, obtain f (Pf₁ : f ∈ stab hom H a) (Pf₂ : h*f = g), from exists_of_mem_image Pl,
+       assert Pfstab : hom f a = a, from of_mem_filter Pf₁,
+       assert PginH : g ∈ H, begin
+        subst Pf₂,
+        apply finsubg_mul_closed H,
+          assumption,
+          apply mem_of_mem_filter Pf₁
+        end,
+      assert Pga : hom g a = hom h a, from calc
+        hom g a = hom (h*f) a : by subst g
+        ... = hom h a         : stab_lmul Pf₁,
+      mem_filter_of_mem PginH Pga)
+      (assume Pr, begin
+       rewrite [↑fin_lcoset, mem_image_iff],
+       existsi h⁻¹*g,
+       split,
+         exact subg_stab_of_move Ph Pr,
+         apply mul_inv_cancel_left
+       end))
+
+lemma subg_moverset_of_orbit_is_lcoset_of_stab (b : S) :
+      b ∈ orbit hom H a → ∃ h, h ∈ H ∧ fin_lcoset (stab hom H a) h = moverset hom H a b :=
+      assume Porb,
+      obtain p (Pp₁ : p ∈ image hom H) (Pp₂ : move_by a p = b), from exists_of_mem_image Porb,
+      obtain h (Ph₁ : h ∈ H) (Ph₂ : hom h = p), from exists_of_mem_image Pp₁,
+      assert Phab : hom h a = b, from by subst p; assumption,
+      exists.intro h (and.intro Ph₁ (Phab ▸ subg_lcoset_eq_moverset Ph₁))
+
+lemma subg_lcoset_of_stab_is_moverset_of_orbit (h : G) :
+      h ∈ H → ∃ b, b ∈ orbit hom H a ∧ moverset hom H a b = fin_lcoset (stab hom H a) h :=
+      assume Ph,
+      have Pha : (hom h a) ∈ orbit hom H a, by
+        apply mem_image_of_mem; apply mem_image_of_mem; exact Ph,
+      exists.intro (hom h a) (and.intro Pha (eq.symm (subg_lcoset_eq_moverset Ph)))
+
+lemma subg_moversets_of_orbit_eq_stab_lcosets :
+      image (moverset hom H a) (orbit hom H a) = fin_lcosets (stab hom H a) H :=
+      ext (take s, iff.intro
+      (assume Pl, obtain b Pb₁ Pb₂, from exists_of_mem_image Pl,
+      obtain h Ph, from subg_moverset_of_orbit_is_lcoset_of_stab b Pb₁, begin
+      rewrite [↑fin_lcosets, mem_image_eq],
+      existsi h, subst Pb₂, assumption
+      end)
+      (assume Pr, obtain h Ph₁ Ph₂, from exists_of_mem_image Pr,
+      obtain b Pb, from @subg_lcoset_of_stab_is_moverset_of_orbit G S ambientG finS deceqS deceqG hom H a Hom subgH h Ph₁, begin
+      rewrite [mem_image_eq],
+      existsi b, subst Ph₂, assumption
+      end))
+
+open nat
+
+theorem orbit_stabilizer_theorem : card H = card (orbit hom H a) * card (stab hom H a) :=
+        calc card H = card (fin_lcosets (stab hom H a) H) * card (stab hom H a) : lagrange_theorem stab_subset
+        ... = card (image (moverset hom H a) (orbit hom H a)) * card (stab hom H a) : subg_moversets_of_orbit_eq_stab_lcosets
+        ... = card (orbit hom H a) * card (stab hom H a) : card_image_eq_of_inj_on moverset_inj_on_orbit
+
+end orbit_stabilizer
+
+section orbit_partition
+
+variables {G S : Type} [ambientG : group G] [finS : fintype S]
+variables [deceqS : decidable_eq S]
+include ambientG finS deceqS
+variables {hom : G → perm S} [Hom : is_hom_class hom] {H : finset G} [subgH : is_finsubg H]
+include Hom subgH
+
+lemma in_orbit_refl {a : S} : a ∈ orbit hom H a :=
+mem_image_of_mem_of_eq (mem_image_of_mem_of_eq (finsubg_has_one H) (hom_map_one hom)) rfl
+
+lemma in_orbit_trans {a b c : S} :
+  a ∈ orbit hom H b → b ∈ orbit hom H c → a ∈ orbit hom H c :=
+assume Painb Pbinc,
+obtain h PhinH Phba, from exists_of_orbit Painb,
+obtain g PginH Pgcb, from exists_of_orbit Pbinc,
+orbit_of_exists (exists.intro (h*g) (and.intro
+  (finsubg_mul_closed H PhinH PginH)
+  (calc hom (h*g) c = perm.f ((hom h) * (hom g)) c : is_hom hom
+                ... = ((hom h) ∘ (hom g)) c : rfl
+                ... = (hom h) b : Pgcb
+                ... = a : Phba)))
+
+lemma in_orbit_symm {a b : S} : a ∈ orbit hom H b → b ∈ orbit hom H a :=
+assume Painb, obtain h PhinH Phba, from exists_of_orbit Painb,
+assert Phinvab : perm.f (hom h)⁻¹ a = b, from
+  calc perm.f (hom h)⁻¹ a = perm.f (hom h)⁻¹ ((hom h) b) : Phba
+                      ... = perm.f ((hom h)⁻¹ * (hom h)) b : rfl
+                      ... = perm.f (1 : perm S) b : mul.left_inv,
+orbit_of_exists (exists.intro h⁻¹ (and.intro
+  (finsubg_has_inv H PhinH)
+  (calc (hom h⁻¹) a = perm.f (hom h)⁻¹ a : hom_map_inv hom h
+                ... = b : Phinvab)))
+
+lemma orbit_is_partition : is_partition (orbit hom H) :=
+take a b, propext (iff.intro
+  (assume Painb, obtain h PhinH Phba, from exists_of_orbit Painb,
+  ext take c, iff.intro
+    (assume Pcina, in_orbit_trans Pcina Painb)
+    (assume Pcinb, obtain g PginH Pgbc, from exists_of_orbit Pcinb,
+      in_orbit_trans Pcinb (in_orbit_symm Painb)))
+  (assume Peq, Peq ▸ in_orbit_refl))
+
+variables (hom) (H)
+open nat finset.partition fintype
+
+definition orbit_partition : @partition S _ :=
+mk univ (orbit hom H) orbit_is_partition
+  (restriction_imp_union (orbit hom H) orbit_is_partition (λ a Pa, !subset_univ))
+
+definition orbits : finset (finset S) := equiv_classes (orbit_partition hom H)
+
+definition fixed_point_orbits : finset (finset S) :=
+  {cls ∈ orbits hom H | card cls = 1}
+
+variables {hom} {H}
+
+lemma exists_iff_mem_orbits (orb : finset S) :
+  orb ∈ orbits hom H ↔ ∃ a : S, orbit hom H a = orb :=
+begin
+  esimp [orbits, equiv_classes, orbit_partition],
+  rewrite [mem_image_iff],
+  apply iff.intro,
+    intro Pl,
+    cases Pl with a Pa,
+    rewrite (and_left_true !mem_univ) at Pa,
+    existsi a, exact Pa,
+    intro Pr,
+    cases Pr with a Pa,
+    rewrite -true_and at Pa, rewrite -(iff_true_intro (mem_univ a)) at Pa,
+    existsi a, exact Pa
+end
+
+lemma exists_of_mem_orbits {orb : finset S} :
+  orb ∈ orbits hom H → ∃ a : S, orbit hom H a = orb :=
+iff.elim_left (exists_iff_mem_orbits orb)
+
+lemma fixed_point_orbits_eq : fixed_point_orbits hom H = image (orbit hom H) (fixed_points hom H) :=
+ext take s, iff.intro
+  (assume Pin,
+   obtain Psin Ps, from iff.elim_left !mem_filter_iff Pin,
+   obtain a Pa, from exists_of_mem_orbits Psin,
+   mem_image_of_mem_of_eq
+     (mem_filter_of_mem !mem_univ (eq.symm
+       (eq_of_card_eq_of_subset (by rewrite [card_singleton, Pa, Ps])
+         (subset_of_forall
+           take x, assume Pxin, eq_of_mem_singleton Pxin ▸ in_orbit_refl))))
+     Pa)
+  (assume Pin,
+   obtain a Pain Porba, from exists_of_mem_image Pin,
+   mem_filter_of_mem
+     (begin esimp [orbits, equiv_classes, orbit_partition], rewrite [mem_image_iff],
+       existsi a, exact and.intro !mem_univ Porba end)
+     (begin substvars, rewrite [of_mem_filter Pain] end))
+
+lemma orbit_inj_on_fixed_points : set.inj_on (orbit hom H) (ts (fixed_points hom H)) :=
+take a₁ a₂, begin
+  rewrite [-*mem_eq_mem_to_set, ↑fixed_points, *mem_filter_iff],
+  intro Pa₁ Pa₂,
+  rewrite [and.right Pa₁, and.right Pa₂],
+  exact eq_of_singleton_eq
+end
+
+lemma card_fixed_point_orbits_eq : card (fixed_point_orbits hom H) = card (fixed_points hom H) :=
+by rewrite fixed_point_orbits_eq; apply card_image_eq_of_inj_on orbit_inj_on_fixed_points
+
+lemma orbit_class_equation : card S = Sum (orbits hom H) card :=
+class_equation (orbit_partition hom H)
+
+lemma card_fixed_point_orbits : Sum (fixed_point_orbits hom H) card = card (fixed_point_orbits hom H) :=
+calc Sum _ _ = Sum (fixed_point_orbits hom H) (λ x, 1) : Sum_ext (take c Pin, of_mem_filter Pin)
+         ... = card (fixed_point_orbits hom H) * 1 : Sum_const_eq_card_mul
+         ... = card (fixed_point_orbits hom H) : mul_one (card (fixed_point_orbits hom H))
+
+lemma orbit_class_equation' : card S = card (fixed_points hom H) + Sum {cls ∈ orbits hom H | card cls ≠ 1} card :=
+calc card S = Sum (orbits hom H) finset.card : orbit_class_equation
+        ... = Sum (fixed_point_orbits hom H) finset.card + Sum {cls ∈ orbits hom H | card cls ≠ 1} card : card_binary_Union_disjoint_sets _ (equiv_class_disjoint _)
+        ... = card (fixed_point_orbits hom H) + Sum {cls ∈ orbits hom H | card cls ≠ 1} card : card_fixed_point_orbits
+        ... = card (fixed_points hom H) + Sum {cls ∈ orbits hom H | card cls ≠ 1} card : card_fixed_point_orbits_eq
+
+end orbit_partition
+
+section cayley
+variables {G : Type}
+variable [ambientG : group G]
+include ambientG
+variable [finG : fintype G]
+include finG
+
+definition action_by_lmul : G → perm G :=
+take g, perm.mk (lmul_by g) (lmul_inj g)
+
+variable [deceqG : decidable_eq G]
+include deceqG
+
+lemma action_by_lmul_hom : homomorphic (@action_by_lmul G _ _) :=
+take g₁ (g₂ : G), eq.symm (calc
+      action_by_lmul g₁ * action_by_lmul g₂
+    = perm.mk ((lmul_by g₁)∘(lmul_by g₂)) _ : rfl
+... = perm.mk (lmul_by (g₁*g₂)) _ : by congruence; apply coset.lmul_compose)
+
+lemma action_by_lmul_inj : injective (@action_by_lmul G _ _) :=
+take g₁ g₂, assume Peq, perm.no_confusion Peq
+  (λ Pfeq Pqeq,
+  have Pappeq : g₁*1 = g₂*1, from congr_fun Pfeq _,
+  calc g₁ = g₁ * 1 : mul_one
+      ... = g₂ * 1 : Pappeq
+      ... = g₂ : mul_one)
+
+definition action_by_lmul_is_iso [instance] : is_iso_class (@action_by_lmul G _ _) :=
+is_iso_class.mk action_by_lmul_hom action_by_lmul_inj
+
+end cayley
+
+section lcosets
+open fintype subtype
+
+variables {G : Type} [ambientG : group G] [finG : fintype G] [deceqG : decidable_eq G]
+include ambientG deceqG finG
+
+variables H : finset G
+
+definition action_on_lcoset : G → perm (lcoset_type univ H) :=
+take g, perm.mk (lcoset_lmul (mem_univ g)) lcoset_lmul_inj
+
+private definition lcoset_of (g : G) : lcoset_type univ H :=
+tag (fin_lcoset H g) (exists.intro g (and.intro !mem_univ rfl))
+
+variable {H}
+
+lemma action_on_lcoset_eq (g : G) (J : lcoset_type univ H)
+  : elt_of (action_on_lcoset H g J) = fin_lcoset (elt_of J) g := rfl
+
+lemma action_on_lcoset_hom : homomorphic (action_on_lcoset H) :=
+take g₁ g₂, eq_of_feq (funext take S, subtype.eq
+  (by rewrite [↑action_on_lcoset, ↑lcoset_lmul, -fin_lcoset_compose]))
+
+definition action_on_lcoset_is_hom [instance] : is_hom_class (action_on_lcoset H) :=
+is_hom_class.mk action_on_lcoset_hom
+
+variable [finsubgH : is_finsubg H]
+include finsubgH
+
+lemma aol_fixed_point_subset_normalizer (J : lcoset_type univ H) :
+  is_fixed_point (action_on_lcoset H) H J → elt_of J ⊆ normalizer H :=
+obtain j Pjin Pj, from exists_of_lcoset_type J,
+assume Pfp,
+assert PH : ∀ {h}, h ∈ H → fin_lcoset (fin_lcoset H j) h = fin_lcoset H j,
+  from take h, assume Ph, by rewrite [Pj, -action_on_lcoset_eq, Pfp h Ph],
+subset_of_forall take g, begin
+  rewrite [-Pj, fin_lcoset_same, -inv_inv at {2}],
+  intro Pg,
+  rewrite -Pg at PH,
+  apply finsubg_has_inv,
+  apply mem_filter_of_mem !mem_univ,
+  intro h Ph,
+  assert Phg : fin_lcoset (fin_lcoset H g) h = fin_lcoset H g, exact PH Ph,
+  revert Phg,
+  rewrite [↑conj_by, inv_inv, mul.assoc, fin_lcoset_compose, -fin_lcoset_same, ↑fin_lcoset, mem_image_iff, ↑lmul_by],
+  intro Pex, cases Pex with k Pand, cases Pand with Pkin Pk,
+  rewrite [-Pk, inv_mul_cancel_left], exact Pkin
+end
+
+lemma aol_fixed_point_of_mem_normalizer {g : G} :
+  g ∈ normalizer H → is_fixed_point (action_on_lcoset H) H (lcoset_of H g) :=
+assume Pgin, take h, assume Phin, subtype.eq
+  (by rewrite [action_on_lcoset_eq, ↑lcoset_of, lrcoset_same_of_mem_normalizer Pgin, fin_lrcoset_comm, finsubg_lcoset_id Phin])
+
+lemma aol_fixed_points_eq_normalizer :
+  Union (fixed_points (action_on_lcoset H) H) elt_of = normalizer H :=
+ext take g, begin
+  rewrite [mem_Union_iff],
+  apply iff.intro,
+    intro Pl,
+    cases Pl with L PL, revert PL,
+    rewrite [is_fixed_point_iff_mem_fixed_points],
+    intro Pg,
+    apply mem_of_subset_of_mem,
+      apply aol_fixed_point_subset_normalizer L, exact and.left Pg,
+      exact and.right Pg,
+    intro Pr,
+    existsi (lcoset_of H g), apply and.intro,
+      rewrite [is_fixed_point_iff_mem_fixed_points],
+      exact aol_fixed_point_of_mem_normalizer Pr,
+      exact fin_mem_lcoset g
+end
+
+open nat
+
+lemma card_aol_fixed_points_eq_card_cosets :
+  card (fixed_points (action_on_lcoset H) H) = card (lcoset_type (normalizer H) H) :=
+have Peq : card (fixed_points (action_on_lcoset H) H) * card H = card (lcoset_type (normalizer H) H) * card H, from calc
+  card _ * card H = card (Union (fixed_points (action_on_lcoset H) H) elt_of) : card_Union_lcosets
+              ... = card (normalizer H) : aol_fixed_points_eq_normalizer
+              ... = card (lcoset_type (normalizer H) H) * card H : lagrange_theorem' subset_normalizer,
+eq_of_mul_eq_mul_right (card_pos_of_mem !finsubg_has_one) Peq
+
+end lcosets
+
+section perm_fin
+open fin nat eq.ops
+
+variable {n : nat}
+
+definition lift_perm (p : perm (fin n)) : perm (fin (succ n)) :=
+perm.mk (lift_fun p) (lift_fun_of_inj (perm.inj p))
+
+definition lower_perm (p : perm (fin (succ n))) (P : p maxi = maxi) : perm (fin n) :=
+perm.mk (lower_inj p (perm.inj p) P)
+  (take i j, begin
+  rewrite [-eq_iff_veq, *lower_inj_apply, eq_iff_veq],
+  apply injective_compose (perm.inj p) lift_succ_inj
+  end)
+
+lemma lift_lower_eq : ∀ {p : perm (fin (succ n))} (P : p maxi = maxi),
+  lift_perm (lower_perm p P) = p
+| (perm.mk pf Pinj) := assume Pmax, begin
+  rewrite [↑lift_perm], congruence,
+  apply funext, intro i,
+  assert Pfmax : pf maxi = maxi, apply Pmax,
+  assert Pd : decidable (i = maxi),
+    exact _,
+    cases Pd with Pe Pne,
+      rewrite [Pe, Pfmax], apply lift_fun_max,
+      rewrite [lift_fun_of_ne_max Pne, ↑lower_perm, ↑lift_succ],
+      rewrite [-eq_iff_veq, -val_lift, lower_inj_apply, eq_iff_veq],
+      congruence, rewrite [-eq_iff_veq]
+  end
+
+lemma lift_perm_inj : injective (@lift_perm n) :=
+take p1 p2, assume Peq, eq_of_feq (lift_fun_inj (feq_of_eq Peq))
+
+lemma lift_perm_inj_on_univ : set.inj_on (@lift_perm n) (ts univ) :=
+eq.symm to_set_univ ▸ iff.elim_left set.injective_iff_inj_on_univ lift_perm_inj
+
+lemma lift_to_stab : image (@lift_perm n) univ = stab id univ maxi :=
+ext (take (pp : perm (fin (succ n))), iff.intro
+  (assume Pimg, obtain p P_ Pp, from exists_of_mem_image Pimg,
+  assert Ppp : pp maxi = maxi, from calc
+    pp maxi = lift_perm p maxi : {eq.symm Pp}
+        ... = lift_fun p maxi : rfl
+        ... = maxi : lift_fun_max,
+  mem_filter_of_mem !mem_univ Ppp)
+  (assume Pstab,
+  assert Ppp : pp maxi = maxi, from of_mem_filter Pstab,
+  mem_image_of_mem_of_eq !mem_univ (lift_lower_eq Ppp)))
+
+definition move_from_max_to (i : fin (succ n)) : perm (fin (succ n)) :=
+perm.mk (madd (i - maxi)) madd_inj
+
+lemma orbit_max : orbit (@id (perm (fin (succ n)))) univ maxi = univ :=
+ext (take i, iff.intro
+  (assume P, !mem_univ)
+  (assume P, begin
+    apply mem_image_of_mem_of_eq,
+      apply mem_image_of_mem_of_eq,
+        apply mem_univ (move_from_max_to i), apply rfl,
+      apply sub_add_cancel
+    end))
+
+lemma card_orbit_max : card (orbit (@id (perm (fin (succ n)))) univ maxi) = succ n :=
+calc card (orbit (@id (perm (fin (succ n)))) univ maxi) = card univ : {orbit_max}
+                                                    ... = succ n : card_fin (succ n)
+
+open fintype
+
+lemma card_lift_to_stab : card (stab (@id (perm (fin (succ n)))) univ maxi) = card (perm (fin n)) :=
+ calc finset.card (stab (@id (perm (fin (succ n)))) univ maxi)
+    = finset.card (image (@lift_perm n) univ) : {eq.symm lift_to_stab}
+... = card univ : card_image_eq_of_inj_on lift_perm_inj_on_univ
+
+lemma card_perm_step : card (perm (fin (succ n))) = (succ n) * card (perm (fin n)) :=
+ calc card (perm (fin (succ n)))
+    = card (orbit id univ maxi) * card (stab id univ maxi) : orbit_stabilizer_theorem
+... = (succ n) * card (stab id univ maxi) : {card_orbit_max}
+... = (succ n) * card (perm (fin n)) : {card_lift_to_stab}
+
+end perm_fin
+end group

library/theories/group_theory/cyclic.lean

@@ -0,0 +1,449 @@
+/-
+Copyright (c) 2015 Haitao Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author : Haitao Zhang
+-/
+
+import data algebra.group algebra.group_power .finsubg .hom .perm
+
+open function algebra finset
+open eq.ops
+
+namespace group
+
+section cyclic
+open nat fin
+
+local attribute madd [reducible]
+
+definition diff [reducible] (i j : nat) :=
+if (i < j) then (j - i) else (i - j)
+
+lemma diff_eq_dist {i j : nat} : diff i j = dist i j :=
+#nat decidable.by_cases
+  (λ Plt : i < j,
+    by rewrite [if_pos Plt, ↑dist, sub_eq_zero_of_le (le_of_lt Plt), zero_add])
+  (λ Pnlt : ¬ i < j,
+    by rewrite [if_neg Pnlt, ↑dist, sub_eq_zero_of_le (le_of_not_gt Pnlt)])
+
+lemma diff_eq_max_sub_min {i j : nat} : diff i j = (max i j) - min i j :=
+decidable.by_cases
+  (λ Plt : i < j, begin rewrite [↑max, ↑min, *(if_pos Plt)] end)
+  (λ Pnlt : ¬ i < j, begin rewrite [↑max, ↑min, *(if_neg Pnlt)] end)
+
+lemma diff_succ {i j : nat} : diff (succ i) (succ j) = diff i j :=
+by rewrite [*diff_eq_dist, ↑dist, *succ_sub_succ]
+
+lemma diff_add {i j k : nat} : diff (i + k) (j + k) = diff i j :=
+by rewrite [*diff_eq_dist, dist_add_add_right]
+
+lemma diff_le_max {i j : nat} : diff i j ≤ max i j :=
+begin rewrite diff_eq_max_sub_min, apply sub_le end
+
+lemma diff_gt_zero_of_ne {i j : nat} : i ≠ j → diff i j > 0 :=
+assume Pne, decidable.by_cases
+  (λ Plt : i < j, begin rewrite [if_pos Plt], apply sub_pos_of_lt Plt end)
+  (λ Pnlt : ¬ i < j, begin
+    rewrite [if_neg Pnlt], apply sub_pos_of_lt,
+    apply lt_of_le_and_ne (nat.le_of_not_gt Pnlt) (ne.symm Pne) end)
+
+variable {A : Type}
+
+open list
+
+variable [ambG : group A]
+include ambG
+
+lemma pow_mod {a : A} {n m : nat} : a ^ m = 1 → a ^ n = a ^ (n mod m) :=
+assume Pid,
+have Pm : a ^ (n div m * m) = 1, from calc
+  a ^ (n div m * m) = a ^ (m * (n div m)) : {mul.comm (n div m) m}
+                ... = (a ^ m) ^ (n div m) : !pow_mul
+                ... = 1 ^ (n div m) : {Pid}
+                ... = 1 : one_pow (n div m),
+calc a ^ n = a ^ (n div m * m + n mod m) : {eq_div_mul_add_mod n m}
+       ... = a ^ (n div m * m) * a ^ (n mod m) : !pow_add
+       ... = 1 * a ^ (n mod m) : {Pm}
+       ... = a ^ (n mod m) : !one_mul
+
+lemma pow_sub_eq_one_of_pow_eq {a : A} {i j : nat} :
+  a^i = a^j → a^(i - j) = 1 :=
+assume Pe, or.elim (lt_or_ge i j)
+  (assume Piltj, begin rewrite [sub_eq_zero_of_le (nat.le_of_lt Piltj)] end)
+  (assume Pigej, begin rewrite [pow_sub a Pigej, Pe, mul.right_inv] end)
+
+lemma pow_diff_eq_one_of_pow_eq {a : A} {i j : nat} :
+  a^i = a^j → a^(diff i j) = 1 :=
+assume Pe, decidable.by_cases
+  (λ Plt : i < j, by rewrite [if_pos Plt]; exact pow_sub_eq_one_of_pow_eq (eq.symm Pe))
+  (λ Pnlt : ¬ i < j, by rewrite [if_neg Pnlt]; exact pow_sub_eq_one_of_pow_eq Pe)
+
+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) : pow_mod Pe
+            ... = a^i * a^j : !pow_add
+
+lemma mk_pow_mod {a : A} {n m : nat} : a ^ (succ m) = 1 → a ^ n = a ^ (mk_mod m n) :=
+assume Pe, pow_mod Pe
+
+variable [finA : fintype A]
+include finA
+
+open fintype
+
+variable [deceqA : decidable_eq A]
+include deceqA
+
+lemma exists_pow_eq_one (a : A) : ∃ n, n < card A ∧ a ^ (succ n) = 1 :=
+let f := (λ i : fin (succ (card A)), a ^ i) in
+assert Pninj : ¬(injective f), from assume Pinj,
+  absurd (card_le_of_inj _ _ (exists.intro f Pinj))
+    (begin rewrite [card_fin], apply not_succ_le_self end),
+obtain i₁ P₁, from exists_not_of_not_forall Pninj,
+obtain i₂ P₂, from exists_not_of_not_forall P₁,
+obtain Pfe Pne, from iff.elim_left not_implies_iff_and_not P₂,
+assert Pvne : val i₁ ≠ val i₂, from assume Pveq, absurd (eq_of_veq Pveq) Pne,
+exists.intro (pred (diff i₁ i₂)) (begin
+  rewrite [succ_pred_of_pos (diff_gt_zero_of_ne Pvne)], apply and.intro,
+    apply lt_of_succ_lt_succ,
+    rewrite [succ_pred_of_pos (diff_gt_zero_of_ne Pvne)],
+    apply nat.lt_of_le_of_lt diff_le_max (max_lt i₁ i₂),
+    apply pow_diff_eq_one_of_pow_eq Pfe
+  end)
+
+-- Another possibility is to generate a list of powers and use find to get the first
+-- unity.
+-- The bound on bex is arbitrary as long as it is large enough (at least card A). Making
+-- it larger simplifies some proofs, such as a ∈ cyc a.
+definition cyc (a : A) : finset A := {x ∈ univ | bex (succ (card A)) (λ n, a ^ n = x)}
+
+definition order (a : A) := card (cyc a)
+
+definition pow_fin (a : A) (n : nat) (i : fin (order a)) := pow a (i + n)
+
+definition cyc_pow_fin (a : A) (n : nat) : finset A := image (pow_fin a n) univ
+
+lemma order_le_group_order {a : A} : order a ≤ card A :=
+card_le_card_of_subset !subset_univ
+
+lemma cyc_has_one (a : A) : 1 ∈ cyc a :=
+begin
+  apply mem_filter_of_mem !mem_univ,
+  existsi 0, apply and.intro,
+    apply zero_lt_succ,
+    apply pow_zero
+end
+
+lemma order_pos (a : A) : 0 < order a :=
+length_pos_of_mem (cyc_has_one a)
+
+lemma cyc_mul_closed (a : A) : finset_mul_closed_on (cyc a) :=
+take g h, assume Pgin Phin,
+obtain n Plt Pe, from exists_pow_eq_one a,
+obtain i Pilt Pig, from of_mem_filter Pgin,
+obtain j Pjlt Pjh, from of_mem_filter Phin,
+begin
+  rewrite [-Pig, -Pjh, -pow_add, pow_mod Pe],
+  apply mem_filter_of_mem !mem_univ,
+  existsi ((i + j) mod (succ n)), apply and.intro,
+    apply nat.lt.trans (mod_lt (i+j) !zero_lt_succ) (succ_lt_succ Plt),
+    apply rfl
+end
+
+lemma cyc_has_inv (a : A) : finset_has_inv (cyc a) :=
+take g, assume Pgin,
+obtain n Plt Pe, from exists_pow_eq_one a,
+obtain i Pilt Pig, from of_mem_filter Pgin,
+let ni := -(mk_mod n i) in
+assert Pinv : g*a^ni = 1, by
+  rewrite [-Pig, mk_pow_mod Pe, -(pow_madd Pe), add.right_inv],
+begin
+  rewrite [inv_eq_of_mul_eq_one Pinv],
+  apply mem_filter_of_mem !mem_univ,
+  existsi ni, apply and.intro,
+    apply nat.lt.trans (is_lt ni) (succ_lt_succ Plt),
+    apply rfl
+end
+
+lemma self_mem_cyc (a : A) : a ∈ cyc a :=
+mem_filter_of_mem !mem_univ
+  (exists.intro (1 : nat) (and.intro (succ_lt_succ card_pos) !pow_one))
+
+lemma mem_cyc (a : A) : ∀ {n : nat}, a^n ∈ cyc a
+| 0        := cyc_has_one a
+| (succ n) :=
+  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
+assert Psub: cyc a ⊆ s, from subset_of_forall
+  (take g, assume Pgin, obtain i Pilt Pig, from of_mem_filter Pgin, begin
+  rewrite [-Pig, pow_mod Pe],
+  apply mem_image_of_mem_of_eq,
+    apply mem_upto_of_lt (mod_lt i !zero_lt_succ),
+    exact rfl end),
+#nat calc order a ≤ card s : card_le_card_of_subset Psub
+              ... ≤ card (upto (succ n)) : !card_image_le
+              ... = 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)
+
+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, assume Peq : a^(i + n) = a^(j + n),
+have Pde : a^(diff i j) = 1, from diff_add ▸ pow_diff_eq_one_of_pow_eq Peq,
+have Pdz : diff i j = 0, from eq_zero_of_pow_eq_one Pde
+  (nat.lt_of_le_of_lt diff_le_max (max_lt i j)),
+eq_of_veq (eq_of_dist_eq_zero (diff_eq_dist ▸ Pdz))
+
+lemma cyc_eq_cyc (a : A) (n : nat) : cyc_pow_fin a n = cyc a :=
+assert Psub : cyc_pow_fin a n ⊆ cyc a, from subset_of_forall
+  (take g, assume Pgin,
+  obtain i Pin Pig, from exists_of_mem_image Pgin, by rewrite [-Pig]; apply mem_cyc),
+eq_of_card_eq_of_subset (begin apply eq.trans,
+    apply card_image_eq_of_inj_on,
+      rewrite [to_set_univ, -set.injective_iff_inj_on_univ], exact pow_fin_inj a n,
+    rewrite [card_fin] end) Psub
+
+lemma pow_order (a : A) : a^(order a) = 1 :=
+obtain i Pin Pone, from exists_of_mem_image (eq.symm (cyc_eq_cyc a 1) ▸ cyc_has_one a),
+or.elim (eq_or_lt_of_le (succ_le_of_lt (is_lt i)))
+  (assume P, P ▸ Pone) (assume P, absurd Pone (pow_ne_of_lt_order P))
+
+lemma eq_one_of_order_eq_one {a : A} : order a = 1 → a = 1 :=
+assume Porder,
+calc a = a^1 : eq.symm (pow_one a)
+   ... = a^(order a) : Porder
+   ... = 1 : pow_order
+
+lemma order_of_min_pow {a : A} {n : nat}
+  (Pone : a^(succ n) = 1) (Pmin : ∀ i, i < n → a^(succ i) ≠ 1) : order a = succ n :=
+or.elim (eq_or_lt_of_le (order_le Pone)) (λ P, P)
+  (λ P : order a < succ n, begin
+  assert Pn : a^(order a) ≠ 1,
+    rewrite [-(succ_pred_of_pos (order_pos a))],
+    apply Pmin, apply nat.lt_of_succ_lt_succ,
+    rewrite [succ_pred_of_pos !order_pos], assumption,
+  exact absurd (pow_order a) Pn end)
+
+lemma order_dvd_of_pow_eq_one {a : A} {n : nat} (Pone : a^n = 1) : order a ∣ n :=
+assert Pe : a^(n mod order a) = 1, from
+  begin
+    revert Pone,
+    rewrite [eq_div_mul_add_mod n (order a) at {1}, pow_add, mul.comm _ (order a), pow_mul, pow_order, one_pow, one_mul],
+    intros, assumption
+  end,
+dvd_of_mod_eq_zero (eq_zero_of_pow_eq_one Pe (mod_lt n !order_pos))
+
+definition cyc_is_finsubg [instance] (a : A) : is_finsubg (cyc a) :=
+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
+
+local attribute group_of_add_group [instance]
+
+lemma pow_fin_hom (a : A) : homomorphic (pow_fin' a) :=
+take i j,
+begin
+  rewrite [↑pow_fin'],
+  apply pow_madd,
+  rewrite [succ_pred_of_pos !order_pos],
+  exact pow_order a
+end
+
+definition pow_fin_is_iso (a : A) : is_iso_class (pow_fin' a) :=
+is_iso_class.mk (pow_fin_hom a)
+  (begin rewrite [↑pow_fin', succ_pred_of_pos !order_pos], exact pow_fin_inj a 0 end)
+
+end cyclic
+
+section rot
+open nat list
+
+open fin fintype list
+
+lemma dmap_map_lift {n : nat} : ∀ l : list nat, (∀ i, i ∈ l → i < n) → dmap (λ i, i < succ n) mk l = map lift_succ (dmap (λ i, i < n) mk l)
+| []     := assume Plt, rfl
+| (i::l) := assume Plt, begin
+  rewrite [@dmap_cons_of_pos _ _ (λ i, i < succ n) _ _ _ (lt_succ_of_lt (Plt i !mem_cons)), @dmap_cons_of_pos _ _ (λ i, i < n) _ _ _ (Plt i !mem_cons), map_cons],
+  congruence,
+  apply dmap_map_lift,
+  intro j Pjinl, apply Plt, apply mem_cons_of_mem, assumption end
+
+lemma upto_succ (n : nat) : upto (succ n) = maxi :: map lift_succ (upto n) :=
+begin
+  rewrite [↑fin.upto, list.upto_succ, @dmap_cons_of_pos _ _ (λ i, i < succ n) _ _ _ (nat.self_lt_succ n)],
+  congruence,
+  apply dmap_map_lift, apply @list.lt_of_mem_upto
+end
+
+definition upto_step : ∀ {n : nat}, fin.upto (succ n) = (map succ (upto n))++[zero n]
+| 0        := rfl
+| (succ n) := begin rewrite [upto_succ n, map_cons, append_cons, succ_max, upto_succ, -lift_zero],
+  congruence, rewrite [map_map, -lift_succ.comm, -map_map, -(map_singleton _ (zero n)), -map_append, -upto_step] end
+
+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
+  assert Psucc : i^(succ k) = madd (i^k) i, apply pow_succ,
+  rewrite [Psucc, pow_eq_mul],
+  apply eq_of_veq,
+  rewrite [mul_succ, val_madd, ↑mk_mod, mod_add_mod]
+  end
+
+end
+
+definition rotl : ∀ {n : nat} m : nat, fin n → fin n
+| 0        := take m i, elim0 i
+| (succ n) := take m, madd (mk_mod n (n*m))
+
+definition rotr : ∀ {n : nat} m : nat, fin n → fin n
+| (0:nat)      := take m i, elim0 i
+| (nat.succ n) := take m, madd (-(mk_mod n (n*m)))
+
+lemma rotl_succ' {n m : nat} : rotl m = madd (mk_mod n (n*m)) := rfl
+
+lemma rotl_zero : ∀ {n : nat}, @rotl n 0 = id
+| 0        := funext take i, elim0 i
+| (succ n) := funext take i, zero_add i
+
+lemma rotl_id : ∀ {n : nat}, @rotl n n = id
+| 0        := funext take i, elim0 i
+| (succ n) :=
+  assert P : mk_mod n (n * succ n) = mk_mod n 0,
+    from eq_of_veq !mul_mod_left,
+  begin rewrite [rotl_succ', P], apply rotl_zero end
+
+lemma rotl_to_zero {n i : nat} : rotl i (mk_mod n i) = zero n :=
+eq_of_veq begin rewrite [↑rotl, val_madd], esimp [mk_mod], rewrite [ mod_add_mod, add_mod_mod, -succ_mul, mul_mod_right] end
+
+lemma rotl_compose : ∀ {n : nat} {j k : nat}, (@rotl n j) ∘ (rotl k) = rotl (j + k)
+| 0        := take j k, funext take i, elim0 i
+| (succ n) :=  take j k, funext take i, eq.symm begin
+  rewrite [*rotl_succ', mul.left_distrib, -(@madd_mk_mod n (n*j)), madd_assoc],
+  end
+
+lemma rotr_rotl : ∀ {n : nat} (m : nat) {i : fin n}, rotr m (rotl m i) = i
+| 0            := take m i, elim0 i
+| (nat.succ n) := take m i, calc (-(mk_mod n (n*m))) + ((mk_mod n (n*m)) + i) = i : by rewrite neg_add_cancel_left
+
+lemma rotl_rotr : ∀ {n : nat} (m : nat), (@rotl n m) ∘ (rotr m) = id
+| 0            := take m, funext take i, elim0 i
+| (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))
+
+definition list.rotl {A : Type} : ∀ l : list A, list A
+| []     := []
+| (a::l) := l++[a]
+
+lemma rotl_cons {A : Type} {a : A} {l} : list.rotl (a::l) = l++[a] := rfl
+
+lemma rotl_map {A B : Type} {f : A → B} : ∀ {l : list A}, list.rotl (map f l) = map f (list.rotl l)
+| []     := rfl
+| (a::l) := begin rewrite [map_cons, *rotl_cons, map_append] end
+
+lemma rotl_eq_rotl : ∀ {n : nat}, map (rotl 1) (upto n) = list.rotl (upto n)
+| 0        := rfl
+| (succ n) := begin
+  rewrite [upto_step at {1}, upto_succ, rotl_cons, map_append],
+  congruence,
+    rewrite [map_map], congruence, exact rotl_succ,
+    rewrite [map_singleton], congruence, rewrite [↑rotl, mul_one n, ↑mk_mod, ↑zero, ↑maxi, ↑madd],
+      congruence, rewrite [ mod_add_mod, nat.add_zero, mod_eq_of_lt !lt_succ_self ]
+  end
+
+definition seq [reducible] (A : Type) (n : nat) := fin n → A
+
+variable {A : Type}
+
+definition rotl_fun {n : nat} (m : nat) (f : seq A n) : seq A n := f ∘ (rotl m)
+definition rotr_fun {n : nat} (m : nat) (f : seq A n) : seq A n := f ∘ (rotr m)
+
+lemma rotl_seq_zero {n : nat} : rotl_fun 0 = @id (seq A n) :=
+funext take f, begin rewrite [↑rotl_fun, rotl_zero] end
+
+lemma rotl_seq_ne_id : ∀ {n : nat}, (∃ a b : A, a ≠ b) → ∀ i, i < n → rotl_fun (succ i) ≠ (@id (seq A (succ n)))
+| 0        := assume Pex, take i, assume Piltn, absurd Piltn !not_lt_zero
+| (succ n) := assume Pex, obtain a b Pne, from Pex, take i, assume Pilt,
+  let f := (λ j : fin (succ (succ n)), if j = zero (succ n) then a else b),
+      fi := mk_mod (succ n) (succ i) in
+  have Pfne : rotl_fun (succ i) f fi ≠ f fi,
+    from begin rewrite [↑rotl_fun, rotl_to_zero, mk_mod_of_lt (succ_lt_succ Pilt), if_pos rfl, if_neg mk_succ_ne_zero], assumption end,
+  have P : rotl_fun (succ i) f ≠ f, from
+    assume Peq, absurd (congr_fun Peq fi) Pfne,
+  assume Peq, absurd (congr_fun Peq f) P
+
+lemma rotr_rotl_fun {n : nat} (m : nat) (f : seq A n) : rotr_fun m (rotl_fun m f) = f :=
+calc f ∘ (rotl m) ∘ (rotr m) = f ∘ ((rotl m) ∘ (rotr m)) : compose.assoc
+                         ... = f ∘ id : {rotl_rotr m}
+
+lemma rotl_fun_inj {n : nat} {m : nat} : @injective (seq A n) (seq A n) (rotl_fun m) :=
+injective_of_has_left_inverse (exists.intro (rotr_fun m) (rotr_rotl_fun m))
+
+lemma seq_rotl_eq_list_rotl {n : nat} (f : seq A n) :
+  fun_to_list (rotl_fun 1 f) = list.rotl (fun_to_list f) :=
+begin
+  rewrite [↑fun_to_list, ↑rotl_fun, -map_map, rotl_map],
+  congruence, exact rotl_eq_rotl
+end
+
+end rot
+
+section rotg
+open nat fin fintype
+
+definition rotl_perm [reducible] (A : Type) [finA : fintype A] [deceqA : decidable_eq A] (n : nat) (m : nat) : perm (seq A n) :=
+perm.mk (rotl_fun m) rotl_fun_inj
+
+variable {A : Type}
+variable [finA : fintype A]
+include finA
+variable [deceqA : decidable_eq A]
+include deceqA
+
+variable {n : nat}
+
+lemma rotl_perm_mul {i j : nat} : (rotl_perm A n i) * (rotl_perm A n j) = rotl_perm A n (j+i) :=
+eq_of_feq (funext take f, calc
+  f ∘ (rotl j) ∘ (rotl i) = f ∘ ((rotl j) ∘ (rotl i)) : compose.assoc
+                      ... = f ∘ (rotl (j+i)) : rotl_compose)
+
+lemma rotl_perm_pow_eq : ∀ {i : nat}, (rotl_perm A n 1) ^ i = rotl_perm A n i
+| 0 := begin rewrite [pow_zero, ↑rotl_perm, perm_one, -eq_iff_feq], esimp, rewrite rotl_seq_zero  end
+| (succ i) := begin rewrite [pow_succ, rotl_perm_pow_eq, rotl_perm_mul, one_add] end
+
+lemma rotl_perm_pow_eq_one : (rotl_perm A n 1) ^ n = 1 :=
+eq.trans rotl_perm_pow_eq (eq_of_feq begin esimp [rotl_perm], rewrite [↑rotl_fun, rotl_id] end)
+
+lemma rotl_perm_mod {i : nat} : rotl_perm A n i = rotl_perm A n (i mod n) :=
+calc rotl_perm A n i = (rotl_perm A n 1) ^ i : rotl_perm_pow_eq
+                 ... = (rotl_perm A n 1) ^ (i mod n) : pow_mod rotl_perm_pow_eq_one
+                 ... = rotl_perm A n (i mod n) : rotl_perm_pow_eq
+
+-- needs A to have at least two elements!
+lemma rotl_perm_pow_ne_one (Pex : ∃ a b : A, a ≠ b) : ∀ i, i < n → (rotl_perm A (succ n) 1)^(succ i) ≠ 1 :=
+take i, assume Piltn, begin
+  intro P, revert P, rewrite [rotl_perm_pow_eq, -eq_iff_feq, perm_one, *perm.f_mk],
+  intro P, exact absurd P (rotl_seq_ne_id Pex i Piltn)
+end
+
+lemma rotl_perm_order (Pex : ∃ a b : A, a ≠ b) : order (rotl_perm A (succ n) 1) = (succ n) :=
+order_of_min_pow rotl_perm_pow_eq_one (rotl_perm_pow_ne_one Pex)
+
+end rotg
+end group

library/theories/group_theory/finsubg.lean

@@ -0,0 +1,535 @@
+/-
+Copyright (c) 2015 Haitao Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author : Haitao Zhang
+-/
+
+-- develop the concept of finite subgroups based on finsets so that the properties
+-- can be used directly without translating from the set based theory first
+
+import data algebra.group .subgroup
+open function algebra finset
+-- ⁻¹ in eq.ops conflicts with group ⁻¹
+open eq.ops
+
+namespace group
+open ops
+
+section subg
+-- we should be able to prove properties using finsets directly
+variable {G : Type}
+variable [ambientG : group G]
+include ambientG
+
+definition finset_mul_closed_on [reducible] (H : finset G) : Prop :=
+           ∀ x y : G, x ∈ H → y ∈ H → x * y ∈ H
+definition finset_has_inv (H : finset G) : Prop :=
+           ∀ a : G, a ∈ H → a⁻¹ ∈ H
+
+structure is_finsubg [class] (H : finset G) : Type :=
+          (has_one : 1 ∈ H)
+          (mul_closed : finset_mul_closed_on H)
+          (has_inv : finset_has_inv H)
+
+definition univ_is_finsubg [instance] [finG : fintype G] : is_finsubg (@finset.univ G _) :=
+is_finsubg.mk !mem_univ (λ x y Px Py, !mem_univ) (λ a Pa, !mem_univ)
+
+definition one_is_finsubg [instance] : is_finsubg (singleton (1:G)) :=
+is_finsubg.mk !mem_singleton
+  (λ x y Px Py, by rewrite [eq_of_mem_singleton Px, eq_of_mem_singleton Py, one_mul]; apply mem_singleton)
+  (λ x Px, by rewrite [eq_of_mem_singleton Px, one_inv]; apply mem_singleton)
+
+lemma finsubg_has_one (H : finset G) [h : is_finsubg H] : 1 ∈ H :=
+      @is_finsubg.has_one G _ H h
+lemma finsubg_mul_closed (H : finset G) [h : is_finsubg H] {x y : G} : x ∈ H → y ∈ H → x * y ∈ H :=
+      @is_finsubg.mul_closed G _ H h x y
+lemma finsubg_has_inv (H : finset G) [h : is_finsubg H] {a : G} :  a ∈ H → a⁻¹ ∈ H :=
+      @is_finsubg.has_inv G _ H h a
+
+variable [deceqG : decidable_eq G]
+include deceqG
+
+definition finsubg_to_subg [instance] {H : finset G} [h : is_finsubg H]
+         : is_subgroup (ts H) :=
+           is_subgroup.mk
+           (mem_eq_mem_to_set H 1 ▸ finsubg_has_one H)
+           (take x y, begin repeat rewrite -mem_eq_mem_to_set,
+             apply finsubg_mul_closed H end)
+           (take a, begin repeat rewrite -mem_eq_mem_to_set,
+             apply finsubg_has_inv H end)
+
+open nat
+lemma finsubg_eq_singleton_one_of_card_one {H : finset G} [h : is_finsubg H] :
+  card H = 1 → H = singleton 1 :=
+assume Pcard, eq.symm (eq_of_card_eq_of_subset (by rewrite [Pcard])
+  (subset_of_forall take g,
+    by rewrite [mem_singleton_eq]; intro Pg; rewrite Pg; exact finsubg_has_one H))
+
+end subg
+
+section fin_lcoset
+
+open set
+
+variable {A : Type}
+variable [deceq : decidable_eq A]
+include deceq
+variable [s : group A]
+include s
+
+definition fin_lcoset (H : finset A) (a : A) := finset.image (lmul_by a) H
+
+definition fin_rcoset (H : finset A) (a : A) : finset A := image (rmul_by a) H
+
+definition fin_lcosets (H G : finset A) := image (fin_lcoset H) G
+
+definition fin_inv : finset A → finset A := image has_inv.inv
+
+variable {H : finset A}
+
+lemma lmul_rmul {a b : A} : (lmul_by a) ∘ (rmul_by b) = (rmul_by b) ∘ (lmul_by a) :=
+funext take c, calc a*(c*b) = (a*c)*b : mul.assoc
+
+lemma fin_lrcoset_comm {a b : A} :
+  fin_lcoset (fin_rcoset H b) a = fin_rcoset (fin_lcoset H a) b :=
+by esimp [fin_lcoset, fin_rcoset]; rewrite [-*image_compose, lmul_rmul]
+
+lemma inv_mem_fin_inv {a : A} : a ∈ H → a⁻¹ ∈ fin_inv H :=
+assume Pin, mem_image_of_mem_of_eq Pin rfl
+
+lemma fin_lcoset_eq (a : A) : ts (fin_lcoset H a) = a ∘> (ts H) := calc
+      ts (fin_lcoset H a) = coset.l a (ts H) : to_set_image
+      ... = a ∘> (ts H) : glcoset_eq_lcoset
+
+lemma fin_lcoset_id : fin_lcoset H 1 = H :=
+by rewrite [eq_eq_to_set_eq, fin_lcoset_eq, glcoset_id]
+
+lemma fin_lcoset_compose (a b : A) : fin_lcoset (fin_lcoset H b) a = fin_lcoset H (a*b) :=
+to_set.inj (by rewrite [*fin_lcoset_eq, glcoset_compose])
+
+lemma fin_lcoset_inv (a : A) : fin_lcoset (fin_lcoset H a) a⁻¹ = H :=
+to_set.inj (by rewrite [*fin_lcoset_eq, glcoset_inv])
+
+lemma fin_lcoset_card (a : A) : card (fin_lcoset H a) = card H :=
+      card_image_eq_of_inj_on (lmul_inj_on a (ts H))
+lemma fin_lcosets_card_eq {G : finset A} : ∀ gH, gH ∈ fin_lcosets H G → card gH = card H :=
+      take gH, assume Pcosets, obtain g Pg, from exists_of_mem_image Pcosets,
+      and.right Pg ▸ fin_lcoset_card g
+
+variable [is_finsubgH : is_finsubg H]
+include is_finsubgH
+
+lemma fin_lcoset_same (x a : A) : x ∈ (fin_lcoset H a) = (fin_lcoset H x = fin_lcoset H a) :=
+      begin
+        rewrite mem_eq_mem_to_set,
+        rewrite [eq_eq_to_set_eq, *(fin_lcoset_eq x), fin_lcoset_eq a],
+        exact (subg_lcoset_same x a)
+      end
+lemma fin_mem_lcoset (g : A) : g ∈ fin_lcoset H g :=
+      have P : g ∈ g ∘> ts H, from and.left (subg_in_coset_refl g),
+      assert P1 : g ∈ ts (fin_lcoset H g), from eq.symm (fin_lcoset_eq g) ▸ P,
+      eq.symm (mem_eq_mem_to_set _ g) ▸ P1
+lemma fin_lcoset_subset {S : finset A} (Psub : S ⊆ H) : ∀ x, x ∈ H → fin_lcoset S x ⊆ H :=
+      assert Psubs : set.subset (ts S) (ts H), from subset_eq_to_set_subset S H ▸ Psub,
+      take x, assume Pxs : x ∈ ts H,
+      assert Pcoset : set.subset (x ∘> ts S) (ts H), from subg_lcoset_subset_subg Psubs x Pxs,
+      by rewrite [subset_eq_to_set_subset, fin_lcoset_eq x]; exact Pcoset
+
+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
+
+lemma finsubg_inv_lcoset_eq_rcoset {a : A} :
+  fin_inv (fin_lcoset H a) = fin_rcoset H a⁻¹ :=
+begin
+  esimp [fin_inv, fin_lcoset, fin_rcoset],
+  rewrite [-image_compose],
+  apply ext, intro b,
+  rewrite [*mem_image_iff, ↑compose, ↑lmul_by, ↑rmul_by],
+  apply iff.intro,
+    intro Pl, cases Pl with h Ph, cases Ph with Pin Peq,
+    existsi h⁻¹, apply and.intro,
+      exact finsubg_has_inv H Pin,
+      rewrite [-mul_inv, Peq],
+    intro Pr, cases Pr with h Ph, cases Ph with Pin Peq,
+    existsi h⁻¹, apply and.intro,
+      exact finsubg_has_inv H Pin,
+      rewrite [mul_inv, inv_inv, Peq],
+end
+
+lemma finsubg_conj_closed {g h : A} : g ∈ H → h ∈ H → g ∘c h ∈ H :=
+assume Pgin Phin, finsubg_mul_closed H (finsubg_mul_closed H Pgin Phin) (finsubg_has_inv H Pgin)
+
+variable {G : finset A}
+variable [is_finsubgG : is_finsubg G]
+include is_finsubgG
+
+open finset.partition
+
+definition fin_lcoset_partition_subg (Psub : H ⊆ G) :=
+      partition.mk G (fin_lcoset H) fin_lcoset_same
+        (restriction_imp_union (fin_lcoset H) fin_lcoset_same (fin_lcoset_subset Psub))
+
+open nat
+
+theorem lagrange_theorem (Psub : H ⊆ G) : card G = card (fin_lcosets H G) * card H := calc
+        card G = nat.Sum (fin_lcosets H G) card : class_equation (fin_lcoset_partition_subg Psub)
+        ... = nat.Sum (fin_lcosets H G) (λ x, card H) : nat.Sum_ext (take g P, fin_lcosets_card_eq g P)
+        ... = card (fin_lcosets H G) * card H : Sum_const_eq_card_mul
+
+end fin_lcoset
+
+section
+open fintype list subtype
+
+lemma dinj_tag {A : Type} (P : A → Prop) : dinj P tag :=
+take a₁ a₂ Pa₁ Pa₂ Pteq, subtype.no_confusion Pteq (λ Pe Pqe, Pe)
+
+open nat
+
+lemma card_pos {A : Type} [ambientA : group A] [finA : fintype A] : 0 < card A :=
+  length_pos_of_mem (mem_univ 1)
+
+end
+
+section lcoset_fintype
+open fintype list subtype
+
+variables {A : Type} [ambientA : group A] [finA : fintype A] [deceqA : decidable_eq A]
+include ambientA deceqA finA
+
+variables G H : finset A
+
+definition is_fin_lcoset [reducible] (S : finset A) : Prop :=
+  ∃ g, g ∈ G ∧ fin_lcoset H g = S
+
+definition to_list : list A := list.filter (λ g, g ∈ G) (elems A)
+
+definition list_lcosets : list (finset A) := erase_dup (map (fin_lcoset H) (to_list G))
+
+definition lcoset_type [reducible] : Type := {S : finset A | is_fin_lcoset G H S}
+
+definition all_lcosets : list (lcoset_type G H) :=
+dmap (is_fin_lcoset G H) tag (list_lcosets G H)
+
+variables {G H} [finsubgG : is_finsubg G]
+
+include finsubgG
+
+lemma self_is_lcoset : is_fin_lcoset G H H :=
+exists.intro 1 (and.intro !finsubg_has_one fin_lcoset_id)
+
+lemma lcoset_subset_of_subset (J : lcoset_type G H) : H ⊆ G → elt_of J ⊆ G :=
+assume Psub, obtain j Pjin Pj, from has_property J,
+by rewrite [-Pj]; apply fin_lcoset_subset Psub; exact Pjin
+
+variables (G H)
+
+definition lcoset_one : lcoset_type G H := tag H self_is_lcoset
+
+variables {G H}
+
+definition lcoset_lmul {g : A} (Pgin : g ∈ G) (S : lcoset_type G H)
+  : lcoset_type G H :=
+tag (fin_lcoset (elt_of S) g)
+  (obtain f Pfin Pf, from has_property S,
+  exists.intro (g*f)
+    (by apply and.intro;
+      exact finsubg_mul_closed G Pgin Pfin;
+      rewrite [-Pf, -fin_lcoset_compose]))
+
+definition lcoset_mul (S₁ S₂ : lcoset_type G H): finset A :=
+Union (elt_of S₁) (fin_lcoset (elt_of S₂))
+
+lemma mul_mem_lcoset_mul (J K : lcoset_type G H) {g h} :
+  g ∈ elt_of J → h ∈ elt_of K → g*h ∈ lcoset_mul J K :=
+assume Pg, begin
+  rewrite [↑lcoset_mul, mem_Union_iff, ↑fin_lcoset],
+  intro Ph, existsi g, apply and.intro, exact Pg,
+  rewrite [mem_image_iff, ↑lmul_by],
+  existsi h, exact and.intro Ph rfl
+end
+
+lemma is_lcoset_of_mem_list_lcosets {S : finset A}
+  : S ∈ list_lcosets G H → is_fin_lcoset G H S :=
+assume Pin, obtain g Pgin Pg, from exists_of_mem_map (mem_of_mem_erase_dup Pin),
+exists.intro g (and.intro (of_mem_filter Pgin) Pg)
+
+lemma mem_list_lcosets_of_is_lcoset {S : finset A}
+  : is_fin_lcoset G H S → S ∈ list_lcosets G H :=
+assume Plcoset, obtain g Pgin Pg, from Plcoset,
+Pg ▸ mem_erase_dup (mem_map _ (mem_filter_of_mem (complete g) Pgin))
+
+lemma fin_lcosets_eq :
+  fin_lcosets H G = to_finset_of_nodup (list_lcosets G H) !nodup_erase_dup :=
+ext (take S, iff.intro
+  (λ Pimg, mem_list_lcosets_of_is_lcoset (exists_of_mem_image Pimg))
+  (λ Pl, obtain g Pg, from is_lcoset_of_mem_list_lcosets Pl,
+    iff.elim_right !mem_image_iff (is_lcoset_of_mem_list_lcosets Pl)))
+
+lemma length_all_lcosets : length (all_lcosets G H) = card (fin_lcosets H G) :=
+eq.trans
+  (show length (all_lcosets G H) = length (list_lcosets G H), from
+    assert Pmap : map elt_of (all_lcosets G H) = list_lcosets G H, from
+      map_dmap_of_inv_of_pos (λ S P, rfl) (λ S, is_lcoset_of_mem_list_lcosets),
+    by rewrite[-Pmap, length_map])
+  (by rewrite fin_lcosets_eq)
+
+lemma lcoset_lmul_compose {f g : A} (Pf : f ∈ G) (Pg : g ∈ G) (S : lcoset_type G H) :
+lcoset_lmul Pf (lcoset_lmul Pg S) = lcoset_lmul (finsubg_mul_closed G Pf Pg) S :=
+subtype.eq !fin_lcoset_compose
+
+lemma lcoset_lmul_one (S : lcoset_type G H) : lcoset_lmul !finsubg_has_one S = S :=
+subtype.eq fin_lcoset_id
+
+lemma lcoset_lmul_inv {g : A} {Pg : g ∈ G} (S : lcoset_type G H) :
+  lcoset_lmul (finsubg_has_inv G Pg) (lcoset_lmul Pg S) = S :=
+subtype.eq (to_set.inj begin
+ esimp [lcoset_lmul],
+ rewrite [fin_lcoset_compose, mul.left_inv, fin_lcoset_eq, glcoset_id]
+end)
+
+lemma lcoset_lmul_inj {g : A} {Pg : g ∈ G}:
+  @injective (lcoset_type G H) _ (lcoset_lmul Pg) :=
+injective_of_has_left_inverse (exists.intro (lcoset_lmul (finsubg_has_inv G Pg)) lcoset_lmul_inv)
+
+lemma card_elt_of_lcoset_type (S : lcoset_type G H) : card (elt_of S) = card H :=
+obtain f Pfin Pf, from has_property S, Pf ▸ fin_lcoset_card f
+
+definition lcoset_fintype [instance] : fintype (lcoset_type G H) :=
+fintype.mk (all_lcosets G H)
+  (dmap_nodup_of_dinj (dinj_tag (is_fin_lcoset G H)) !nodup_erase_dup)
+  (take s, subtype.destruct s (take S, assume PS, mem_dmap PS (mem_list_lcosets_of_is_lcoset PS)))
+
+lemma card_lcoset_type : card (lcoset_type G H) = card (fin_lcosets H G) :=
+length_all_lcosets
+
+open nat
+variable [finsubgH : is_finsubg H]
+include finsubgH
+
+theorem lagrange_theorem' (Psub : H ⊆ G) : card G = card (lcoset_type G H) * card H :=
+calc card G = card (fin_lcosets H G) * card H : lagrange_theorem Psub
+        ... = card (lcoset_type G H) * card H : card_lcoset_type
+
+lemma lcoset_disjoint {S₁ S₂ : lcoset_type G H} : S₁ ≠ S₂ → elt_of S₁ ∩ elt_of S₂ = ∅ :=
+obtain f₁ Pfin₁ Pf₁, from has_property S₁,
+obtain f₂ Pfin₂ Pf₂, from has_property S₂,
+assume Pne, inter_eq_empty_of_disjoint (disjoint.intro
+  take g, begin
+  rewrite [-Pf₁, -Pf₂, *fin_lcoset_same],
+  intro Pgf₁, rewrite [Pgf₁, Pf₁, Pf₂],
+  intro Peq, exact absurd (subtype.eq Peq) Pne
+  end )
+
+lemma card_Union_lcosets (lcs : finset (lcoset_type G H)) :
+  card (Union lcs elt_of) = card lcs * card H :=
+calc card (Union lcs elt_of) = ∑ lc ∈ lcs, card (elt_of lc) : card_Union_of_disjoint lcs elt_of (λ (S₁ S₂ : lcoset_type G H) P₁ P₂ Pne, lcoset_disjoint Pne)
+                         ... = ∑ lc ∈ lcs, card H : Sum_ext (take lc P, card_elt_of_lcoset_type _)
+                         ... = card lcs * card H : Sum_const_eq_card_mul
+
+lemma exists_of_lcoset_type (J : lcoset_type G H) :
+  ∃ j, j ∈ elt_of J ∧ fin_lcoset H j = elt_of J :=
+obtain j Pjin Pj, from has_property J,
+exists.intro j (and.intro (Pj ▸ !fin_mem_lcoset) Pj)
+
+lemma lcoset_not_empty (J : lcoset_type G H) : elt_of J ≠ ∅ :=
+obtain j Pjin Pj, from has_property J,
+assume Pempty, absurd (by rewrite [-Pempty, -Pj]; apply fin_mem_lcoset) (not_mem_empty j)
+
+end lcoset_fintype
+
+section normalizer
+open subtype
+
+variables {G : Type} [ambientG : group G] [finG : fintype G] [deceqG : decidable_eq G]
+include ambientG deceqG finG
+
+variable H : finset G
+
+definition normalizer : finset G := {g ∈ univ | ∀ h, h ∈ H → g ∘c h ∈ H}
+
+variable {H}
+
+variable [finsubgH : is_finsubg H]
+include finsubgH
+
+lemma subset_normalizer : H ⊆ normalizer H :=
+subset_of_forall take g, assume PginH, mem_filter_of_mem !mem_univ
+  (take h, assume PhinH, finsubg_conj_closed PginH PhinH)
+
+lemma normalizer_has_one : 1 ∈ normalizer H :=
+mem_of_subset_of_mem subset_normalizer (finsubg_has_one H)
+
+lemma normalizer_mul_closed : finset_mul_closed_on (normalizer H) :=
+take f g, assume Pfin Pgin,
+mem_filter_of_mem !mem_univ take h, assume Phin, begin
+  rewrite [-conj_compose],
+  apply of_mem_filter Pfin,
+  apply of_mem_filter Pgin,
+  exact Phin
+end
+
+lemma conj_eq_of_mem_normalizer {g : G} : g ∈ normalizer H → image (conj_by g) H = H :=
+assume Pgin,
+eq_of_card_eq_of_subset (card_image_eq_of_inj_on (take h j, assume P1 P2, !conj_inj))
+  (subset_of_forall take h, assume Phin,
+  obtain j Pjin Pj, from exists_of_mem_image Phin,
+  begin substvars, apply of_mem_filter Pgin, exact Pjin end)
+
+lemma normalizer_has_inv : finset_has_inv (normalizer H) :=
+take g, assume Pgin,
+mem_filter_of_mem !mem_univ take h, begin
+  rewrite [-(conj_eq_of_mem_normalizer Pgin) at {1}, mem_image_iff],
+  intro Pex, cases Pex with k Pk,
+  rewrite [-(and.right Pk), conj_compose, mul.left_inv, conj_id],
+  exact and.left Pk
+end
+
+definition normalizer_is_finsubg [instance] : is_finsubg (normalizer H) :=
+is_finsubg.mk normalizer_has_one normalizer_mul_closed normalizer_has_inv
+
+lemma lcoset_subset_normalizer (J : lcoset_type (normalizer H) H) :
+  elt_of J ⊆ normalizer H :=
+lcoset_subset_of_subset J subset_normalizer
+
+lemma lcoset_subset_normalizer_of_mem {g : G} :
+  g ∈ normalizer H → fin_lcoset H g ⊆ normalizer H :=
+assume Pgin, fin_lcoset_subset subset_normalizer g Pgin
+
+lemma lrcoset_same_of_mem_normalizer {g : G} :
+  g ∈ normalizer H → fin_lcoset H g = fin_rcoset H g :=
+assume Pg, ext take h, iff.intro
+  (assume Pl, obtain j Pjin Pj, from exists_of_mem_image Pl,
+  mem_image_of_mem_of_eq (of_mem_filter Pg j Pjin)
+    (calc g*j*g⁻¹*g = g*j : inv_mul_cancel_right
+                ... = h   : Pj))
+  (assume Pr, obtain j Pjin Pj, from exists_of_mem_image Pr,
+  mem_image_of_mem_of_eq (of_mem_filter (finsubg_has_inv (normalizer H) Pg) j Pjin)
+    (calc g*(g⁻¹*j*g⁻¹⁻¹) = g*(g⁻¹*j*g)   : inv_inv
+                      ... = g*(g⁻¹*(j*g)) : mul.assoc
+                      ... = j*g           : mul_inv_cancel_left
+                      ... = h             : Pj))
+
+lemma lcoset_mul_eq_lcoset (J K : lcoset_type (normalizer H) H) {g : G} :
+  g ∈ elt_of J → (lcoset_mul J K) = fin_lcoset (elt_of K) g :=
+assume Pgin,
+obtain j Pjin Pj, from has_property J,
+obtain k Pkin Pk, from has_property K,
+Union_const (lcoset_not_empty J) begin
+  rewrite [-Pk], intro h Phin,
+  assert Phinn : h ∈ normalizer H,
+    apply mem_of_subset_of_mem (lcoset_subset_normalizer_of_mem Pjin),
+    rewrite Pj, assumption,
+  revert Phin Pgin,
+  rewrite [-Pj, *fin_lcoset_same],
+  intro Pheq Pgeq,
+  rewrite [*(lrcoset_same_of_mem_normalizer Pkin), *fin_lrcoset_comm, Pheq, Pgeq]
+end
+
+lemma lcoset_mul_is_lcoset (J K : lcoset_type (normalizer H) H) :
+  is_fin_lcoset (normalizer H) H (lcoset_mul J K) :=
+obtain j Pjin Pj, from has_property J,
+obtain k Pkin Pk, from has_property K,
+exists.intro (j*k) (and.intro (finsubg_mul_closed _ Pjin Pkin)
+  begin rewrite [lcoset_mul_eq_lcoset J K (Pj ▸ fin_mem_lcoset j), -fin_lcoset_compose, Pk] end)
+
+lemma lcoset_inv_is_lcoset (J : lcoset_type (normalizer H) H) :
+  is_fin_lcoset (normalizer H) H (fin_inv (elt_of J)) :=
+obtain j Pjin Pj, from has_property J, exists.intro j⁻¹
+begin
+  rewrite [-Pj, finsubg_inv_lcoset_eq_rcoset],
+  apply and.intro,
+    apply normalizer_has_inv, assumption,
+    apply lrcoset_same_of_mem_normalizer, apply normalizer_has_inv, assumption
+end
+
+definition fin_coset_mul (J K : lcoset_type (normalizer H) H) : lcoset_type (normalizer H) H :=
+tag (lcoset_mul J K) (lcoset_mul_is_lcoset J K)
+
+definition fin_coset_inv (J : lcoset_type (normalizer H) H) : lcoset_type (normalizer H) H :=
+tag (fin_inv (elt_of J)) (lcoset_inv_is_lcoset J)
+
+definition fin_coset_one : lcoset_type (normalizer H) H :=
+tag H self_is_lcoset
+
+local infix `^` := fin_coset_mul
+
+lemma fin_coset_mul_eq_lcoset (J K : lcoset_type (normalizer H) H) {g : G} :
+  g ∈ (elt_of J) → elt_of (J ^ K) = fin_lcoset (elt_of K) g :=
+assume Pgin, lcoset_mul_eq_lcoset J K Pgin
+
+lemma fin_coset_mul_assoc (J K L : lcoset_type (normalizer H) H) :
+  J ^ K ^ L = J ^ (K ^ L) :=
+obtain j Pjin Pj, from exists_of_lcoset_type J,
+obtain k Pkin Pk, from exists_of_lcoset_type K,
+assert Pjk : j*k ∈ elt_of (J ^ K), from mul_mem_lcoset_mul J K Pjin Pkin,
+obtain l Plin Pl, from has_property L,
+subtype.eq (begin
+  rewrite [fin_coset_mul_eq_lcoset (J ^ K) _ Pjk,
+    fin_coset_mul_eq_lcoset J _ Pjin,
+    fin_coset_mul_eq_lcoset K _ Pkin,
+    -Pl, *fin_lcoset_compose]
+  end)
+
+lemma fin_coset_mul_one (J : lcoset_type (normalizer H) H) :
+  J ^ fin_coset_one = J :=
+obtain j Pjin Pj, from exists_of_lcoset_type J,
+subtype.eq begin
+  rewrite [↑fin_coset_one, fin_coset_mul_eq_lcoset _ _ Pjin, -Pj]
+end
+
+lemma fin_coset_one_mul (J : lcoset_type (normalizer H) H) :
+  fin_coset_one ^ J = J :=
+subtype.eq begin
+  rewrite [↑fin_coset_one, fin_coset_mul_eq_lcoset _ _ (finsubg_has_one H), fin_lcoset_id]
+end
+
+lemma fin_coset_left_inv (J : lcoset_type (normalizer H) H) :
+  (fin_coset_inv J) ^ J = fin_coset_one :=
+obtain j Pjin Pj, from exists_of_lcoset_type J,
+assert Pjinv : j⁻¹ ∈ elt_of (fin_coset_inv J), from inv_mem_fin_inv Pjin,
+subtype.eq begin
+  rewrite [↑fin_coset_one, fin_coset_mul_eq_lcoset _ _ Pjinv, -Pj, fin_lcoset_inv]
+end
+
+variable (H)
+
+definition fin_coset_group [instance] : group (lcoset_type (normalizer H) H) :=
+group.mk fin_coset_mul fin_coset_mul_assoc fin_coset_one fin_coset_one_mul fin_coset_mul_one fin_coset_inv fin_coset_left_inv
+
+variables {H} (Hc : finset (lcoset_type (normalizer H) H))
+
+definition fin_coset_Union : finset G := Union Hc elt_of
+
+variables {Hc} [finsubgHc : is_finsubg Hc]
+include finsubgHc
+
+lemma mem_normalizer_of_mem_fcU {j : G} : j ∈ fin_coset_Union Hc → j ∈ normalizer H :=
+assume Pjin, obtain J PJ PjJ, from iff.elim_left !mem_Union_iff Pjin,
+mem_of_subset_of_mem !lcoset_subset_normalizer PjJ
+
+lemma fcU_has_one : (1:G) ∈ fin_coset_Union Hc :=
+iff.elim_right (mem_Union_iff Hc elt_of (1:G))
+  (exists.intro 1 (and.intro (finsubg_has_one Hc) (finsubg_has_one H)))
+
+lemma fcU_has_inv : finset_has_inv (fin_coset_Union Hc) :=
+take j, assume Pjin, obtain J PJ PjJ, from iff.elim_left !mem_Union_iff Pjin,
+have PJinv : J⁻¹ ∈ Hc, from finsubg_has_inv Hc PJ,
+have Pjinv : j⁻¹ ∈ elt_of J⁻¹, from inv_mem_fin_inv PjJ,
+iff.elim_right !mem_Union_iff (exists.intro J⁻¹ (and.intro PJinv Pjinv))
+
+lemma fcU_mul_closed : finset_mul_closed_on (fin_coset_Union Hc) :=
+take j k, assume Pjin Pkin,
+obtain J PJ PjJ, from iff.elim_left !mem_Union_iff Pjin,
+obtain K PK PkK, from iff.elim_left !mem_Union_iff Pkin,
+assert Pjk : j*k ∈ elt_of (J*K), from mul_mem_lcoset_mul J K PjJ PkK,
+iff.elim_right !mem_Union_iff
+  (exists.intro (J*K) (and.intro (finsubg_mul_closed Hc PJ PK) Pjk))
+
+definition fcU_is_finsubg [instance] : is_finsubg (fin_coset_Union Hc) :=
+is_finsubg.mk fcU_has_one fcU_mul_closed fcU_has_inv
+
+end normalizer
+
+end group

library/theories/group_theory/group_theory.md

@@ -0,0 +1,18 @@
+theories.group_theory
+=====================
+
+Group theory (especially finite group theory).
+
+[subgroup](subgroup.lean) : general subgroup theories, quotient group using quot
+
+[finsubg](finsubg.lean)   : finite subgroups (finset and fintype), Lagrange theorem, finite cosets and lcoset_type, normalizer for finite groups, coset product and quotient group based on lcoset_type, semidirect product
+
+[hom](hom.lean) 	  : homomorphism and isomorphism, kernel, first isomorphism theorem
+
+[perm](perm.lean)	  : permutation group
+
+[cyclic](cyclic.lean)	  : cyclic subgroup, finite generator, order of generator, sequence and rotation
+
+[action](action.lean)	  : fixed point, action, stabilizer, orbit stabilizer theorem, orbit partition, Cayley theorem, action on lcoset, cardinality of permutation group
+
+[pgroup](pgroup.lean)	  : subgroup with order of prime power, Cauchy theorem, first Sylow theorem

library/theories/group_theory/hom.lean

@@ -0,0 +1,196 @@
+/-
+Copyright (c) 2015 Haitao Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author : Haitao Zhang
+-/
+import algebra.group data.set .subgroup
+
+namespace group
+
+open algebra
+-- ⁻¹ in eq.ops conflicts with group ⁻¹
+-- open eq.ops
+notation H1 ▸ H2 := eq.subst H1 H2
+open set
+open function
+open group.ops
+open quot
+local attribute set [reducible]
+
+section defs
+
+variables {A B : Type}
+variable [s1 : group A]
+variable [s2 : group B]
+include s1
+include s2
+
+-- the Prop of being hom
+definition homomorphic [reducible] (f : A → B) : Prop := ∀ a b, f (a*b) = (f a)*(f b)
+-- type class for inference
+structure is_hom_class [class] (f : A → B) : Type :=
+          (is_hom : homomorphic f)
+-- the proof of hom_prop if the class can be inferred
+definition is_hom (f : A → B) [h : is_hom_class f] : homomorphic f :=
+           @is_hom_class.is_hom A B s1 s2 f h
+
+definition ker (f : A → B) [h : is_hom_class f] : set A := {a : A | f a = 1}
+check @ker
+
+definition isomorphic (f : A → B) := injective f ∧ homomorphic f
+structure is_iso_class [class] (f : A → B) extends is_hom_class f : Type :=
+          (inj : injective f)
+lemma iso_is_inj (f : A → B) [h : is_iso_class f] : injective f:=
+      @is_iso_class.inj A B s1 s2 f h
+lemma iso_is_iso (f : A → B) [h : is_iso_class f] : isomorphic f:=
+      and.intro (iso_is_inj f) (is_hom f)
+
+end defs
+
+section
+variables {A B : Type}
+variable [s1 : group A]
+
+definition id_is_iso [instance] : @is_hom_class A A s1 s1 (@id A) :=
+is_iso_class.mk (take a b, rfl) injective_id
+
+variable [s2 : group B]
+include s1
+include s2
+
+variable f : A → B
+
+variable [h : is_hom_class f]
+include h
+
+theorem hom_map_one : f 1 = 1 :=
+        have P : f 1 = (f 1) * (f 1), from
+        calc f 1 = f (1*1) : mul_one
+        ... = (f 1) * (f 1) : is_hom f,
+        eq.symm (mul.right_inv (f 1) ▸ (mul_inv_eq_of_eq_mul P))
+
+theorem hom_map_inv (a : A) : f a⁻¹ = (f a)⁻¹ :=
+        assert P : f 1 = 1, from hom_map_one f,
+        assert P1 : f (a⁻¹ * a) = 1, from (eq.symm (mul.left_inv a)) ▸ P,
+        assert P2 : (f a⁻¹) * (f a) = 1, from (is_hom f a⁻¹ a) ▸ P1,
+        assert P3 : (f a⁻¹) * (f a) = (f a)⁻¹ * (f a), from eq.symm (mul.left_inv (f a)) ▸ P2,
+        mul_right_cancel P3
+
+theorem hom_map_mul_closed (H : set A) : mul_closed_on H → mul_closed_on (f '[H]) :=
+        assume Pclosed, assume b1, assume b2,
+        assume Pb1 : b1 ∈ f '[ H], assume Pb2 : b2 ∈ f '[ H],
+        obtain a1 (Pa1 : a1 ∈ H ∧ f a1 = b1), from Pb1,
+        obtain a2 (Pa2 : a2 ∈ H ∧ f a2 = b2), from Pb2,
+        assert Pa1a2 : a1 * a2 ∈ H, from Pclosed a1 a2 (and.left Pa1) (and.left Pa2),
+        assert Pb1b2 : f (a1 * a2) = b1 * b2, from calc
+        f (a1 * a2) = f a1 * f a2 : is_hom f a1 a2
+        ... = b1 * f a2 : {and.right Pa1}
+        ... = b1 * b2 : {and.right Pa2},
+        mem_image Pa1a2 Pb1b2
+
+lemma ker.has_one : 1 ∈ ker f := hom_map_one f
+
+lemma ker.has_inv : subgroup.has_inv (ker f) :=
+      take a, assume Pa : f a = 1, calc
+      f a⁻¹ = (f a)⁻¹ : by rewrite (hom_map_inv f)
+      ... = 1⁻¹ : by rewrite Pa
+      ... = 1 : by rewrite one_inv
+
+lemma ker.mul_closed : mul_closed_on (ker f) :=
+      take x y, assume (Px : f x = 1) (Py : f y = 1), calc
+      f (x*y) = (f x) * (f y) : by rewrite [is_hom f]
+      ... = 1 : by rewrite [Px, Py, mul_one]
+
+lemma ker.normal : same_left_right_coset (ker f) :=
+      take a, funext (assume x, begin
+      esimp [ker, set_of, glcoset, grcoset],
+      rewrite [*(is_hom f), mul_eq_one_iff_mul_eq_one (f a⁻¹) (f x)]
+      end)
+
+definition ker_is_normal_subgroup : is_normal_subgroup (ker f) :=
+  is_normal_subgroup.mk (ker.has_one f) (ker.mul_closed f) (ker.has_inv f)
+    (ker.normal f)
+
+-- additional subgroup variable
+variable {H : set A}
+variable [is_subgH : is_subgroup H]
+include is_subgH
+
+theorem hom_map_subgroup : is_subgroup (f '[H]) :=
+        have Pone : 1 ∈ f '[H], from mem_image subg_has_one (hom_map_one f),
+        have Pclosed : mul_closed_on (f '[H]), from hom_map_mul_closed f H subg_mul_closed,
+        assert Pinv : ∀ b, b ∈ f '[H] → b⁻¹ ∈ f '[H], from
+          assume b, assume Pimg,
+          obtain a (Pa : a ∈ H ∧ f a = b), from Pimg,
+          assert Painv : a⁻¹ ∈ H, from subg_has_inv a (and.left Pa),
+          assert Pfainv : (f a)⁻¹ ∈ f '[H], from mem_image Painv (hom_map_inv f a),
+          and.right Pa ▸ Pfainv,
+        is_subgroup.mk Pone Pclosed Pinv
+
+end
+
+section hom_theorem
+
+variables {A B : Type}
+variable [s1 : group A]
+variable [s2 : group B]
+include s1
+include s2
+
+variable {f : A → B}
+
+variable [h : is_hom_class f]
+include h
+
+definition ker_nsubg [instance] : is_normal_subgroup (ker f) :=
+           is_normal_subgroup.mk (ker.has_one f) (ker.mul_closed f)
+           (ker.has_inv f) (ker.normal f)
+
+definition quot_over_ker [instance] : group (coset_of (ker f)) := mk_quotient_group (ker f)
+-- under the wrap the tower of concepts collapse to a simple condition
+example (a x : A) : (x ∈ a ∘> ker f) = (f (a⁻¹*x) = 1) := rfl
+lemma ker_coset_same_val (a b : A): same_lcoset (ker f) a b → f a = f b :=
+      assume Psame,
+      assert Pin : f (b⁻¹*a) = 1, from subg_same_lcoset_in_lcoset a b Psame,
+      assert P : (f b)⁻¹ * (f a) = 1, from calc
+      (f b)⁻¹ * (f a) = (f b⁻¹) * (f a) :  (hom_map_inv f)
+      ... = f (b⁻¹*a) : by rewrite [is_hom f]
+      ... = 1 : by rewrite Pin,
+      eq.symm (inv_inv (f b) ▸ inv_eq_of_mul_eq_one P)
+
+definition ker_natural_map : (coset_of (ker f)) → B :=
+           quot.lift f ker_coset_same_val
+
+example (a : A) : ker_natural_map ⟦a⟧ = f a := rfl
+lemma ker_coset_hom (a b : A) :
+      ker_natural_map (⟦a⟧*⟦b⟧) = (ker_natural_map ⟦a⟧) * (ker_natural_map ⟦b⟧) := calc
+      ker_natural_map (⟦a⟧*⟦b⟧) = ker_natural_map ⟦a*b⟧ : rfl
+      ... = f (a*b) : rfl
+      ... = (f a) * (f b) : by rewrite [is_hom f]
+      ... = (ker_natural_map ⟦a⟧) * (ker_natural_map ⟦b⟧) : rfl
+
+lemma ker_map_is_hom : homomorphic (ker_natural_map : coset_of (ker f) → B) :=
+  take aK bK,
+      quot.ind (λ a, quot.ind (λ b, ker_coset_hom a b) bK) aK
+
+check @subg_in_lcoset_same_lcoset
+lemma ker_coset_inj (a b : A) : (ker_natural_map ⟦a⟧ = ker_natural_map ⟦b⟧) → ⟦a⟧ = ⟦b⟧ :=
+      assume Pfeq : f a = f b,
+      assert Painb : a ∈ b ∘> ker f, from calc
+      f (b⁻¹*a) = (f b⁻¹) * (f a) : by rewrite [is_hom f]
+      ... = (f b)⁻¹ * (f a)       : by rewrite (hom_map_inv f)
+      ... = (f a)⁻¹ * (f a)       : by rewrite Pfeq
+      ... = 1                     : by rewrite (mul.left_inv (f a)),
+      quot.sound (@subg_in_lcoset_same_lcoset _ _ (ker f) _ a b Painb)
+
+lemma ker_map_is_inj : injective (ker_natural_map : coset_of (ker f) → B) :=
+      take aK bK,
+      quot.ind (λ a, quot.ind (λ b, ker_coset_inj a b) bK) aK
+
+-- a special case of the fundamental homomorphism theorem or the first isomorphism theorem
+theorem first_isomorphism_theorem : isomorphic (ker_natural_map : coset_of (ker f) → B) :=
+        and.intro ker_map_is_inj ker_map_is_hom
+
+end hom_theorem
+end group

library/theories/group_theory/perm.lean

@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2015 Haitao Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author : Haitao Zhang
+-/
+import algebra.group data data.fintype.function
+
+open nat list algebra function
+
+namespace group
+open fintype
+
+section perm
+variable {A : Type}
+variable [finA : fintype A]
+include finA
+variable [deceqA : decidable_eq A]
+include deceqA
+variable {f : A → A}
+
+lemma perm_surj : injective f → surjective f :=
+      surj_of_inj_eq_card (eq.refl (card A))
+
+variable (perm : injective f)
+
+definition perm_inv : A → A :=
+      right_inv (perm_surj perm)
+
+lemma perm_inv_right : f ∘ (perm_inv perm) = id :=
+      right_inv_of_surj (perm_surj perm)
+
+lemma perm_inv_left : (perm_inv perm) ∘ f = id :=
+      have H : left_inverse f (perm_inv perm), from congr_fun (perm_inv_right perm),
+      funext (take x, right_inverse_of_injective_of_left_inverse perm H x)
+
+lemma perm_inv_inj : injective (perm_inv perm) :=
+      injective_of_has_left_inverse (exists.intro f (congr_fun (perm_inv_right perm)))
+
+end perm
+
+structure perm (A : Type) [h : fintype A] : Type :=
+  (f : A → A) (inj : injective f)
+local attribute perm.f [coercion]
+check perm.mk
+
+section perm
+variable {A : Type}
+variable [finA : fintype A]
+include finA
+
+lemma eq_of_feq : ∀ {p₁ p₂ : perm A}, (perm.f p₁) = p₂ → p₁ = p₂
+| (perm.mk f₁ P₁) (perm.mk f₂ P₂) := assume (feq : f₁ = f₂), by congruence; assumption
+
+lemma feq_of_eq : ∀ {p₁ p₂ : perm A}, p₁ = p₂ → (perm.f p₁) = p₂
+| (perm.mk f₁ P₁) (perm.mk f₂ P₂) := assume Peq,
+  have feq : f₁ = f₂, from perm.no_confusion Peq (λ Pe Pqe, Pe), feq
+
+lemma eq_iff_feq {p₁ p₂ : perm A} : (perm.f p₁) = p₂ ↔ p₁ = p₂ :=
+iff.intro eq_of_feq feq_of_eq
+
+lemma perm.f_mk {f : A → A} {Pinj : injective f} : perm.f (perm.mk f Pinj) = f := rfl
+
+definition move_by [reducible] (a : A) (f : perm A) : A := f a
+
+variable [deceqA : decidable_eq A]
+include deceqA
+
+lemma perm.has_decidable_eq [instance] : decidable_eq (perm A) :=
+      take f g,
+      perm.destruct f (λ ff finj, perm.destruct g (λ gf ginj,
+      decidable.rec_on (decidable_eq_fun ff gf)
+      (λ Peq, decidable.inl (by substvars))
+      (λ Pne, decidable.inr begin intro P, injection P, contradiction end)))
+
+lemma dinj_perm_mk : dinj (@injective A A) perm.mk :=
+      take a₁ a₂ Pa₁ Pa₂ Pmkeq, perm.no_confusion Pmkeq (λ Pe Pqe, Pe)
+
+definition all_perms : list (perm A) :=
+           dmap injective perm.mk (all_injs A)
+
+lemma nodup_all_perms : nodup (@all_perms A _ _) :=
+      dmap_nodup_of_dinj dinj_perm_mk nodup_all_injs
+
+lemma all_perms_complete : ∀ p : perm A, p ∈ all_perms :=
+      take p, perm.destruct p (take f Pinj,
+        assert Pin : f ∈ all_injs A, from all_injs_complete Pinj,
+        mem_dmap Pinj Pin)
+
+definition perm_is_fintype [instance] : fintype (perm A) :=
+           fintype.mk all_perms nodup_all_perms all_perms_complete
+
+definition perm.mul (f g : perm A) :=
+           perm.mk (f∘g) (injective_compose (perm.inj f) (perm.inj g))
+definition perm.one [reducible] : perm A := perm.mk id injective_id
+definition perm.inv (f : perm A) := let inj := perm.inj f in
+           perm.mk (perm_inv inj) (perm_inv_inj inj)
+
+local infix `^` := perm.mul
+lemma perm.assoc (f g h : perm A) : f ^ g ^ h = f ^ (g ^ h) := rfl
+lemma perm.one_mul (p : perm A) : perm.one ^ p = p :=
+      perm.cases_on p (λ f inj, rfl)
+lemma perm.mul_one (p : perm A) : p ^ perm.one = p :=
+      perm.cases_on p (λ f inj, rfl)
+lemma perm.left_inv (p : perm A) : (perm.inv p) ^ p = perm.one :=
+      begin rewrite [↑perm.one], generalize @injective_id A,
+      rewrite [-perm_inv_left (perm.inj p)], intros, exact rfl
+      end
+lemma perm.right_inv (p : perm A) : p ^ (perm.inv p) = perm.one :=
+      begin rewrite [↑perm.one], generalize @injective_id A,
+      rewrite [-perm_inv_right (perm.inj p)], intros, exact rfl
+      end
+
+definition perm_group [instance] : group (perm A) :=
+           group.mk perm.mul perm.assoc perm.one perm.one_mul perm.mul_one perm.inv perm.left_inv
+
+lemma perm_one : (1 : perm A) = perm.one := rfl
+
+end perm
+
+end group

library/theories/group_theory/pgroup.lean

@@ -0,0 +1,392 @@
+/-
+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_filter_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

library/theories/group_theory/subgroup.lean

@@ -0,0 +1,379 @@
+/-
+Copyright (c) 2015 Haitao Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author : Haitao Zhang
+-/
+import data algebra.group data
+open function eq.ops
+
+open set
+
+namespace algebra
+
+namespace coset
+-- semigroup coset definition
+section
+variable {A : Type}
+variable [s : semigroup A]
+include s
+definition lmul (a : A) := λ x, a * x
+definition rmul (a : A) := λ x, x * a
+definition l a (S : set A) := (lmul a) '[S]
+definition r a (S : set A) := (rmul a) '[S]
+lemma lmul_compose : ∀ (a b : A), (lmul a) ∘ (lmul b) = lmul (a*b) :=
+      take a, take b,
+      funext (assume x, by
+        rewrite [↑function.compose, ↑lmul, mul.assoc])
+lemma rmul_compose : ∀ (a b : A), (rmul a) ∘ (rmul b) = rmul (b*a) :=
+      take a, take b,
+      funext (assume x, by
+        rewrite [↑function.compose, ↑rmul, mul.assoc])
+lemma lcompose a b (S : set A) : l a (l b S) = l (a*b) S :=
+      calc (lmul a) '[(lmul b) '[S]] = ((lmul a) ∘ (lmul b)) '[S] : image_compose
+      ... = lmul (a*b) '[S] : lmul_compose
+lemma rcompose a b (S : set A) : r a (r b S) = r (b*a) S :=
+      calc (rmul a) '[(rmul b) '[S]] = ((rmul a) ∘ (rmul b)) '[S] : image_compose
+      ... = rmul (b*a) '[S] : rmul_compose
+lemma l_sub a (S H : set A) : S ⊆ H → (l a S) ⊆ (l a H) := image_subset (lmul a)
+definition l_same S (a b : A) := l a S = l b S
+definition r_same S (a b : A) := r a S = r b S
+lemma l_same.refl S (a : A) : l_same S a a := rfl
+lemma l_same.symm S (a b : A) : l_same S a b → l_same S b a := eq.symm
+lemma l_same.trans S (a b c : A) : l_same S a b → l_same S b c → l_same S a c := eq.trans
+example (S : set A) : equivalence (l_same S) := mk_equivalence (l_same S) (l_same.refl S) (l_same.symm S) (l_same.trans S)
+end
+end coset
+
+section
+variable {A : Type}
+variable [s : group A]
+include s
+definition lmul_by (a : A) := λ x, a * x
+definition rmul_by (a : A) := λ x, x * a
+definition glcoset a (H : set A) : set A := λ x, H (a⁻¹ * x)
+definition grcoset H (a : A) : set A := λ x, H (x * a⁻¹)
+end
+end algebra
+
+namespace group
+open algebra
+  namespace ops
+    infixr `∘>`:55 := glcoset -- stronger than = (50), weaker than * (70)
+    infixl `<∘`:55 := grcoset
+    infixr `∘c`:55 := conj_by
+  end ops
+end group
+
+namespace algebra
+open group.ops
+section
+variable {A : Type}
+variable [s : group A]
+include s
+
+lemma conj_inj (g : A) : injective (conj_by g) :=
+injective_of_has_left_inverse (exists.intro (conj_by g⁻¹) take a, !conj_inv_cancel)
+
+lemma lmul_inj (a : A) : injective (lmul_by a) :=
+take x₁ x₂ Peq, by esimp [lmul_by] at Peq;
+  rewrite [-(inv_mul_cancel_left a x₁), -(inv_mul_cancel_left a x₂), Peq]
+lemma lmul_inv_on (a : A) (H : set A) : left_inv_on (lmul_by a⁻¹) (lmul_by a) H :=
+      take x Px, show a⁻¹*(a*x) = x, by rewrite inv_mul_cancel_left
+lemma lmul_inj_on (a : A) (H : set A) : inj_on (lmul_by a) H :=
+      inj_on_of_left_inv_on (lmul_inv_on a H)
+
+lemma glcoset_eq_lcoset a (H : set A) : a ∘> H = coset.l a H :=
+      setext
+      begin
+      intro x,
+      rewrite [↑glcoset, ↑coset.l, ↑image, ↑set_of, ↑mem, ↑coset.lmul],
+      apply iff.intro,
+        intro P1,
+        apply (exists.intro (a⁻¹ * x)),
+        apply and.intro,
+          exact P1,
+          exact (mul_inv_cancel_left a x),
+        show (∃ (x_1 : A), H x_1 ∧ a * x_1 = x) → H (a⁻¹ * x), from
+          assume P2, obtain x_1 P3, from P2,
+          have P4 : a * x_1 = x, from and.right P3,
+          have P5 : x_1 = a⁻¹ * x, from eq_inv_mul_of_mul_eq P4,
+          eq.subst P5 (and.left P3)
+      end
+lemma grcoset_eq_rcoset a (H : set A) : H <∘ a = coset.r a H :=
+      begin
+        rewrite [↑grcoset, ↑coset.r, ↑image, ↑coset.rmul, ↑set_of],
+        apply setext, rewrite ↑mem,
+        intro x,
+        apply iff.intro,
+          show H (x * a⁻¹) → (∃ (x_1 : A), H x_1 ∧ x_1 * a = x), from
+            assume PH,
+              exists.intro (x * a⁻¹)
+                           (and.intro PH (inv_mul_cancel_right x a)),
+          show (∃ (x_1 : A), H x_1 ∧ x_1 * a = x) → H (x * a⁻¹), from
+            assume Pex,
+              obtain x_1 Pand, from Pex,
+                eq.subst (eq_mul_inv_of_mul_eq (and.right Pand)) (and.left Pand)
+      end
+lemma glcoset_sub a (S H : set A) : S ⊆ H → (a ∘> S) ⊆ (a ∘> H) :=
+      assume Psub,
+      assert P : _, from coset.l_sub a S H Psub,
+      eq.symm (glcoset_eq_lcoset a S) ▸ eq.symm (glcoset_eq_lcoset a H) ▸ P
+lemma glcoset_compose (a b : A) (H : set A) : a ∘> b ∘> H = a*b ∘> H :=
+      begin
+      rewrite [*glcoset_eq_lcoset], exact (coset.lcompose a b H)
+      end
+lemma grcoset_compose (a b : A) (H : set A) : H <∘ a <∘ b = H <∘ a*b :=
+      begin
+      rewrite [*grcoset_eq_rcoset], exact (coset.rcompose b a H)
+      end
+lemma glcoset_id (H : set A) : 1 ∘> H = H :=
+      funext (assume x,
+        calc (1 ∘> H) x = H (1⁻¹*x) : rfl
+        ... = H (1*x) : {one_inv}
+        ... = H x : {one_mul x})
+lemma grcoset_id (H : set A) : H <∘ 1 = H :=
+      funext (assume x,
+        calc H (x*1⁻¹) = H (x*1) : {one_inv}
+        ... = H x : {mul_one x})
+--lemma glcoset_inv a (H : set A) : a⁻¹ ∘> a ∘> H = H :=
+--      funext (assume x,
+--        calc glcoset a⁻¹ (glcoset a H) x = H x : {mul_inv_cancel_left a⁻¹ x})
+lemma glcoset_inv a (H : set A) : a⁻¹ ∘> a ∘> H = H :=
+      calc a⁻¹ ∘> a ∘> H = (a⁻¹*a) ∘> H : glcoset_compose
+      ... = 1 ∘> H : mul.left_inv
+      ... = H : glcoset_id
+lemma grcoset_inv H (a : A) : (H <∘ a) <∘ a⁻¹ = H :=
+      funext (assume x,
+        calc grcoset (grcoset H a) a⁻¹ x = H x : {inv_mul_cancel_right x a⁻¹})
+lemma glcoset_cancel a b (H : set A) : (b*a⁻¹) ∘> a ∘> H = b ∘> H :=
+      calc (b*a⁻¹) ∘> a ∘> H = b*a⁻¹*a ∘> H : glcoset_compose
+      ... = b ∘> H : {inv_mul_cancel_right b a}
+lemma grcoset_cancel a b (H : set A) : H <∘ a <∘ a⁻¹*b = H <∘ b :=
+      calc H <∘ a <∘ a⁻¹*b = H <∘ a*(a⁻¹*b) : grcoset_compose
+      ... = H <∘ b : {mul_inv_cancel_left a b}
+-- test how precedence breaks tie: infixr takes hold since its encountered first
+example a b (H : set A) : a ∘> H <∘ b = a ∘> (H <∘ b) := rfl
+-- should be true for semigroup as well but irrelevant
+lemma lcoset_rcoset_assoc a b (H : set A) : a ∘> H <∘ b = (a ∘> H) <∘ b :=
+  funext (assume x, begin
+  esimp [glcoset, grcoset], rewrite mul.assoc
+  end)
+definition mul_closed_on H := ∀ (x y : A), x ∈ H → y ∈ H → x * y ∈ H
+lemma closed_lcontract a (H : set A) : mul_closed_on H → a ∈ H → a ∘> H ⊆ H :=
+      begin
+      rewrite [↑mul_closed_on, ↑glcoset, ↑subset, ↑mem],
+      intro Pclosed, intro PHa, intro x, intro PHainvx,
+      exact (eq.subst (mul_inv_cancel_left a x)
+                      (Pclosed a (a⁻¹*x) PHa PHainvx))
+      end
+lemma closed_rcontract a (H : set A) : mul_closed_on H → a ∈ H → H <∘ a ⊆ H :=
+      assume P1 : mul_closed_on H,
+      assume P2 : H a,
+      begin
+        rewrite ↑subset,
+        intro x,
+        rewrite [↑grcoset, ↑mem],
+        intro P3,
+        exact (eq.subst (inv_mul_cancel_right x a) (P1 (x * a⁻¹) a P3 P2))
+      end
+lemma closed_lcontract_set a (H G : set A) : mul_closed_on G → H ⊆ G → a∈G → a∘>H ⊆ G :=
+      assume Pclosed, assume PHsubG, assume PainG,
+      assert PaGsubG : a ∘> G ⊆ G, from closed_lcontract a G Pclosed PainG,
+      assert PaHsubaG : a ∘> H ⊆ a ∘> G, from
+        eq.symm (glcoset_eq_lcoset a H) ▸ eq.symm (glcoset_eq_lcoset a G) ▸ (coset.l_sub a H G PHsubG),
+      subset.trans _ _ _ PaHsubaG PaGsubG
+definition subgroup.has_inv H := ∀ (a : A), a ∈ H → a⁻¹ ∈ H
+-- two ways to define the same equivalence relatiohship for subgroups
+definition in_lcoset [reducible] H (a b : A) := a ∈ b ∘> H
+definition in_rcoset [reducible] H (a b : A) := a ∈ H <∘ b
+definition same_lcoset [reducible] H (a b : A) := a ∘> H = b ∘> H
+definition same_rcoset [reducible] H (a b : A) := H <∘ a = H <∘ b
+definition same_left_right_coset (N : set A) := ∀ x, x ∘> N = N <∘ x
+structure is_subgroup [class] (H : set A) : Type :=
+  (has_one : H 1)
+  (mul_closed : mul_closed_on H)
+  (has_inv : subgroup.has_inv H)
+structure is_normal_subgroup [class] (N : set A) extends is_subgroup N :=
+  (normal : same_left_right_coset N)
+end
+
+section subgroup
+variable {A : Type}
+variable [s : group A]
+include s
+variable {H : set A}
+variable [is_subg : is_subgroup H]
+include is_subg
+
+lemma subg_has_one : H (1 : A) := @is_subgroup.has_one A s H is_subg
+lemma subg_mul_closed : mul_closed_on H := @is_subgroup.mul_closed A s H is_subg
+lemma subg_has_inv : subgroup.has_inv H := @is_subgroup.has_inv A s H is_subg
+lemma subgroup_coset_id : ∀ a, a ∈ H → (a ∘> H = H ∧ H <∘ a = H) :=
+      take a, assume PHa : H a,
+      assert Pl : a ∘> H ⊆ H, from closed_lcontract a H subg_mul_closed PHa,
+      assert Pr : H <∘ a ⊆ H, from closed_rcontract a H subg_mul_closed PHa,
+      assert PHainv : H a⁻¹, from subg_has_inv a PHa,
+      and.intro
+      (setext (assume x,
+        begin
+          esimp [glcoset, mem],
+          apply iff.intro,
+            apply Pl,
+            intro PHx, exact (subg_mul_closed a⁻¹ x PHainv PHx)
+        end))
+      (setext (assume x,
+        begin
+          esimp [grcoset, mem],
+          apply iff.intro,
+            apply Pr,
+            intro PHx, exact (subg_mul_closed x a⁻¹ PHx PHainv)
+        end))
+lemma subgroup_lcoset_id : ∀ a, a ∈ H → a ∘> H = H :=
+      take a, assume PHa : H a,
+      and.left (subgroup_coset_id a PHa)
+lemma subgroup_rcoset_id : ∀ a, a ∈ H → H <∘ a = H :=
+      take a, assume PHa : H a,
+      and.right (subgroup_coset_id a PHa)
+lemma subg_in_coset_refl (a : A) : a ∈ a ∘> H ∧ a ∈ H <∘ a :=
+      assert PH1 : H 1, from subg_has_one,
+      assert PHinvaa : H (a⁻¹*a), from (eq.symm (mul.left_inv a)) ▸ PH1,
+      assert PHainva : H (a*a⁻¹), from (eq.symm (mul.right_inv a)) ▸ PH1,
+      and.intro PHinvaa PHainva
+lemma subg_in_lcoset_same_lcoset (a b : A) : in_lcoset H a b → same_lcoset H a b :=
+      assume Pa_in_b : H (b⁻¹*a),
+      have Pbinva : b⁻¹*a ∘> H = H, from subgroup_lcoset_id (b⁻¹*a) Pa_in_b,
+      have Pb_binva : b ∘> b⁻¹*a ∘> H = b ∘> H, from Pbinva ▸ rfl,
+      have Pbbinva : b*(b⁻¹*a)∘>H = b∘>H, from glcoset_compose b (b⁻¹*a) H ▸ Pb_binva,
+      mul_inv_cancel_left b a ▸ Pbbinva
+lemma subg_same_lcoset_in_lcoset (a b : A) : same_lcoset H a b → in_lcoset H a b :=
+      assume Psame : a∘>H = b∘>H,
+      assert Pa : a ∈ a∘>H, from and.left (subg_in_coset_refl a),
+      by exact (Psame ▸ Pa)
+lemma subg_lcoset_same (a b : A) : in_lcoset H a b = (a∘>H = b∘>H) :=
+      propext(iff.intro (subg_in_lcoset_same_lcoset a b) (subg_same_lcoset_in_lcoset a b))
+lemma subg_rcoset_same (a b : A) : in_rcoset H a b = (H<∘a = H<∘b) :=
+      propext(iff.intro
+      (assume Pa_in_b : H (a*b⁻¹),
+      have Pabinv : H<∘a*b⁻¹ = H, from subgroup_rcoset_id (a*b⁻¹) Pa_in_b,
+      have Pabinv_b : H <∘ a*b⁻¹ <∘ b = H <∘ b, from Pabinv ▸ rfl,
+      have Pabinvb : H <∘ a*b⁻¹*b = H <∘ b, from grcoset_compose (a*b⁻¹) b H ▸ Pabinv_b,
+      inv_mul_cancel_right a b ▸ Pabinvb)
+      (assume Psame,
+      assert Pa : a ∈ H<∘a, from and.right (subg_in_coset_refl a),
+      by exact (Psame ▸ Pa)))
+lemma subg_same_lcoset.refl (a : A) : same_lcoset H a a := rfl
+lemma subg_same_rcoset.refl (a : A) : same_rcoset H a a := rfl
+lemma subg_same_lcoset.symm (a b : A) : same_lcoset H a b → same_lcoset H b a := eq.symm
+lemma subg_same_rcoset.symm (a b : A) : same_rcoset H a b → same_rcoset H b a := eq.symm
+lemma subg_same_lcoset.trans (a b c : A) : same_lcoset H a b → same_lcoset H b c → same_lcoset H a c :=
+      eq.trans
+lemma subg_same_rcoset.trans (a b c : A) : same_rcoset H a b → same_rcoset H b c → same_rcoset H a c :=
+      eq.trans
+variable {S : set A}
+lemma subg_lcoset_subset_subg (Psub : S ⊆ H) (a : A) : a ∈ H → a ∘> S ⊆ H :=
+      assume Pin, have P : a ∘> S ⊆ a ∘> H, from glcoset_sub a S H Psub,
+      subgroup_lcoset_id a Pin ▸ P
+
+end subgroup
+
+section normal_subg
+open quot
+variable {A : Type}
+variable [s : group A]
+include s
+variable (N : set A)
+variable [is_nsubg : is_normal_subgroup N]
+include is_nsubg
+
+local notation a `~` b := same_lcoset N a b -- note : does not bind as strong as →
+
+lemma nsubg_normal : same_left_right_coset N := @is_normal_subgroup.normal A s N is_nsubg
+lemma nsubg_same_lcoset_product : ∀ a1 a2 b1 b2, (a1 ~ b1) → (a2 ~ b2) →  ((a1*a2) ~ (b1*b2)) :=
+  take a1, take a2, take b1, take b2,
+  assume Psame1 : a1 ∘> N = b1 ∘> N,
+  assume Psame2 : a2 ∘> N = b2 ∘> N,
+  calc
+  a1*a2 ∘> N = a1 ∘> a2 ∘> N : glcoset_compose
+  ... = a1 ∘> b2 ∘> N :    by rewrite Psame2
+  ... = a1 ∘> (N <∘ b2) :  by rewrite (nsubg_normal N)
+  ... = (a1 ∘> N) <∘ b2 :  by rewrite lcoset_rcoset_assoc
+  ... = (b1 ∘> N) <∘ b2 :  by rewrite Psame1
+  ... = N <∘ b1 <∘ b2 :    by rewrite (nsubg_normal N)
+  ... = N <∘ (b1*b2) :     by rewrite grcoset_compose
+  ... = (b1*b2) ∘> N :     by rewrite (nsubg_normal N)
+
+example (a b : A) : (a⁻¹ ~ b⁻¹) = (a⁻¹ ∘> N = b⁻¹ ∘> N) := rfl
+lemma nsubg_same_lcoset_inv : ∀ a b, (a ~ b) → (a⁻¹ ~ b⁻¹) :=
+  take a b, assume Psame : a ∘> N = b ∘> N, calc
+  a⁻¹ ∘> N = a⁻¹*b*b⁻¹ ∘> N    : by rewrite mul_inv_cancel_right
+  ... = a⁻¹*b ∘> b⁻¹ ∘> N      : by rewrite glcoset_compose
+  ... = a⁻¹*b ∘> (N <∘ b⁻¹)    : by rewrite nsubg_normal
+  ... = (a⁻¹*b ∘> N) <∘ b⁻¹    : by rewrite lcoset_rcoset_assoc
+  ... = (a⁻¹ ∘> b ∘> N) <∘ b⁻¹ : by rewrite glcoset_compose
+  ... = (a⁻¹ ∘> a ∘> N) <∘ b⁻¹ : by rewrite Psame
+  ... = N <∘ b⁻¹               : by rewrite glcoset_inv
+  ... = b⁻¹ ∘> N               : by rewrite nsubg_normal
+definition nsubg_setoid [instance] : setoid A :=
+  setoid.mk (same_lcoset N)
+  (mk_equivalence (same_lcoset N) (subg_same_lcoset.refl) (subg_same_lcoset.symm) (subg_same_lcoset.trans))
+definition coset_of : Type := quot (nsubg_setoid N)
+
+definition coset_inv_base (a : A) : coset_of N := ⟦a⁻¹⟧
+definition coset_product (a b : A) : coset_of N := ⟦a*b⟧
+lemma coset_product_well_defined : ∀ a1 a2 b1 b2, (a1 ~ b1) → (a2 ~ b2) → ⟦a1*a2⟧ = ⟦b1*b2⟧ :=
+      take a1 a2 b1 b2, assume P1 P2,
+      quot.sound (nsubg_same_lcoset_product N a1 a2 b1 b2 P1 P2)
+definition coset_mul (aN bN : coset_of N) : coset_of N :=
+  quot.lift_on₂ aN bN (coset_product N) (coset_product_well_defined N)
+lemma coset_inv_well_defined : ∀ a b, (a ~ b) → ⟦a⁻¹⟧ = ⟦b⁻¹⟧ :=
+      take a b, assume P, quot.sound (nsubg_same_lcoset_inv N a b P)
+definition coset_inv (aN : coset_of N) : coset_of N :=
+           quot.lift_on aN (coset_inv_base N) (coset_inv_well_defined N)
+definition coset_one :  coset_of N := ⟦1⟧
+
+local infixl `cx`:70 := coset_mul N
+example (a b c : A) : ⟦a⟧ cx ⟦b*c⟧ = ⟦a*(b*c)⟧ := rfl
+
+lemma coset_product_assoc (a b c : A) : ⟦a⟧ cx ⟦b⟧ cx ⟦c⟧ = ⟦a⟧ cx (⟦b⟧ cx ⟦c⟧) := calc
+      ⟦a*b*c⟧ = ⟦a*(b*c)⟧ : {mul.assoc a b c}
+      ... = ⟦a⟧ cx ⟦b*c⟧ : rfl
+lemma coset_product_left_id (a : A) : ⟦1⟧ cx ⟦a⟧ = ⟦a⟧ := calc
+      ⟦1*a⟧ = ⟦a⟧ : {one_mul a}
+lemma coset_product_right_id (a : A) : ⟦a⟧ cx ⟦1⟧ = ⟦a⟧ := calc
+      ⟦a*1⟧ = ⟦a⟧ : {mul_one a}
+lemma coset_product_left_inv (a : A) : ⟦a⁻¹⟧ cx ⟦a⟧ = ⟦1⟧ := calc
+      ⟦a⁻¹*a⟧ = ⟦1⟧ : {mul.left_inv a}
+lemma coset_mul.assoc (aN bN cN : coset_of N) : aN cx bN cx cN = aN cx (bN cx cN) :=
+      quot.ind (λ a, quot.ind (λ b, quot.ind (λ c, coset_product_assoc N a b c) cN) bN) aN
+lemma coset_mul.one_mul (aN : coset_of N) : coset_one N cx aN = aN :=
+      quot.ind (coset_product_left_id N) aN
+lemma coset_mul.mul_one (aN : coset_of N) : aN cx (coset_one N) = aN :=
+      quot.ind (coset_product_right_id N) aN
+lemma coset_mul.left_inv (aN : coset_of N) : (coset_inv N aN) cx aN = (coset_one N) :=
+      quot.ind (coset_product_left_inv N) aN
+definition mk_quotient_group : group (coset_of N):=
+           group.mk (coset_mul N) (coset_mul.assoc N) (coset_one N)  (coset_mul.one_mul N) (coset_mul.mul_one N) (coset_inv N) (coset_mul.left_inv N)
+
+end normal_subg
+
+namespace group
+namespace quotient
+section
+open quot
+variable {A : Type}
+variable [s : group A]
+include s
+variable {N : set A}
+variable [is_nsubg : is_normal_subgroup N]
+include is_nsubg
+definition quotient_group [instance] : group (coset_of N) := mk_quotient_group N
+
+example (aN : coset_of N) : aN * aN⁻¹ = 1 := mul.right_inv aN
+definition natural (a : A) : coset_of N := ⟦a⟧
+
+end
+end quotient
+end group
+
+end algebra