ActualCompactTypeCompletion58.lean

1 import PaperXI.ActualNormalizerTypeExtension58
2 import PaperXI.CompactTypeTensorNormalizer58
3 
4 /-!
5 # Same-factor actual compact type extension
6 
7 The literal tensor action retains the prescribed Heisenberg factor. Its
8 irreducibility and smoothness, and the whole-type normalizer intertwiner, are
9 constructed. Actual embedded-field arithmetic supplies cyclic freeness.
10 Normalization of the actual compact subgroup, quotient-triviality, and one
11 nonzero first-factor intertwiner remain explicit type-theoretic inputs.
12 -/
13 set_option autoImplicit false
14 noncomputable section
15 namespace PaperXI.ActualCompactTypeCompletion58
16 
17 open Matrix ValuativeRel Representation
18 open scoped TensorProduct
19 open ActualEmbeddedUniformizer58 NormalizerExtensionInducing58
20 
21 section FirstFactor
22 variable {J W : Type*} [Group J] [AddCommGroup W] [Module ℂ W]
23 
24 /-- Irreducibility on a subgroup already implies irreducibility of the extension. -/
25 theorem firstFactor_irreducible (N : Subgroup J) (κ : Representation ℂ J W)
26     [IsIrreducible (κ.comp N.subtype)] : IsIrreducible κ := by
27   let : Nontrivial W := GeneratedIrreducibility.nontrivial_space (κ.comp N.subtype)
28   apply RepresentationStability.irreducible_of_stable
29   intro S hS
30   apply RepresentationStability.eq_bot_or_top (κ.comp N.subtype) S
31   intro n w hw
32   exact hS (n : J) w hw
33 end FirstFactor
34 
35 variable (K E : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K]
36   [IsNonarchimedeanLocalField K]
37   [Field E] [ValuativeRel E] [TopologicalSpace E] [IsNonarchimedeanLocalField E]
38   [Algebra K E]
39 variable (n : Type*) [Fintype n] [DecidableEq n] [Nonempty n]
40   (ι : E →ₐ[K] Matrix n n K)
41 variable (J : Subgroup (GeneralLinearGroup n K))
42   (ht : embeddedUniformizer K E n ι ∈ Subgroup.normalizer (J : Set (GeneralLinearGroup n K)))
43 variable {Q W U : Type*} [Group Q] [Finite Q]
44   [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
45   [AddCommGroup U] [Module ℂ U]
46 variable (N : Subgroup J) (q : J →* Q) (hN : N ≤ q.ker)
47   (κ : Representation ℂ J W) (σ : Representation ℂ Q U)
48 
49 include hN in
50 /-- The prescribed compact first factor is retained in one smooth irreducible
51 tensor action and its actual noncentral uniformizer extension. No whole-type
52 irreducibility, whole-type intertwiner or extension is supplied as an input. -/
53 theorem completed
54     (hK : Continuous (algebraMap K E))
55     (hcompact : IsCompact (J : Set (GeneralLinearGroup n K)))
56     (hopen : IsOpen (J : Set (GeneralLinearGroup n K)))
57     (hNopen : IsOpen (N : Set J)) (hq : Function.Surjective q)
58     (hqa : ∀ j, q (conjugation J (embeddedUniformizer K E n ι) ht j) = q j)
59     [IsIrreducible (κ.comp N.subtype)] [IsIrreducible σ]
60     (hκ : SmoothDegreeQuotient.IsSmooth κ)
61     (T : IntertwiningMap κ
62       (κ.comp (conjugation J (embeddedUniformizer K E n ι) ht).toMonoidHom))
63     (hT : T ≠ 0) :
64     FiniteDimensional ℂ (W ⊗[ℂ] U) ∧
65     IsIrreducible (CompactTypeTensor58.action q κ σ) ∧
66     SmoothDegreeQuotient.IsSmooth (CompactTypeTensor58.action q κ σ) ∧
67     (CompactTypeTensor58.action q κ σ).comp N.subtype =
68       Representation.tprod (κ.comp N.subtype) (1 : Representation ℂ N U) ∧
69     (∃ Λ : Representation ℂ (extendedSubgroup J (embeddedUniformizer K E n ι) ht)
70         (W ⊗[ℂ] U),
71       (∀ j : J, Λ (subgroupInclusion J (embeddedUniformizer K E n ι) ht j) =
72         CompactTypeTensor58.action q κ σ j) ∧
73       (∀ w u, Λ (generator J (embeddedUniformizer K E n ι) ht) (w ⊗ₜ[ℂ] u) =
74         T w ⊗ₜ[ℂ] u) ∧
75       IsIrreducible Λ ∧ SmoothDegreeQuotient.IsSmooth Λ) := by
76   let t := embeddedUniformizer K E n ι
77   let a := conjugation J t ht
78   let : IsIrreducible κ := firstFactor_irreducible N κ
79   let e := T.ofBijective (intertwiner_bijective J t ht κ T hT)
80   have hA : ∀ j w, e.toLinearEquiv (κ j w) = κ (a j) (e.toLinearEquiv w) := by
81     intro j w
82     exact LinearMap.congr_fun (e.isIntertwining' j) w
83   let eTensor := CompactTypeTensorNormalizer58.normalizerEquiv q κ σ a hqa e.toLinearEquiv hA
84   have hfree := embeddedUniformizer_free_of_algebraMap K E n ι hK J hcompact
85   obtain ⟨hi, hf, hs, hr⟩ := CompactTypeTensor58.completed N q hN κ σ hq hNopen hκ
86   let : IsIrreducible (CompactTypeTensor58.action q κ σ) := hi
87   refine ⟨hf, hi, hs, hr,
88     extensionOfEquiv J t ht (CompactTypeTensor58.action q κ σ) eTensor hfree, ?_, ?_, ?_, ?_⟩
89   · intro j
90     exact extensionOfEquiv_restrict J t ht (CompactTypeTensor58.action q κ σ) eTensor hfree j
91   · intro w u
92     rw [extensionOfEquiv_generator]
93     rfl
94   · exact extendedRepresentation_irreducible J t ht (CompactTypeTensor58.action q κ σ) _ _ hfree
95   · exact extendedRepresentation_smooth J t ht (CompactTypeTensor58.action q κ σ) _ _ hfree hopen hs
96 
97 end PaperXI.ActualCompactTypeCompletion58

Back to source controls