feat(group_theory/index): Index of top and bottom subgroups (#9819)

This PR computes the index of the top and bottom subgroups.



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

src/group_theory/index.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 -/
 
-import group_theory.coset
+import group_theory.quotient_group
 import set_theory.cardinal
 
 /-!
@@ -31,13 +31,15 @@ In this file we define the index of a subgroup, and prove several divisibility p
 
 namespace subgroup
 
+open_locale cardinal
+
 variables {G : Type*} [group G] (H K L : 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
+(#(quotient_group.quotient H)).to_nat
 
 /-- The relative index of a subgroup as a natural number,
   and returns 0 if the relative index is infinite. -/
@@ -90,6 +92,15 @@ end
 
 variables (H K L)
 
+@[simp, to_additive] lemma index_top : (⊤ : subgroup G).index = 1 :=
+cardinal.to_nat_eq_one_iff_unique.mpr ⟨quotient_group.subsingleton_quotient_top, ⟨1⟩⟩
+
+@[to_additive] lemma index_bot : (⊥ : subgroup G).index = cardinal.to_nat (#G) :=
+cardinal.to_nat_congr (quotient_group.quotient_bot.to_equiv)
+
+@[to_additive] lemma index_bot_eq_card [fintype G] : (⊥ : subgroup G).index = fintype.card G :=
+index_bot.trans cardinal.mk_to_nat_eq_card
+
 @[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

src/set_theory/cardinal.lean

@@ -982,13 +982,21 @@ lemma mk_to_nat_eq_card [fintype α] : (#α).to_nat = fintype.card α :=
 by simp [fintype_card]
 
 @[simp]
-lemma zero_to_nat : cardinal.to_nat 0 = 0 :=
+lemma zero_to_nat : to_nat 0 = 0 :=
 by rw [← to_nat_cast 0, nat.cast_zero]
 
 @[simp]
-lemma one_to_nat : cardinal.to_nat 1 = 1 :=
+lemma one_to_nat : to_nat 1 = 1 :=
 by rw [← to_nat_cast 1, nat.cast_one]
 
+@[simp] lemma to_nat_eq_one {c : cardinal} : to_nat c = 1 ↔ c = 1 :=
+⟨λ h, (cast_to_nat_of_lt_omega (lt_of_not_ge (one_ne_zero ∘ h.symm.trans ∘
+  to_nat_apply_of_omega_le))).symm.trans ((congr_arg coe h).trans nat.cast_one),
+  λ h, (congr_arg to_nat h).trans one_to_nat⟩
+
+lemma to_nat_eq_one_iff_unique {α : Type*} : (#α).to_nat = 1 ↔ subsingleton α ∧ nonempty α :=
+to_nat_eq_one.trans eq_one_iff_unique
+
 @[simp] lemma to_nat_lift (c : cardinal.{v}) : (lift.{u v} c).to_nat = c.to_nat :=
 begin
   apply nat_cast_injective,