feat(group_theory/index): define the index of a subgroup (#8971)

Defines `subgroup.index` and proves various divisibility properties.



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

src/group_theory/coset.lean

@@ -376,8 +376,45 @@ calc α ≃ Σ L : quotient s, {x : α // (x : quotient s) = L} :
     ... ≃ quotient s × s :
   equiv.sigma_equiv_prod _ _
 
-lemma card_eq_card_quotient_mul_card_subgroup [fintype α] (s : subgroup α) [fintype s]
-  [decidable_pred (λ a, a ∈ s)] : fintype.card α = fintype.card (quotient s) * fintype.card s :=
+variables {t : subgroup α}
+
+/-- If `H ≤ K`, then `G/H ≃ G/K × K/H` constructively, using the provided right inverse
+of the quotient map `G → G/K`. The classical version is `quotient_equiv_prod_of_le`. -/
+@[to_additive "If `H ≤ K`, then `G/H ≃ G/K × K/H` constructively, using the provided right inverse
+of the quotient map `G → G/K`. The classical version is `quotient_equiv_prod_of_le`.", simps]
+def quotient_equiv_prod_of_le' (h_le : s ≤ t)
+  (f : quotient t → α) (hf : function.right_inverse f quotient_group.mk) :
+  quotient s ≃ quotient t × quotient (s.subgroup_of t) :=
+{ to_fun := λ a, ⟨a.map' id (λ b c h, h_le h),
+    a.map' (λ g : α, ⟨(f (quotient.mk' g))⁻¹ * g, quotient.exact' (hf g)⟩) (λ b c h, by
+    { change ((f b)⁻¹ * b)⁻¹ * ((f c)⁻¹ * c) ∈ s,
+      have key : f b = f c := congr_arg f (quotient.sound' (h_le h)),
+      rwa [key, mul_inv_rev, inv_inv, mul_assoc, mul_inv_cancel_left] })⟩,
+  inv_fun := λ a, a.2.map' (λ b, f a.1 * b) (λ b c h, by
+  { change (f a.1 * b)⁻¹ * (f a.1 * c) ∈ s,
+    rwa [mul_inv_rev, mul_assoc, inv_mul_cancel_left] }),
+  left_inv := by
+  { refine quotient.ind' (λ a, _),
+    simp_rw [quotient.map'_mk', id.def, t.coe_mk, mul_inv_cancel_left] },
+  right_inv := by
+  { refine prod.rec _,
+    refine quotient.ind' (λ a, _),
+    refine quotient.ind' (λ b, _),
+    have key : quotient.mk' (f (quotient.mk' a) * b) = quotient.mk' a :=
+      (quotient_group.mk_mul_of_mem (f a) ↑b b.2).trans (hf a),
+    simp_rw [quotient.map'_mk', id.def, key, inv_mul_cancel_left, subtype.coe_eta] } }
+
+/-- If `H ≤ K`, then `G/H ≃ G/K × K/H` nonconstructively.
+The constructive version is `quotient_equiv_prod_of_le'`. -/
+@[to_additive "If `H ≤ K`, then `G/H ≃ G/K × K/H` nonconstructively.
+The constructive version is `quotient_equiv_prod_of_le'`.", simps]
+noncomputable def quotient_equiv_prod_of_le (h_le : s ≤ t) :
+  quotient s ≃ quotient t × quotient (s.subgroup_of t) :=
+quotient_equiv_prod_of_le' h_le quotient.out' quotient.out_eq'
+
+@[to_additive] lemma card_eq_card_quotient_mul_card_subgroup
+  [fintype α] (s : subgroup α) [fintype s] [decidable_pred (λ a, a ∈ s)] :
+  fintype.card α = fintype.card (quotient s) * fintype.card s :=
 by rw ← fintype.card_prod;
   exact fintype.card_congr (subgroup.group_equiv_quotient_times_subgroup)
 

src/group_theory/index.lean

@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2021 Thomas Browning. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas Browning
+-/
+
+import group_theory.coset
+import set_theory.cardinal
+
+/-!
+# Index of a Subgroup
+
+In this file we define the index of a subgroup, and prove several divisibility properties.
+
+## Main definitions
+
+- `H.index` : the index of `H : subgroup G` as a natural number,
+  and returns 0 if the index is infinite.
+
+# Main results
+
+- `index_mul_card` : `H.index * fintype.card H = fintype.card G`
+- `index_dvd_card` : `H.index ∣ fintype.card G`
+- `index_eq_mul_of_le` : If `H ≤ K`, then `H.index = K.index * (H.subgroup_of K).index`
+- `index_dvd_of_le` : If `H ≤ K`, then `K.index ∣ H.index`
+
+-/
+
+namespace subgroup
+
+variables {G : Type*} [group G] (H : subgroup G)
+
+/-- The index of a subgroup as a natural number, and returns 0 if the index is infinite. -/
+@[to_additive "The index of a subgroup as a natural number,
+and returns 0 if the index is infinite."]
+noncomputable def index : ℕ :=
+(cardinal.mk (quotient_group.quotient H)).to_nat
+
+@[to_additive] lemma index_eq_card [fintype (quotient_group.quotient H)] :
+  H.index = fintype.card (quotient_group.quotient H) :=
+cardinal.mk_to_nat_eq_card
+
+@[to_additive] lemma index_mul_card [fintype G] [hH : fintype H] :
+  H.index * fintype.card H = fintype.card G :=
+begin
+  classical,
+  rw H.index_eq_card,
+  apply H.card_eq_card_quotient_mul_card_subgroup.symm,
+end
+
+@[to_additive] lemma index_dvd_card [fintype G] : H.index ∣ fintype.card G :=
+begin
+  classical,
+  exact ⟨fintype.card H, H.index_mul_card.symm⟩,
+end
+
+variables {H} {K : subgroup G}
+
+@[to_additive] lemma index_eq_mul_of_le (h : H ≤ K) :
+  H.index = K.index * (H.subgroup_of K).index :=
+(congr_arg cardinal.to_nat (by exact cardinal.eq_congr (quotient_equiv_prod_of_le h))).trans
+  (cardinal.to_nat_mul _ _)
+
+@[to_additive] lemma index_dvd_of_le (h : H ≤ K) : K.index ∣ H.index :=
+⟨(H.subgroup_of K).index, index_eq_mul_of_le h⟩
+
+end subgroup

src/group_theory/quotient_group.lean

@@ -263,6 +263,13 @@ def quotient_ker_equiv_of_right_inverse (ψ : H → G) (hφ : function.right_inv
   right_inv := hφ,
   .. ker_lift φ }
 
+/-- The canonical isomorphism `G/⊥ ≃* G`. -/
+@[to_additive quotient_add_group.quotient_ker_equiv_of_right_inverse
+"The canonical isomorphism `G/⊥ ≃+ G`.",
+  simps]
+def quotient_bot : quotient (⊥ : subgroup G) ≃* G :=
+quotient_ker_equiv_of_right_inverse (monoid_hom.id G) id (λ x, rfl)
+
 /-- The canonical isomorphism `G/(ker φ) ≃* H` induced by a surjection `φ : G →* H`.
 
 For a `computable` version, see `quotient_group.quotient_ker_equiv_of_right_inverse`.