Source: ProCGroups.NormalSubgroups.SimpleQuotients.Compactness

1import ProCGroups.NormalSubgroups.SimpleQuotients.FiniteIntersections

3/-!

4# Compactness for intersections above a simple-quotient kernel

6This module upgrades a finite-intersection property for closed normal subgroups of a compact

7group to the corresponding arbitrary-intersection property.

8-/

10namespace ProCGroups.NormalSubgroups

12universe u

14/--

15Compactness step: if the closed normal subgroups satisfying \(M \sqcup K = \top\) are already

16stable under finite intersections, then they are stable under arbitrary intersections.

17-/

18theorem maximal_open_normal_intersections_compactness_step

19 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]

20 (K : Subgroup G) [K.Normal] (hKclosed : IsClosed (K : Set G))

21 (𝓜 : Set (Subgroup G))

22 (hMclosed : ∀ M ∈ 𝓜, IsClosed (M : Set G))

23 (hfinite :

24 ∀ S : Set (Subgroup G), S.Finite → S ⊆ 𝓜 → sInf S ⊔ K = ⊤) :

25 sInf 𝓜 ⊔ K = ⊤ := by

26 rw [eq_top_iff]

27 intro g _

28 by_cases h𝓜 : 𝓜.Nonempty

29 · rcases h𝓜 with ⟨M₀, hM₀⟩

30 let coset : Set G := {x | g⁻¹ * x ∈ K}

31 let I := {M : Subgroup G // M ∈ 𝓜}

32 let F : I → Set G := fun i => (i.1 : Set G) ∩ coset

33 have hcosetClosed : IsClosed coset := by

34 change IsClosed ((fun x : G => g⁻¹ * x) ⁻¹' (K : Set G))

35 exact hKclosed.preimage (continuous_const_mul g⁻¹)

36 have hclosed : ∀ i : I, IsClosed (F i) := by

37 intro i

38 exact (hMclosed i.1 i.2).inter hcosetClosed

39 have hfiniteNonempty : ∀ s : Finset I, (⋂ i ∈ s, F i).Nonempty := by

40 intro s

41 let S : Set (Subgroup G) := (fun i : I => i.1) '' (s : Set _)

42 have hSfinite : S.Finite := s.finite_toSet.image _

43 have hSsub : S ⊆ 𝓜 := by

44 rintro M ⟨i, _hi, rfl⟩

45 exact i.2

46 have htop : sInf S ⊔ K = ⊤ := hfinite S hSfinite hSsub

47 have hgmem : g ∈ sInf S ⊔ K := by

48 rw [htop]

49 exact Subgroup.mem_top g

50 rcases (Subgroup.mem_sup_of_normal_right (s := sInf S) (t := K) (x := g)).1 hgmem with

51 ⟨l, hlS, k, hk, hlk⟩

52 refine ⟨l, ?_⟩

53 simp only [Set.mem_iInter]

54 intro i hi

55 constructor

56 · exact (Subgroup.mem_sInf.mp hlS) i.1 ⟨i, hi, rfl⟩

57 · have hg : g = l * k := hlk.symm

58 have : g⁻¹ * l = k⁻¹ := by

59 rw [hg]

60 simp only [mul_inv_rev, mul_assoc, inv_mul_cancel, mul_one]

61 change g⁻¹ * l ∈ K

62 rw [this]

63 exact K.inv_mem hk

64 rcases CompactSpace.iInter_nonempty (t := F) hclosed hfiniteNonempty with ⟨x, hx⟩

65 have hxall : ∀ i : I, x ∈ F i := by

66 simpa [F] using hx

67 have hxL : x ∈ sInf 𝓜 := by

68 rw [Subgroup.mem_sInf]

69 intro M hM

70 exact (hxall ⟨M, hM⟩).1

71 have hxK : g⁻¹ * x ∈ K := (hxall ⟨M₀, hM₀⟩).2

72 have hxmem : x * (g⁻¹ * x)⁻¹ ∈ sInf 𝓜 ⊔ K :=

73 Subgroup.mul_mem_sup hxL (K.inv_mem hxK)

74 simpa [mul_assoc] using hxmem

75 · have h𝓜_empty : 𝓜 = ∅ := Set.not_nonempty_iff_eq_empty.mp h𝓜

76 have htop : sInf 𝓜 = ⊤ := by

77 rw [h𝓜_empty, sInf_empty]

78 simp only [htop, le_top, sup_of_le_left, Subgroup.mem_top]

80/--

81Maximal open normal subgroups with a fixed nonabelian simple quotient are closed under arbitrary

82intersections.

83-/

84theorem maximal_open_normal_intersections_nonabelian_simple

85 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]

86 (K : Subgroup G) [K.Normal] [IsSimpleGroup (G ⧸ K)]

87 (hquotNoncomm : ProCGroups.IsNoncommutativeGroup (G ⧸ K))

88 (hKclosed : IsClosed (K : Set G))

89 (𝓜 : Set (Subgroup G))

90 (hMnormal : ∀ M ∈ 𝓜, M.Normal)

91 (hMclosed : ∀ M ∈ 𝓜, IsClosed (M : Set G))

92 (hMtop : ∀ M ∈ 𝓜, M ⊔ K = ⊤) :

93 sInf 𝓜 ⊔ K = ⊤ :=

94 maximal_open_normal_intersections_compactness_step K hKclosed 𝓜 hMclosed

95 (fun _S hSfinite hSsub =>

96 finite_sInf_sup_eq_top_of_noncomm_simple_quotient K hquotNoncomm hSfinite

97 (fun M hM => hMnormal M (hSsub hM))

98 (fun M hM => hMtop M (hSsub hM)))

100end ProCGroups.NormalSubgroups