Source: ProCGroups.NormalSubgroups.SimpleQuotients.FiniteIntersections
1import ProCGroups.NormalSubgroups.SimpleQuotients.Algebraic
3/-!
4# Finite intersections above a simple-quotient kernel
6This module proves normality of indexed intersections and shows that finite intersections retain
7the full-product property with the kernel of a noncommutative simple quotient.
8-/
10namespace ProCGroups.NormalSubgroups
12universe u
14/--
15An arbitrary infimum of normal subgroups is normal, when normality is known for every subgroup
16in the indexing set.
17-/
18theorem sInf_normal_of_forall_normal
19 {G : Type u} [Group G] {S : Set (Subgroup G)}
20 (hSnormal : ∀ M ∈ S, M.Normal) :
21 (sInf S).Normal := by
22 rw [sInf_eq_iInf']
23 exact Subgroup.normal_iInf_normal (fun M : S => hSnormal M.1 M.2)
25/--
26Finite-intersection step: in a noncommutative simple quotient, any finite intersection of normal
27subgroups whose product with K is all of G still has product \(\top\) with K.
28-/
29theorem finite_sInf_sup_eq_top_of_noncomm_simple_quotient
30 {G : Type u} [Group G] (K : Subgroup G) [K.Normal]
31 [IsSimpleGroup (G ⧸ K)]
32 (hquotNoncomm : ProCGroups.IsNoncommutativeGroup (G ⧸ K))
33 {S : Set (Subgroup G)} (hSfinite : S.Finite)
34 (hSnormal : ∀ M ∈ S, M.Normal)
35 (hStop : ∀ M ∈ S, M ⊔ K = ⊤) :
36 sInf S ⊔ K = ⊤ := by
37 induction S, hSfinite using Set.Finite.induction_on with
38 | empty =>
39 simp only [sInf_empty, le_top, sup_of_le_left]
40 | @insert a S ha hSfinite ih =>
41 have hSnormal' : ∀ M ∈ S, M.Normal := by
42 intro M hM
43 exact hSnormal M (by simp only [Set.mem_insert_iff, hM, or_true])
44 have hStop' : ∀ M ∈ S, M ⊔ K = ⊤ := by
45 intro M hM
46 exact hStop M (by simp only [Set.mem_insert_iff, hM, or_true])
47 haveI : a.Normal := hSnormal a (by simp only [Set.mem_insert_iff, true_or])
48 have hInfNormal : (sInf S).Normal := sInf_normal_of_forall_normal hSnormal'
49 haveI : (sInf S).Normal := hInfNormal
50 rw [sInf_insert]
51 exact inf_sup_eq_top_of_noncomm_simple_quotient K a (sInf S)
52 hquotNoncomm (hStop a (by simp only [Set.mem_insert_iff, true_or])) (ih hSnormal' hStop')
54end ProCGroups.NormalSubgroups