feat(group_theory/subgroup): lemmas for normal subgroups of subgroups (…

…#7271)

Co-authored-by: Hanting Zhang <76727734+acxxa@users.noreply.github.com>

src/group_theory/subgroup.lean

@@ -366,7 +366,6 @@ lemma subtype_comp_inclusion {H K : subgroup G} (hH : H ≤ K) :
   K.subtype.comp (inclusion hH) = H.subtype :=
 by { ext, simp }
 
-
 /-- The subgroup `G` of the group `G`. -/
 @[to_additive "The `add_subgroup G` of the `add_group G`."]
 instance : has_top (subgroup G) :=
@@ -821,6 +820,14 @@ lemma map_supr {ι : Sort*} (f : G →* N) (s : ι → subgroup G) :
   (supr s).map f = ⨆ i, (s i).map f :=
 (gc_map_comap f).l_supr
 
+@[to_additive] lemma comap_sup_comap_le
+  (H K : subgroup N) (f : G →* N) : comap f H ⊔ comap f K ≤ comap f (H ⊔ K) :=
+monotone.le_map_sup (λ _ _, comap_mono) H K
+
+@[to_additive] lemma supr_comap_le {ι : Sort*} (f : G →* N) (s : ι → subgroup N) :
+  (⨆ i, (s i).comap f) ≤ (supr s).comap f :=
+monotone.le_map_supr (λ _ _, comap_mono)
+
 @[to_additive]
 lemma comap_inf (H K : subgroup N) (f : G →* N) : (H ⊓ K).comap f = H.comap f ⊓ K.comap f :=
 (gc_map_comap f).u_inf
@@ -830,6 +837,17 @@ lemma comap_infi {ι : Sort*} (f : G →* N) (s : ι → subgroup N) :
   (infi s).comap f = ⨅ i, (s i).comap f :=
 (gc_map_comap f).u_infi
 
+@[to_additive] lemma map_inf_le (H K : subgroup G) (f : G →* N) :
+  map f (H ⊓ K) ≤ map f H ⊓ map f K :=
+le_inf (map_mono inf_le_left) (map_mono inf_le_right)
+
+@[to_additive] lemma map_inf_eq (H K : subgroup G) (f : G →* N) (hf : function.injective f) :
+  map f (H ⊓ K) = map f H ⊓ map f K :=
+begin
+  rw ← set_like.coe_set_eq,
+  simp [set.image_inter hf],
+end
+
 @[simp, to_additive] lemma map_bot (f : G →* N) : (⊥ : subgroup G).map f = ⊥ :=
 (gc_map_comap f).l_bot
 
@@ -844,6 +862,25 @@ ext $ λ x, and_iff_right_of_imp (λ _, x.prop)
 lemma comap_subtype_inf_right {H K : subgroup G} : comap K.subtype (H ⊓ K) = comap K.subtype H :=
 ext $ λ x, and_iff_left_of_imp (λ _, x.prop)
 
+/-- For any subgroups `H` and `K`, view `H ⊓ K` as a subgroup of `K`. -/
+@[to_additive "For any subgroups `H` and `K`, view `H ⊓ K` as a subgroup of `K`."]
+def subgroup_of (H K : subgroup G) : subgroup K := H.comap K.subtype
+
+@[to_additive] lemma coe_subgroup_of (H K : subgroup G) :
+  (H.subgroup_of K : set K) = K.subtype ⁻¹' H := rfl
+
+@[to_additive] lemma mem_subgroup_of {H K : subgroup G} {h : K} :
+  h ∈ H.subgroup_of K ↔ (h : G) ∈ H :=
+iff.rfl
+
+@[to_additive] lemma subgroup_of_map_subtype (H K : subgroup G) :
+  (H.subgroup_of K).map K.subtype = H ⊓ K := set_like.ext'
+begin
+  convert set.image_preimage_eq_inter_range,
+  simp only [subtype.range_coe_subtype, coe_subtype, coe_inf],
+  refl,
+end
+
 /-- Given `subgroup`s `H`, `K` of groups `G`, `N` respectively, `H × K` as a subgroup of `G × N`. -/
 @[to_additive prod "Given `add_subgroup`s `H`, `K` of `add_group`s `A`, `B` respectively, `H × K`
 as an `add_subgroup` of `A × B`."]
@@ -1294,7 +1331,10 @@ instance decidable_mem_ker [decidable_eq N] (f : G →* N) :
 @[to_additive]
 lemma comap_ker (g : N →* P) (f : G →* N) : g.ker.comap f = (g.comp f).ker := rfl
 
-@[to_additive] lemma range_restrict_ker (f : G →* N) : ker (range_restrict f) = ker f :=
+@[simp, to_additive] lemma comap_bot (f : G →* N) :
+  (⊥ : subgroup N).comap f = f.ker := rfl
+
+@[to_additive] lemma range_restrict_ker  (f : G →* N) : ker (range_restrict f) = ker f :=
 begin
   ext,
   change (⟨f x, _⟩ : range f) = ⟨1, _⟩ ↔ f x = 1,
@@ -1391,35 +1431,34 @@ namespace subgroup
 
 open monoid_hom
 
-variables {H : Type*} [group H]
+variables {N : Type*} [group N] (f : G →* N)
 
 @[to_additive]
-lemma map_le_range (f : G →* H) (K : subgroup G) : map f K ≤ f.range :=
+lemma map_le_range (H : subgroup G) : map f H ≤ f.range :=
 (range_eq_map f).symm ▸ map_mono le_top
 
 @[to_additive]
-lemma ker_le_comap (f : G →* H) (K : subgroup H) : f.ker ≤ comap f K :=
+lemma ker_le_comap (H : subgroup N) : f.ker ≤ comap f H :=
 comap_mono bot_le
 
 @[to_additive]
-lemma map_comap_le (f : G →* H) (K : subgroup H) : map f (comap f K) ≤ K :=
+lemma map_comap_le (H : subgroup N) : map f (comap f H) ≤ H :=
 (gc_map_comap f).l_u_le _
 
 @[to_additive]
-lemma le_comap_map (f : G →* H) (K : subgroup G) : K ≤ comap f (map f K) :=
+lemma le_comap_map (H : subgroup G) : H ≤ comap f (map f H) :=
 (gc_map_comap f).le_u_l _
 
 @[to_additive]
-lemma map_comap_eq (f : G →* H) (K : subgroup H) :
-  map f (comap f K) = f.range ⊓ K :=
+lemma map_comap_eq (H : subgroup N) :
+  map f (comap f H) = f.range ⊓ H :=
 set_like.ext' begin
   convert set.image_preimage_eq_inter_range,
   simp [set.inter_comm],
 end
 
 @[to_additive]
-lemma comap_map_eq (f : G →* H) (K : subgroup G) :
-  comap f (map f K) = K ⊔ f.ker :=
+lemma comap_map_eq (H : subgroup G) : comap f (map f H) = H ⊔ f.ker :=
 begin
   refine le_antisymm _ (sup_le (le_comap_map _ _) (ker_le_comap _ _)),
   intros x hx, simp only [exists_prop, mem_map, mem_comap] at hx,
@@ -1430,38 +1469,58 @@ begin
 end
 
 @[to_additive]
-lemma map_comap_eq_self {f : G →* H} {K : subgroup H} (h : K ≤ f.range) :
-  map f (comap f K) = K :=
+lemma map_comap_eq_self {f : G →* N} {H : subgroup N} (h : H ≤ f.range) :
+  map f (comap f H) = H :=
 by rwa [map_comap_eq, inf_eq_right]
 
 @[to_additive]
-lemma map_comap_eq_self_of_surjective {f : G →* H} (h : function.surjective f) (K : subgroup H) :
-  map f (comap f K) = K :=
+lemma map_comap_eq_self_of_surjective {f : G →* N} (h : function.surjective f) (H : subgroup N) :
+  map f (comap f H) = H :=
 map_comap_eq_self ((range_top_of_surjective _ h).symm ▸ le_top)
 
 @[to_additive]
-lemma comap_injective {f : G →* H} (h : function.surjective f) : function.injective (comap f) :=
+lemma comap_injective {f : G →* N} (h : function.surjective f) : function.injective (comap f) :=
 λ K L hKL, by { apply_fun map f at hKL, simpa [map_comap_eq_self_of_surjective h] using hKL }
 
 @[to_additive]
-lemma comap_map_eq_self {f : G →* H} {K : subgroup G} (h : f.ker ≤ K) :
-  comap f (map f K) = K :=
+lemma comap_map_eq_self {f : G →* N} {H : subgroup G} (h : f.ker ≤ H) :
+  comap f (map f H) = H :=
 by rwa [comap_map_eq, sup_eq_left]
 
 @[to_additive]
-lemma comap_map_eq_self_of_injective {f : G →* H} (h : function.injective f) (K : subgroup G) :
-  comap f (map f K) = K :=
+lemma comap_map_eq_self_of_injective {f : G →* N} (h : function.injective f) (H : subgroup G) :
+  comap f (map f H) = H :=
 comap_map_eq_self (((ker_eq_bot_iff _).mpr h).symm ▸ bot_le)
 
 @[to_additive]
-lemma map_injective {f : G →* H} (h : function.injective f) : function.injective (map f) :=
+lemma map_injective {f : G →* N} (h : function.injective f) : function.injective (map f) :=
 λ K L hKL, by { apply_fun comap f at hKL, simpa [comap_map_eq_self_of_injective h] using hKL }
 
 @[to_additive]
-lemma map_eq_comap_of_inverse {f : G →* H} {g : H →* G} (hl : function.left_inverse g f)
-  (hr : function.right_inverse g f) (K : subgroup G) : map f K = comap g K :=
+lemma map_eq_comap_of_inverse {f : G →* N} {g : N →* G} (hl : function.left_inverse g f)
+  (hr : function.right_inverse g f) (H : subgroup G) : map f H = comap g H :=
 set_like.ext' $ by rw [coe_map, coe_comap, set.image_eq_preimage_of_inverse hl hr]
 
+/-- Given `f(A) = f(B)`, `ker f ≤ A`, and `ker f ≤ B`, deduce that `A = B`  -/
+@[to_additive] lemma map_injective_of_ker_le
+  {H K : subgroup G} (hH : f.ker ≤ H) (hK : f.ker ≤ K) (hf : map f H = map f K) :
+  H = K :=
+begin
+  apply_fun comap f at hf,
+  rwa [comap_map_eq, comap_map_eq, sup_of_le_left hH, sup_of_le_left hK] at hf,
+end
+
+@[to_additive] lemma comap_sup_eq
+  (H K : subgroup N) (hf : function.surjective f):
+  comap f H ⊔ comap f K = comap f (H ⊔ K) :=
+begin
+  have : map f (comap f H ⊔ comap f K) = map f (comap f (H ⊔ K)),
+  { simp [subgroup.map_comap_eq, map_sup, f.range_top_of_surjective hf], },
+  refine map_injective_of_ker_le f _ _ this,
+  { calc f.ker ≤ comap f H : ker_le_comap f _
+           ... ≤ comap f H ⊔ comap f K : le_sup_left, },
+  exact ker_le_comap _ _,
+end
 
 end subgroup
 
@@ -1776,10 +1835,10 @@ end is_simple_group
 
 end
 
-section pointwise
-
 namespace subgroup
 
+section pointwise
+
 @[to_additive]
 lemma closure_mul_le (S T : set G) : closure (S * T) ≤ closure S ⊔ closure T :=
 Inf_le $ λ x ⟨s, t, hs, ht, hx⟩, hx ▸ (closure S ⊔ closure T).mul_mem
@@ -1837,10 +1896,113 @@ set.subset.antisymm
     by { rw sup_eq_closure, apply Inf_le _, dsimp, refl })
   ((sup_eq_closure N H).symm ▸ subset_closure)
 
-end subgroup
+@[to_additive] lemma mul_inf_assoc (A B C : subgroup G) (h : A ≤ C) :
+  (A : set G) * ↑(B ⊓ C) = (A * B) ⊓ C :=
+begin
+  ext,
+  simp only [coe_inf, set.inf_eq_inter, set.mem_mul, set.mem_inter_iff],
+  split,
+  { rintros ⟨y, z, hy, ⟨hzB, hzC⟩, rfl⟩,
+    refine ⟨_, mul_mem C (h hy) hzC⟩,
+    exact ⟨y, z, hy, hzB, rfl⟩ },
+  rintros ⟨⟨y, z, hy, hz, rfl⟩, hyz⟩,
+  refine ⟨y, z, hy, ⟨hz, _⟩, rfl⟩,
+  suffices : y⁻¹ * (y * z) ∈ C, { simpa },
+  exact mul_mem C (inv_mem C (h hy)) hyz
+end
+
+@[to_additive] lemma inf_mul_assoc (A B C : subgroup G) (h : C ≤ A) :
+  ((A ⊓ B : subgroup G) : set G) * C = A ⊓ (B * C) :=
+begin
+  ext,
+  simp only [coe_inf, set.inf_eq_inter, set.mem_mul, set.mem_inter_iff],
+  split,
+  { rintros ⟨y, z, ⟨hyA, hyB⟩, hz, rfl⟩,
+    refine ⟨mul_mem A hyA (h hz), _⟩,
+    exact ⟨y, z, hyB, hz, rfl⟩ },
+  rintros ⟨hyz, y, z, hy, hz, rfl⟩,
+  refine ⟨y, z, ⟨_, hy⟩, hz, rfl⟩,
+  suffices : (y * z) * z⁻¹ ∈ A, { simpa },
+  exact mul_mem A hyz (inv_mem A (h hz))
+end
 
 end pointwise
 
+section subgroup_normal
+
+@[to_additive] lemma normal_subgroup_of_iff {H K : subgroup G} (hHK : H ≤ K) :
+  (H.subgroup_of K).normal ↔ ∀ h k, h ∈ H → k ∈ K → k * h * k⁻¹ ∈ H :=
+⟨λ hN h k hH hK, hN.conj_mem ⟨h, hHK hH⟩ hH ⟨k, hK⟩,
+  λ hN, { conj_mem := λ h hm k, (hN h.1 k.1 hm k.2) }⟩
+
+@[to_additive] instance prod_subgroup_of_prod_normal
+  {H₁ K₁ : subgroup G} {H₂ K₂ : subgroup N}
+  [h₁ : (H₁.subgroup_of K₁).normal] [h₂ : (H₂.subgroup_of K₂).normal] :
+  ((H₁.prod H₂).subgroup_of (K₁.prod K₂)).normal :=
+{ conj_mem := λ n hgHK g,
+    ⟨h₁.conj_mem ⟨(n : G × N).fst, (mem_prod.mp n.2).1⟩
+      hgHK.1 ⟨(g : G × N).fst, (mem_prod.mp g.2).1⟩,
+    h₂.conj_mem ⟨(n : G × N).snd, (mem_prod.mp n.2).2⟩
+      hgHK.2 ⟨(g : G × N).snd, (mem_prod.mp g.2).2⟩⟩ }
+
+@[to_additive] instance prod_normal
+  (H : subgroup G) (K : subgroup N) [hH : H.normal] [hK : K.normal] :
+  (H.prod K).normal :=
+{ conj_mem := λ n hg g,
+    ⟨hH.conj_mem n.fst (subgroup.mem_prod.mp hg).1 g.fst,
+     hK.conj_mem n.snd (subgroup.mem_prod.mp hg).2 g.snd⟩ }
+
+@[to_additive] lemma inf_subgroup_of_inf_normal_of_right
+  (A B' B : subgroup G) (hB : B' ≤ B) [hN : (B'.subgroup_of B).normal] :
+  ((A ⊓ B').subgroup_of (A ⊓ B)).normal :=
+{ conj_mem := λ n hn g,
+    ⟨mul_mem A (mul_mem A (mem_inf.1 g.2).1 (mem_inf.1 n.2).1) (inv_mem A (mem_inf.1 g.2).1),
+    (normal_subgroup_of_iff hB).mp hN n g hn.2 (mem_inf.mp g.2).2⟩ }
+
+@[to_additive] lemma inf_subgroup_of_inf_normal_of_left
+  {A' A : subgroup G} (B : subgroup G) (hA : A' ≤ A) [hN : (A'.subgroup_of A).normal] :
+  ((A' ⊓ B).subgroup_of (A ⊓ B)).normal :=
+{ conj_mem := λ n hn g,
+    ⟨(normal_subgroup_of_iff hA).mp hN n g hn.1  (mem_inf.mp g.2).1,
+    mul_mem B (mul_mem B (mem_inf.1 g.2).2 (mem_inf.1 n.2).2) (inv_mem B (mem_inf.1 g.2).2)⟩ }
+
+instance sup_normal (H K : subgroup G) [hH : H.normal] [hK : K.normal] : (H ⊔ K).normal :=
+{ conj_mem := λ n hmem g,
+  begin
+    change n ∈ ↑(H ⊔ K) at hmem,
+    change g * n * g⁻¹ ∈ ↑(H ⊔ K),
+    rw [normal_mul, set.mem_mul] at *,
+    rcases hmem with ⟨h, k, hh, hk, rfl⟩,
+    refine ⟨g * h * g⁻¹, g * k * g⁻¹, hH.conj_mem h hh g, hK.conj_mem k hk g, _⟩,
+    simp
+  end }
+
+@[to_additive] instance normal_inf_normal (H K : subgroup G) [hH : H.normal] [hK : K.normal] :
+  (H ⊓ K).normal :=
+{ conj_mem := λ n hmem g,
+  by { rw mem_inf at *, exact ⟨hH.conj_mem n hmem.1 g, hK.conj_mem n hmem.2 g⟩ } }
+
+@[to_additive] lemma subgroup_of_sup (A A' B : subgroup G) (hA : A ≤ B) (hA' : A' ≤ B) :
+  (A ⊔ A').subgroup_of B = A.subgroup_of B ⊔ A'.subgroup_of B :=
+begin
+  refine map_injective_of_ker_le B.subtype
+    (ker_le_comap _ _) (le_trans (ker_le_comap B.subtype _) le_sup_left) _,
+  { simp only [subgroup_of, map_comap_eq, map_sup, subtype_range],
+    rw [inf_of_le_right (sup_le hA hA'), inf_of_le_right hA', inf_of_le_right hA] },
+end
+
+@[to_additive] lemma subgroup_normal.mem_comm {H K : subgroup G}
+  (hK : H ≤ K) [hN : (H.subgroup_of K).normal] {a b : G} (hb : b ∈ K) (h : a * b ∈ H) :
+  b * a ∈ H :=
+begin
+  have := (normal_subgroup_of_iff hK).mp hN (a * b) b h hb,
+  rwa [mul_assoc, mul_assoc, mul_right_inv, mul_one] at this,
+end
+
+end subgroup_normal
+
+end subgroup
+
 namespace is_conj
 open subgroup