PacketTransport.lean

1 import PaperXI.TameProjectors
2 
3 /-! Actual Frobenius transport between the ranges of the computed projectors. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.PacketTransport
7 open PaperXI.CyclicAction
8 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
9 variable {M : ℕ} [NeZero M]
10 
11 abbrev packet (ρ : Action (K := ℂ) (V := V) (M := M)) (j : ZMod M) :=
12   PaperXI.FourierPackets.packet ρ ZMod.stdAddChar j
13 
14 abbrev projector (ρ : Action (K := ℂ) (V := V) (M := M)) (j : ZMod M) :=
15   PaperXI.TameProjectors.projector ρ j
16 
17 theorem mem_iff_projector (ρ : Action (K := ℂ) (V := V) (M := M))
18     (j : ZMod M) (v : V) : v ∈ packet ρ j ↔ projector ρ j v = v := by
19   constructor
20   · exact PaperXI.FourierPackets.projector_on_packet ρ _ (NeZero.ne (M : ℂ)) j
21   · intro h
22     rw [← h]
23     exact PaperXI.FourierPackets.projector_mem_packet ρ _ j v
24 
25 theorem projector_on_other_packet (ρ : Action (K := ℂ) (V := V) (M := M))
26     {i j : ZMod M} (hij : i ≠ j) {v : V} (hv : v ∈ packet ρ j) :
27     projector ρ i v = 0 := by
28   have hp := LinearMap.congr_fun (PaperXI.TameProjectors.orthogonal ρ hij) v
29   change projector ρ i (projector ρ j v) = 0 at hp
30   rwa [(mem_iff_projector ρ j v).mp hv] at hp
31 
32 theorem inertia_mem (ρ : Action (K := ℂ) (V := V) (M := M))
33     (a j : ZMod M) {v : V} (hv : v ∈ packet ρ j) : operator ρ a v ∈ packet ρ j := by
34   change ∀ b, operator ρ b v = ZMod.stdAddChar (j * b) • v at hv
35   rw [hv a]
36   exact (packet ρ j).smul_mem _ (by exact hv)
37 
38 theorem transport_of_conjugation (ρ : Action (K := ℂ) (V := V) (M := M))
39     (F : V ≃ₗ[ℂ] V) {i j : ZMod M}
40     (h : F.conj (projector ρ i) = projector ρ j) {v : V} (hv : v ∈ packet ρ i) :
41     F v ∈ packet ρ j := by
42   apply (mem_iff_projector ρ j (F v)).mpr
43   have hp := LinearMap.congr_fun h (F v)
44   simpa [LinearEquiv.conj_apply_apply, (mem_iff_projector ρ i v).mp hv] using hp.symm
45 
46 theorem forward_mem (ρ : Action (K := ℂ) (V := V) (M := M))
47     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
48     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
49     (j : ZMod M) {v : V} (hv : v ∈ packet ρ j) :
50     F v ∈ packet ρ ((q : ZMod M) * j) :=
51   transport_of_conjugation ρ F (PaperXI.TameProjectors.geometric_covariance ρ F q h j) hv
52 
53 theorem backward_mem (ρ : Action (K := ℂ) (V := V) (M := M))
54     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
55     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M))
56     (j : ZMod M) {v : V} (hv : v ∈ packet ρ j) :
57     F.symm v ∈ packet ρ (((q⁻¹ : (ZMod M)ˣ) : ZMod M) * j) :=
58   transport_of_conjugation ρ F.symm
59     (PaperXI.TameProjectors.forward_generator_covariance ρ F.symm q h j) hv
60 
61 /-- Frobenius is an actual linear equivalence between the two packet spaces. -/
62 def packetEquiv (ρ : Action (K := ℂ) (V := V) (M := M))
63     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
64     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M)) (j : ZMod M) :
65     packet ρ j ≃ₗ[ℂ] packet ρ ((q : ZMod M) * j) where
66   toFun v := ⟨F v, forward_mem ρ F q h j v.property⟩
67   invFun w := ⟨F.symm w, by
68     simpa only [← mul_assoc, Units.inv_mul, one_mul] using
69       backward_mem ρ F q h ((q : ZMod M) * j) w.property⟩
70   left_inv v := by ext; simp
71   right_inv w := by ext; simp
72   map_add' v w := by ext; simp
73   map_smul' c v := by ext; simp
74 
75 theorem packet_finrank_step (ρ : Action (K := ℂ) (V := V) (M := M))
76     (F : V ≃ₗ[ℂ] V) (q : (ZMod M)ˣ)
77     (h : F.symm.conj (operator ρ 1) = operator ρ (q : ZMod M)) (j : ZMod M) :
78     Module.finrank ℂ (packet ρ j) = Module.finrank ℂ (packet ρ ((q : ZMod M) * j)) :=
79   (packetEquiv ρ F q h j).finrank_eq
80 
81 end PaperXI.PacketTransport

Back to source controls