Source: ProCGroups.NormalSubgroups.SimpleQuotients.Algebraic
1import ProCGroups.NormalSubgroups.Framework
3/-!
4# Algebraic properties of simple quotients
6This module translates simplicity of `G ⧸ K` into a dichotomy for normal subgroups above `K` and
7derives the intersection property needed for noncommutative simple quotients.
8-/
10namespace ProCGroups.NormalSubgroups
12universe u
14/--
15If \(G/K\) is simple, every normal subgroup of \(G\) containing \(K\) is either \(K\) or all of
16\(G\). This is the correspondence theorem form of the simple-quotient dichotomy.
17-/
18theorem normal_subgroup_eq_kernel_or_top_of_simple_quotient
19 {G : Type u} [Group G] (K L : Subgroup G) [K.Normal] (hL : L.Normal)
20 [IsSimpleGroup (G ⧸ K)] (hKL : K ≤ L) :
21 L = K ∨ L = ⊤ := by
22 haveI : L.Normal := hL
23 let qL : Subgroup (G ⧸ K) := Subgroup.map (QuotientGroup.mk' K) L
24 have hqLnormal : qL.Normal := inferInstance
25 rcases hqLnormal.eq_bot_or_eq_top with hbot | htop
26 · left
27 apply le_antisymm
28 · have hLK : L ≤ K := by
29 have hker : L ≤ (QuotientGroup.mk' K).ker :=
30 (Subgroup.map_eq_bot_iff L).mp hbot
31 simpa [QuotientGroup.ker_mk'] using hker
32 exact hLK
33 · exact hKL
34 · right
35 have hcomap : Subgroup.comap (QuotientGroup.mk' K) qL = L := by
36 dsimp [qL]
37 rw [QuotientGroup.comap_map_mk']
38 exact sup_of_le_right hKL
39 rw [← hcomap, htop]
40 simp only [Subgroup.comap_top]
42/--
43If subgroups above \(K\) satisfy the two-point dichotomy induced by a simple noncommutative
44quotient, then two normal subgroups whose products with \(K\) equal \(G\) retain that property
45after intersection.
46-/
47theorem inf_sup_eq_top_of_simple_quotient_dichotomy
48 {G : Type u} [Group G] (K M N : Subgroup G) [K.Normal] [M.Normal] [N.Normal]
49 (hsimple : ∀ L : Subgroup G, L.Normal → K ≤ L → L = K ∨ L = ⊤)
50 (hquotNoncomm : ProCGroups.IsNoncommutativeGroup (G ⧸ K))
51 (hMK : M ⊔ K = ⊤) (hNK : N ⊔ K = ⊤) :
52 M ⊓ N ⊔ K = ⊤ := by
53 let L : Subgroup G := M ⊓ N ⊔ K
54 have hLnormal : L.Normal := inferInstance
55 have hKleL : K ≤ L := le_sup_right
56 rcases hsimple L hLnormal hKleL with hLK | hLtop
57 · exfalso
58 have hMNK : ⁅M, N⁆ ≤ K := by
59 exact (Subgroup.commutator_le_inf M N).trans ((le_sup_left : M ⊓ N ≤ L).trans_eq hLK)
60 have hmapK : Subgroup.map (QuotientGroup.mk' K) K = ⊥ := by
61 rw [Subgroup.map_eq_bot_iff, QuotientGroup.ker_mk']
62 have hmapM : Subgroup.map (QuotientGroup.mk' K) M = ⊤ := by
63 have hmapSup : Subgroup.map (QuotientGroup.mk' K) (M ⊔ K) = ⊤ := by
64 rw [hMK]
65 exact Subgroup.map_top_of_surjective (QuotientGroup.mk' K)
66 (QuotientGroup.mk'_surjective K)
67 rw [Subgroup.map_sup, hmapK, sup_bot_eq] at hmapSup
68 exact hmapSup
69 have hmapN : Subgroup.map (QuotientGroup.mk' K) N = ⊤ := by
70 have hmapSup : Subgroup.map (QuotientGroup.mk' K) (N ⊔ K) = ⊤ := by
71 rw [hNK]
72 exact Subgroup.map_top_of_surjective (QuotientGroup.mk' K)
73 (QuotientGroup.mk'_surjective K)
74 rw [Subgroup.map_sup, hmapK, sup_bot_eq] at hmapSup
75 exact hmapSup
76 have hcommBot : commutator (G ⧸ K) = ⊥ := by
77 rw [commutator_def]
78 nth_rewrite 1 [← hmapM]
79 nth_rewrite 1 [← hmapN]
80 rw [← Subgroup.map_commutator]
81 apply (Subgroup.map_eq_bot_iff ⁅M, N⁆).2
82 simpa [QuotientGroup.ker_mk'] using hMNK
83 exact hquotNoncomm hcommBot
84 · exact hLtop
86/-- Algebraic core with the simple quotient written directly. -/
87theorem inf_sup_eq_top_of_noncomm_simple_quotient
88 {G : Type u} [Group G] (K M N : Subgroup G) [K.Normal] [M.Normal] [N.Normal]
89 [IsSimpleGroup (G ⧸ K)]
90 (hquotNoncomm : ProCGroups.IsNoncommutativeGroup (G ⧸ K))
91 (hMK : M ⊔ K = ⊤) (hNK : N ⊔ K = ⊤) :
92 M ⊓ N ⊔ K = ⊤ :=
93 inf_sup_eq_top_of_simple_quotient_dichotomy K M N
94 (fun L hL hKL => normal_subgroup_eq_kernel_or_top_of_simple_quotient K L hL hKL)
95 hquotNoncomm hMK hNK
97end ProCGroups.NormalSubgroups