GroupFixed.lean

1 import PaperXI.CycleFixed
2 import PaperXI.InertiaQuotient
3 
4 /-! Fixedness under an actual group, including supplied inertia quotient data. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.GroupFixed
8 open scoped BigOperators Classical
9 open PaperXI.CycleFixed PaperXI.GeneratedIrreducibility
10 variable {K V G I : Type*} [Field K] [AddCommGroup V] [Module K V] [Group G] [Group I]
11 
12 theorem fixed_of_generators (π : Representation K G V) (S : Set G)
13     (hgen : Submonoid.closure S = ⊤) (x : V) (hx : ∀ g ∈ S, π g x = x) :
14     x ∈ π.invariants := by
15   intro g
16   have hg : g ∈ Submonoid.closure S := by rw [hgen]; trivial
17   induction hg using Submonoid.closure_induction with
18   | mem g hg => exact hx g hg
19   | one => simp
20   | mul a b _ _ ha hb => simp [map_mul, Module.End.mul_apply, ha, hb]
21 
22 theorem invariants_eq_common (π : Representation K G V) (ι : I →* G) (φ : G)
23     (hgen : Submonoid.closure (Set.range ι ∪ {φ, φ⁻¹}) = ⊤) :
24     π.invariants = (Representation.invariants (π.comp ι)) ⊓ fixedSpace (π φ) := by
25   ext x
26   constructor
27   · intro hx
28     exact ⟨fun a => hx (ι a), (mem_fixedSpace _ _).mpr (hx φ)⟩
29   · rintro ⟨hI, hF⟩
30     have hF' := (mem_fixedSpace _ _).mp hF
31     apply fixed_of_generators π _ hgen x
32     intro g hg
33     rcases hg with ⟨a, rfl⟩ | hg
34     · exact hI a
35     · rcases hg with hg | hg
36       · have he : g = φ := hg
37         simpa [he] using hF'
38       · have he : g = φ⁻¹ := hg
39         subst g
40         have h := congrArg (π φ⁻¹) hF'
41         simpa using h.symm
42 
43 variable {U : Type*} [AddCommGroup U] [Module ℂ U]
44 open PaperXI.CyclicAction PaperXI.PacketTransport
45 
46 theorem orbit_basis_steps (F : U ≃ₗ[ℂ] U) {n : ℕ} (hn : 0 < n)
47     (b : Module.Basis (Fin n) ℂ U) (v : U)
48     (hb : ∀ i : Fin n, b i = (F ^ (i : ℕ)) v) (c : ℂ)
49     (hclose : (F ^ n) v = c • v) :
50     (∀ (i : Fin n) (hi : (i : ℕ) + 1 < n), F (b i) = b ⟨i + 1, hi⟩) ∧
51     F (b ⟨n - 1, by omega⟩) = c • b ⟨0, hn⟩ := by
52   constructor
53   · intro i hi
54     rw [hb, hb, pow_succ']
55     rfl
56   · rw [hb, hb]
57     have hn' : n = (n - 1) + 1 := by omega
58     have h := hclose
59     conv_lhs at h => rw [hn', pow_succ']
60     simpa using h
61 
62 /-- The count for one packet uses the actual full-group invariant space. -/
63 theorem packet_finrank {M : ℕ} [NeZero M]
64     (π : Representation ℂ G U) (ι : I →* G) (φ : G)
65     (hgen : Submonoid.closure (Set.range ι ∪ {φ, φ⁻¹}) = ⊤)
66     (ρ : Action (K := ℂ) (V := U) (M := M))
67     (s : I →* Multiplicative (ZMod M)) (hs : Function.Surjective s)
68     (hfactor : π.comp ι = ρ.comp s) (q : (ZMod M)ˣ)
69     (hrel : (actionEquiv π φ).symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
70     {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) ℂ U) (j : ZMod M) {v : U}
71     (hv : v ∈ packet ρ j) (hb : ∀ i : Fin n, b i = (actionEquiv π φ ^ (i : ℕ)) v)
72     (c : ℂ) (hclose : (actionEquiv π φ ^ n) v = c • v) :
73     Module.finrank ℂ π.invariants = if j = 0 ∧ c = 1 then 1 else 0 := by
74   have hI : Representation.invariants (π.comp ι) = if j = 0 then ⊤ else ⊥ := by
75     rw [hfactor, PaperXI.InertiaQuotient.invariants_comp_of_surjective ρ s hs]
76     exact PaperXI.InertiaFixed.invariants_of_cycle_basis ρ (actionEquiv π φ) q hrel b j hv hb
77   have hsteps := orbit_basis_steps (actionEquiv π φ) hn b v hb c hclose
78   rw [invariants_eq_common π ι φ hgen, hI]
79   by_cases hj : j = 0
80   · rw [ite_eq_left hj, top_inf_eq]
81     simpa only [hj, true_and] using fixedSpace_finrank (π φ) hn b hsteps.1 c hsteps.2
82   · rw [ite_eq_right hj, bot_inf_eq]
83     simp [hj]
84 
85 end PaperXI.GroupFixed

Back to source controls