CliffordEnvelope.lean

1 import PaperXI.CliffordSource
2 import PaperXI.CliffordTransport
3 import PaperXI.ElementaryEnvelopeTransport
4 
5 /-! The actual elementary commutator envelope of the source Clifford datum.
6 No cocycle, projective operator family, bilinear form or transport on the
7 multiplicity space is supplied in place of its construction. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.CliffordEnvelope
11 open CocycleCommutator
12 open scoped IsMulCommutative
13 
14 variable {G W X : Type*} [Group G] [Finite G]
15 variable [AddCommGroup W] [Module ℂ W] [AddCommGroup X] [Module ℂ X]
16 variable (N : Subgroup G) [N.Normal] [IsMulCommutative (G ⧸ N)]
17 variable (ρ : Representation ℂ N W) (π : Representation ℂ G X)
18 variable [Representation.IsIrreducible ρ] [Representation.IsIrreducible π]
19 variable (hIso : CliffordIrreducible.Isotypic N ρ π) (hρ : CliffordDatum.Invariant N ρ)
20 variable {p : ℕ} [Fact (∀ a : G ⧸ N, a ^ p = 1)]
21 
22 /-- The actual scalar commutator, bundled in the pth roots of unity. -/
23 def pairing : (G ⧸ N) →* ((G ⧸ N) →* rootsOfUnity p ℂ) :=
24   ElementaryEnvelope.rootCommutator (CliffordSource.cocycle N ρ π hIso hρ) Fact.out
25 
26 @[simp] theorem pairing_coe (a b : G ⧸ N) :
27     (pairing (p := p) N ρ π hIso hρ a b : ℂˣ) =
28       (CliffordSource.cocycle N ρ π hIso hρ).coeff a b /
29         (CliffordSource.cocycle N ρ π hIso hρ).coeff b a := rfl
30 
31 theorem pairing_self (a : G ⧸ N) : pairing (p := p) N ρ π hIso hρ a a = 1 :=
32   ElementaryEnvelope.rootCommutator_self _ _ a
33 
34 /-- The original Clifford datum's actual additive radical quotient. -/
35 abbrev Space := ElementaryEnvelope.Space (CliffordSource.cocycle N ρ π hIso hρ)
36 
37 variable [Fact p.Prime]
38 
39 /-- The form is constructed by the fixed standard additive character. -/
40 def form : LinearMap.BilinForm (ZMod p) (Space N ρ π hIso hρ) :=
41   ElementaryEnvelope.form (CliffordSource.cocycle N ρ π hIso hρ)
42 
43 theorem form_isAlt : (form (p := p) N ρ π hIso hρ).IsAlt :=
44   ElementaryEnvelope.form_isAlt _
45 
46 theorem form_nondegenerate : (form (p := p) N ρ π hIso hρ).Nondegenerate :=
47   ElementaryEnvelope.form_nondegenerate _
48 
49 theorem finiteDimensional : FiniteDimensional (ZMod p) (Space N ρ π hIso hρ) :=
50   inferInstance
51 
52 /-- The constructed prime-field form recovers the actual multiplicity commutator
53 on every pair of original quotient representatives. -/
54 theorem form_on_classes (a b : G ⧸ N) :
55     ZMod.stdAddChar (form (p := p) N ρ π hIso hρ
56       (Additive.ofMul (QuotientGroup.mk a)) (Additive.ofMul (QuotientGroup.mk b))) =
57       ((CocycleCommutator.commutator (CliffordSource.cocycle N ρ π hIso hρ) a b : ℂˣ) : ℂ) :=
58   ElementaryEnvelope.form_stdAddChar _ _ _
59 
60 section Transport
61 variable {G' W' X' : Type*} [Group G'] [Finite G']
62 variable [AddCommGroup W'] [Module ℂ W'] [AddCommGroup X'] [Module ℂ X']
63 variable (N' : Subgroup G') [N'.Normal] [IsMulCommutative (G' ⧸ N')]
64 variable (ρ' : Representation ℂ N' W') (π' : Representation ℂ G' X')
65 variable [Representation.IsIrreducible ρ'] [Representation.IsIrreducible π']
66 variable (hIso' : CliffordIrreducible.Isotypic N' ρ' π') (hρ' : CliffordDatum.Invariant N' ρ')
67 variable [Fact (∀ a : G' ⧸ N', a ^ p = 1)]
68 variable (e : G ≃* G') (hN : N.map e.toMonoidHom = N')
69 variable (E : Representation.Equiv ρ
70   (ρ'.comp (CliffordTransport.subgroupEquiv N N' e hN).toMonoidHom))
71 variable (F : Representation.Equiv π (π'.comp e.toMonoidHom))
72 
73 include E F
74 
75 /-- Actual isomorphisms of the original subgroup and ambient representations
76 preserve the intrinsic scalar pairing. -/
77 theorem commutator_preserved (a b : G ⧸ N) :
78     commutator (CliffordSource.cocycle N' ρ' π' hIso' hρ')
79       (CliffordTransport.quotientEquiv N N' e hN a)
80       (CliffordTransport.quotientEquiv N N' e hN b) =
81       commutator (CliffordSource.cocycle N ρ π hIso hρ) a b := by
82   let : FiniteDimensional ℂ W := FiniteRepresentation.finiteDimensional ρ
83   let : FiniteDimensional ℂ W' := FiniteRepresentation.finiteDimensional ρ'
84   let : Nontrivial (CliffordMultiplicity.Space N ρ π) :=
85     CliffordIrreducible.multiplicity_nontrivial N ρ π hIso
86   let : Nontrivial (CliffordMultiplicity.Space N' ρ' π') :=
87     CliffordIrreducible.multiplicity_nontrivial N' ρ' π' hIso'
88   exact CliffordTransport.commutator_preserved N N' e hN ρ ρ' π π' E F hρ hρ' a b
89 
90 /-- The actual datum isomorphism also preserves the cocycle class, witnessed
91 by a constructed normalized scalar cochain on the actual quotient. -/
92 theorem exists_normalized_cochain :
93     ∃ s : (G ⧸ N) → ℂˣ, s 1 = 1 ∧ ∀ a b : G ⧸ N,
94       (CliffordSource.cocycle N' ρ' π' hIso' hρ').coeff
95         (CliffordTransport.quotientEquiv N N' e hN a)
96         (CliffordTransport.quotientEquiv N N' e hN b) =
97       s a * s b / s (a * b) * (CliffordSource.cocycle N ρ π hIso hρ).coeff a b := by
98   let : FiniteDimensional ℂ W := FiniteRepresentation.finiteDimensional ρ
99   let : FiniteDimensional ℂ W' := FiniteRepresentation.finiteDimensional ρ'
100   let : Nontrivial (CliffordMultiplicity.Space N ρ π) :=
101     CliffordIrreducible.multiplicity_nontrivial N ρ π hIso
102   let : Nontrivial (CliffordMultiplicity.Space N' ρ' π') :=
103     CliffordIrreducible.multiplicity_nontrivial N' ρ' π' hIso'
104   exact ⟨CliffordTransport.cochain N N' e hN ρ ρ' E hρ hρ',
105     CliffordTransport.cochain_one N N' e hN ρ ρ' π π' E F hρ hρ',
106     CliffordTransport.cocycle_transport N N' e hN ρ ρ' π π' E F hρ hρ'⟩
107 
108 omit [Fact p.Prime] in
109 /-- The target μp-valued bicharacter is the transport of the source one. -/
110 theorem pairing_preserved (a b : G ⧸ N) :
111     pairing (p := p) N' ρ' π' hIso' hρ'
112       (CliffordTransport.quotientEquiv N N' e hN a)
113       (CliffordTransport.quotientEquiv N N' e hN b) =
114       pairing (p := p) N ρ π hIso hρ a b :=
115   Subtype.ext (commutator_preserved N ρ π hIso hρ N' ρ' π' hIso' hρ' e hN E F a b)
116 
117 /-- The actual datum map induces the prime-field equivalence of its constructed envelopes. -/
118 def equiv : Space N ρ π hIso hρ ≃ₗ[ZMod p] Space N' ρ' π' hIso' hρ' :=
119   ElementaryEnvelope.linearEquiv
120     (CliffordSource.cocycle N ρ π hIso hρ) (CliffordSource.cocycle N' ρ' π' hIso' hρ')
121     (CliffordTransport.quotientEquiv N N' e hN)
122     (commutator_preserved N ρ π hIso hρ N' ρ' π' hIso' hρ' e hN E F)
123 
124 @[simp] theorem equiv_mk (a : G) :
125     equiv (p := p) N ρ π hIso hρ N' ρ' π' hIso' hρ' e hN E F
126       (Additive.ofMul (QuotientGroup.mk (QuotientGroup.mk' N a))) =
127       Additive.ofMul (QuotientGroup.mk (QuotientGroup.mk' N' (e a))) := rfl
128 
129 /-- Source 9.7: the map induced by an isomorphism of the actual Clifford data
130 is an isometry for the same standard root-coordinate convention. -/
131 theorem equiv_form (x y : Space N ρ π hIso hρ) :
132     form (p := p) N' ρ' π' hIso' hρ'
133       (equiv (p := p) N ρ π hIso hρ N' ρ' π' hIso' hρ' e hN E F x)
134       (equiv (p := p) N ρ π hIso hρ N' ρ' π' hIso' hρ' e hN E F y) =
135       form (p := p) N ρ π hIso hρ x y :=
136   ElementaryEnvelope.linearEquiv_form _ _ _ _ x y
137 
138 /-- Auxiliary representation equivalences do not change the induced quotient map. -/
139 theorem equiv_independent
140     (E' : Representation.Equiv ρ
141       (ρ'.comp (CliffordTransport.subgroupEquiv N N' e hN).toMonoidHom))
142     (F' : Representation.Equiv π (π'.comp e.toMonoidHom)) :
143     equiv (p := p) N ρ π hIso hρ N' ρ' π' hIso' hρ' e hN E F =
144       equiv (p := p) N ρ π hIso hρ N' ρ' π' hIso' hρ' e hN E' F' := rfl
145 
146 end Transport
147 end PaperXI.CliffordEnvelope

Back to source controls