CompactIntersection108.lean

1 import PaperXI.IntersectionModel108
2 import PaperXI.FiniteJointQuotient108
3 
4 /-! The finite model of the actual conjugate-intersection Hom space exists for
5 any continuous embedded compact group with a smooth finite-dimensional action. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CompactIntersection108
9 open Representation IntersectionModel108
10 variable {k K G W : Type*} [Field k] [Group K] [Group G]
11   [AddCommGroup W] [Module k W]
12   [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K]
13   [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
14 
15 omit [IsTopologicalGroup K] in
16 /-- The relation is closed in the compact product K × K. -/
17 theorem compact_pairs (ι : K →* G) (hi : Continuous ι) (g : G) :
18     CompactSpace (pairs ι g) := by
19   apply isCompact_iff_compactSpace.mp
20   apply IsClosed.isCompact
21   exact isClosed_eq (hi.comp continuous_snd)
22     ((continuous_const.mul (hi.comp continuous_fst)).mul continuous_const)
23 
24 omit [IsTopologicalGroup K] [CompactSpace K] in
25 /-- Smoothness is preserved by a continuous group homomorphism. -/
26 theorem smooth_comp {P : Type*} [Group P] [TopologicalSpace P]
27     (ρ : Representation k K W) (hρ : SmoothDegreeQuotient.IsSmooth ρ)
28     (p : P →* K) (hp : Continuous p) : SmoothDegreeQuotient.IsSmooth (ρ.comp p) := by
29   intro v
30   exact (hρ v).preimage hp
31 
32 variable [FiniteDimensional k W]
33 
34 /-- Both conjugate actions descend through one canonically specified quotient. -/
35 theorem finite_quotient (ι : K →* G) (hi : Continuous ι)
36     (ρ : Representation k K W) (hρ : SmoothDegreeQuotient.IsSmooth ρ) (g : G) :
37     Finite (FiniteJointQuotient108.quotient (ρ.comp (left ι g)) (ρ.comp (right ι g))) := by
38   let : CompactSpace (pairs ι g) := compact_pairs ι hi g
39   exact FiniteJointQuotient108.finite _ _
40     (smooth_comp ρ hρ (left ι g) (continuous_fst.comp continuous_subtype_val))
41     (smooth_comp ρ hρ (right ι g) (continuous_snd.comp continuous_subtype_val))
42 
43 omit [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K]
44   [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] [FiniteDimensional k W] in
45 /-- This is the actual Hom dimension, on the original vector space. -/
46 theorem finrank_quotient (ι : K →* G) (ρ : Representation k K W) (g : G) :
47     Module.finrank k (IntertwiningSpace107.space ι ρ g) =
48       Module.finrank k (IntertwiningMap
49         (FiniteJointQuotient108.first (ρ.comp (left ι g)) (ρ.comp (right ι g)))
50         (FiniteJointQuotient108.second (ρ.comp (left ι g)) (ρ.comp (right ι g)))) := by
51   exact finrank_model ι ρ g
52     (QuotientGroup.mk' (FiniteJointQuotient108.kernel (ρ.comp (left ι g)) (ρ.comp (right ι g))))
53     QuotientGroup.mk_surjective _ _ rfl rfl
54 
55 end PaperXI.CompactIntersection108

Back to source controls