HeckeFibers.lean

1 import PaperXII.FieldFibers
2 import PaperXII.SupportTransport
3 
4 /-! Paper XII, Corollary 7.5 and Theorem 9.3. Actual Hecke tensor fibers and scalar actions. -/
5 namespace PaperXII.HeckeFibers
6 
7 open scoped TensorProduct
8 open FieldFibers
9 
10 variable {R T E H : Type*} [CommRing R] [CommRing T] [Field E]
11 
12 /-- Transport a field-valued point through the inverse ring identification. -/
13 def transportedPoint (e : R ≃+* T) (x : R →+* E) : T →+* E :=
14   x.comp e.symm.toRingHom
15 
16 /-- The transported point has the prescribed pullback. -/
17 theorem transportedPoint_comp (e : R ≃+* T) (x : R →+* E) :
18     (transportedPoint e x).comp e.toRingHom = x := by
19   ext r
20   simp [transportedPoint]
21 
22 /-- Exact kernel transport for the field-valued point. -/
23 theorem comap_pointPrime (e : R ≃+* T) (x : R →+* E) :
24     PrimeSpectrum.comap e.toRingHom (pointPrime (transportedPoint e x)) = pointPrime x := by
25   ext r
26   change x (e.symm (e r)) = 0 ↔ x r = 0
27   rw [e.symm_apply_apply]
28 
29 variable [AddCommGroup H] [Module T H]
30 
31 /-- Corollary 7.5 with the Hecke point explicitly constructed as x ∘ e⁻¹. -/
32 theorem supported_hecke_fiber [Algebra R T] [Module R H] [IsScalarTower R T H]
33     [Module.Finite T H] (e : R ≃ₐ[R] T) (x : R →+* E)
34     (hx : pointPrime x ∈ Module.support R H) :
35     letI : Algebra T E := (transportedPoint e.toRingEquiv x).toAlgebra
36     Nontrivial (E ⊗[T] H) := by
37   apply (nontrivial_fiber_iff_support (M := H) (transportedPoint e.toRingEquiv x)).mpr
38   have he : e.toRingHom = algebraMap R T := by
39     ext r
40     exact e.commutes r
41   have hf : Function.Surjective (algebraMap R T) := by
42     rw [← he]
43     exact e.surjective
44   apply (SupportTransport.mem_support_comap_iff hf _).mp
45   rw [← he, comap_pointPrime]
46   exact hx
47 
48 /-- The tensor relation giving the scalar action on pure tensors. -/
49 theorem pure_tensor_hecke_action (y : T →+* E) (t : T) (a : E) (h : H) :
50     letI : Algebra T E := y.toAlgebra
51     a ⊗ₜ[T] (t • h) = y t • (a ⊗ₜ[T] h) := by
52   let : Algebra T E := y.toAlgebra
53   rw [← TensorProduct.smul_tmul, TensorProduct.smul_tmul']
54   rfl
55 
56 /-- Base change of the actual operator h ↦ t • h on the Hecke module. -/
57 noncomputable def heckeOperator (y : T →+* E) (t : T) :
58     letI : Algebra T E := y.toAlgebra
59     Module.End E (E ⊗[T] H) :=
60   letI : Algebra T E := y.toAlgebra
61   (t • (LinearMap.id : H →ₗ[T] H)).baseChange E
62 
63 /-- The induced Hecke endomorphism equals scalar multiplication on the whole fiber. -/
64 theorem heckeOperator_eq_scalar (y : T →+* E) (t : T) :
65     letI : Algebra T E := y.toAlgebra
66     heckeOperator (H := H) y t = y t • (LinearMap.id : Module.End E (E ⊗[T] H)) := by
67   let : Algebra T E := y.toAlgebra
68   ext h
69   change (1 : E) ⊗ₜ[T] (t • h) = y t • ((1 : E) ⊗ₜ[T] h)
70   exact pure_tensor_hecke_action y t 1 h
71 
72 /-- Every element of the actual tensor fiber has the prescribed scalar Hecke action. -/
73 theorem hecke_action_is_scalar (y : T →+* E) (t : T) :
74     letI : Algebra T E := y.toAlgebra
75     ∀ z : E ⊗[T] H, t • z = y t • z := by
76   let : Algebra T E := y.toAlgebra
77   intro z
78   exact (IsScalarTower.algebraMap_smul E t z).symm
79 
80 /-- Theorem 9.3: a supported point gives a nonzero fiber, with its full scalar action. -/
81 theorem support_gives_hecke_eigensystem [Algebra R T] [Module R H]
82     [IsScalarTower R T H] [Module.Finite T H]
83     (e : R ≃ₐ[R] T) (x : R →+* E) (hx : pointPrime x ∈ Module.support R H) :
84     letI : Algebra T E := (transportedPoint e.toRingEquiv x).toAlgebra
85     Nontrivial (E ⊗[T] H) ∧
86       ∀ t : T, heckeOperator (H := H) (transportedPoint e.toRingEquiv x) t =
87         transportedPoint e.toRingEquiv x t • (LinearMap.id : Module.End E (E ⊗[T] H)) := by
88   exact ⟨supported_hecke_fiber e x hx, fun t ↦ heckeOperator_eq_scalar _ t⟩
89 
90 end PaperXII.HeckeFibers

Back to source controls