WeilCopies.lean

1 import PaperX.WeilData
2 
3 /-! Actual finite-copy group/monodromy actions and their inertia-fixed kernels. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperX.WeilCopies
7 open scoped BigOperators
8 open PaperX.CarrierSummands PaperX.CarrierPolynomials PaperX.WeilData
9 variable {K G I : Type*} [Field K] [Group G] [Fintype I]
10 variable {ν : G →* Kˣ} {W : I → Type*}
11 variable [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
12 
13 def copiesDatum (D : ∀ i, Datum ν (W i)) (m : I → ℕ) : Datum ν (Copies W m) where
14   r := copiesRep (fun i => (D i).r) m
15   N := PaperX.MonodromyData.copiesN (fun i => (D i).N) m
16   nilpotent := PaperX.MonodromyData.copiesN_nilpotent _ (fun i => (D i).nilpotent) m
17   relation g x := by funext i k; exact (D i).relation g (x i k)
18 
19 /-- Both sides use their own fixed-vector and kernel equations. -/
20 def fixedCopiesEquiv (D : ∀ i, Datum ν (W i)) (H : Subgroup G) (m : I → ℕ) :
21     fixedKernel (copiesDatum D m) H ≃ₗ[K] Copies (fun i => fixedKernel (D i) H) m where
22   toFun x i k := ⟨x.val i k, ⟨congrFun (congrFun x.property.1 i) k,
23     fun h => congrFun (congrFun (x.property.2 h) i) k⟩⟩
24   invFun x := ⟨fun i k => (x i k).val, ⟨by
25     funext i k
26     exact (x i k).property.1, by
27     intro h
28     funext i k
29     exact (x i k).property.2 h⟩⟩
30   left_inv x := by apply Subtype.ext; rfl
31   right_inv x := rfl
32   map_add' x y := rfl
33   map_smul' a x := rfl
34 
35 theorem fixed_equivariant (D : ∀ i, Datum ν (W i)) (H : Subgroup G) [H.Normal]
36     (m : I → ℕ) (g : G) (x : fixedKernel (copiesDatum D m) H) :
37     fixedCopiesEquiv D H m (fixedRep (copiesDatum D m) H g x) =
38       copiesRep (fun i => fixedRep (D i) H) m g (fixedCopiesEquiv D H m x) := rfl
39 
40 theorem fixed_conjugate (D : ∀ i, Datum ν (W i)) (H : Subgroup G) [H.Normal]
41     (m : I → ℕ) (g : G) :
42     (fixedCopiesEquiv D H m).conj (fixedRep (copiesDatum D m) H g) =
43       piEnd (fun i => piEnd (fun _ : Fin (m i) => fixedRep (D i) H g)) := by
44   apply LinearMap.ext
45   intro x
46   rfl
47 
48 variable [∀ i, FiniteDimensional K (W i)]
49 
50 theorem local_charpoly_product (D : ∀ i, Datum ν (W i)) (H : Subgroup G) [H.Normal]
51     (m : I → ℕ) (φ : G) :
52     localCharpoly (copiesDatum D m) H φ = ∏ i, localCharpoly (D i) H φ ^ m i := by
53   unfold localCharpoly
54   rw [← LinearEquiv.charpoly_conj (fixedCopiesEquiv D H m), fixed_conjugate, charpoly_piEnd]
55   apply Finset.prod_congr rfl
56   intro i _
57   rw [charpoly_piEnd]
58   simp
59 
60 theorem fixed_dimension_sum (D : ∀ i, Datum ν (W i)) (H : Subgroup G) (m : I → ℕ) :
61     Module.finrank K (fixedKernel (copiesDatum D m) H) =
62       ∑ i, m i * Module.finrank K (fixedKernel (D i) H) := by
63   rw [(fixedCopiesEquiv D H m).finrank_eq, copies_finrank]
64 
65 theorem fixed_trace_sum (D : ∀ i, Datum ν (W i)) (H : Subgroup G) [H.Normal]
66     (m : I → ℕ) (φ : G) :
67     LinearMap.trace K _ (fixedRep (copiesDatum D m) H φ) =
68       ∑ i, (m i : K) * LinearMap.trace K _ (fixedRep (D i) H φ) := by
69   rw [← LinearMap.trace_conj' _ (fixedCopiesEquiv D H m), fixed_conjugate, trace_piEnd]
70   apply Finset.sum_congr rfl
71   intro i _
72   rw [trace_piEnd]
73   simp
74 
75 theorem common_local_polynomial {E : Type*} [CommRing E] (σ : E →+* K)
76     (D : ∀ i, Datum ν (W i)) (H : Subgroup G) [H.Normal] (m : I → ℕ) (φ : G)
77     (P : I → Polynomial E) (hP : ∀ i, localCharpoly (D i) H φ = (P i).map σ) :
78     localCharpoly (copiesDatum D m) H φ = (∏ i, P i ^ m i).map σ := by
79   rw [local_charpoly_product]
80   simp [hP, Polynomial.map_prod]
81 
82 end PaperX.WeilCopies

Back to source controls