TensorFixed.lean

1 import PaperXI.InvariantAssembly
2 
3 /-! Proposition 5.6 for an actual representation with supplied refined packets. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.TensorFixed
7 open scoped Classical
8 open PaperXI.CyclicAction PaperXI.PacketTransport PaperXI.GeneratedIrreducibility
9 variable {G I U : Type*} [Group G] [Group I] [AddCommGroup U] [Module ℂ U]
10 variable {A : Type*} [Fintype A] {V : A → Type*}
11 variable [∀ a, AddCommGroup (V a)] [∀ a, Module ℂ (V a)] [∀ a, FiniteDimensional ℂ (V a)]
12 variable {M : ℕ} [NeZero M]
13 
14 /-- The right side counts packet indices, not polynomial root multiplicities. -/
15 theorem count_trivial_packets
16     (π : Representation ℂ G U) (τ : ∀ a, Representation ℂ G (V a))
17     (e : U ≃ₗ[ℂ] (∀ a, V a)) (he : ∀ g x a, e (π g x) a = τ a g (e x a))
18     (ι : I →* G) (φ : G) (hgen : Submonoid.closure (Set.range ι ∪ {φ, φ⁻¹}) = ⊤)
19     (ρ : ∀ a, Action (K := ℂ) (V := V a) (M := M))
20     (s : I →* Multiplicative (ZMod M)) (hs : Function.Surjective s)
21     (hfactor : ∀ a, (τ a).comp ι = (ρ a).comp s) (q : (ZMod M)ˣ)
22     (hrel : ∀ a, (actionEquiv (τ a) φ).symm.conj (operator (ρ a) 1) =
23       operator (ρ a) (q : ZMod M))
24     (n : A → ℕ) (hn : ∀ a, 0 < n a) (b : ∀ a, Module.Basis (Fin (n a)) ℂ (V a))
25     (j : A → ZMod M) (v : ∀ a, V a) (hv : ∀ a, v a ∈ packet (ρ a) (j a))
26     (hb : ∀ a (i : Fin (n a)), b a i = (actionEquiv (τ a) φ ^ (i : ℕ)) (v a))
27     (c : A → ℂ) (hclose : ∀ a, (actionEquiv (τ a) φ ^ n a) (v a) = c a • v a) :
28     Module.finrank ℂ π.invariants = (Finset.univ.filter (fun a => j a = 0 ∧ c a = 1)).card := by
29   have hP (a : A) : Module.finrank ℂ (τ a).invariants = if j a = 0 ∧ c a = 1 then 1 else 0 :=
30     PaperXI.GroupFixed.packet_finrank (τ a) ι φ hgen (ρ a) s hs (hfactor a) q
31       (hrel a) (hn a) (b a) (j a) (hv a) (hb a) (c a) (hclose a)
32   simpa using PaperXI.InvariantAssembly.count_invariants π τ e he (fun a => j a = 0 ∧ c a = 1) hP
33 
34 end PaperXI.TensorFixed

Back to source controls