EquivariantRepresentation113.lean

1 import PaperXI.ActualScalarLift113
2 
3 /-! The corrected scalar cochain constructs an actual representation that
4 retains the original theta and intertwines the original packet generator.
5 Actual groups and their full automorphisms remain explicit inputs. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.EquivariantRepresentation113
9 open Representation ScalarRepresentation112 ActualScalarLift113 CyclicDefect113
10 
11 section Covariance
12 variable {G P A V : Type*} [Group G] [Group P] [CommGroup A]
13   [AddCommGroup V] [Module ℂ V]
14   (D : Subgroup G) [D.Normal] (θ : D →* ℂˣ)
15   (hinv : TypeSideDescent.Invariant D θ)
16   (q : G →* A) (hker : q.ker = D)
17   (t : A → G) (ht : ∀ a, q (t a) = a) (ht1 : t 1 = 1)
18   (H : Subgroup P) [H.Normal] (χ : H →* ℂˣ)
19   (r : P →* A) (hkerP : r.ker = H)
20   (u : A → P) (hu : ∀ a, r (u a) = a) (hu1 : u 1 = 1)
21   (ρ : Representation ℂ P V)
22   (hρ : ∀ h : H, ρ h = (χ h : ℂ) • LinearMap.id)
23   (α : G ≃* G) (γ : P ≃* P) (β : A ≃* A)
24   (hq : ∀ g, q (α g) = β (q g)) (hr : ∀ p, r (γ p) = β (r p))
25   (hθ : ∀ d : D, θ (subgroupMap D q hker α β hq d) = θ d)
26   (U : V ≃ₗ[ℂ] V) (hU : ∀ p v, U (ρ p v) = ρ (γ p) (U v))
27   (s : A → ℂˣ) (hs1 : s 1 = 1)
28   (hc : ∀ a b, sectionCocycle D θ q hker t ht a b =
29     (s a * s b / s (a*b)) * sectionCocycle H χ r hkerP u hu a b)
30   (hcov : ∀ a, actualPhase D θ q hker t ht α a * s (β a) =
31     s a * actualPhase H χ r hkerP u hu γ a)
32 
33 omit [H.Normal] in
34 include hq hr hθ hU hcov in
35 /-- A covariant comparison cochain transfers the original packet generator
36 without changing that operator or the original theta. The final existence
37 theorem below derives the required cochain covariance. -/
38 theorem scalarTransport_covariant (g : G) (v : V) :
39     U (scalarTransport D θ hinv q hker t ht ht1 H χ r hkerP u hu hu1 ρ hρ s hs1 hc g v) =
40       scalarTransport D θ hinv q hker t ht ht1 H χ r hkerP u hu hu1 ρ hρ s hs1 hc (α g) (U v) := by
41   have hcoeff :
42       (sectionScalar D θ q hker t ht g * s (q g)) * actualPhase H χ r hkerP u hu γ (q g) =
43         sectionScalar D θ q hker t ht (α g) * s (q (α g)) := by
44     rw [sectionScalar_action D θ hinv q hker t ht ht1 α β hq hθ, hq]
45     rw [mul_assoc, ← hcov, mul_assoc]
46   change U (((sectionScalar D θ q hker t ht g * s (q g) : ℂˣ) : ℂ) • ρ (u (q g)) v) =
47     ((sectionScalar D θ q hker t ht (α g) * s (q (α g)) : ℂˣ) : ℂ) •
48       ρ (u (q (α g))) (U v)
49   rw [map_smul, hU, packet_normalForm H χ r hkerP u hu ρ hρ (γ (u (q g)))]
50   simp only [LinearMap.smul_apply, smul_smul]
51   change (((sectionScalar D θ q hker t ht g * s (q g) : ℂˣ) : ℂ) *
52     (actualPhase H χ r hkerP u hu γ (q g) : ℂ)) •
53       ρ (u (r (γ (u (q g))))) (U v) = _
54   rw [← Units.val_mul, hcoeff, hr, hu, hq]
55 
56 end Covariance
57 
58 
59 section Existence
60 variable {G P A V : Type*} [Group G] [Group P] [CommGroup A]
61   [AddCommGroup V] [Module ℂ V]
62 
63 /-- The full finite-action interface: actual groups, original characters,
64 exact quotient maps, honest coprime automorphisms and equal labelled commutators
65 construct an irreducible actual action with its original theta and the unchanged
66 packet generator. No scalar cochain or covariance correction is assumed. -/
67 theorem exists_equivariant_actual_action
68     (D : Subgroup G) [D.Normal] (θ : D →* ℂˣ)
69     (hinv : TypeSideDescent.Invariant D θ)
70     (q : G →* A) (hker : q.ker = D)
71     (t : A → G) (ht : ∀ a, q (t a) = a) (ht1 : t 1 = 1)
72     (H : Subgroup P) [H.Normal] (χ : H →* ℂˣ)
73     (hχinv : TypeSideDescent.Invariant H χ)
74     (r : P →* A) (hkerP : r.ker = H)
75     (u : A → P) (hu : ∀ a, r (u a) = a) (hu1 : u 1 = 1)
76     (ρ : Representation ℂ P V) [IsIrreducible ρ]
77     (hρ : ∀ h : H, ρ h = (χ h : ℂ) • LinearMap.id)
78     (α : G ≃* G) (γ : P ≃* P) (β : A ≃* A)
79     (hq : ∀ g, q (α g) = β (q g)) (hr : ∀ p, r (γ p) = β (r p))
80     (hθ : ∀ d : D, θ (subgroupMap D q hker α β hq d) = θ d)
81     (hχ : ∀ h : H, χ (subgroupMap H r hkerP γ β hr h) = χ h)
82     (U : V ≃ₗ[ℂ] V) (hU : ∀ p v, U (ρ p v) = ρ (γ p) (U v))
83     (n m : ℕ) (hα : α ^ n = 1) (hγ : γ ^ n = 1)
84     (hm : ∀ a : A, a ^ m = 1) (hcop : n.Coprime m)
85     (hcomm : ∀ a b,
86       sectionCocycle D θ q hker t ht a b / sectionCocycle D θ q hker t ht b a =
87         sectionCocycle H χ r hkerP u hu a b / sectionCocycle H χ r hkerP u hu b a) :
88     ∃ Ξ : Representation ℂ G V,
89       IsIrreducible Ξ ∧ TypeSideDescent.Contains D θ Ξ ∧
90         (∀ d : D, Ξ d = (θ d : ℂ) • LinearMap.id) ∧
91         (∀ g v, U (Ξ g v) = Ξ (α g) (U v)) := by
92   let c := actualScalarCocycle D θ hinv q hker t ht ht1
93   let d := actualScalarCocycle H χ hχinv r hkerP u hu hu1
94   let L := actualLift D θ hinv q hker t ht ht1 α β hq hθ
95   let M := actualLift H χ hχinv r hkerP u hu hu1 γ β hr hχ
96   have hβ : β ^ n = 1 := quotient_power_eq_one q t ht α β hq n hα
97   have hL : L.action ^ n = 1 :=
98     actualLift_power_eq_one D θ hinv q hker t ht ht1 α β hq hθ n hα
99   have hM : M.action ^ n = 1 :=
100     actualLift_power_eq_one H χ hχinv r hkerP u hu hu1 γ β hr hχ n hγ
101   obtain ⟨s, hs1, hc, hsCov⟩ :=
102     exists_equivariant_cochain c d β L M n m hβ hL hM hm hcop hcomm
103   have hcov : ∀ a, actualPhase D θ q hker t ht α a * s (β a) =
104       s a * actualPhase H χ r hkerP u hu γ a := by
105     intro a
106     simpa only [L, M, actualLift_phase] using hsCov a
107   let Ξ := scalarTransport D θ hinv q hker t ht ht1 H χ r hkerP u hu hu1 ρ hρ s hs1 hc
108   let : Nontrivial V := GeneratedIrreducibility.nontrivial_space ρ
109   refine ⟨Ξ, scalarTransport_irreducible D θ hinv q hker t ht ht1 H χ r hkerP u hu hu1 ρ hρ s hs1 hc,
110     scalarTransport_contains D θ hinv q hker t ht ht1 H χ r hkerP u hu hu1 ρ hρ s hs1 hc,
111     scalarTransport_on_subgroup D θ hinv q hker t ht ht1 H χ r hkerP u hu hu1 ρ hρ s hs1 hc, ?_⟩
112   exact scalarTransport_covariant D θ hinv q hker t ht ht1 H χ r hkerP u hu hu1 ρ hρ
113     α γ β hq hr hθ U hU s hs1 hc hcov
114 
115 end Existence
116 
117 end PaperXI.EquivariantRepresentation113

Back to source controls