InteractionPolynomial.lean

1 import PaperXI.InvariantPolynomial
2 import PaperXI.PacketCycle
3 
4 /-! Both local-polynomial branches for a cyclic interaction packet. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.InteractionPolynomial
8 open Polynomial
9 open PaperXI.CyclicAction PaperXI.PacketTransport PaperXI.InertiaFixed
10 open PaperXI.InvariantPolynomial
11 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
12 variable {M : ℕ} [NeZero M]
13 
14 theorem character_trivial_iff (j : ZMod M) :
15     (∀ a : ZMod M, ZMod.stdAddChar (j * a) = (1 : ℂ)) ↔ j = 0 := by
16   constructor
17   · intro h
18     apply ZMod.injective_stdAddChar
19     simpa using h 1
20   · rintro rfl
21     simp
22 
23 /-- Proposition 5.4: the determinant is on actual inertia invariants. -/
24 theorem local_polynomial [FiniteDimensional ℂ V]
25     (ρ : Action (K := ℂ) (V := V) (M := M)) (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
26     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
27     {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) ℂ V) (j : ZMod M) {v : V}
28     (hv : v ∈ packet ρ j) (hb : ∀ i : Fin n, b i = (F ^ (i : ℕ)) v)
29     (c : ℂ) (hclose : (F ^ n) v = c • v) :
30     localPolynomial ρ F q h = if j = 0 then 1 - C c * X ^ n else 1 := by
31   classical
32   have hinv := invariants_of_cycle_basis ρ F q h b j hv hb
33   by_cases hj : j = 0
34   · rw [ite_eq_left hj] at hinv ⊢
35     rw [localPolynomial_of_top ρ F q h hinv, operatorPolynomial]
36     have hlin (i : Fin n) : b i = (F.toLinearMap ^ (i : ℕ)) v := by
37       rw [PaperXI.PacketCycle.linear_power]
38       exact hb i
39     have hcl : (F.toLinearMap ^ n) v = c • v := by
40       simpa only [PaperXI.PacketCycle.linear_power] using hclose
41     rw [PaperXI.CyclicPolynomial.charpoly_of_orbit_basis F.toLinearMap hn b v hlin c hcl,
42       PaperXI.CyclicPolynomial.reverse_cycle_polynomial]
43   · rw [ite_eq_right hj] at hinv ⊢
44     exact localPolynomial_of_bot ρ F q h hinv
45 
46 /-- The same formula using the literal trivial-character condition. -/
47 theorem local_polynomial_character_form [FiniteDimensional ℂ V]
48     (ρ : Action (K := ℂ) (V := V) (M := M)) (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
49     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
50     {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) ℂ V) (j : ZMod M) {v : V}
51     (hv : v ∈ packet ρ j) (hb : ∀ i : Fin n, b i = (F ^ (i : ℕ)) v)
52     (c : ℂ) (hclose : (F ^ n) v = c • v) :
53     localPolynomial ρ F q h =
54       if (∀ a : ZMod M, ZMod.stdAddChar (j * a) = (1 : ℂ))
55       then 1 - C c * X ^ n else 1 := by
56   simpa only [character_trivial_iff] using local_polynomial ρ F q h hn b j hv hb c hclose
57 
58 variable {G : Type*} [Group G]
59 
60 /-- Applied to an actual group action with the geometric inertia relation.
61 No irreducibility or group-generation hypothesis is required. -/
62 theorem group_local_polynomial [FiniteDimensional ℂ V]
63     (π : Representation ℂ G V) (ι : Multiplicative (ZMod M) →* G)
64     (φ : G) (q : (ZMod M)ˣ)
65     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
66       ι (Multiplicative.ofAdd (q : ZMod M)))
67     {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) ℂ V) (j : ZMod M) {v : V}
68     (hv : v ∈ packet (PaperXI.TameOrbitTransitivity.tameRestriction π ι) j)
69     (hb : ∀ i : Fin n, b i = (PaperXI.GeneratedIrreducibility.actionEquiv π φ ^ (i : ℕ)) v)
70     (c : ℂ) (hclose : (PaperXI.GeneratedIrreducibility.actionEquiv π φ ^ n) v = c • v) :
71     localPolynomial (PaperXI.TameOrbitTransitivity.tameRestriction π ι)
72       (PaperXI.GeneratedIrreducibility.actionEquiv π φ) q
73       (PaperXI.TameOrbitTransitivity.geometric_relation π ι φ q hrel) =
74         if j = 0 then 1 - C c * X ^ n else 1 :=
75   local_polynomial _ _ _ _ hn b j hv hb c hclose
76 
77 end PaperXI.InteractionPolynomial

Back to source controls