InvariantAssembly.lean

1 import PaperXI.GroupFixed
2 import Mathlib.LinearAlgebra.Dimension.Constructions
3 
4 /-! Actual invariant spaces under a supplied equivariant finite decomposition. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.InvariantAssembly
8 open scoped BigOperators Classical
9 variable {K G U : Type*} [Field K] [Group G] [AddCommGroup U] [Module K U]
10 variable {ι : Type*} {V : ι → Type*} [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
11 
12 /-- Restrict an equivariant decomposition to the canonical invariant spaces. -/
13 def invariantsEquiv (π : Representation K G U) (τ : ∀ i, Representation K G (V i))
14     (e : U ≃ₗ[K] (∀ i, V i)) (he : ∀ g x i, e (π g x) i = τ i g (e x i)) :
15     π.invariants ≃ₗ[K] (∀ i, (τ i).invariants) where
16   toFun x i := ⟨e x i, fun g => by rw [← he, x.property g]⟩
17   invFun x := ⟨e.symm (fun i => x i), by
18     intro g
19     apply e.injective
20     ext i
21     rw [he, e.apply_symm_apply]
22     exact (x i).property g⟩
23   left_inv x := by apply Subtype.ext; exact e.symm_apply_apply x
24   right_inv x := by ext i; exact congrFun (e.apply_symm_apply (fun i => x i)) i
25   map_add' x y := by ext i; simp
26   map_smul' c x := by ext i; simp
27 
28 theorem invariantsEquiv_apply (π : Representation K G U) (τ : ∀ i, Representation K G (V i))
29     (e : U ≃ₗ[K] (∀ i, V i)) (he : ∀ g x i, e (π g x) i = τ i g (e x i))
30     (x : π.invariants) (i : ι) : (invariantsEquiv π τ e he x i : V i) = e x i := rfl
31 
32 theorem finrank_invariants [Fintype ι] [∀ i, FiniteDimensional K (V i)]
33     (π : Representation K G U) (τ : ∀ i, Representation K G (V i))
34     (e : U ≃ₗ[K] (∀ i, V i)) (he : ∀ g x i, e (π g x) i = τ i g (e x i)) :
35     Module.finrank K π.invariants = ∑ i, Module.finrank K (τ i).invariants := by
36   rw [(invariantsEquiv π τ e he).finrank_eq, Module.finrank_pi_fintype]
37 
38 /-- A literal count, after independently computing each actual packet fixed space. -/
39 theorem count_invariants [Fintype ι] [∀ i, FiniteDimensional K (V i)]
40     (π : Representation K G U) (τ : ∀ i, Representation K G (V i))
41     (e : U ≃ₗ[K] (∀ i, V i)) (he : ∀ g x i, e (π g x) i = τ i g (e x i))
42     (P : ι → Prop) [DecidablePred P] (hP : ∀ i, Module.finrank K (τ i).invariants = if P i then 1 else 0) :
43     Module.finrank K π.invariants = (Finset.univ.filter P).card := by
44   rw [finrank_invariants π τ e he]
45   simp_rw [hP]
46   simp
47 
48 end PaperXI.InvariantAssembly

Back to source controls