refactor(group_theory/schur_zassenhaus): Golf proof of abelian case (#…

…13622)

This PR golfs the proof of the abelian case of Schur-Zassenhaus by switching from a nonstandard definition of the difference of two left transversals to the definition used in `transfer.lean`.

src/group_theory/schur_zassenhaus.lean

@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 -/
 
-import group_theory.complement
-import group_theory.group_action.basic
 import group_theory.sylow
+import group_theory.transfer
 
 /-!
 # The Schur-Zassenhaus Theorem
@@ -29,110 +28,80 @@ namespace subgroup
 
 section schur_zassenhaus_abelian
 
-open mem_left_transversals
+open mul_opposite mul_action subgroup.left_transversals mem_left_transversals
 
-variables {G : Type*} [group G] {H : subgroup G}
+variables {G : Type*} [group G] (H : subgroup G) [is_commutative H] [fintype (G ⧸ H)]
+  (α β : left_transversals (H : set G))
 
-variables [is_commutative H] [fintype (G ⧸ H)]
+/-- The quotient of the transversals of an abelian normal `N` by the `diff` relation. -/
+def quotient_diff :=
+quotient (setoid.mk (λ α β, diff (monoid_hom.id H) α β = 1) ⟨λ α, diff_self (monoid_hom.id H) α,
+  λ α β h, by rw [←diff_inv, h, one_inv], λ α β γ h h', by rw [←diff_mul_diff, h, h', one_mul]⟩)
 
-variables (α β γ : left_transversals (H : set G))
+instance : inhabited H.quotient_diff := quotient.inhabited _
 
-/-- The difference of two left transversals -/
-@[to_additive "The difference of two left transversals"]
-noncomputable def diff [hH : normal H] : H :=
-∏ (q : G ⧸ H), ⟨(to_equiv α.2 q) * (to_equiv β.2 q)⁻¹, hH.mem_comm (quotient.exact'
-  (((to_equiv β.2).symm_apply_apply q).trans ((to_equiv α.2).symm_apply_apply q).symm))⟩
-
-@[to_additive] lemma diff_mul_diff [normal H] : diff α β * diff β γ = diff α γ :=
-finset.prod_mul_distrib.symm.trans (finset.prod_congr rfl (λ x hx, subtype.ext
-  (by rw [coe_mul, coe_mk, coe_mk, coe_mk, mul_assoc, inv_mul_cancel_left])))
-
-@[to_additive] lemma diff_self [normal H] : diff α α = 1 :=
-mul_right_eq_self.mp (diff_mul_diff α α α)
-
-@[to_additive] lemma diff_inv [normal H]: (diff α β)⁻¹ = diff β α :=
-inv_eq_of_mul_eq_one ((diff_mul_diff α β α).trans (diff_self α))
-
-lemma smul_diff_smul [hH : normal H] (g : G) :
-  diff (g • α) (g • β) = ⟨g * diff α β * g⁻¹, hH.conj_mem (diff α β).1 (diff α β).2 g⟩ :=
+lemma smul_diff_smul' [hH : normal H] (g : Gᵐᵒᵖ) :
+  diff (monoid_hom.id H) (g • α) (g • β) = ⟨g.unop⁻¹ * (diff (monoid_hom.id H) α β : H) * g.unop,
+    hH.mem_comm ((congr_arg (∈ H) (mul_inv_cancel_left _ _)).mpr (set_like.coe_mem _))⟩ :=
 begin
   let ϕ : H →* H :=
-  { to_fun := λ h, ⟨g * h * g⁻¹, hH.conj_mem h.1 h.2 g⟩,
-    map_one' := subtype.ext (by rw [coe_mk, coe_one, mul_one, mul_inv_self]),
-    map_mul' := λ h₁ h₂, subtype.ext (by rw [coe_mk, coe_mul, coe_mul, coe_mk, coe_mk, mul_assoc,
-      mul_assoc, mul_assoc, mul_assoc, mul_assoc, inv_mul_cancel_left]) },
-  refine eq.trans (finset.prod_bij' (λ q _, (↑g)⁻¹ * q) (λ _ _, finset.mem_univ _)
-    (λ q _, subtype.ext _) (λ q _, ↑g * q) (λ _ _, finset.mem_univ _)
-    (λ q _, mul_inv_cancel_left g q) (λ q _, inv_mul_cancel_left g q)) (ϕ.map_prod _ _).symm,
-  change _ * _ = g * (_ * _) * g⁻¹,
-  simp_rw [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul, mul_inv_rev, mul_assoc],
-  refl,
+  { to_fun := λ h, ⟨g.unop⁻¹ * h * g.unop,
+      hH.mem_comm ((congr_arg (∈ H) (mul_inv_cancel_left _ _)).mpr (set_like.coe_mem _))⟩,
+    map_one' := by rw [subtype.ext_iff, coe_mk, coe_one, mul_one, inv_mul_self],
+    map_mul' := λ h₁ h₂, by rw [subtype.ext_iff, coe_mk, coe_mul, coe_mul, coe_mk, coe_mk,
+      mul_assoc, mul_assoc, mul_assoc, mul_assoc, mul_assoc, mul_inv_cancel_left] },
+  refine eq.trans (finset.prod_bij' (λ q _, g⁻¹ • q) (λ q _, finset.mem_univ _)
+    (λ q _, subtype.ext _) (λ q _, g • q) (λ q _, finset.mem_univ _) (λ q _, smul_inv_smul g q)
+    (λ q _, inv_smul_smul g q)) (map_prod ϕ _ _).symm,
+  simp_rw [monoid_hom.id_apply, monoid_hom.coe_mk, coe_mk, smul_apply_eq_smul_apply_inv_smul,
+    smul_eq_mul_unop, mul_inv_rev, mul_assoc],
 end
 
-lemma smul_diff [H.normal] (h : H) :
-  diff (h • α) β = h ^ H.index * diff α β :=
+variables {H} [normal H]
+
+instance : mul_action G H.quotient_diff :=
+{ smul := λ g, quotient.map' (λ α, op g⁻¹ • α) (λ α β h, subtype.ext (by rwa [smul_diff_smul',
+    coe_mk, coe_one, mul_eq_one_iff_eq_inv, mul_right_eq_self, ←coe_one, ←subtype.ext_iff])),
+  mul_smul := λ g₁ g₂ q, quotient.induction_on' q (λ T, congr_arg quotient.mk'
+    (by rw mul_inv_rev; exact mul_smul (op g₁⁻¹) (op g₂⁻¹) T)),
+  one_smul := λ q, quotient.induction_on' q (λ T, congr_arg quotient.mk'
+    (by rw one_inv; apply one_smul Gᵐᵒᵖ T)) }
+
+lemma smul_diff' (h : H) :
+  diff (monoid_hom.id H) α ((op (h : G)) • β) = diff (monoid_hom.id H) α β * h ^ H.index :=
 begin
   rw [diff, diff, index_eq_card, ←finset.card_univ, ←finset.prod_const, ←finset.prod_mul_distrib],
   refine finset.prod_congr rfl (λ q _, _),
-  rw [subtype.ext_iff, coe_mul, coe_mk, coe_mk, ←mul_assoc, mul_right_cancel_iff],
-  rw [smul_def, smul_apply_eq_smul_apply_inv_smul, smul_eq_mul],
-  rw [mul_left_cancel_iff, ←subtype.ext_iff, equiv.apply_eq_iff_eq, inv_smul_eq_iff],
-  exact self_eq_mul_left.mpr ((quotient_group.eq_one_iff _).mpr h.2),
+  simp_rw [subtype.ext_iff, monoid_hom.id_apply, coe_mul, coe_mk, mul_assoc, mul_right_inj],
+  rw [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, unop_op,
+      mul_left_inj, ←subtype.ext_iff, equiv.apply_eq_iff_eq, inv_smul_eq_iff],
+  exact self_eq_mul_right.mpr ((quotient_group.eq_one_iff _).mpr h.2),
 end
 
-variables (H)
-
-instance setoid_diff [H.normal] : setoid (left_transversals (H : set G)) :=
-setoid.mk (λ α β, diff α β = 1) ⟨λ α, diff_self α, λ α β h₁,
-  by rw [←diff_inv, h₁, one_inv], λ α β γ h₁ h₂, by rw [←diff_mul_diff, h₁, h₂, one_mul]⟩
-
-/-- The quotient of the transversals of an abelian normal `N` by the `diff` relation -/
-def quotient_diff [H.normal] :=
-quotient H.setoid_diff
-
-instance [H.normal] : inhabited H.quotient_diff := quotient.inhabited _
-
-variables {H}
-
-instance [H.normal] : mul_action G H.quotient_diff :=
-{ smul := λ g, quotient.map (λ α, g • α) (λ α β h, (smul_diff_smul α β g).trans
-    (subtype.ext (mul_inv_eq_one.mpr (mul_right_eq_self.mpr (subtype.ext_iff.mp h))))),
-  mul_smul := λ g₁ g₂ q, quotient.induction_on q (λ α, congr_arg quotient.mk (mul_smul g₁ g₂ α)),
-  one_smul := λ q, quotient.induction_on q (λ α, congr_arg quotient.mk (one_smul G α)) }
-
 variables [fintype H]
 
-lemma exists_smul_eq [H.normal] (α β : H.quotient_diff)
-  (hH : nat.coprime (fintype.card H) H.index) :
-  ∃ h : H, h • α = β :=
-quotient.induction_on α (quotient.induction_on β
-  (λ β α, exists_imp_exists (λ n, quotient.sound)
-    ⟨(pow_coprime hH).symm (diff α β)⁻¹, by
-    { change diff ((_ : H) • _) _ = 1,
-      rw smul_diff,
-      change pow_coprime hH ((pow_coprime hH).symm (diff α β)⁻¹) * (diff α β) = 1,
-      rw [equiv.apply_symm_apply, inv_mul_self] }⟩))
-
-lemma smul_left_injective [H.normal] (α : H.quotient_diff)
-  (hH : nat.coprime (fintype.card H) H.index) :
-  function.injective (λ h : H, h • α) :=
-λ h₁ h₂, begin
-  refine quotient.induction_on α (λ α hα, _),
-  replace hα : diff (h₁ • α) (h₂ • α) = 1 := quotient.exact hα,
-  rw [smul_diff, ←diff_inv, smul_diff, diff_self, mul_one, mul_inv_eq_one] at hα,
-  exact (pow_coprime hH).injective hα,
-end
+lemma eq_one_of_smul_eq_one (hH : nat.coprime (fintype.card H) H.index)
+  (α : H.quotient_diff) (h : H) : h • α = α → h = 1 :=
+quotient.induction_on' α $ λ α hα, (pow_coprime hH).injective $
+  calc h ^ H.index = diff (monoid_hom.id H) ((op ((h⁻¹ : H) : G)) • α) α :
+    by rw [←diff_inv, smul_diff', diff_self, one_mul, inv_pow, inv_inv]
+  ... = 1 ^ H.index : (quotient.exact' hα).trans (one_pow H.index).symm
+
+lemma exists_smul_eq (hH : nat.coprime (fintype.card H) H.index)
+  (α β : H.quotient_diff) : ∃ h : H, h • α = β :=
+quotient.induction_on' α (quotient.induction_on' β (λ β α, exists_imp_exists (λ n, quotient.sound')
+  ⟨(pow_coprime hH).symm (diff (monoid_hom.id H) β α), (diff_inv _ _ _).symm.trans
+  (inv_eq_one.mpr ((smul_diff' β α ((pow_coprime hH).symm (diff (monoid_hom.id H) β α))⁻¹).trans
+  (by rw [inv_pow, ←pow_coprime_apply hH, equiv.apply_symm_apply, mul_inv_self])))⟩))
 
-lemma is_complement'_stabilizer_of_coprime [H.normal] {α : H.quotient_diff}
-  (hH : nat.coprime (fintype.card H) H.index) : is_complement' H (mul_action.stabilizer G α) :=
-is_complement'_stabilizer α (λ h hh, smul_left_injective α hH (hh.trans (one_smul H α).symm))
-  (λ g, exists_smul_eq (g • α) α hH)
+lemma is_complement'_stabilizer_of_coprime {α : H.quotient_diff}
+  (hH : nat.coprime (fintype.card H) H.index) : is_complement' H (stabilizer G α) :=
+is_complement'_stabilizer α (eq_one_of_smul_eq_one hH α) (λ g, exists_smul_eq hH (g • α) α)
 
 /-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime` -/
-private lemma exists_right_complement'_of_coprime_aux [H.normal]
+private lemma exists_right_complement'_of_coprime_aux
   (hH : nat.coprime (fintype.card H) H.index) : ∃ K : subgroup G, is_complement' H K :=
-nonempty_of_inhabited.elim
-  (λ α : H.quotient_diff, ⟨mul_action.stabilizer G α, is_complement'_stabilizer_of_coprime hH⟩)
+nonempty_of_inhabited.elim (λ α, ⟨stabilizer G α, is_complement'_stabilizer_of_coprime hH⟩)
 
 end schur_zassenhaus_abelian