EquivariantSplitting68.lean

1 import PaperXI.SmoothHomOrbit68
2 import PaperXI.FiniteOrbitAverage68
3 
4 /-! A compact-mod-scalar equivariant splitting, constructed by a finite orbit sum. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.EquivariantSplitting68
8 
9 open Representation PaperXI.SmoothDegreeQuotient
10 
11 variable {k G V W : Type*} [Field k] [CharZero k] [Group G]
12   [TopologicalSpace G] [IsTopologicalGroup G]
13   [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W]
14   [FiniteDimensional k V]
15 
16 /-- Every smooth surjective intertwiner onto a finite-dimensional source splits
17 equivariantly when a normal subgroup has compact quotient and acts by the same
18 scalars on both representations. Neither equivariant splitting nor orbit
19 finiteness is a premise. -/
20 theorem exists_equivariant_section
21     (N : Subgroup G) [N.Normal] [CompactSpace (G ⧸ N)] (χ : N →* kˣ)
22     (ρ : Representation k G V) (τ : Representation k G W)
23     (hρ : IsSmooth ρ) (hτ : IsSmooth τ)
24     (hcρ : ∀ z : N, ∀ v, ρ (z : G) v = (χ z : k) • v)
25     (hcτ : ∀ z : N, ∀ w, τ (z : G) w = (χ z : k) • w)
26     (p : IntertwiningMap τ ρ) (hp : Function.Surjective p) :
27     ∃ a : IntertwiningMap ρ τ, ∀ v, p (a v) = v := by
28   obtain ⟨s, hs⟩ := p.toLinearMap.exists_rightInverse_of_surjective
29     (LinearMap.range_eq_top.mpr hp)
30   apply FiniteOrbitAverage68.equivariant_section_of_finite_orbit ρ τ p s
31   · intro v
32     exact LinearMap.congr_fun hs v
33   · exact SmoothHomOrbit68.linHom_orbit_finite N χ ρ τ hρ hτ hcρ hcτ s
34 
35 end PaperXI.EquivariantSplitting68

Back to source controls