chore(group_theory): move order_of into its own file; base costes on …

…left_coset

group_theory/coset.lean

@@ -4,49 +4,48 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mitchell Rowett, Scott Morrison
 -/
 import group_theory.subgroup data.set.basic
+open set function
 
-open set
+variable {α : Type*}
 
-variable {γ : Type*}
-
-def left_coset [has_mul γ] (a : γ) (s : set γ) : set γ := (λ x, a * x) '' s
-def right_coset [has_mul γ] (s : set γ) (a : γ) : set γ := (λ x, x * a) '' s
+def left_coset [has_mul α] (a : α) (s : set α) : set α := (λ x, a * x) '' s
+def right_coset [has_mul α] (s : set α) (a : α) : set α := (λ x, x * a) '' s
 
 local infix ` *l `:70 := left_coset
 local infix ` *r `:70 := right_coset
 
 section coset_mul
-variable [has_mul γ]
+variable [has_mul α]
 
-lemma mem_left_coset {s : set γ} {x : γ} (a : γ) (hxS : x ∈ s) : a * x ∈ a *l s :=
-mem_image_of_mem (λ b : γ, a * b) hxS
+lemma mem_left_coset {s : set α} {x : α} (a : α) (hxS : x ∈ s) : a * x ∈ a *l s :=
+mem_image_of_mem (λ b : α, a * b) hxS
 
-lemma mem_right_coset {s : set γ} {x : γ} (a : γ) (hxS : x ∈ s) : x * a ∈ s *r a :=
-mem_image_of_mem (λ b : γ, b * a) hxS
+lemma mem_right_coset {s : set α} {x : α} (a : α) (hxS : x ∈ s) : x * a ∈ s *r a :=
+mem_image_of_mem (λ b : α, b * a) hxS
 
-def left_coset_equiv (s : set γ) (a b : γ) := a *l s = b *l s
+def left_coset_equiv (s : set α) (a b : α) := a *l s = b *l s
 
-lemma left_coset_equiv_rel (s : set γ) : equivalence (left_coset_equiv s) :=
+lemma left_coset_equiv_rel (s : set α) : equivalence (left_coset_equiv s) :=
 mk_equivalence (left_coset_equiv s) (λ a, rfl) (λ a b, eq.symm) (λ a b c, eq.trans)
 
 end coset_mul
 
 section coset_semigroup
-variable [semigroup γ]
+variable [semigroup α]
 
-@[simp] lemma left_coset_assoc (s : set γ) (a b : γ) : a *l (b *l s) = (a * b) *l s :=
+@[simp] lemma left_coset_assoc (s : set α) (a b : α) : a *l (b *l s) = (a * b) *l s :=
 by simp [left_coset, right_coset, (image_comp _ _ _).symm, function.comp, mul_assoc]
 
-@[simp] lemma right_coset_assoc (s : set γ) (a b : γ) : s *r a *r b = s *r (a * b) :=
+@[simp] lemma right_coset_assoc (s : set α) (a b : α) : s *r a *r b = s *r (a * b) :=
 by simp [left_coset, right_coset, (image_comp _ _ _).symm, function.comp, mul_assoc]
 
-lemma left_coset_right_coset (s : set γ) (a b : γ) : a *l s *r b = a *l (s *r b) :=
+lemma left_coset_right_coset (s : set α) (a b : α) : a *l s *r b = a *l (s *r b) :=
 by simp [left_coset, right_coset, (image_comp _ _ _).symm, function.comp, mul_assoc]
 
 end coset_semigroup
 
 section coset_monoid
-variables [monoid γ] (s : set γ)
+variables [monoid α] (s : set α)
 
 @[simp] lemma one_left_coset : 1 *l s = s :=
 set.ext $ by simp [left_coset]
@@ -58,33 +57,33 @@ end coset_monoid
 
 section coset_submonoid
 open is_submonoid
-variables [monoid γ] (s : set γ) [is_submonoid s]
+variables [monoid α] (s : set α) [is_submonoid s]
 
-lemma mem_own_left_coset (a : γ) : a ∈ a *l s :=
+lemma mem_own_left_coset (a : α) : a ∈ a *l s :=
 suffices a * 1 ∈ a *l s, by simpa,
 mem_left_coset a (one_mem s)
 
-lemma mem_own_right_coset (a : γ) : a ∈ s *r a :=
+lemma mem_own_right_coset (a : α) : a ∈ s *r a :=
 suffices 1 * a ∈ s *r a, by simpa,
 mem_right_coset a (one_mem s)
 
-lemma mem_left_coset_left_coset {a : γ} (ha : a *l s = s) : a ∈ s :=
+lemma mem_left_coset_left_coset {a : α} (ha : a *l s = s) : a ∈ s :=
 by rw [←ha]; exact mem_own_left_coset s a
 
-lemma mem_right_coset_right_coset {a : γ} (ha : s *r a = s) : a ∈ s :=
+lemma mem_right_coset_right_coset {a : α} (ha : s *r a = s) : a ∈ s :=
 by rw [←ha]; exact mem_own_right_coset s a
 
 end coset_submonoid
 
 section coset_group
-variables [group γ] {s : set γ} {x : γ}
+variables [group α] {s : set α} {x : α}
 
-lemma mem_left_coset_iff (a : γ) : x ∈ a *l s ↔ a⁻¹ * x ∈ s :=
+lemma mem_left_coset_iff (a : α) : x ∈ a *l s ↔ a⁻¹ * x ∈ s :=
 iff.intro
   (assume ⟨b, hb, eq⟩, by simp [eq.symm, hb])
   (assume h, ⟨a⁻¹ * x, h, by simp⟩)
 
-lemma mem_right_coset_iff (a : γ) : x ∈ s *r a ↔ x * a⁻¹ ∈ s :=
+lemma mem_right_coset_iff (a : α) : x ∈ s *r a ↔ x * a⁻¹ ∈ s :=
 iff.intro
   (assume ⟨b, hb, eq⟩, by simp [eq.symm, hb])
   (assume h, ⟨x * a⁻¹, h, by simp⟩)
@@ -94,15 +93,15 @@ end coset_group
 section coset_subgroup
 open is_submonoid
 open is_subgroup
-variables [group γ] (s : set γ) [is_subgroup s]
+variables [group α] (s : set α) [is_subgroup s]
 
-lemma left_coset_mem_left_coset {a : γ} (ha : a ∈ s) : a *l s = s :=
+lemma left_coset_mem_left_coset {a : α} (ha : a ∈ s) : a *l s = s :=
 set.ext $ by simp [mem_left_coset_iff, mul_mem_cancel_right s (inv_mem ha)]
 
-lemma right_coset_mem_right_coset {a : γ} (ha : a ∈ s) : s *r a = s :=
+lemma right_coset_mem_right_coset {a : α} (ha : a ∈ s) : s *r a = s :=
 set.ext $ assume b, by simp [mem_right_coset_iff, mul_mem_cancel_left s (inv_mem ha)]
 
-theorem normal_of_eq_cosets [normal_subgroup s] (g : γ) : g *l s = s *r g :=
+theorem normal_of_eq_cosets [normal_subgroup s] (g : α) : g *l s = s *r g :=
 set.ext $ assume a, by simp [mem_left_coset_iff, mem_right_coset_iff]; rw [mem_norm_comm_iff]
 
 theorem eq_cosets_of_normal (h : ∀ g, g *l s = s *r g) : normal_subgroup s :=
@@ -113,3 +112,48 @@ theorem normal_iff_eq_cosets : normal_subgroup s ↔ ∀ g, g *l s = s *r g :=
 ⟨@normal_of_eq_cosets _ _ s _, eq_cosets_of_normal s⟩
 
 end coset_subgroup
+
+def left_cosets [group α] (s : set α) : set (set α) := range (λa, a *l s)
+
+namespace is_subgroup
+open is_submonoid
+variable [group α]
+
+lemma subgroup_mem_left_cosets (s : set α) [is_subgroup s] : s ∈ left_cosets s :=
+⟨1, by simp⟩
+
+lemma left_cosets_disjoint {s : set α} [is_subgroup s] :
+  ∀{s₁ s₂ : set α}, s₁ ∈ left_cosets s → s₂ ∈ left_cosets s → ∀{a}, a ∈ s₁ → a ∈ s₂ → s₁ = s₂
+| _ _ ⟨a₁, rfl⟩ ⟨a₂, rfl⟩ a h₁ h₂ :=
+  have h₁ : a₁⁻¹ * a ∈ s, by simpa [mem_left_coset_iff] using h₁,
+  have h₂ : a₂⁻¹ * a ∈ s, by simpa [mem_left_coset_iff] using h₂,
+  have a₁⁻¹ * a₂ ∈ s, by simpa [mul_assoc] using mul_mem h₁ (inv_mem h₂),
+  have a₁ *l s = a₁ *l ((a₁⁻¹ * a₂) *l s), by rw [left_coset_mem_left_coset _ this],
+  by simpa
+
+lemma pairwise_left_cosets_disjoint {s : set α} (hs : is_subgroup s) :
+  pairwise_on (left_cosets s) disjoint :=
+assume s₁ h₁ s₂ h₂ ne, eq_empty_iff_forall_not_mem.mpr $ assume a ⟨ha₁, ha₂⟩,
+  ne $ left_cosets_disjoint h₁ h₂ ha₁ ha₂
+
+lemma left_cosets_equiv_subgroup {s : set α} (hs : is_subgroup s) :
+  ∀{t : set α}, t ∈ left_cosets s → nonempty (t ≃ s)
+| _ ⟨a, rfl⟩ := ⟨(equiv.set.image ((*) a) s injective_mul).symm⟩
+
+lemma Union_left_cosets_eq_univ {s : set α} (hs : is_subgroup s) : ⋃₀ left_cosets s = univ :=
+eq_univ_of_forall $ assume a, ⟨(*) a '' s, mem_range_self _, ⟨1, hs.one_mem, mul_one _⟩⟩
+
+lemma group_equiv_left_cosets_times_subgroup {s : set α} (hs : is_subgroup s) :
+  nonempty (α ≃ (left_cosets s × s)) :=
+⟨calc α ≃ (@set.univ α) :
+    (equiv.set.univ α).symm
+  ... ≃ (⋃t∈left_cosets s, t) :
+    by rw [←hs.Union_left_cosets_eq_univ]; simp
+  ... ≃ (Σt:left_cosets s, t) :
+    equiv.set.bUnion_eq_sigma_of_disjoint hs.pairwise_left_cosets_disjoint
+  ... ≃ (Σt:left_cosets s, s) :
+    equiv.sigma_congr_right $ λ⟨t, ht⟩, classical.choice $ hs.left_cosets_equiv_subgroup ht
+  ... ≃ (left_cosets s × s) :
+    equiv.sigma_equiv_prod _ _⟩
+
+end is_subgroup

group_theory/order_of_element.lean

@@ -0,0 +1,154 @@
+/-
+Copyright (c) 2018 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl
+-/
+import group_theory.coset
+open set function
+
+variables {α : Type*} {s : set α} {a a₁ a₂ b c: α}
+
+-- TODO this lemma isn't used anywhere in this file, and should be moved elsewhere.
+namespace finset
+open finset
+
+lemma mem_range_iff_mem_finset_range_of_mod_eq [decidable_eq α] {f : ℤ → α} {a : α} {n : ℕ}
+  (hn : 0 < n) (h : ∀i, f (i % n) = f i) :
+  a ∈ set.range f ↔ a ∈ (finset.range n).image (λi, f i) :=
+suffices (∃i, f (i % n) = a) ↔ ∃i, i < n ∧ f ↑i = a, by simpa [h],
+have hn' : 0 < (n : ℤ), from int.coe_nat_lt.mpr hn,
+iff.intro
+  (assume ⟨i, hi⟩,
+    have 0 ≤ i % ↑n, from int.mod_nonneg _ (ne_of_gt hn'),
+    ⟨int.to_nat (i % n),
+      by rw [←int.coe_nat_lt, int.to_nat_of_nonneg this]; exact ⟨int.mod_lt_of_pos i hn', hi⟩⟩)
+  (assume ⟨i, hi, ha⟩,
+    ⟨i, by rw [int.mod_eq_of_lt (int.coe_zero_le _) (int.coe_nat_lt_coe_nat_of_lt hi), ha]⟩)
+
+end finset
+
+section order_of
+variables [group α] [fintype α] [decidable_eq α]
+
+lemma exists_gpow_eq_one (a : α) : ∃i≠0, a ^ (i:ℤ) = 1 :=
+have ¬ injective (λi, a ^ i),
+  from not_injective_int_fintype,
+let ⟨i, j, a_eq, ne⟩ := show ∃(i j : ℤ), a ^ i = a ^ j ∧ i ≠ j,
+  by rw [injective] at this; simpa [classical.not_forall] in
+have a ^ (i - j) = 1,
+  by simp [gpow_add, gpow_neg, a_eq],
+⟨i - j, sub_ne_zero.mpr ne, this⟩
+
+lemma exists_pow_eq_one (a : α) : ∃i≠0, a ^ i = 1 :=
+let ⟨i, hi, eq⟩ := exists_gpow_eq_one a in
+begin
+  cases i,
+  { exact ⟨i, by simp [int.of_nat_eq_coe, *] at *, eq⟩ },
+  { exact ⟨i + 1, dec_trivial, inv_eq_one.1 eq⟩ }
+end
+
+/-- `order_of a` is the order of the element `a`, i.e. the `n ≥ 1`, s.t. `a ^ n = 1` -/
+def order_of (a : α) : ℕ := nat.find (exists_pow_eq_one a)
+
+lemma pow_order_of_eq_one (a : α) : a ^ order_of a = 1 :=
+let ⟨h₁, h₂⟩ := nat.find_spec (exists_pow_eq_one a) in h₂
+
+lemma order_of_ne_zero (a : α) : order_of a ≠ 0 :=
+let ⟨h₁, h₂⟩ := nat.find_spec (exists_pow_eq_one a) in h₁
+
+private lemma pow_injective_aux {n m : ℕ} (a : α) (h : n ≤ m)
+  (hn : n < order_of a) (hm : m < order_of a) (eq : a ^ n = a ^ m) : n = m :=
+decidable.by_contradiction $ assume ne : n ≠ m,
+  have h₁ : m - n ≠ 0, by simp [nat.sub_eq_iff_eq_add h, ne.symm],
+  have h₂ : a ^ (m - n) = 1, by simp [pow_sub _ h, eq],
+  have le : order_of a ≤ m - n, from nat.find_min' (exists_pow_eq_one a) ⟨h₁, h₂⟩,
+  have lt : m - n < order_of a,
+    from (nat.sub_lt_left_iff_lt_add h).mpr $ nat.lt_add_left _ _ _ hm,
+  lt_irrefl _ (lt_of_le_of_lt le lt)
+
+lemma pow_injective_of_lt_order_of {n m : ℕ} (a : α)
+  (hn : n < order_of a) (hm : m < order_of a) (eq : a ^ n = a ^ m) : n = m :=
+(le_total n m).elim
+  (assume h, pow_injective_aux a h hn hm eq)
+  (assume h, (pow_injective_aux a h hm hn eq.symm).symm)
+
+lemma order_of_le_card_univ : order_of a ≤ fintype.card α :=
+finset.card_le_of_inj_on ((^) a)
+  (assume n _, fintype.complete _)
+  (assume i j, pow_injective_of_lt_order_of a)
+
+lemma pow_eq_mod_order_of {n : ℕ} : a ^ n = a ^ (n % order_of a) :=
+calc a ^ n = a ^ (n % order_of a + order_of a * (n / order_of a)) :
+    by rw [nat.mod_add_div]
+  ... = a ^ (n % order_of a) :
+    by simp [pow_add, pow_mul, pow_order_of_eq_one]
+
+lemma gpow_eq_mod_order_of {i : ℤ} : a ^ i = a ^ (i % order_of a) :=
+calc a ^ i = a ^ (i % order_of a + order_of a * (i / order_of a)) :
+    by rw [int.mod_add_div]
+  ... = a ^ (i % order_of a) :
+    by simp [gpow_add, gpow_mul, pow_order_of_eq_one]
+
+lemma mem_range_gpow_iff_mem_range_order_of {a a' : α} :
+  a' ∈ range ((^) a : ℤ → α) ↔ a' ∈ (finset.range (order_of a)).image ((^) a : ℕ → α) :=
+finset.mem_range_iff_mem_finset_range_of_mod_eq
+  (nat.pos_iff_ne_zero.mpr (order_of_ne_zero a))
+  (assume i, gpow_eq_mod_order_of.symm)
+
+instance decidable_range_gpow : decidable_pred (range ((^) a : ℤ → α)) :=
+assume a', decidable_of_iff'
+  (a' ∈ (finset.range (order_of a)).image ((^) a))
+  mem_range_gpow_iff_mem_range_order_of
+
+section
+local attribute [instance] set_fintype
+
+lemma order_eq_card_range_gpow : order_of a = fintype.card (range ((^) a : ℤ → α)) :=
+begin
+  refine (finset.card_eq_of_bijective _ _ _ _).symm,
+  { exact λn hn, ⟨gpow a n, mem_range_self n⟩ },
+  { exact assume ⟨_, i, rfl⟩ _,
+      have pos: (0:int) < order_of a,
+        from int.coe_nat_lt.mpr $ nat.pos_iff_ne_zero.mpr $ order_of_ne_zero a,
+      have 0 ≤ i % (order_of a),
+        from int.mod_nonneg _ $ ne_of_gt pos,
+      ⟨int.to_nat (i % order_of a),
+        by rw [← int.coe_nat_lt, int.to_nat_of_nonneg this];
+          exact ⟨int.mod_lt_of_pos _ pos, subtype.eq gpow_eq_mod_order_of.symm⟩⟩ },
+  { intros, exact finset.mem_univ _ },
+  { exact assume i j hi hj eq, pow_injective_of_lt_order_of a hi hj $ by simpa using eq }
+end
+
+section classical
+local attribute [instance] classical.prop_decidable
+
+/- TODO: use cardinal theory, introduce `card : set α → ℕ`, or setup decidability for cosets -/
+lemma order_of_dvd_card_univ : order_of a ∣ fintype.card α :=
+let ⟨equiv⟩ := (gpowers.is_subgroup a).group_equiv_left_cosets_times_subgroup in
+have ft_prod : fintype (left_cosets (gpowers a) × (gpowers a)),
+  from fintype.of_equiv α equiv,
+have ft_s : fintype (gpowers a),
+  from @fintype.fintype_prod_right _ _ _ ft_prod
+    ⟨⟨(gpowers a), @is_subgroup.subgroup_mem_left_cosets α _ _ (gpowers.is_subgroup a)⟩⟩,
+have ft_cosets : fintype (left_cosets (gpowers a)),
+  from @fintype.fintype_prod_left _ _ _ ft_prod ⟨⟨1, is_submonoid.one_mem (gpowers a)⟩⟩,
+have ft : fintype (left_cosets (gpowers a) × (gpowers a)),
+  from @prod.fintype _ _ ft_cosets ft_s,
+have eq₁ : fintype.card α = @fintype.card _ ft_cosets * @fintype.card _ ft_s,
+  from calc fintype.card α = @fintype.card _ ft_prod :
+      (@fintype.card_eq _ _ _ ft_prod).2 (gpowers.is_subgroup a).group_equiv_left_cosets_times_subgroup
+    ... = @fintype.card _ (@prod.fintype _ _ ft_cosets ft_s) :
+      congr_arg (@fintype.card _) $ subsingleton.elim _ _
+    ... = @fintype.card _ ft_cosets * @fintype.card _ ft_s :
+      @fintype.card_prod _ _ ft_cosets ft_s,
+have eq₂ : order_of a = @fintype.card _ ft_s,
+  from calc order_of a = _ : order_eq_card_range_gpow
+    ... = _ : congr_arg (@fintype.card _) $ subsingleton.elim _ _,
+dvd.intro (@fintype.card (left_cosets (gpowers a)) ft_cosets) $
+  by rw [eq₁, eq₂, mul_comm]
+
+end classical
+
+end
+
+end order_of