WeilMorphisms.lean

1 import PaperX.WeilCopies
2 
3 /-! Maps commute with every group element and with monodromy. Restrictions
4 therefore respect the actual inertia-fixed kernel, including split summands. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperX.WeilMorphisms
8 open PaperX.WeilData PaperX.WeilCopies PaperX.CarrierSummands
9 variable {K G : Type*} [Field K] [Group G] {ν : G →* Kˣ}
10 variable {U V W : Type*} [AddCommGroup U] [Module K U]
11 variable [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
12 
13 structure Hom (D : Datum ν V) (E : Datum ν W) where
14   map : V →ₗ[K] W
15   group_eq : ∀ g x, map (D.r g x) = E.r g (map x)
16   monodromy_eq : ∀ x, map (D.N x) = E.N (map x)
17 
18 def fixedMap {D : Datum ν V} {E : Datum ν W} (f : Hom D E) (H : Subgroup G) :
19     fixedKernel D H →ₗ[K] fixedKernel E H where
20   toFun x := ⟨f.map x.val, ⟨by
21     change E.N (f.map x.val) = 0
22     rw [← f.monodromy_eq, show D.N x.val = 0 from x.property.1, map_zero], by
23     intro h
24     change E.r h (f.map x.val) = f.map x.val
25     rw [← f.group_eq]
26     exact congrArg f.map (x.property.2 h)⟩⟩
27   map_add' x y := by apply Subtype.ext; exact f.map.map_add _ _
28   map_smul' a x := by apply Subtype.ext; exact f.map.map_smul _ _
29 
30 theorem fixedMap_equivariant {D : Datum ν V} {E : Datum ν W}
31     (f : Hom D E) (H : Subgroup G) [H.Normal] (g : G) (x : fixedKernel D H) :
32     fixedMap f H (fixedRep D H g x) = fixedRep E H g (fixedMap f H x) := by
33   apply Subtype.ext
34   exact f.group_eq g x.val
35 
36 /-- An actual group-and-monodromy equivalence restricts to an equivalence of local spaces. -/
37 def fixedEquiv {D : Datum ν V} {E : Datum ν W} (e : V ≃ₗ[K] W)
38     (he : ∀ g x, e (D.r g x) = E.r g (e x))
39     (hN : ∀ x, e (D.N x) = E.N (e x)) (H : Subgroup G) :
40     fixedKernel D H ≃ₗ[K] fixedKernel E H where
41   toFun := fixedMap ⟨e.toLinearMap, he, hN⟩ H
42   invFun := fixedMap ⟨e.symm.toLinearMap,
43     fun g y => by apply e.injective; simp [he],
44     fun y => by apply e.injective; simp [hN]⟩ H
45   left_inv x := by apply Subtype.ext; exact e.symm_apply_apply x.val
46   right_inv x := by apply Subtype.ext; exact e.apply_symm_apply x.val
47   map_add' x y := (fixedMap ⟨e.toLinearMap, he, hN⟩ H).map_add x y
48   map_smul' a x := (fixedMap ⟨e.toLinearMap, he, hN⟩ H).map_smul a x
49 
50 theorem localCharpoly_equiv [FiniteDimensional K V] [FiniteDimensional K W]
51     {D : Datum ν V} {E : Datum ν W} (e : V ≃ₗ[K] W)
52     (he : ∀ g x, e (D.r g x) = E.r g (e x))
53     (hN : ∀ x, e (D.N x) = E.N (e x)) (H : Subgroup G) [H.Normal] (φ : G) :
54     localCharpoly D H φ = localCharpoly E H φ := by
55   have hc : (fixedEquiv e he hN H).conj (fixedRep D H φ) = fixedRep E H φ := by
56     ext x
57     change e (D.r φ (e.symm x.val)) = E.r φ x.val
58     rw [he, e.apply_symm_apply]
59   unfold localCharpoly
60   rw [← LinearEquiv.charpoly_conj (fixedEquiv e he hN H), hc]
61 
62 variable {I : Type*} [Fintype I] {X : I → Type*}
63 variable [∀ i, AddCommGroup (X i)] [∀ i, Module K (X i)]
64 
65 def inclusionHom (D : ∀ i, Datum ν (X i)) {m c : I → ℕ} (h : ∀ i, m i ≤ c i) :
66     Hom (copiesDatum D m) (copiesDatum D c) where
67   map := inclusion h
68   group_eq := inclusion_equivariant (fun i => (D i).r) h
69   monodromy_eq := PaperX.MonodromyData.inclusion_intertwines_N (fun i => (D i).N) h
70 
71 def retractionHom (D : ∀ i, Datum ν (X i)) {m c : I → ℕ} (h : ∀ i, m i ≤ c i) :
72     Hom (copiesDatum D c) (copiesDatum D m) where
73   map := retraction h
74   group_eq := retraction_equivariant (fun i => (D i).r) h
75   monodromy_eq := PaperX.MonodromyData.retraction_intertwines_N (fun i => (D i).N) h
76 
77 theorem fixed_split (D : ∀ i, Datum ν (X i)) (H : Subgroup G)
78     {m c : I → ℕ} (h : ∀ i, m i ≤ c i) (x : fixedKernel (copiesDatum D m) H) :
79     fixedMap (retractionHom D h) H (fixedMap (inclusionHom D h) H x) = x := by
80   apply Subtype.ext
81   exact retraction_inclusion h x.val
82 
83 end PaperX.WeilMorphisms

Back to source controls