feat(group_theory/perm/basic): Bundle sigma_congr_right and sum_congr…

… into monoid_homs (#5301)

This makes the corresponding subgroups available as `monoid_hom.range`.

As a result, the old subgroup definitions can be removed.

This also adds injectivity and cardinality lemmas.

src/group_theory/perm/basic.lean

@@ -5,6 +5,9 @@ Authors: Leonardo de Moura, Mario Carneiro
 -/
 import data.equiv.basic
 import algebra.group.basic
+import algebra.group.hom
+import algebra.group.pi
+import algebra.group.prod
 /-!
 # The group of permutations (self-equivalences) of a type `α`
 
@@ -62,6 +65,27 @@ sum_congr_symm e f
   sum_congr (1 : perm α) (1 : perm β) = 1 :=
 sum_congr_refl
 
+/-- `equiv.perm.sum_congr` as a `monoid_hom`, with its two arguments bundled into a single `prod`.
+
+This is particularly useful for its `monoid_hom.range` projection, which is the subgroup of
+permutations which do not exchange elements between `α` and `β`. -/
+@[simps]
+def sum_congr_hom (α β : Type*) :
+  perm α × perm β →* perm (α ⊕ β) :=
+{ to_fun := λ a, sum_congr a.1 a.2,
+  map_one' := sum_congr_one,
+  map_mul' := λ a b, (sum_congr_mul _ _ _ _).symm}
+
+lemma sum_congr_hom_injective {α β : Type*} :
+  function.injective (sum_congr_hom α β) :=
+begin
+  rintros ⟨⟩ ⟨⟩ h,
+  rw prod.mk.inj_iff,
+  split; ext i,
+  { simpa using equiv.congr_fun h (sum.inl i), },
+  { simpa using equiv.congr_fun h (sum.inr i), },
+end
+
 @[simp] lemma sum_congr_swap_one {α β : Type*} [decidable_eq α] [decidable_eq β] (i j : α) :
   sum_congr (equiv.swap i j) (1 : perm β) = equiv.swap (sum.inl i) (sum.inl j) :=
 sum_congr_swap_refl i j
@@ -72,19 +96,38 @@ sum_congr_refl_swap i j
 
 /-! Lemmas about `equiv.perm.sigma_congr_right` re-expressed via the group structure. -/
 
-@[simp] lemma sigma_congr_right_mul {α} {β : α → Type*}
+@[simp] lemma sigma_congr_right_mul {α : Type*} {β : α → Type*}
   (F : Π a, perm (β a)) (G : Π a, perm (β a)) :
-  sigma_congr_right F * sigma_congr_right G = sigma_congr_right (λ a, F a * G a) :=
+  sigma_congr_right F * sigma_congr_right G = sigma_congr_right (F * G) :=
 sigma_congr_right_trans G F
 
-@[simp] lemma sigma_congr_right_inv {α} {β : α → Type*} (F : Π a, perm (β a)) :
+@[simp] lemma sigma_congr_right_inv {α : Type*} {β : α → Type*} (F : Π a, perm (β a)) :
   (sigma_congr_right F)⁻¹ = sigma_congr_right (λ a, (F a)⁻¹) :=
 sigma_congr_right_symm F
 
-@[simp] lemma sigma_congr_right_one {α} {β : α → Type*} :
-  (sigma_congr_right (λ a, (1 : equiv.perm $ β a))) = 1 :=
+@[simp] lemma sigma_congr_right_one {α : Type*} {β : α → Type*} :
+  (sigma_congr_right (1 : Π a, equiv.perm $ β a)) = 1 :=
 sigma_congr_right_refl
 
+/-- `equiv.perm.sigma_congr_right` as a `monoid_hom`.
+
+This is particularly useful for its `monoid_hom.range` projection, which is the subgroup of
+permutations which do not exchange elements between fibers. -/
+@[simps]
+def sigma_congr_right_hom {α : Type*} (β : α → Type*) :
+  (Π a, perm (β a)) →* perm (Σ a, β a) :=
+{ to_fun := sigma_congr_right,
+  map_one' := sigma_congr_right_one,
+  map_mul' := λ a b, (sigma_congr_right_mul _ _).symm }
+
+lemma sigma_congr_right_hom_injective {α : Type*} {β : α → Type*} :
+  function.injective (sigma_congr_right_hom β) :=
+begin
+  intros x y h,
+  ext a b,
+  simpa using equiv.congr_fun h ⟨a, b⟩,
+end
+
 end perm
 
 section swap

src/group_theory/perm/subgroup.lean

@@ -4,47 +4,32 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import group_theory.perm.basic
-import group_theory.subgroup
-import group_theory.coset
 import data.fintype.basic
+import group_theory.subgroup
 /-!
-# Subgroups within the permutations (self-equivalences) of a type `α`
+# Lemmas about subgroups within the permutations (self-equivalences) of a type `α`
 
-This file defines some `subgroup`s that exist within `equiv.perm α`.
-
-Where possible, it provides `decidable` instances so that `subgroup.quotient` is computably
-finite.
+This file provides extra lemmas about some `subgroup`s that exist within `equiv.perm α`.
+`group_theory.subgroup` depends on `group_theory.perm.basic`, so these need to be in a separate
+file.
 -/
 
 namespace equiv
 namespace perm
 
-/-- The subgroup of permutations which do not exchange elements between `α` and `β`;
-those which are of the form `sum_congr sl sr`. -/
-def sum_congr_subgroup (α β : Type*) : subgroup (perm (α ⊕ β)) :=
-{ carrier := λ σ, ∃ (sl : perm α) (sr : perm β), σ = sum_congr sl sr,
-  one_mem' := ⟨1, 1, sum_congr_one.symm⟩,
-  mul_mem' := λ σ₁ σ₂ ⟨sl₁₂, sr₁₂, h₁₂⟩ ⟨sl₂₃, sr₂₃, h₂₃⟩,
-    ⟨sl₁₂ * sl₂₃, sr₁₂ * sr₂₃, h₂₃.symm ▸ h₁₂.symm ▸ sum_congr_mul sl₁₂ sr₁₂ sl₂₃ sr₂₃⟩,
-  inv_mem' := λ σ₁ ⟨sl, sr, h⟩, ⟨sl⁻¹, sr⁻¹, h.symm ▸ sum_congr_inv sl sr⟩ }
+universes u
 
-instance sum_congr_subgroup.decidable_mem {α β : Type*}
+@[simp]
+lemma sum_congr_hom.card_range {α β : Type*}
   [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
-  decidable_pred (λ x, x ∈ sum_congr_subgroup α β) := λ x, fintype.decidable_exists_fintype
-
-/-- The subgroup of permutations which do not exchange elements between fibers;
-those which are of the form `sigma_congr_right s`. -/
-def sigma_congr_right_subgroup {α : Type*} (β : α → Type*) : subgroup (perm (Σ a, β a)) :=
-{ carrier := λ σ, ∃ (s : Π a, perm (β a)), σ = sigma_congr_right s,
-  one_mem' := ⟨λ i, 1, sigma_congr_right_one.symm⟩,
-  mul_mem' := λ σ₁ σ₂ ⟨s₁₂, h₁₂⟩ ⟨s₂₃, h₂₃⟩,
-    ⟨λ i, s₁₂ i * s₂₃ i, h₂₃.symm ▸ h₁₂.symm ▸ sigma_congr_right_mul s₁₂ s₂₃⟩,
-  inv_mem' := λ σ₁ ⟨s, h⟩, ⟨λ i, (s i)⁻¹, h.symm ▸ sigma_congr_right_inv s⟩ }
+  fintype.card (sum_congr_hom α β).range = fintype.card (perm α × perm β) :=
+fintype.card_eq.mpr ⟨(set.range (sum_congr_hom α β) sum_congr_hom_injective).symm⟩
 
-instance sigma_congr_right_subgroup.decidable_mem {α : Type*} {β : α → Type*}
+@[simp]
+lemma sigma_congr_right_hom.card_range {α : Type*} {β : α → Type*}
   [decidable_eq α] [∀ a, decidable_eq (β a)] [fintype α] [∀ a, fintype (β a)] :
-  decidable_pred (λ x, x ∈ sigma_congr_right_subgroup β) :=
-λ x, fintype.decidable_exists_fintype
+  fintype.card (sigma_congr_right_hom β).range = fintype.card (Π a, perm (β a)) :=
+fintype.card_eq.mpr ⟨(set.range (sigma_congr_right_hom β) sigma_congr_right_hom_injective).symm⟩
 
 end perm
 end equiv