feat(group_theory/index): Relative index (#9780)

Defines relative index between subgroups, and proves that relative index is multiplicative in towers.

Author: tb65536

src/group_theory/index.lean

@@ -16,26 +16,36 @@ In this file we define the index of a subgroup, and prove several divisibility p
 
 - `H.index` : the index of `H : subgroup G` as a natural number,
   and returns 0 if the index is infinite.
+- `H.relindex K` : the relative index of `H : subgroup G` in `K : subgroup G` as a natural number,
+  and returns 0 if the relative 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`
+- `relindex_mul_relindex` : `relindex` is multiplicative in towers
 
 -/
 
 namespace subgroup
 
-variables {G : Type*} [group G] (H : subgroup G)
+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
 
+/-- The relative index of a subgroup as a natural number,
+  and returns 0 if the relative index is infinite. -/
+@[to_additive "The relative index of a subgroup as a natural number,
+  and returns 0 if the relative index is infinite."]
+noncomputable def relindex : ℕ :=
+(H.subgroup_of K).index
+
 @[to_additive] lemma index_comap_of_surjective {G' : Type*} [group G'] {f : G' →* G}
   (hf : function.surjective f) : (H.comap f).index = H.index :=
 begin
@@ -53,6 +63,33 @@ begin
     exact ⟨y, (quotient.map'_mk' f _ y).trans (congr_arg quotient.mk' hy)⟩ },
 end
 
+@[to_additive] lemma index_comap {G' : Type*} [group G'] (f : G' →* G) :
+  (H.comap f).index = H.relindex f.range :=
+eq.trans (congr_arg index (by refl))
+  ((H.subgroup_of f.range).index_comap_of_surjective f.range_restrict_surjective)
+
+variables {H K L}
+
+@[to_additive] lemma relindex_mul_index (h : H ≤ K) : H.relindex K * K.index = H.index :=
+((mul_comm _ _).trans (cardinal.to_nat_mul _ _).symm).trans
+  (congr_arg cardinal.to_nat (equiv.cardinal_eq (quotient_equiv_prod_of_le h))).symm
+
+@[to_additive] lemma index_dvd_of_le (h : H ≤ K) : K.index ∣ H.index :=
+dvd_of_mul_left_eq (H.relindex K) (relindex_mul_index h)
+
+@[to_additive] lemma relindex_subgroup_of (hKL : K ≤ L) :
+  (H.subgroup_of L).relindex (K.subgroup_of L) = H.relindex K :=
+((index_comap (H.subgroup_of L) (inclusion hKL)).trans (congr_arg _ (inclusion_range hKL))).symm
+
+@[to_additive] lemma relindex_mul_relindex (hHK : H ≤ K) (hKL : K ≤ L) :
+  H.relindex K * K.relindex L = H.relindex L :=
+begin
+  rw [←relindex_subgroup_of hKL],
+  exact relindex_mul_index (λ x hx, hHK hx),
+end
+
+variables (H K L)
+
 @[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
@@ -71,14 +108,4 @@ begin
   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 (quotient_equiv_prod_of_le h).cardinal_eq)).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