CliffordHeisenbergAttachment.lean

1 import PaperXI.OddEnvelopeHeisenberg
2 import PaperXI.DyadicHeisenbergLift
3 import PaperXI.CliffordEnvelope
4 
5 /-! Source-facing Corollary 9.9. The form comes from the actual Clifford
6 multiplicity cocycle. Odd characteristic uses its intrinsic half-form group;
7 characteristic two retains a declared quadratic refinement and constructs a
8 bilinear lift. No irreducible Heisenberg representation is supplied as input. -/
9 set_option autoImplicit false
10 set_option maxHeartbeats 800000
11 set_option maxRecDepth 3000
12 noncomputable section
13 namespace PaperXI.CliffordHeisenbergAttachment
14 open scoped IsMulCommutative
15 open BilinearHeisenberg
16 
17 variable {G W X : Type*} [Group G] [Finite G]
18 variable [AddCommGroup W] [Module ℂ W] [AddCommGroup X] [Module ℂ X]
19 variable (N : Subgroup G) [N.Normal] [IsMulCommutative (G ⧸ N)]
20 variable (ρ : Representation ℂ N W) (π : Representation ℂ G X)
21 variable [Representation.IsIrreducible ρ] [Representation.IsIrreducible π]
22 variable (hIso : CliffordIrreducible.Isotypic N ρ π) (hρ : CliffordDatum.Invariant N ρ)
23 
24 section Odd
25 variable {p : ℕ} [Fact p.Prime] [Fact (∀ a : G ⧸ N, a ^ p = 1)]
26 
27 def oddFactor : LinearMap.BilinForm (ZMod p) (CliffordEnvelope.Space N ρ π hIso hρ) :=
28   OddEnvelopeHeisenberg.factor (CliffordEnvelope.form (p := p) N ρ π hIso hρ)
29 
30 /-- The actual extension commutator recovers the actual Clifford commutator
31 on the original quotient representatives with the source's character convention. -/
32 theorem odd_commutator_on_classes (hp : p ≠ 2) (a b : G ⧸ N) :
33     ZMod.stdAddChar ((CentralExtension.centralCommutator
34       (datum (oddFactor (p := p) N ρ π hIso hρ))
35       ⟨Additive.ofMul (QuotientGroup.mk a), 0⟩
36       ⟨Additive.ofMul (QuotientGroup.mk b), 0⟩).toAdd) =
37     ((CocycleCommutator.commutator (CliffordSource.cocycle N ρ π hIso hρ) a b : ℂˣ) : ℂ) := by
38   rw [BilinearHeisenberg.centralCommutator]
39   exact (congrArg (fun t : ZMod p => ZMod.stdAddChar t)
40     (OddEnvelopeHeisenberg.factor_commutator
41       (CliffordEnvelope.form (p := p) N ρ π hIso hρ)
42       (CliffordEnvelope.form_isAlt N ρ π hIso hρ)
43       (HeisenbergPrime.two_ne_zero hp)
44       (Additive.ofMul (QuotientGroup.mk a))
45       (Additive.ofMul (QuotientGroup.mk b)))).trans
46     (CliffordEnvelope.form_on_classes N ρ π hIso hρ a b)
47 
48 /-- Odd source 9.9: the group and an irreducible representation are constructed
49 from the intrinsic one-break envelope and the declared nontrivial central character. -/
50 theorem odd_exists (hp : p ≠ 2) (ψ : AddChar (ZMod p) ℂ) (hψ : ψ ≠ 1) :
51     let c := oddFactor (p := p) N ρ π hIso hρ
52     let B : Type _ := CentralCharacter.Algebra (datum c)
53       (SymplecticCentralExtension.scalarCharacter ψ)
54     letI : Ring B := inferInstance
55     letI : Algebra ℂ B := inferInstance
56     ∃ I : Ideal B, ∃ σ : Representation ℂ (Element c) I,
57       Representation.IsIrreducible σ ∧
58       (∀ t : ZMod p, σ (i c (Multiplicative.ofAdd t)) = ψ t •
59         (LinearMap.id : Module.End ℂ I)) ∧
60       Module.finrank ℂ I = Nat.sqrt (Nat.card (CliffordEnvelope.Space N ρ π hIso hρ)) := by
61   let : Fintype (CliffordEnvelope.Space N ρ π hIso hρ) := Fintype.ofFinite _
62   simpa only [Nat.card_eq_fintype_card] using
63     BilinearHeisenberg.exists_irreducible (oddFactor (p := p) N ρ π hIso hρ)
64       (CliffordEnvelope.form (p := p) N ρ π hIso hρ)
65       (OddEnvelopeHeisenberg.factor_commutator _ (CliffordEnvelope.form_isAlt N ρ π hIso hρ)
66         (HeisenbergPrime.two_ne_zero hp))
67       (CliffordEnvelope.form_nondegenerate (p := p) N ρ π hIso hρ).1 ψ hψ
68 
69 variable {U U' : Type*} [AddCommGroup U] [Module ℂ U] [AddCommGroup U'] [Module ℂ U']
70 
71 /-- The first comparison equivalence is a conclusion, on the constructed odd group. -/
72 theorem odd_unique (hp : p ≠ 2) (ψ : AddChar (ZMod p) ℂ) (hψ : ψ ≠ 1)
73     (σ : Representation ℂ (Element (oddFactor (p := p) N ρ π hIso hρ)) U)
74     (τ : Representation ℂ (Element (oddFactor (p := p) N ρ π hIso hρ)) U')
75     [Representation.IsIrreducible σ] [Representation.IsIrreducible τ]
76     (hσ : ∀ t, σ (i _ (Multiplicative.ofAdd t)) = ψ t • LinearMap.id)
77     (hτ : ∀ t, τ (i _ (Multiplicative.ofAdd t)) = ψ t • LinearMap.id) :
78     Nonempty (Representation.Equiv σ τ) := by
79   let : Fintype (CliffordEnvelope.Space N ρ π hIso hρ) := Fintype.ofFinite _
80   exact BilinearHeisenberg.exists_equiv (oddFactor (p := p) N ρ π hIso hρ)
81     (CliffordEnvelope.form (p := p) N ρ π hIso hρ)
82     (OddEnvelopeHeisenberg.factor_commutator _ (CliffordEnvelope.form_isAlt N ρ π hIso hρ)
83       (HeisenbergPrime.two_ne_zero hp))
84     (CliffordEnvelope.form_nondegenerate (p := p) N ρ π hIso hρ).1 ψ hψ σ τ hσ hτ
85 
86 end Odd
87 
88 section Dyadic
89 variable [Fact (∀ a : G ⧸ N, a ^ (2 : ℕ) = 1)]
90 
91 def dyadicFactor (Q : DyadicAffine.Refinement (CliffordEnvelope.form (p := 2) N ρ π hIso hρ)) :
92     LinearMap.BilinForm (ZMod 2) (CliffordEnvelope.Space N ρ π hIso hρ) :=
93   DyadicHeisenbergLift.factor (CliffordEnvelope.form (p := 2) N ρ π hIso hρ)
94     (CliffordEnvelope.form_isAlt N ρ π hIso hρ)
95     (CliffordEnvelope.form_nondegenerate (p := 2) N ρ π hIso hρ).1 Q
96 
97 /-- The declared refinement is exactly the square of each quotient lift. -/
98 theorem dyadic_square (Q : DyadicAffine.Refinement
99     (CliffordEnvelope.form (p := 2) N ρ π hIso hρ))
100     (h : Element (dyadicFactor N ρ π hIso hρ Q)) :
101     h * h = i (dyadicFactor N ρ π hIso hρ Q) (Multiplicative.ofAdd (Q.value h.vector)) :=
102   DyadicHeisenbergLift.square_profile _ _ _ Q h
103 
104 /-- Dyadic source 9.9 at its corrected contract: the square-refined group and
105 its irreducible representation are constructed, not assumed. -/
106 theorem dyadic_exists (Q : DyadicAffine.Refinement
107     (CliffordEnvelope.form (p := 2) N ρ π hIso hρ))
108     (ψ : AddChar (ZMod 2) ℂ) (hψ : ψ ≠ 1) :
109     let c := dyadicFactor N ρ π hIso hρ Q
110     let B : Type _ := CentralCharacter.Algebra (datum c)
111       (SymplecticCentralExtension.scalarCharacter ψ)
112     letI : Ring B := inferInstance
113     letI : Algebra ℂ B := inferInstance
114     ∃ I : Ideal B, ∃ σ : Representation ℂ (Element c) I,
115       Representation.IsIrreducible σ ∧
116       (∀ t : ZMod 2, σ (i c (Multiplicative.ofAdd t)) = ψ t •
117         (LinearMap.id : Module.End ℂ I)) ∧
118       Module.finrank ℂ I = Nat.sqrt (Nat.card (CliffordEnvelope.Space N ρ π hIso hρ)) := by
119   let : Fintype (CliffordEnvelope.Space N ρ π hIso hρ) := Fintype.ofFinite _
120   simpa only [Nat.card_eq_fintype_card] using
121     BilinearHeisenberg.exists_irreducible (dyadicFactor N ρ π hIso hρ Q)
122       (CliffordEnvelope.form (p := 2) N ρ π hIso hρ)
123       (DyadicHeisenbergLift.factor_commutator _ _ _ Q)
124       (CliffordEnvelope.form_nondegenerate (p := 2) N ρ π hIso hρ).1 ψ hψ
125 
126 variable {U U' : Type*} [AddCommGroup U] [Module ℂ U] [AddCommGroup U'] [Module ℂ U']
127 
128 theorem dyadic_unique (Q : DyadicAffine.Refinement
129     (CliffordEnvelope.form (p := 2) N ρ π hIso hρ))
130     (ψ : AddChar (ZMod 2) ℂ) (hψ : ψ ≠ 1)
131     (σ : Representation ℂ (Element (dyadicFactor N ρ π hIso hρ Q)) U)
132     (τ : Representation ℂ (Element (dyadicFactor N ρ π hIso hρ Q)) U')
133     [Representation.IsIrreducible σ] [Representation.IsIrreducible τ]
134     (hσ : ∀ t, σ (i _ (Multiplicative.ofAdd t)) = ψ t • LinearMap.id)
135     (hτ : ∀ t, τ (i _ (Multiplicative.ofAdd t)) = ψ t • LinearMap.id) :
136     Nonempty (Representation.Equiv σ τ) := by
137   let : Fintype (CliffordEnvelope.Space N ρ π hIso hρ) := Fintype.ofFinite _
138   exact BilinearHeisenberg.exists_equiv (dyadicFactor N ρ π hIso hρ Q)
139     (CliffordEnvelope.form (p := 2) N ρ π hIso hρ)
140     (DyadicHeisenbergLift.factor_commutator _ _ _ Q)
141     (CliffordEnvelope.form_nondegenerate (p := 2) N ρ π hIso hρ).1 ψ hψ σ τ hσ hτ
142 
143 end Dyadic
144 end PaperXI.CliffordHeisenbergAttachment

Back to source controls