SmoothDegreeQuotient.lean

1 import PaperXI.QuotientRepresentation
2 import PaperXI.TameDegree
3 import Mathlib.Topology.Algebra.Group.Quotient
4 import Mathlib.Topology.Compactness.Compact
5 
6 /-!
7 # A smooth representation quotient which retains every integer degree
8 
9 The quotient kernel is the intersection of the representation kernel and
10 integer-degree kernel.  No finiteness of the original inertia group and no
11 identification with an absolute local-field Weil group is assumed here.
12 -/
13 set_option autoImplicit false
14 noncomputable section
15 namespace PaperXI.SmoothDegreeQuotient
16 
17 variable {k G V : Type*} [Field k] [Group G]
18   [AddCommGroup V] [Module k V]
19 
20 /-- The subgroup fixing a particular vector. -/
21 def vectorStabilizer (ρ : Representation k G V) (v : V) : Subgroup G where
22   carrier := {g | ρ g v = v}
23   one_mem' := by simp
24   mul_mem' := by
25     intro g h hg hh
26     change ρ (g * h) v = v
27     rw [map_mul, Module.End.mul_apply, hh, hg]
28   inv_mem' := by
29     intro g hg
30     apply (ρ.apply_bijective g).injective
31     simpa using hg.symm
32 
33 @[simp] theorem mem_vectorStabilizer (ρ : Representation k G V) (v : V) (g : G) :
34     g ∈ vectorStabilizer ρ v ↔ ρ g v = v := Iff.rfl
35 
36 section Topology
37 variable [TopologicalSpace G]
38 
39 /-- Algebraic smoothness means that every vector has an open stabilizer. -/
40 def IsSmooth (ρ : Representation k G V) : Prop :=
41   ∀ v, IsOpen (vectorStabilizer ρ v : Set G)
42 
43 /-- A finite basis turns pointwise open stabilizers into one open action kernel. -/
44 theorem isOpen_kernel_of_smooth [FiniteDimensional k V]
45     (ρ : Representation k G V) (hρ : IsSmooth ρ) :
46     IsOpen (ρ.ker : Set G) := by
47   let b := Module.finBasis k V
48   have heq : (ρ.ker : Set G) = ⋂ i, (vectorStabilizer ρ (b i) : Set G) := by
49     ext g
50     simp only [Set.mem_iInter]
51     change (ρ g = 1) ↔ ∀ i, ρ g (b i) = b i
52     constructor
53     · intro hg i
54       change ρ g = 1 at hg
55       rw [hg]
56       rfl
57     · intro hg
58       apply b.ext
59       exact hg
60   rw [heq]
61   exact isOpen_iInter_of_finite fun i => hρ (b i)
62 end Topology
63 
64 variable (ρ : Representation k G V) (δ : G →* Multiplicative ℤ)
65 
66 /-- Only elements invisible both to the action and the integer degree are killed. -/
67 def jointKernel : Subgroup G := ρ.ker ⊓ δ.ker
68 
69 instance jointKernel_normal : (jointKernel ρ δ).Normal := by
70   unfold jointKernel
71   infer_instance
72 
73 /-- The representation-dependent quotient, without discarding Frobenius degree. -/
74 abbrev DegreeQuotient := G ⧸ jointKernel ρ δ
75 
76 /-- The literal quotient map. -/
77 abbrev quotientMap : G →* DegreeQuotient ρ δ :=
78   QuotientGroup.mk' (jointKernel ρ δ)
79 
80 /-- The integer degree descends because the kernel inclusion is proved. -/
81 def descendedDegree : DegreeQuotient ρ δ →* Multiplicative ℤ :=
82   QuotientGroup.lift (jointKernel ρ δ) δ inf_le_right
83 
84 /-- The original action descends through this same quotient. -/
85 def descendedRepresentation : Representation k (DegreeQuotient ρ δ) V :=
86   QuotientRepresentation.descend (jointKernel ρ δ) ρ inf_le_left
87 
88 @[simp] theorem descendedDegree_mk (g : G) :
89     descendedDegree ρ δ (quotientMap ρ δ g) = δ g := rfl
90 
91 @[simp] theorem descendedRepresentation_mk (g : G) :
92     descendedRepresentation ρ δ (quotientMap ρ δ g) = ρ g := rfl
93 
94 @[simp] theorem descendedDegree_comp :
95     (descendedDegree ρ δ).comp (quotientMap ρ δ) = δ := rfl
96 
97 @[simp] theorem descendedRepresentation_comp :
98     (descendedRepresentation ρ δ).comp (quotientMap ρ δ) = ρ := rfl
99 
100 /-- Irreducibility is preserved, not supplied independently for the quotient. -/
101 theorem descended_irreducible [Representation.IsIrreducible ρ] :
102     Representation.IsIrreducible (descendedRepresentation ρ δ) :=
103   QuotientRepresentation.descend_irreducible (jointKernel ρ δ) ρ inf_le_left
104 
105 /-- Surjectivity of the actual integer degree is unchanged by the quotient. -/
106 theorem degree_surjective_iff :
107     Function.Surjective (descendedDegree ρ δ) ↔ Function.Surjective δ := by
108   constructor
109   · intro h z
110     obtain ⟨x, hx⟩ := h z
111     obtain ⟨g, rfl⟩ := QuotientGroup.mk_surjective x
112     exact ⟨g, hx⟩
113   · intro h z
114     obtain ⟨g, hg⟩ := h z
115     exact ⟨quotientMap ρ δ g, hg⟩
116 
117 /-- The degree-divisible subgroup pulls back literally, not just up to its index. -/
118 theorem degreeSubgroup_comap (n : ℕ) :
119     (TameDegree.degreeSubgroup (descendedDegree ρ δ) n).comap
120         (quotientMap ρ δ) = TameDegree.degreeSubgroup δ n := by
121   ext g
122   simp only [Subgroup.mem_comap, TameDegree.mem_degreeSubgroup]
123   rfl
124 
125 /-- The action and degree have no common invisible element after descent. -/
126 theorem jointKernel_descended :
127     (descendedRepresentation ρ δ).ker ⊓ (descendedDegree ρ δ).ker = ⊥ := by
128   apply Subgroup.ext
129   intro x
130   obtain ⟨g, rfl⟩ := QuotientGroup.mk_surjective x
131   change (ρ g = 1 ∧ δ g = 1) ↔ quotientMap ρ δ g = 1
132   exact (QuotientGroup.eq_one_iff (N := jointKernel ρ δ) g).symm
133 
134 /-- A quotient can retain the original degree exactly if its kernel is invisible to degree. -/
135 theorem degree_descends_iff (N : Subgroup G) [N.Normal] :
136     (∃ d : G ⧸ N →* Multiplicative ℤ,
137       d.comp (QuotientGroup.mk' N) = δ) ↔ N ≤ δ.ker := by
138   constructor
139   · rintro ⟨d, hd⟩ g hg
140     change δ g = 1
141     have he : d (QuotientGroup.mk' N g) = δ g := congrArg (fun f => f g) hd
142     have hmk : QuotientGroup.mk' N g = 1 :=
143       (QuotientGroup.eq_one_iff (N := N) g).mpr hg
144     rw [hmk, map_one] at he
145     exact he.symm
146   · intro hN
147     exact ⟨QuotientGroup.lift N δ hN, rfl⟩
148 
149 /-- The quotient inertia is exactly the image of original inertia. -/
150 theorem inertia_image :
151     (quotientMap ρ δ) '' (δ.ker : Set G) =
152       ((descendedDegree ρ δ).ker : Set (DegreeQuotient ρ δ)) := by
153   ext x
154   constructor
155   · rintro ⟨g, hg, rfl⟩
156     exact hg
157   · intro hx
158     obtain ⟨g, rfl⟩ := QuotientGroup.mk_surjective x
159     exact ⟨g, hx, rfl⟩
160 
161 section Topology
162 variable [TopologicalSpace G]
163 
164 /-- Smoothness and an open inertia subgroup make the joint quotient kernel open. -/
165 theorem isOpen_jointKernel [FiniteDimensional k V]
166     (hρ : IsSmooth ρ) (hδ : IsOpen (δ.ker : Set G)) :
167     IsOpen (jointKernel ρ δ : Set G) :=
168   (isOpen_kernel_of_smooth ρ hρ).inter hδ
169 
170 /-- The quotient carries its actual quotient topology, which is discrete. -/
171 theorem quotient_discrete [IsTopologicalGroup G] [FiniteDimensional k V]
172     (hρ : IsSmooth ρ) (hδ : IsOpen (δ.ker : Set G)) :
173     DiscreteTopology (DegreeQuotient ρ δ) :=
174   QuotientGroup.discreteTopology (isOpen_jointKernel ρ δ hρ hδ)
175 
176 /-- The quotient map is continuous for the original group topology. -/
177 theorem quotientMap_continuous : Continuous (quotientMap ρ δ) :=
178   QuotientGroup.continuous_mk
179 
180 /-- Compact original inertia has finite image in the discrete smooth quotient.
181 The original inertia itself is not assumed finite. -/
182 theorem finite_descended_inertia [IsTopologicalGroup G] [FiniteDimensional k V]
183     (hρ : IsSmooth ρ) (hδ : IsOpen (δ.ker : Set G))
184     (hc : IsCompact (δ.ker : Set G)) :
185     Finite (descendedDegree ρ δ).ker := by
186   let : DiscreteTopology (DegreeQuotient ρ δ) := quotient_discrete ρ δ hρ hδ
187   have hfinite := (hc.image (quotientMap_continuous ρ δ)).finite_of_discrete
188   rw [inertia_image] at hfinite
189   exact Set.finite_coe_iff.mpr hfinite
190 
191 end Topology
192 end PaperXI.SmoothDegreeQuotient

Back to source controls