WeilSmooth.lean

1 import PaperX.WeilCopies
2 import PaperX.CarrierCompatibility
3 
4 /-! The finite-image and open-kernel inertia conditions are predicates on the
5 actual representation, and their preservation under finite sums is proved. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.WeilSmooth
9 open PaperX.WeilData PaperX.WeilCopies PaperX.CarrierSummands PaperX.CarrierPolynomials
10 variable {K G I : Type*} [Field K] [Group G] [Fintype I]
11 variable {W : I → Type*} [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
12 
13 omit [Fintype I] in
14 theorem copies_eq_one_iff (ρ : ∀ i, Representation K G (W i)) (m : I → ℕ) (g : G) :
15     copiesRep ρ m g = 1 ↔ ∀ i, 0 < m i → ρ i g = 1 := by
16   classical
17   constructor
18   · intro h i hi
19     apply LinearMap.ext
20     intro x
21     have hh := congrFun (congrFun (LinearMap.congr_fun h
22       (Pi.single i (fun _ : Fin (m i) => x))) i) (⟨0, hi⟩ : Fin (m i))
23     simpa using hh
24   · intro h
25     apply LinearMap.ext
26     intro x
27     funext i k
28     have hi := h i (lt_of_le_of_lt (Nat.zero_le k.val) k.isLt)
29     simp [hi]
30 
31 theorem copies_inertia_finite (ρ : ∀ i, Representation K G (W i)) (m : I → ℕ)
32     (H : Subgroup G) (h : ∀ i, Set.Finite (Set.range (fun g : H => ρ i g))) :
33     Set.Finite (Set.range (fun g : H => copiesRep ρ m g)) := by
34   classical
35   have : ∀ i, Finite (Set.range (fun g : H => ρ i g)) := fun i => (h i).to_subtype
36   have ht := Set.finite_range (fun z : ∀ i, Set.range (fun g : H => ρ i g) =>
37     piEnd (fun i => piEnd (fun _ : Fin (m i) => (z i).val)))
38   apply ht.subset
39   rintro _ ⟨g, rfl⟩
40   refine ⟨fun i => ⟨ρ i g, ⟨g, rfl⟩⟩, ?_⟩
41   ext x i k
42   rfl
43 
44 theorem copies_inertia_open [TopologicalSpace G]
45     (ρ : ∀ i, Representation K G (W i)) (m : I → ℕ) (H : Subgroup G)
46     (h : ∀ i, IsOpen {g : H | ρ i g = 1}) :
47     IsOpen {g : H | copiesRep ρ m g = 1} := by
48   have he : {g : H | copiesRep ρ m g = 1} =
49       ⋂ i, {g : H | 0 < m i → ρ i g = 1} := by
50     ext g
51     simp [copies_eq_one_iff]
52   rw [he]
53   apply isOpen_iInter_of_finite
54   intro i
55   by_cases hi : 0 < m i
56   · simpa [hi] using h i
57   · simp [hi]
58 
59 structure InertialDatum {ν : G →* Kˣ} (H : Subgroup G) [TopologicalSpace G]
60     (V : Type*) [AddCommGroup V] [Module K V] extends Datum ν V where
61   inertia_finite : Set.Finite (Set.range (fun g : H => toDatum.r g))
62   inertia_open : IsOpen {g : H | toDatum.r g = 1}
63 
64 def copiesInertialDatum {ν : G →* Kˣ} [TopologicalSpace G] (H : Subgroup G)
65     (D : ∀ i, InertialDatum (ν := ν) H (W i)) (m : I → ℕ) :
66     InertialDatum (ν := ν) H (Copies W m) where
67   toDatum := copiesDatum (fun i => (D i).toDatum) m
68   inertia_finite := copies_inertia_finite _ m H (fun i => (D i).inertia_finite)
69   inertia_open := copies_inertia_open _ m H (fun i => (D i).inertia_open)
70 
71 end PaperX.WeilSmooth

Back to source controls