ActualPacketTypeRealization70.lean

1 import PaperXI.PacketTypeAttachment70
2 import PaperXI.PrescribedFieldType70
3 import PaperXI.ArithmeticTypeCertificate69
4 import PaperXI.ActualCharacterIdentification61
5 import PaperXI.ActualCharacterResidue61
6 
7 /-! Same-theta, same-kappa construction at the actual residue map and field join.
8 This replaces the old compact-subgroup Mackey premise by a full-locus condition
9 on the newly constructed extension. Standard character/type leaves remain
10 explicit; this is not a formalization of their classification theorem. -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperXI.ActualPacketTypeRealization70
14 open Matrix ValuativeRel Representation
15 open scoped TensorProduct
16 open ActualCharacterType61 ActualCharacterIdentification61 ActualCharacterResidue61
17 open ActualELatticeTopology60 ActualELatticeResidue59 ActualEmbeddedUniformizer58
18 open LatticeCongruenceTopology60
19 open NormalizerExtensionInducing58 ActualFieldTypeQuotient69
20 
21 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
22   [IsNonarchimedeanLocalField F] [Field E] [ValuativeRel E] [TopologicalSpace E]
23   [IsNonarchimedeanLocalField E] [Algebra F E]
24 variable (m n : Type*) [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
25   [Nonempty n] (e : (m → E) ≃L[F] (n → F))
26   (D : Subgroup (GeneralLinearGroup n F)) (θ : D →* ℂˣ)
27 
28 variable (hmodel : (compactGroup F E m n e D θ) ≤ matrixType F E m n e)
29 variable {W U : Type*} [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
30   [AddCommGroup U] [Module ℂ U]
31   (κ : Representation ℂ (compactGroup F E m n e D θ) W) (σ : Representation ℂ (GeneralLinearGroup m 𝓀[E]) U)
32 
33 /-- Construct the exact arithmetic extended tensor type. All later full-locus
34 and induced-category claims refer to this same Lambda. No arbitrary Atom type,
35 assumed whole-type irreducibility, or compact-J off-normalizer bound is used. -/
36 theorem candidate_exists
37     (hF : Continuous (algebraMap F E))
38     (hDo : IsOpen (D : Set (GeneralLinearGroup n F)))
39     (hB : ∀ b : GeneralLinearGroup m 𝒪[E],
40       (coordinateAut e).symm (integralMatrix F E m b) ∈ CharacterNormalizer61.normalizer D θ)
41     (hfull : ∀ g : GeneralLinearGroup n F,
42       g ∈ CharacterNormalizer61.normalizer D θ ↔
43         ∃ a : Eˣ, ∃ j : (compactGroup F E m n e D θ), unitsEmbedding F E n (scalarMatrixEmbedding F E m n e) a * (j : GeneralLinearGroup n F) = g)
44     [IsIrreducible (κ.comp (firstSubgroup F E m n e D θ).subtype)] [IsIrreducible σ]
45     (hκ : SmoothDegreeQuotient.IsSmooth κ)
46     (hβ : ∀ g : GeneralLinearGroup n F,
47       NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g →
48       NormalizerIntertwining60.IntertwinedAt (compactGroup F E m n e D θ) κ g) :
49     (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)) = CharacterNormalizer61.normalizer D θ ∧
50     FiniteDimensional ℂ (W ⊗[ℂ] U) ∧
51     ∃ Λ : Representation ℂ (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)) (W ⊗[ℂ] U),
52       (∀ j : (compactGroup F E m n e D θ), Λ (PrescribedFieldType70.compactInclusion F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ) j) =
53         CompactTypeTensor58.action (reduction F E m n e D θ hmodel) κ σ j) ∧
54       (∃ A : Module.End ℂ W, A ≠ 0 ∧
55         ∀ w u, Λ (PrescribedFieldType70.fieldGenerator F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)) (w ⊗ₜ[ℂ] u) =
56           A w ⊗ₜ[ℂ] u) ∧
57       IsIrreducible Λ ∧ SmoothDegreeQuotient.IsSmooth Λ ∧
58       Function.Injective (TensorTypeOperators70.realize (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)) Λ) ∧
59       (∀ j : (firstSubgroup F E m n e D θ), PacketTypeAttachment70.typeAction (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)) Λ
60         (PrescribedFieldType70.compactInclusion F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ) (j : (compactGroup F E m n e D θ))) =
61           TensorTypeOperators70.realize (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)) Λ (κ (j : (compactGroup F E m n e D θ)))) ∧
62       (∀ xs : List (Module.End ℂ W),
63         (xs.map (TensorTypeOperators70.realize (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)) Λ)).prod = 1 ↔ xs.prod = 1) ∧
64       (FullIntertwiningLocus69.locus (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)) Λ = ((fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)) : Set (GeneralLinearGroup n F)) →
65         Nontrivial (IndV (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)).subtype Λ) ∧
66         SmoothDegreeQuotient.IsSmooth (ind (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)).subtype Λ) ∧
67         IsIrreducible (ind (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)).subtype Λ) ∧
68         (∀ f : IntertwiningMap Λ ((ind (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)).subtype Λ).comp (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)).subtype), f ≠ 0 →
69           LinearMap.range f.toLinearMap = InducedTypeSpace68.typeSpace (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)) Λ)) := by
70   have hθ := uniformizer_mem_full_normalizer F E m n e D θ (compactGroup F E m n e D θ) hfull
71   let ht := uniformizer_normalizes_compactGroup F E m n e D θ hθ
72   have htop := compactGroup_compact_open F E m n e D θ hF hDo
73   have hu := integralUnit_mem_compactGroup F E m n e D θ hB
74   have hq := reduction_surjective F E m n e D θ hmodel hB
75   have hN : (firstSubgroup F E m n e D θ) ≤ (reduction F E m n e D θ hmodel).ker := (reduction_kernel F E m n e D θ hmodel).ge
76   obtain ⟨T, hT⟩ := NormalizerIntertwining60.exists_normalizerIntertwiner (compactGroup F E m n e D θ) κ (embeddedUniformizer F E n (scalarMatrixEmbedding F E m n e)) ht
77     (hβ (embeddedUniformizer F E n (scalarMatrixEmbedding F E m n e)) (CharacterNormalizer61.character_intertwinedAt D θ hθ))
78   obtain ⟨hf, Λ, hr, hg, hi, hs⟩ := PrescribedFieldType70.exists_prescribed_extension
79     F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ) ht hu (firstSubgroup F E m n e D θ) (reduction F E m n e D θ hmodel) hN κ σ hF htop.1 htop.2
80     (firstSubgroup_open F E m n e D θ hF) hq
81     (reduction_conjugation F E m n e D θ hmodel hθ) hκ T hT
82   have hdom : (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)) = CharacterNormalizer61.normalizer D θ := by
83     change (compactGroup F E m n e D θ) ⊔ (unitsEmbedding F E n (scalarMatrixEmbedding F E m n e)).range = _
84     rw [← ActualNormalizerTypeExtension58.extendedSubgroup_eq_field_join F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ) ht hu]
85     exact extendedSubgroup_eq_full_normalizer F E m n e D θ (compactGroup F E m n e D θ) hF inf_le_right hu hfull
86   let : Nontrivial U := GeneratedIrreducibility.nontrivial_space σ
87   refine ⟨hdom, hf, Λ, hr, ⟨T.toLinearMap, ?_, hg⟩, hi, hs,
88     TensorTypeOperators70.realize_injective (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)) Λ, ?_,
89     TensorTypeOperators70.holonomy_iff (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)) Λ, ?_⟩
90   · intro hz
91     apply hT
92     ext w
93     exact LinearMap.congr_fun hz w
94   · intro j
95     exact PacketTypeAttachment70.first_factor_action (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)) Λ
96       (PrescribedFieldType70.compactInclusion F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)) (reduction F E m n e D θ hmodel) κ σ hr
97       (j : (compactGroup F E m n e D θ)) (hN j.property)
98   · intro hI
99     let : FiniteDimensional ℂ (W ⊗[ℂ] U) := hf
100     let : IsIrreducible Λ := hi
101     obtain ⟨hn, hsm, hir, _⟩ := ArithmeticTypeCertificate69.from_full_intertwining_locus
102       F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ) Λ hF htop.1 htop.2 ht hu hs hI
103     refine ⟨hn, hsm, hir, ?_⟩
104     let : Nontrivial (W ⊗[ℂ] U) := GeneratedIrreducibility.nontrivial_space Λ
105     intro f hf0
106     exact InducedTypeSpace68.range_eq_identity (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)) Λ
107       ((FullIntertwiningLocus69.locus_eq_iff (fieldGroup F E n (scalarMatrixEmbedding F E m n e) (compactGroup F E m n e D θ)) Λ).mp hI) f hf0
108 
109 end PaperXI.ActualPacketTypeRealization70

Back to source controls