CarrierPolynomials.lean

1 import PaperX.CarrierSummands
2 import PaperX.TraceRecovery
3 import Mathlib.LinearAlgebra.Charpoly.ToMatrix
4 import Mathlib.LinearAlgebra.Trace
5 import Mathlib.Data.Fintype.Option
6 
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.CarrierPolynomials
10 open scoped BigOperators
11 open PaperX.CarrierSummands
12 
13 variable {K : Type*} [Field K]
14 
15 def piEnd {I : Type*} {V : I → Type*}
16     [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
17     (f : ∀ i, Module.End K (V i)) : Module.End K (∀ i, V i) :=
18   LinearMap.pi (fun i => (f i).comp (LinearMap.proj i))
19 
20 @[simp] theorem piEnd_apply {I : Type*} {V : I → Type*}
21     [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
22     (f : ∀ i, Module.End K (V i)) (x : ∀ i, V i) (i : I) :
23     piEnd f x i = f i (x i) := rfl
24 
25 /-- Determinant polynomial of an actual finite dependent product of maps. -/
26 theorem charpoly_piEnd (I : Type*) [Fintype I] (V : I → Type*)
27     [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)] [∀ i, FiniteDimensional K (V i)]
28     (f : ∀ i, Module.End K (V i)) :
29     (piEnd f).charpoly = ∏ i, (f i).charpoly := by
30   classical
31   revert V
32   refine Fintype.induction_empty_option (P := fun J _ =>
33     ∀ (U : J → Type _) [∀ j, AddCommGroup (U j)] [∀ j, Module K (U j)]
34       [∀ j, FiniteDimensional K (U j)] (f : ∀ j, Module.End K (U j)),
35       (piEnd f).charpoly = ∏ j, (f j).charpoly) ?_ ?_ ?_ I
36   · intro A B _ e ih V _ _ _ f
37     let : Fintype A := Fintype.ofEquiv B e.symm
38     let D := LinearEquiv.piCongrLeft K V e
39     have hD : D.conj (piEnd (fun i => f (e i))) = piEnd f := by
40       apply LinearMap.ext
41       intro x
42       change D (piEnd (fun i => f (e i)) (D.symm x)) = piEnd f x
43       apply D.symm.injective
44       rw [LinearEquiv.symm_apply_apply]
45       rfl
46     rw [← hD, LinearEquiv.charpoly_conj, ih]
47     exact Fintype.prod_equiv e _ _ (fun _ => rfl)
48   · intro V _ _ _ f
49     have hf : piEnd f = 0 := Subsingleton.elim _ _
50     simp [hf, Module.finrank_zero_of_subsingleton]
51   · intro A _ ih V _ _ _ f
52     let D := LinearEquiv.piOptionEquivProd K (M := V)
53     have hD : D.conj (piEnd f) = (f none).prodMap (piEnd (fun i => f (some i))) := by
54       apply LinearMap.ext
55       intro x
56       apply Prod.ext <;> rfl
57     rw [← LinearEquiv.charpoly_conj D (piEnd f), hD,
58       LinearMap.charpoly_prodMap, ih, Fintype.prod_option]
59 
60 /-- Actual traces add under the same dependent product construction. -/
61 theorem trace_piEnd (I : Type*) [Fintype I] (V : I → Type*)
62     [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)] [∀ i, FiniteDimensional K (V i)]
63     (f : ∀ i, Module.End K (V i)) :
64     LinearMap.trace K _ (piEnd f) = ∑ i, LinearMap.trace K _ (f i) := by
65   classical
66   revert V
67   refine Fintype.induction_empty_option (P := fun J _ =>
68     ∀ (U : J → Type _) [∀ j, AddCommGroup (U j)] [∀ j, Module K (U j)]
69       [∀ j, FiniteDimensional K (U j)] (f : ∀ j, Module.End K (U j)),
70       LinearMap.trace K _ (piEnd f) = ∑ j, LinearMap.trace K _ (f j)) ?_ ?_ ?_ I
71   · intro A B _ e ih V _ _ _ f
72     let : Fintype A := Fintype.ofEquiv B e.symm
73     let D := LinearEquiv.piCongrLeft K V e
74     have hD : D.conj (piEnd (fun i => f (e i))) = piEnd f := by
75       apply LinearMap.ext
76       intro x
77       change D (piEnd (fun i => f (e i)) (D.symm x)) = piEnd f x
78       apply D.symm.injective
79       rw [LinearEquiv.symm_apply_apply]
80       rfl
81     rw [← hD, LinearMap.trace_conj', ih]
82     exact Fintype.sum_equiv e _ _ (fun _ => rfl)
83   · intro V _ _ _ f
84     have hf : piEnd f = 0 := Subsingleton.elim _ _
85     simp [hf]
86   · intro A _ ih V _ _ _ f
87     let D := LinearEquiv.piOptionEquivProd K (M := V)
88     have hD : D.conj (piEnd f) = (f none).prodMap (piEnd (fun i => f (some i))) := by
89       apply LinearMap.ext
90       intro x
91       apply Prod.ext <;> rfl
92     rw [← LinearMap.trace_conj' (piEnd f) D, hD,
93       LinearMap.trace_prodMap', ih, Fintype.sum_option]
94 
95 variable {G I : Type*} [Monoid G] [Fintype I]
96 variable {V : I → Type*} [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
97 variable [∀ i, FiniteDimensional K (V i)]
98 
99 theorem copies_charpoly (ρ : ∀ i, Representation K G (V i)) (m : I → ℕ) (g : G) :
100     (copiesRep ρ m g).charpoly = ∏ i, (ρ i g).charpoly ^ m i := by
101   change (piEnd (fun i => piEnd (fun _ : Fin (m i) => ρ i g))).charpoly = _
102   rw [charpoly_piEnd]
103   apply Finset.prod_congr rfl
104   intro i _
105   rw [charpoly_piEnd]
106   simp
107 
108 theorem copies_trace (ρ : ∀ i, Representation K G (V i)) (m : I → ℕ) (g : G) :
109     LinearMap.trace K _ (copiesRep ρ m g) = ∑ i, (m i : K) * LinearMap.trace K _ (ρ i g) := by
110   change LinearMap.trace K _ (piEnd (fun i => piEnd (fun _ : Fin (m i) => ρ i g))) = _
111   rw [trace_piEnd]
112   apply Finset.sum_congr rfl
113   intro i _
114   rw [trace_piEnd]
115   simp
116 
117 theorem copies_finrank (m : I → ℕ) :
118     Module.finrank K (Copies V m) = ∑ i, m i * Module.finrank K (V i) := by
119   simp [Copies, Module.finrank_pi_fintype]
120 
121 end PaperX.CarrierPolynomials

Back to source controls