TensorPolynomial.lean

1 import PaperXI.PolynomialAssembly
2 
3 /-! Corollary 5.5: actual inertia determinant and rational local-factor products. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.TensorPolynomial
7 open scoped BigOperators Classical
8 open Polynomial PaperXI.CyclicAction PaperXI.PacketTransport
9 open PaperXI.InvariantPolynomial PaperXI.InertiaQuotient PaperXI.PolynomialAssembly
10 variable {I W : Type*} [Group I] [AddCommGroup W] [Module ℂ W]
11 variable {M : ℕ} [NeZero M]
12 
13 theorem quotient_stable (ρ : Action (K := ℂ) (V := W) (M := M))
14     (F : W ≃ₗ[ℂ] W) (q : (ZMod M)ˣ)
15     (hrel : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
16     (s : I →* Multiplicative (ZMod M)) (hs : Function.Surjective s) :
17     ∀ x ∈ Representation.invariants (ρ.comp s), F x ∈ Representation.invariants (ρ.comp s) := by
18   rw [invariants_comp_of_surjective ρ s hs]
19   intro x hx
20   exact PaperXI.InertiaFixed.fixed_forward ρ F q hrel hx
21 
22 theorem restricted_eq_factored (ρ : Action (K := ℂ) (V := W) (M := M))
23     (F : W ≃ₗ[ℂ] W) (q : (ZMod M)ˣ)
24     (hrel : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
25     (s : I →* Multiplicative (ZMod M)) (hs : Function.Surjective s) :
26     restricted (ρ.comp s) F.toLinearMap (quotient_stable ρ F q hrel s hs) =
27       (factoredFrobenius ρ F q hrel s hs).toLinearMap := by
28   apply LinearMap.ext
29   intro x
30   apply Subtype.ext
31   exact (factoredFrobenius_apply ρ F q hrel s hs x).symm
32 
33 theorem cyclePolynomial_ne_zero {n : ℕ} (hn : 0 < n) (c : ℂ) :
34     (1 - C c * X ^ n : ℂ[X]) ≠ 0 := by
35   intro h
36   have hc := congrArg (fun p : ℂ[X] => p.coeff 0) h
37   simp [Ne.symm hn.ne'] at hc
38 
39 variable {U : Type*} [AddCommGroup U] [Module ℂ U] [FiniteDimensional ℂ U]
40 variable {A : Type*} [Fintype A] {V : A → Type*}
41 variable [∀ a, AddCommGroup (V a)] [∀ a, Module ℂ (V a)] [∀ a, FiniteDimensional ℂ (V a)]
42 variable (ρ₀ : Representation ℂ I U) (ρ : ∀ a, Action (K := ℂ) (V := V a) (M := M))
43 variable (s : I →* Multiplicative (ZMod M)) (hs : Function.Surjective s)
44 variable (e : U ≃ₗ[ℂ] (∀ a, V a)) (he : ∀ g x a, e (ρ₀ g x) a = ρ a (s g) (e x a))
45 variable (F : U ≃ₗ[ℂ] U) (T : ∀ a, V a ≃ₗ[ℂ] V a) (q : (ZMod M)ˣ)
46 variable (hrel : ∀ a, (T a).symm.conj (operator (ρ a) 1) = operator (ρ a) (q : ZMod M))
47 variable (hmap : ∀ x a, e (F x) a = T a (e x a))
48 variable (n : A → ℕ) (hn : ∀ a, 0 < n a) (b : ∀ a, Module.Basis (Fin (n a)) ℂ (V a))
49 variable (j : A → ZMod M) (v : ∀ a, V a) (hv : ∀ a, v a ∈ packet (ρ a) (j a))
50 variable (hb : ∀ a (i : Fin (n a)), b a i = (T a ^ (i : ℕ)) (v a))
51 variable (c : A → ℂ) (hclose : ∀ a, (T a ^ n a) (v a) = c a • v a)
52 
53 omit [FiniteDimensional ℂ U] [Fintype A] [∀ a, FiniteDimensional ℂ (V a)] in
54 include he hmap hrel hs in
55 /-- Invariance of the total fixed space is derived from the packet action. -/
56 theorem total_stable : ∀ x ∈ ρ₀.invariants, F x ∈ ρ₀.invariants :=
57   stable_of_decomposition ρ₀ (fun a => (ρ a).comp s) e he F.toLinearMap
58     (fun a => (T a).toLinearMap) (fun a => quotient_stable (ρ a) (T a) q (hrel a) s hs) hmap
59 
60 variable (hF : ∀ x ∈ ρ₀.invariants, F x ∈ ρ₀.invariants)
61 include he hmap hrel hs hn hv hb hclose
62 
63 theorem polynomial_packets :
64     operatorPolynomial (restricted ρ₀ F.toLinearMap hF) =
65       ∏ a ∈ Finset.univ.filter (fun a => j a = 0), (1 - C (c a) * X ^ n a) := by
66   rw [polynomial_product ρ₀ (fun a => (ρ a).comp s) e he F.toLinearMap
67     (fun a => (T a).toLinearMap) hF
68     (fun a => quotient_stable (ρ a) (T a) q (hrel a) s hs) hmap]
69   rw [Finset.prod_filter]
70   apply Finset.prod_congr rfl
71   intro a _
72   rw [restricted_eq_factored]
73   exact factored_local_polynomial (ρ a) (T a) q (hrel a) s hs (hn a) (b a) (j a) (hv a) (hb a) (c a) (hclose a)
74 
75 theorem determinant_packets {κ : Type*} [Fintype κ] [DecidableEq κ]
76     (B : Module.Basis κ ℂ ρ₀.invariants) :
77     Matrix.det (1 - (X : ℂ[X]) • (LinearMap.toMatrix B B (restricted ρ₀ F.toLinearMap hF)).map C) =
78       ∏ a ∈ Finset.univ.filter (fun a => j a = 0), (1 - C (c a) * X ^ n a) := by
79   rw [← operatorPolynomial_eq_det]
80   exact polynomial_packets ρ₀ ρ s hs e he F T q hrel hmap n hn b j v hv hb c hclose hF
81 
82 theorem localFactor_packets :
83     localFactor ρ₀ F.toLinearMap hF =
84       ∏ a ∈ Finset.univ.filter (fun a => j a = 0),
85         (algebraMap ℂ[X] (RatFunc ℂ) (1 - C (c a) * X ^ n a))⁻¹ := by
86   rw [localFactor, polynomial_packets ρ₀ ρ s hs e he F T q hrel hmap n hn b j v hv hb c hclose hF]
87   simp only [map_prod, Finset.prod_inv_distrib]
88 
89 end PaperXI.TensorPolynomial

Back to source controls