ActualLocalCartan106.lean

1 import PaperXI.DVRCartan106
2 import PaperXI.ActualLocalUnitDecomposition
3 import PaperXI.ActualIntegralGeneralLinear
4 import PaperXI.ActualResidueGeneralLinear
5 
6 /-! The arithmetic Cartan and residue support theorems on actual local-field
7 matrices, with a uniformizer chosen from the proved valuation-ring structure. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.ActualLocalCartan106
11 open Matrix ValuativeRel
12 variable (E : Type*) [Field E] [ValuativeRel E] [TopologicalSpace E]
13   [IsNonarchimedeanLocalField E]
14 variable (ι : Type*) [Fintype ι] [DecidableEq ι] [Nonempty ι]
15 
16 theorem uniformizer_residue_zero :
17     IsLocalRing.residue 𝒪[E] (ActualLocalUnitDecomposition.uniformizer E) = 0 := by
18   apply (IsLocalRing.residue_eq_zero_iff _).mpr
19   rw [(ActualLocalUnitDecomposition.uniformizer_irreducible E).maximalIdeal_eq]
20   exact Ideal.subset_span (Set.mem_singleton _)
21 
22 theorem hasCartan :
23     CuspidalCartan105.HasCartan (ι := ι) (valuation E).integer.subtype
24       (ActualLocalUnitDecomposition.uniformizer E)
25       (ActualLocalUnitDecomposition.uniformizer_ne_zero E) :=
26   DVRCartan106.hasCartan (F := E) _ (ActualLocalUnitDecomposition.uniformizer_irreducible E)
27 
28 variable {C V : Type*} [Field C] [CharZero C] [AddCommGroup V] [Module C V]
29 
30 /-- No arithmetic decomposition is supplied to this support bound. -/
31 theorem intertwining_support [Fintype 𝓀[E]]
32     (σ : Representation C (GL ι 𝓀[E]) V) (hσ : CuspidalCartan105.Cuspidal σ)
33     (g : GL ι E)
34     (hg : IntertwiningAlong105.ExistsAt (ActualIntegralGeneralLinear.embedding E ι)
35       (σ.comp (ActualResidueGeneralLinear.reduction E ι)) g) :
36     ∃ c : Eˣ, ∃ u : GL ι 𝒪[E],
37       g = GeneralLinearGroup.scalar ι c * ActualIntegralGeneralLinear.embedding E ι u :=
38   CuspidalCartan105.intertwining_support (valuation E).integer.subtype
39     (IsLocalRing.residue 𝒪[E]) IsLocalRing.residue_surjective
40     (ActualLocalUnitDecomposition.uniformizer E)
41     (ActualLocalUnitDecomposition.uniformizer_ne_zero E)
42     (uniformizer_residue_zero E) (hasCartan E ι) σ hσ g hg
43 
44 end PaperXI.ActualLocalCartan106

Back to source controls