SmoothHomOrbit68.lean

1 import PaperXI.CompactSmoothSemisimple
2 
3 /-!
4 # Finite orbits on actual linear-map spaces modulo a scalar subgroup
5 
6 The subgroup and quotient are literal.  Compactness is imposed on G / N, not
7 on G.  Finiteness of the Hom orbit is derived from smoothness and equal scalar
8 actions, rather than supplied as a splitting certificate.
9 -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.SmoothHomOrbit68
13 
14 open Representation PaperXI.SmoothDegreeQuotient
15 
16 variable {k G V W : Type*} [Field k] [Group G]
17   [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W]
18   [TopologicalSpace G] [IsTopologicalGroup G]
19 
20 /-- A finite-dimensional smooth source makes the actual Hom action smooth,
21 even when its target is infinite dimensional. -/
22 theorem linHom_smooth [FiniteDimensional k V]
23     (ρ : Representation k G V) (τ : Representation k G W)
24     (hρ : IsSmooth ρ) (hτ : IsSmooth τ) : IsSmooth (linHom ρ τ) := by
25   intro f
26   let b := Module.finBasis k V
27   let S : Subgroup G := ρ.ker ⊓ ⨅ i, vectorStabilizer τ (f (b i))
28   have hopen : IsOpen (S : Set G) := by
29     have he : (S : Set G) = (ρ.ker : Set G) ∩ ⋂ i, (vectorStabilizer τ (f (b i)) : Set G) := by
30       ext g
31       simp only [S, Subgroup.mem_inf, Subgroup.mem_iInf, Set.mem_inter_iff, Set.mem_iInter, SetLike.mem_coe]
32     rw [he]
33     exact (isOpen_kernel_of_smooth ρ hρ).inter
34       (isOpen_iInter_of_finite fun i => hτ (f (b i)))
35   apply Subgroup.isOpen_mono (H₁ := S) (H₂ := vectorStabilizer (linHom ρ τ) f) _ hopen
36   intro g hg
37   change linHom ρ τ g f = f
38   apply b.ext
39   intro i
40   have hinv : ρ g⁻¹ = 1 := ρ.ker.inv_mem hg.1
41   change τ g (f (ρ g⁻¹ (b i))) = f (b i)
42   rw [hinv, Module.End.one_apply]
43   exact Subgroup.mem_iInf.mp hg.2 i
44 
45 omit [IsTopologicalGroup G] in
46 /-- Smoothness descends through the actual topological quotient when the
47 normal subgroup acts trivially. -/
48 theorem descend_smooth (N : Subgroup G) [N.Normal]
49     (ρ : Representation k G V) (hN : N ≤ ρ.ker) (hρ : IsSmooth ρ) :
50     IsSmooth (QuotientRepresentation.descend N ρ hN) := by
51   intro v
52   apply (QuotientGroup.isQuotientMap_mk N).isOpen_preimage.mp
53   exact hρ v
54 
55 /-- A smooth action with compact effective quotient has finite vector orbits. -/
56 theorem orbit_finite_of_compact_quotient (N : Subgroup G) [N.Normal]
57     [CompactSpace (G ⧸ N)] (ρ : Representation k G V)
58     (hN : N ≤ ρ.ker) (hρ : IsSmooth ρ) (v : V) :
59     Set.Finite (Set.range fun g => ρ g v) := by
60   have h := CompactSmoothSemisimple.orbit_finite
61     (QuotientRepresentation.descend N ρ hN) (descend_smooth N ρ hN hρ) v
62   apply h.subset
63   rintro w ⟨g, rfl⟩
64   exact ⟨QuotientGroup.mk' N g, rfl⟩
65 
66 omit [TopologicalSpace G] [IsTopologicalGroup G] in
67 /-- Equal scalar actions cancel on Hom.  No unitarity or finite scalar image
68 is required. -/
69 theorem scalar_subgroup_le_linHom_kernel (N : Subgroup G)
70     (χ : N →* kˣ) (ρ : Representation k G V) (τ : Representation k G W)
71     (hρ : ∀ z : N, ∀ v, ρ (z : G) v = (χ z : k) • v)
72     (hτ : ∀ z : N, ∀ w, τ (z : G) w = (χ z : k) • w) :
73     N ≤ (linHom ρ τ).ker := by
74   intro g hg
75   change linHom ρ τ g = 1
76   ext f v
77   let z : N := ⟨g, hg⟩
78   change τ (z : G) (f (ρ ((z⁻¹ : N) : G) v)) = f v
79   rw [hρ, map_smul, map_smul, hτ, smul_smul]
80   simp
81 
82 /-- Every actual linear map between these representations has a finite orbit.
83 This is the compact-mod-scalar input needed for averaging a splitting. -/
84 theorem linHom_orbit_finite [FiniteDimensional k V]
85     (N : Subgroup G) [N.Normal] [CompactSpace (G ⧸ N)]
86     (χ : N →* kˣ) (ρ : Representation k G V) (τ : Representation k G W)
87     (hρ : IsSmooth ρ) (hτ : IsSmooth τ)
88     (hcρ : ∀ z : N, ∀ v, ρ (z : G) v = (χ z : k) • v)
89     (hcτ : ∀ z : N, ∀ w, τ (z : G) w = (χ z : k) • w)
90     (f : V →ₗ[k] W) : Set.Finite (Set.range fun g => linHom ρ τ g f) :=
91   orbit_finite_of_compact_quotient N (linHom ρ τ)
92     (scalar_subgroup_le_linHom_kernel N χ ρ τ hcρ hcτ)
93     (linHom_smooth ρ τ hρ hτ) f
94 
95 end PaperXI.SmoothHomOrbit68

Back to source controls