ResidueRestriction107.lean

1 import PaperXI.ActualCuspidalCandidate105
2 
3 /-! The previously constructed residue map agrees with literal entrywise
4 reduction on integral centralizer matrices. This identity is proved, not supplied. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.ResidueRestriction107
8 open Matrix ValuativeRel
9 open ActualCharacterType61 ActualCharacterResidue61 ActualCuspidalCandidate105
10 open ActualELatticeResidue59 ActualELatticeTopology60 ActualEmbeddedUniformizer58 LatticeCongruenceTopology60
11 
12 theorem quotient_inclusion {G Q : Type*} [Group G] [Group Q]
13     (H N : Subgroup G) (hn : H ≤ Subgroup.normalizer (N : Set G))
14     (q : H →* Q) (hq : Function.Surjective q) (hk : N.subgroupOf H = q.ker)
15     (h : H) :
16     let := Subgroup.normal_subgroupOf_sup_of_le_normalizer hn
17     ProductNormalizerQuotient59.quotientEquivOfKernel H N hn q hq hk
18       (QuotientGroup.mk' (N.subgroupOf (H ⊔ N)) (Subgroup.inclusion le_sup_left h)) = q h := by
19   dsimp only
20   let := Subgroup.normal_subgroupOf_of_le_normalizer hn
21   let := Subgroup.normal_subgroupOf_sup_of_le_normalizer hn
22   have he : QuotientGroup.quotientInfEquivProdNormalizerQuotient H N hn
23       (QuotientGroup.mk' (N.subgroupOf H) h) =
24       QuotientGroup.mk' (N.subgroupOf (H ⊔ N)) (Subgroup.inclusion le_sup_left h) := rfl
25   rw [← he]
26   change (QuotientGroup.quotientKerEquivOfSurjective q hq)
27     (QuotientGroup.quotientMulEquivOfEq hk
28       ((QuotientGroup.quotientInfEquivProdNormalizerQuotient H N hn).symm
29         (QuotientGroup.quotientInfEquivProdNormalizerQuotient H N hn
30           (QuotientGroup.mk' (N.subgroupOf H) h)))) = q h
31   rw [MulEquiv.symm_apply_apply]
32   rfl
33 
34 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
35   [IsNonarchimedeanLocalField F] [Field E] [ValuativeRel E] [TopologicalSpace E]
36   [IsNonarchimedeanLocalField E] [Algebra F E]
37 variable (m n : Type*) [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
38   [Nonempty n] (e : (m → E) ≃L[F] (n → F))
39   (D : Subgroup (GL n F)) (θ : D →* ℂˣ)
40   (hmodel : compact F E m n e D θ ≤ matrixType F E m n e)
41   (hB : ∀ u : GL m 𝒪[E],
42     (coordinateAut e).symm (integralMatrix F E m u) ∈ CharacterNormalizer61.normalizer D θ)
43 
44 def integralInclusion : GL m 𝒪[E] →* compact F E m n e D θ :=
45   (centralizerMap F E m n e |>.comp (ActualIntegralGeneralLinear.embedding E m)).codRestrict _
46     (fun u => integralMatrix_mem_compactGroup F E m n e D θ hB u)
47 
48 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Nonempty n] in
49 @[simp] theorem integralInclusion_coe (u : GL m 𝒪[E]) :
50     (integralInclusion F E m n e D θ hB u : GL n F) =
51       centralizerMap F E m n e (ActualIntegralGeneralLinear.embedding E m u) := rfl
52 
53 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Nonempty n] in
54 /-- Equality on the exact old quotient construction; no unspecified residue
55 isomorphism or conjugate finite representation is substituted. -/
56 theorem reduction_integral (u : GL m 𝒪[E]) :
57     reduction F E m n e D θ hmodel (integralInclusion F E m n e D θ hB u) =
58       ActualResidueGeneralLinear.reduction E m u := by
59   have he : intoModel F E m n e D θ hmodel (integralInclusion F E m n e D θ hB u) =
60       Subgroup.inclusion (show integralImage F E m ≤ ActualELatticeTypeGroup59.typeGroup F E m
61         from le_sup_left) (integralImageEquiv F E m u) := by
62     apply Subtype.ext
63     exact (coordinateAut e).apply_symm_apply (integralMatrix F E m u)
64   change ActualELatticeQuotient59.reduction F E m _ = _
65   rw [he]
66   have h := quotient_inclusion (integralImage F E m)
67     (ActualELatticeTypeGroup59.congruence F E m)
68     (ActualELatticeTypeGroup59.integralImage_normalizes F E m)
69     (residueAction F E m) (residueAction_surjective F E m)
70     (ActualELatticeTypeGroup59.congruence_subgroupOf_integralImage F E m)
71     (integralImageEquiv F E m u)
72   exact h.trans (congrArg (ActualResidueGeneralLinear.reduction E m)
73     ((integralImageEquiv F E m).symm_apply_apply u))
74 
75 end PaperXI.ResidueRestriction107

Back to source controls