feat(group_theory/coset): Construct the embedding `H ⧸ ⨅ i, f i → Π i…

…, H ⧸ f i` (#16560)

This PR constructs the embedding `H ⧸ ⨅ i, f i  → Π i, H ⧸ f i`, which is needed for #16393.



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

src/group_theory/coset.lean

@@ -491,18 +491,46 @@ noncomputable def quotient_equiv_prod_of_le (h_le : s ≤ t) :
   α ⧸ s ≃ (α ⧸ t) × (t ⧸ s.subgroup_of t) :=
 quotient_equiv_prod_of_le' h_le quotient.out' quotient.out_eq'
 
-/-- If `K ≤ L`, then there is an embedding `K ⧸ (H.subgroup_of K) ↪ L ⧸ (H.subgroup_of L)`. -/
-@[to_additive "If `K ≤ L`, then there is an embedding
-  `K ⧸ (H.add_subgroup_of K) ↪ L ⧸ (H.add_subgroup_of L)`."]
-def quotient_subgroup_of_embedding_of_le (H : subgroup α) {K L : subgroup α} (h : K ≤ L) :
-  K ⧸ (H.subgroup_of K) ↪ L ⧸ (H.subgroup_of L) :=
-{ to_fun := quotient.map' (set.inclusion h) (λ a b, by { simp [left_rel_apply], exact id }),
-  inj' := begin
-    refine quotient.ind₂' (λ a b, _),
-    refine λ h, (quotient.eq'.mpr ∘ left_rel_apply.mpr) _,
-    have := left_rel_apply.mp (quotient.eq'.mp h),
-    exact this,
-  end }
+/-- If `s ≤ t`, then there is an embedding `s ⧸ H.subgroup_of s ↪ t ⧸ H.subgroup_of t`. -/
+@[to_additive "If `s ≤ t`, then there is an embedding
+  `s ⧸ H.add_subgroup_of s ↪ t ⧸ H.add_subgroup_of t`."]
+def quotient_subgroup_of_embedding_of_le (H : subgroup α) (h : s ≤ t) :
+  s ⧸ H.subgroup_of s ↪ t ⧸ H.subgroup_of t :=
+{ to_fun := quotient.map' (inclusion h) (λ a b, by { simp_rw left_rel_eq, exact id }),
+  inj' := quotient.ind₂' $ by
+  { intros a b h, simpa only [quotient.map'_mk', quotient_group.eq'] using h } }
+
+@[simp, to_additive]
+lemma quotient_subgroup_of_embedding_of_le_apply_mk (H : subgroup α) (h : s ≤ t) (g : s) :
+  quotient_subgroup_of_embedding_of_le H h (quotient_group.mk g) =
+    quotient_group.mk (inclusion h g) :=
+rfl
+
+/-- If `s ≤ t`, then there is a map `H ⧸ s.subgroup_of H → H ⧸ t.subgroup_of H`. -/
+@[to_additive "If `s ≤ t`, then there is an map
+  `H ⧸ s.add_subgroup_of H → H ⧸ t.add_subgroup_of H`."]
+def quotient_subgroup_of_map_of_le (H : subgroup α) (h : s ≤ t) :
+  H ⧸ s.subgroup_of H → H ⧸ t.subgroup_of H :=
+quotient.map' id (λ a b, by { simp_rw [left_rel_eq], apply h })
+
+@[simp, to_additive]
+lemma quotient_subgroup_of_map_of_le_apply_mk (H : subgroup α) (h : s ≤ t) (g : H) :
+  quotient_subgroup_of_map_of_le H h (quotient_group.mk g) = quotient_group.mk g :=
+rfl
+
+/-- The natural embedding `H ⧸ (⨅ i, f i).subgroup_of H ↪ Π i, H ⧸ (f i).subgroup_of H`. -/
+@[to_additive "There is an embedding
+  `H ⧸ (⨅ i, f i).add_subgroup_of H) ↪ Π i, H ⧸ (f i).add_subgroup_of H`."]
+def quotient_infi_embedding {ι : Type*} (f : ι → subgroup α) (H : subgroup α) :
+  H ⧸ (⨅ i, f i).subgroup_of H ↪ Π i, H ⧸ (f i).subgroup_of H :=
+{ to_fun := λ q i, quotient_subgroup_of_map_of_le H (infi_le f i) q,
+  inj' := quotient.ind₂' $ by simp_rw [funext_iff, quotient_subgroup_of_map_of_le_apply_mk,
+    quotient_group.eq', mem_subgroup_of, mem_infi, imp_self, forall_const] }
+
+@[simp, to_additive] lemma quotient_infi_embedding_apply_mk
+  {ι : Type*} (f : ι → subgroup α) (H : subgroup α) (g : H) (i : ι) :
+  quotient_infi_embedding f H (quotient_group.mk g) i = quotient_group.mk g :=
+rfl
 
 @[to_additive] lemma card_eq_card_quotient_mul_card_subgroup
   [fintype α] (s : subgroup α) [fintype s] [decidable_pred (λ a, a ∈ s)] :