refactor(group_theory/coset): left_cosets is now a quotient (#103)

data/equiv.lean

@@ -287,6 +287,10 @@ def sum_equiv_sigma_bool (α β : Sort*) : (α ⊕ β) ≃ (Σ b: bool, cond b 
  λ s, by cases s; refl,
  λ s, by rcases s with ⟨_|_, _⟩; refl⟩
 
+def equiv_fib {α β : Type*} (f : α → β) :
+  α ≃ Σ y : β, {x // f x = y} :=
+⟨λ x, ⟨f x, x, rfl⟩, λ x, x.2.1, λ x, rfl, λ ⟨y, x, rfl⟩, rfl⟩
+
 end
 
 section

group_theory/coset.lean

@@ -113,47 +113,41 @@ theorem normal_iff_eq_cosets : normal_subgroup s ↔ ∀ g, g *l s = s *r g :=
 
 end coset_subgroup
 
-def left_cosets [group α] (s : set α) : set (set α) := range (λa, a *l s)
+instance left_rel [group α] (s : set α) [is_subgroup s] : setoid α :=
+⟨λ x y, x⁻¹ * y ∈ s,
+  assume x, by simp [is_submonoid.one_mem],
+  assume x y hxy,
+  have (x⁻¹ * y)⁻¹ ∈ s, from is_subgroup.inv_mem hxy,
+  by simpa using this,
+  assume x y z hxy hyz,
+  have x⁻¹ * y * (y⁻¹ * z) ∈ s, from is_submonoid.mul_mem hxy hyz,
+  by simpa [mul_assoc] using this⟩
+
+def left_cosets [group α] (s : set α) [is_subgroup s] : Type* := quotient (left_rel s)
+
+instance left_cosets.inhabited [group α] (s : set α) [is_subgroup s] : inhabited (left_cosets s) := ⟨⟦1⟧⟩
+
+def left_cosets.left_coset [group α] (s : set α) [is_subgroup s] (g : α) : {x | ⟦x⟧ = ⟦g⟧} = left_coset g s :=
+set.ext $ λ z, by simp [eq_comm, mem_left_coset_iff]; refl
 
 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 _ _⟩
+variables [group α] {s : set α}
+
+def left_coset_equiv_subgroup (g : α) : left_coset g s ≃ s :=
+⟨λ x, ⟨g⁻¹ * x.1, (mem_left_coset_iff _).1 x.2⟩,
+ λ x, ⟨g * x.1, x.1, x.2, rfl⟩,
+ λ ⟨x, hx⟩, subtype.eq $ by simp,
+ λ ⟨g, hg⟩, subtype.eq $ by simp⟩
+
+noncomputable def group_equiv_left_cosets_times_subgroup (hs : is_subgroup s) :
+  α ≃ (left_cosets s × s) :=
+calc α ≃ Σ L : left_cosets s, {x // ⟦x⟧ = L} :
+  equiv.equiv_fib quotient.mk
+    ... ≃ Σ L : left_cosets s, left_coset (quotient.out L) s :
+  equiv.sigma_congr_right (λ L, by rw ← left_cosets.left_coset; simp)
+    ... ≃ Σ L : left_cosets s, s :
+  equiv.sigma_congr_right (λ L, left_coset_equiv_subgroup _)
+    ... ≃ (left_cosets s × s) :
+  equiv.sigma_equiv_prod _ _
 
 end is_subgroup

group_theory/order_of_element.lean

@@ -124,19 +124,17 @@ 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,
+  from fintype.of_equiv α (gpowers.is_subgroup a).group_equiv_left_cosets_times_subgroup,
 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)⟩⟩,
+  from @fintype.fintype_prod_right _ _ _ ft_prod _,
 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_congr _ _ _ ft_prod (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 :