chore(group_theory/subgroup/basic): split out finiteness (#18242)

Ruben-VandeVelde · Ruben-VandeVelde · commit 6f9f36364eae · 2023-01-20T23:55:55.000Z
It feels like it should be possible to define subgroups without relying on all the infrastructure about finite sets and types, and it turns out that it is with fairly limited work. This also has the advantage of removing a few hundred lines of code from what's still one of mathlib's biggest files.
diff --git a/src/algebra/module/submodule/basic.lean b/src/algebra/module/submodule/basic.lean
@@ -6,6 +6,8 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 import algebra.module.linear_map
 import algebra.module.equiv
 import group_theory.group_action.sub_mul_action
+import group_theory.submonoid.membership
+
 /-!
 
 # Submodules of a module
diff --git a/src/algebra/periodic.lean b/src/algebra/periodic.lean
@@ -3,12 +3,14 @@ Copyright (c) 2021 Benjamin Davidson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Benjamin Davidson
 -/
+import algebra.big_operators.basic
 import algebra.field.opposite
 import algebra.module.basic
 import algebra.order.archimedean
 import data.int.parity
 import group_theory.coset
 import group_theory.subgroup.zpowers
+import group_theory.submonoid.membership
 
 /-!
 # Periodicity
diff --git a/src/group_theory/commutator.lean b/src/group_theory/commutator.lean
@@ -5,7 +5,7 @@ Authors: Jordan Brown, Thomas Browning, Patrick Lutz
 -/
 
 import data.bracket
-import group_theory.subgroup.basic
+import group_theory.subgroup.finite
 import tactic.group
 
 /-!
diff --git a/src/group_theory/coset.lean b/src/group_theory/coset.lean
@@ -5,6 +5,7 @@ Authors: Mitchell Rowett, Scott Morrison
 -/
 
 import algebra.quotient
+import data.fintype.prod
 import group_theory.group_action.basic
 import group_theory.subgroup.mul_opposite
 import tactic.group
diff --git a/src/group_theory/free_group.lean b/src/group_theory/free_group.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 import data.fintype.basic
+import data.list.sublists
 import group_theory.subgroup.basic
 
 /-!
diff --git a/src/group_theory/group_action/basic.lean b/src/group_theory/group_action/basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
+import data.fintype.card
 import group_theory.group_action.defs
 import group_theory.group_action.group
 import data.setoid.basic
@@ -28,7 +29,7 @@ of `•` belong elsewhere.
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
-open_locale big_operators pointwise
+open_locale pointwise
 open function
 
 namespace mul_action
diff --git a/src/group_theory/noncomm_pi_coprod.lean b/src/group_theory/noncomm_pi_coprod.lean
@@ -7,6 +7,7 @@ import group_theory.order_of_element
 import data.finset.noncomm_prod
 import data.fintype.big_operators
 import data.nat.gcd.big_operators
+import order.sup_indep
 
 /-!
 # Canonical homomorphism from a finite family of monoids
@@ -42,6 +43,44 @@ images of different morphisms commute, we obtain a canonical morphism
 
 open_locale big_operators
 
+namespace subgroup
+
+variables {G : Type*} [group G]
+
+/-- `finset.noncomm_prod` is “injective” in `f` if `f` maps into independent subgroups.  This
+generalizes (one direction of) `subgroup.disjoint_iff_mul_eq_one`. -/
+@[to_additive "`finset.noncomm_sum` is “injective” in `f` if `f` maps into independent subgroups.
+This generalizes (one direction of) `add_subgroup.disjoint_iff_add_eq_zero`. "]
+lemma eq_one_of_noncomm_prod_eq_one_of_independent {ι : Type*} (s : finset ι) (f : ι → G) (comm)
+  (K : ι → subgroup G) (hind : complete_lattice.independent K) (hmem : ∀ (x ∈ s), f x ∈ K x)
+  (heq1 : s.noncomm_prod f comm = 1) : ∀ (i ∈ s), f i = 1 :=
+begin
+  classical,
+  revert heq1,
+  induction s using finset.induction_on with i s hnmem ih,
+  { simp, },
+  { have hcomm := comm.mono (finset.coe_subset.2 $ finset.subset_insert _ _),
+    simp only [finset.forall_mem_insert] at hmem,
+    have hmem_bsupr: s.noncomm_prod f hcomm ∈ ⨆ (i ∈ (s : set ι)), K i,
+    { refine subgroup.noncomm_prod_mem _ _ _,
+      intros x hx,
+      have : K x ≤ ⨆ (i ∈ (s : set ι)), K i := le_supr₂ x hx,
+      exact this (hmem.2 x hx), },
+    intro heq1,
+    rw finset.noncomm_prod_insert_of_not_mem _ _ _ _ hnmem at heq1,
+    have hnmem' : i ∉ (s : set ι), by simpa,
+    obtain ⟨heq1i : f i = 1, heq1S : s.noncomm_prod f _ = 1⟩ :=
+      subgroup.disjoint_iff_mul_eq_one.mp (hind.disjoint_bsupr hnmem') hmem.1 hmem_bsupr heq1,
+    intros i h,
+    simp only [finset.mem_insert] at h,
+    rcases h with ⟨rfl | _⟩,
+    { exact heq1i },
+    { exact ih hcomm hmem.2 heq1S _ h } }
+end
+
+end subgroup
+
+
 section family_of_monoids
 
 variables {M : Type*} [monoid M]
diff --git a/src/group_theory/perm/subgroup.lean b/src/group_theory/perm/subgroup.lean
@@ -5,7 +5,7 @@ Authors: Eric Wieser
 -/
 import group_theory.perm.basic
 import data.fintype.perm
-import group_theory.subgroup.basic
+import group_theory.subgroup.finite
 /-!
 # Lemmas about subgroups within the permutations (self-equivalences) of a type `α`
 
diff --git a/src/group_theory/quotient_group.lean b/src/group_theory/quotient_group.lean
@@ -7,6 +7,7 @@ This file is to a certain extent based on `quotient_module.lean` by Johannes Hö
 -/
 import group_theory.congruence
 import group_theory.coset
+import group_theory.subgroup.finite
 import group_theory.subgroup.pointwise
 
 /-!
diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
diff --git a/src/group_theory/subgroup/finite.lean b/src/group_theory/subgroup/finite.lean
