CharacterNormalizer61.lean

1 import PaperXI.NormalizerIntertwining60
2 import Mathlib.Topology.Algebra.OpenSubgroup
3 
4 /-!
5 # The literal normalizer of a subgroup-character pair
6 
7 The group is defined from the graph of the actual character. It is therefore
8 sensitive to both its domain and its values, rather than a separately supplied
9 group label. Compact parts are formed by intersection with a compact subgroup.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperXI.CharacterNormalizer61
14 variable {G A : Type*} [Group G] [CommGroup A]
15 variable (H : Subgroup G) (θ : H →* A)
16 
17 /-- The literal graph of the character in the product group. -/
18 def graph : Subgroup (G × A) := (H.subtype.prod θ).range
19 
20 /-- The exact normalizer of the domain and the character, defined through its graph. -/
21 def normalizer : Subgroup G :=
22   (Subgroup.normalizer (graph H θ : Set (G × A))).comap (MonoidHom.inl G A)
23 
24 /-- A pair normalizer carries every domain element back into the actual domain. -/
25 theorem conjugation_mem {g : G} (hg : g ∈ normalizer H θ) (h : H) :
26     g * (h : G) * g⁻¹ ∈ H := by
27   have hp : ((h : G), θ h) ∈ graph H θ := ⟨h, rfl⟩
28   have hx := (Subgroup.mem_normalizer_iff.mp hg ((h : G), θ h)).mp hp
29   obtain ⟨k, hk⟩ := hx
30   have he : (k : G) = g * (h : G) * g⁻¹ := congrArg Prod.fst hk
31   exact he ▸ k.property
32 
33 /-- Character values are preserved by literal conjugation. -/
34 theorem character_covariance {g : G} (hg : g ∈ normalizer H θ) (h k : H)
35     (hk : g * (h : G) * g⁻¹ = k) : θ k = θ h := by
36   have hp : ((h : G), θ h) ∈ graph H θ := ⟨h, rfl⟩
37   have hx := (Subgroup.mem_normalizer_iff.mp hg ((h : G), θ h)).mp hp
38   obtain ⟨j, hj⟩ := hx
39   have he : (j : G) = g * (h : G) * g⁻¹ := congrArg Prod.fst hj
40   have hjk : j = k := Subtype.ext (he.trans hk)
41   have hv : θ j = θ h := by simpa using congrArg Prod.snd hj
42   simpa only [hjk] using hv
43 
44 /-- The graph normalizer really normalizes the character domain. -/
45 theorem normalizes_domain : normalizer H θ ≤ Subgroup.normalizer (H : Set G) := by
46   intro g hg
47   apply Subgroup.mem_normalizer_iff.mpr
48   intro x
49   constructor
50   · intro hx
51     exact conjugation_mem H θ hg ⟨x, hx⟩
52   · intro hx
53     have hi := conjugation_mem H θ ((normalizer H θ).inv_mem hg) ⟨g * x * g⁻¹, hx⟩
54     simpa [mul_assoc] using hi
55 
56 /-- The domain always normalizes its own multiplicative character. -/
57 theorem domain_le_normalizer : H ≤ normalizer H θ := by
58   have step (h : H) (p : G × A) (hp : p ∈ graph H θ) :
59       ((h : G), (1 : A)) * p * ((h : G), (1 : A))⁻¹ ∈ graph H θ := by
60     obtain ⟨k, rfl⟩ := hp
61     refine ⟨h * k * h⁻¹, ?_⟩
62     apply Prod.ext
63     · rfl
64     · simp [map_mul, mul_comm]
65   intro g hg
66   apply Subgroup.mem_normalizer_iff.mpr
67   intro p
68   constructor
69   · exact step ⟨g, hg⟩ p
70   · intro hp
71     have hi := step ⟨g⁻¹, H.inv_mem hg⟩ (((g, (1 : A))) * p * (g, (1 : A))⁻¹) hp
72     convert hi using 1
73     ext <;> simp [mul_assoc]
74 
75 /-- A normalizing element intertwines the same actual character on the actual intersection. -/
76 theorem character_intertwinedAt (χ : H →* ℂˣ) {g : G}
77     (hg : g ∈ normalizer H χ) :
78     NormalizerIntertwining60.IntertwinedAt H (MonomialInduction.scalarRepresentation χ) g := by
79   apply NormalizerIntertwining60.character_intertwinedAt
80   intro h
81   exact (character_covariance H χ hg h
82     (InductionIrreducibility.intersectionConjugation H g h) rfl).symm
83 
84 /-- The compact part of a character normalizer is an actual intersection subgroup. -/
85 def compactPart (S : Subgroup G) : Subgroup G := normalizer H θ ⊓ S
86 
87 section Topology
88 variable [TopologicalSpace G] [IsTopologicalGroup G]
89 
90 /-- Openness follows from the actual open character domain. -/
91 theorem normalizer_open (hH : IsOpen (H : Set G)) : IsOpen (normalizer H θ : Set G) :=
92   Subgroup.isOpen_mono (domain_le_normalizer H θ) hH
93 
94 /-- Intersecting with a compact open subgroup gives the literal compact open part. -/
95 theorem compactPart_compact_open (S : Subgroup G) (hH : IsOpen (H : Set G))
96     (hSc : IsCompact (S : Set G)) (hSo : IsOpen (S : Set G)) :
97     IsCompact (compactPart H θ S : Set G) ∧ IsOpen (compactPart H θ S : Set G) := by
98   have hN := normalizer_open H θ hH
99   constructor
100   · exact hSc.inter_left ((normalizer H θ).isClosed_of_isOpen hN)
101   · exact hN.inter hSo
102 
103 end Topology
104 end PaperXI.CharacterNormalizer61

Back to source controls