CarrierCompatibility.lean

1 import PaperX.CarrierPolynomials
2 import Mathlib.Topology.Constructions
3 
4 /-! Coefficient-independent multiplicities produce common polynomials at the
5 explicitly permitted samples. This is not the full arithmetic notion of strict
6 compatibility: no Hodge--Tate or Weil--Deligne realization is postulated here. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.CarrierCompatibility
10 open scoped BigOperators Matrix
11 open PaperX.CarrierSummands PaperX.CarrierPolynomials PaperX.TraceRecovery
12 
13 variable {K G I : Type*} [Field K] [Monoid G] [Fintype I]
14 variable {V : I → Type*} [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
15 variable [∀ i, FiniteDimensional K (V i)]
16 
17 theorem common_polynomial {E : Type*} [CommRing E] (σ : E →+* K)
18     (ρ : ∀ i, Representation K G (V i)) (m : I → ℕ) (g : G)
19     (P : I → Polynomial E) (hP : ∀ i, (ρ i g).charpoly = (P i).map σ) :
20     (copiesRep ρ m g).charpoly = (∏ i, P i ^ m i).map σ := by
21   rw [copies_charpoly]
22   simp only [hP]
23   simp [Polynomial.map_prod]
24 
25 /-- The observed vector is made from traces of the constructed representation. -/
26 theorem sampled_trace [DecidableEq I] (ρ : ∀ i, Representation K G (V i))
27     (m : I → ℕ) (s : I → G) :
28     (fun j => LinearMap.trace K _ (copiesRep ρ m (s j))) =
29       (fun j i => LinearMap.trace K _ (ρ i (s j))) *ᵥ (fun i => (m i : K)) := by
30   funext j
31   simp [copies_trace, Matrix.mulVec, dotProduct, mul_comm]
32 
33 theorem recovery_of_actual_summand [DecidableEq I]
34     (ρ : ∀ i, Representation K G (V i)) (m : I → ℕ) (s : I → G)
35     (h : Matrix.det (fun j i => LinearMap.trace K _ (ρ i (s j))) ≠ 0) :
36     recover (fun j i => LinearMap.trace K _ (ρ i (s j)))
37       (fun j => LinearMap.trace K _ (copiesRep ρ m (s j))) = (fun i => (m i : K)) := by
38   rw [sampled_trace, recover_trace _ h]
39 
40 theorem multiplicities_unique_from_actual_traces [DecidableEq I] [CharZero K]
41     (ρ : ∀ i, Representation K G (V i)) (m n : I → ℕ) (s : I → G)
42     (h : Matrix.det (fun j i => LinearMap.trace K _ (ρ i (s j))) ≠ 0)
43     (ht : ∀ j, LinearMap.trace K _ (copiesRep ρ m (s j)) =
44       LinearMap.trace K _ (copiesRep ρ n (s j))) : m = n := by
45   apply natural_multiplicity_unique (fun j i => LinearMap.trace K _ (ρ i (s j))) h
46   rw [← sampled_trace, ← sampled_trace]
47   exact funext ht
48 
49 omit [Fintype I] [∀ i, FiniteDimensional K (V i)] in
50 /-- Triviality on a supplied subgroup (or set) is preserved by construction. -/
51 theorem copies_trivial_on (ρ : ∀ i, Representation K G (V i)) (m : I → ℕ)
52     (S : Set G) (h : ∀ i g, g ∈ S → ρ i g = 1) (g : G) (hg : g ∈ S) :
53     copiesRep ρ m g = 1 := by
54   apply LinearMap.ext
55   intro x
56   funext i k
57   simp [h i g hg]
58 
59 section Topology
60 variable [TopologicalSpace G] [∀ i, TopologicalSpace (V i)]
61 
62 omit [Fintype I] [∀ i, FiniteDimensional K (V i)] in
63 /-- Jointly continuous constituent actions give a jointly continuous sum action. -/
64 theorem continuous_copies_action (ρ : ∀ i, Representation K G (V i)) (m : I → ℕ)
65     (h : ∀ i, Continuous (fun p : G × V i => ρ i p.1 p.2)) :
66     Continuous (fun p : G × Copies V m => copiesRep ρ m p.1 p.2) := by
67   apply continuous_pi
68   intro i
69   apply continuous_pi
70   intro k
71   exact (h i).comp (continuous_fst.prodMk
72     ((continuous_apply k).comp ((continuous_apply i).comp continuous_snd)))
73 
74 omit [Fintype I] [∀ i, FiniteDimensional K (V i)] in
75 theorem continuous_inclusion {m c : I → ℕ} (h : ∀ i, m i ≤ c i) :
76     Continuous (inclusion (R := K) (V := V) h) := by
77   apply continuous_pi
78   intro i
79   apply continuous_pi
80   intro k
81   by_cases hk : k.val < m i
82   · simpa [inclusion, hk, Function.comp_def] using
83       (continuous_apply (⟨k.val, hk⟩ : Fin (m i))).comp (continuous_apply i)
84   · simpa [inclusion, hk, Function.comp_def] using
85       (continuous_const : Continuous (fun _ : Copies V m => (0 : V i)))
86 
87 omit [Fintype I] [∀ i, FiniteDimensional K (V i)] in
88 theorem continuous_retraction {m c : I → ℕ} (h : ∀ i, m i ≤ c i) :
89     Continuous (retraction (R := K) (V := V) h) := by
90   apply continuous_pi
91   intro i
92   apply continuous_pi
93   intro k
94   exact (continuous_apply (⟨k.val, lt_of_lt_of_le k.isLt (h i)⟩ : Fin (c i))).comp
95     (continuous_apply i)
96 end Topology
97 
98 end PaperX.CarrierCompatibility

Back to source controls