PiPolynomial.lean

1 import PaperXI.InvariantPolynomial
2 import Mathlib.LinearAlgebra.Dimension.Constructions
3 
4 /-! Characteristic and local polynomials of finite families of varying spaces. -/
5 set_option autoImplicit false
6 noncomputable section
7 universe u v
8 namespace PaperXI.PiPolynomial
9 open scoped BigOperators Classical
10 open Polynomial PaperXI.InvariantPolynomial
11 variable {K : Type*} [Field K]
12 
13 theorem charpoly_pi {ι : Type u} [Fintype ι] (V : ι → Type v)
14     [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)] [∀ i, FiniteDimensional K (V i)]
15     (F : ∀ i, Module.End K (V i)) :
16     (LinearMap.piMap F).charpoly = ∏ i, (F i).charpoly := by
17   classical
18   refine Fintype.induction_empty_option (P := fun α _ =>
19     ∀ (W : α → Type v) [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
20       [∀ i, FiniteDimensional K (W i)] (A : ∀ i, Module.End K (W i)),
21       (LinearMap.piMap A).charpoly = ∏ i, (A i).charpoly) ?_ ?_ ?_ ι V F
22   · intro α β _ e ih V _ _ _ F
23     let : Fintype α := Fintype.ofEquiv β e.symm
24     let E := LinearEquiv.piCongrLeft K V e
25     have he : E.conj (LinearMap.piMap (fun a => F (e a))) = LinearMap.piMap F := by
26       apply LinearMap.ext
27       intro x
28       apply E.symm.injective
29       rw [LinearEquiv.conj_apply_apply, E.symm_apply_apply]
30       rfl
31     rw [← he, LinearEquiv.charpoly_conj, ih]
32     exact e.prod_comp (fun i => (F i).charpoly)
33   · intro V _ _ _ F
34     have hF : LinearMap.piMap F = 0 := Subsingleton.elim _ _
35     simp [hF, Module.finrank_zero_of_subsingleton]
36   · intro α _ ih V _ _ _ F
37     let E := LinearEquiv.piOptionEquivProd K (M := V)
38     have he : E.conj (LinearMap.piMap F) =
39         (F none).prodMap (LinearMap.piMap (fun i => F (some i))) := by
40       apply LinearMap.ext
41       intro x
42       apply Prod.ext <;> rfl
43     rw [← LinearEquiv.charpoly_conj E, he, LinearMap.charpoly_prodMap, ih]
44     simp
45 
46 theorem operatorPolynomial_pi {ι : Type u} [Fintype ι] (V : ι → Type v)
47     [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)] [∀ i, FiniteDimensional K (V i)]
48     (F : ∀ i, Module.End K (V i)) :
49     operatorPolynomial (LinearMap.piMap F) = ∏ i, operatorPolynomial (F i) := by
50   simp only [operatorPolynomial, charpoly_pi]
51   have hp (s : Finset ι) : (∏ i ∈ s, (F i).charpoly).reverse =
52       ∏ i ∈ s, (F i).charpoly.reverse := by
53     induction s using Finset.induction_on with
54     | empty => simp [Polynomial.reverse]
55     | @insert a s ha ih => simp only [Finset.prod_insert ha, Polynomial.reverse_mul_of_domain, ih]
56   exact hp Finset.univ
57 
58 end PaperXI.PiPolynomial

Back to source controls