FiniteBreakAssembly.lean

1 import PaperXI.BreakBridgeAlong
2 import PaperXI.CentralExtensionComparison
3 import PaperXI.TraceDiscrepancy
4 
5 /-! Construct the initial tensor bridge and close its honest stabilizer action.
6 The central extensions (including dyadic square data), their actual lifts,
7 central characters and actions are inputs. No initial intertwiner, discrepancy
8 character, finite-dimensional certificate, or final comparison is an input. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.FiniteBreakAssembly
12 
13 variable {I Z C : Type*} [Fintype I] [CommGroup Z] [Group C]
14 variable {H A H' A' V W : I → Type*}
15 variable [∀ i, Group (H i)] [∀ i, CommGroup (A i)] [∀ i, Fintype (A i)]
16 variable [∀ i, Group (H' i)] [∀ i, CommGroup (A' i)]
17 variable [∀ i, AddCommGroup (V i)] [∀ i, Module ℂ (V i)]
18 variable [∀ i, AddCommGroup (W i)] [∀ i, Module ℂ (W i)]
19 
20 /-- Concrete break data. A group lift is required, not merely an alternating
21 form isometry in residue characteristic two. -/
22 structure Data where
23   source : ∀ i, CentralExtension.Datum Z (H i) (A i)
24   target : ∀ i, CentralExtension.Datum Z (H' i) (A' i)
25   lift : ∀ i, H i ≃* H' i
26   lift_center : ∀ i z, lift i ((source i).i z) = (target i).i z
27   centralCharacter : Z →* ℂˣ
28   nondegenerate : ∀ i, CocycleCommutator.radical
29     (CentralExtension.scalarCocycle (source i) centralCharacter) = ⊥
30   leftAction : ∀ i, Representation ℂ (H i) (V i)
31   rightAction : ∀ i, Representation ℂ (H' i) (W i)
32   leftIrreducible : ∀ i, Representation.IsIrreducible (leftAction i)
33   rightIrreducible : ∀ i, Representation.IsIrreducible (rightAction i)
34   leftCentral : ∀ i z, leftAction i ((source i).i z) =
35     (centralCharacter z : ℂ) • LinearMap.id
36   rightCentral : ∀ i z, rightAction i ((target i).i z) =
37     (centralCharacter z : ℂ) • LinearMap.id
38 
39 variable (d : Data (I := I) (Z := Z) (H := H) (A := A) (H' := H') (A' := A')
40   (V := V) (W := W))
41 
42 /-- Every factor intertwiner is obtained from actual central-extension uniqueness. -/
43 def factor (i : I) : V i ≃ₗ[ℂ] W i := by
44   letI := d.leftIrreducible i
45   letI := d.rightIrreducible i
46   exact (CentralExtensionComparison.equivAlong (d.source i) d.centralCharacter
47     (d.nondegenerate i) (d.lift i) (d.leftAction i) (d.rightAction i)
48     (d.leftCentral i) (by intro z; rw [d.lift_center]; exact d.rightCentral i z)).toLinearEquiv
49 
50 omit [Fintype I] in
51 @[simp] theorem factor_intertwines (i : I) (h : H i) (x : V i) :
52     factor d i (d.leftAction i h x) = d.rightAction i (d.lift i h) (factor d i x) := by
53   let := d.leftIrreducible i
54   let := d.rightIrreducible i
55   exact CentralExtensionComparison.equivAlong_intertwines (d.source i) d.centralCharacter
56     (d.nondegenerate i) (d.lift i) (d.leftAction i) (d.rightAction i)
57     (d.leftCentral i) (by intro z; rw [d.lift_center]; exact d.rightCentral i z) h x
58 
59 /-- The full break intertwiner is the literal tensor product of the constructed maps. -/
60 def tensorBridge : PiTensorProduct ℂ V ≃ₗ[ℂ] PiTensorProduct ℂ W :=
61   BreakTensorMap.tensor (factor d)
62 
63 def sourceAction : Representation ℂ (CentralProduct.Group d.source) (PiTensorProduct ℂ V) :=
64   HeisenbergTensor.descend d.source d.centralCharacter d.leftAction d.leftCentral
65 
66 /-- The actual target central product is pulled back by the constructed quotient isomorphism. -/
67 def targetAction : Representation ℂ (CentralProduct.Group d.source) (PiTensorProduct ℂ W) :=
68   (HeisenbergTensor.descend d.target d.centralCharacter d.rightAction d.rightCentral).comp
69     (CentralProduct.congr d.source d.target d.lift d.lift_center).toMonoidHom
70 
71 theorem tensor_intertwines (h : CentralProduct.Group d.source) (x : PiTensorProduct ℂ V) :
72     tensorBridge d (sourceAction d h x) = targetAction d h (tensorBridge d x) := by
73   exact BreakBridgeAlong.quotient_intertwines d.source d.target d.lift d.lift_center
74     d.centralCharacter d.leftAction d.rightAction d.leftCentral d.rightCentral
75     (factor d) (factor_intertwines d) h x
76 
77 include d in
78 /-- Finite dimensionality and irreducibility are derived before Schur is used. -/
79 theorem source_finiteDimensional : FiniteDimensional ℂ (PiTensorProduct ℂ V) := by
80   let := d.leftIrreducible
81   exact HeisenbergTensor.finiteDimensional d.source d.centralCharacter d.nondegenerate
82     d.leftAction d.leftCentral
83 
84 theorem source_irreducible : Representation.IsIrreducible (sourceAction d) := by
85   let := d.leftIrreducible
86   exact HeisenbergTensor.irreducible d.source d.centralCharacter d.nondegenerate
87     d.leftAction d.leftCentral
88 
89 variable (α : C →* MulAut (CentralProduct.Group d.source))
90 variable (R : Representation ℂ C (PiTensorProduct ℂ V))
91 variable (T : Representation ℂ C (PiTensorProduct ℂ W))
92 variable (hR : ∀ g h x, R g (sourceAction d h x) = sourceAction d (α g h) (R g x))
93 variable (hT : ∀ g h x, T g (targetAction d h x) = targetAction d (α g h) (T g x))
94 
95 /-- The actual total discrepancy character, chosen only from the proved Schur law. -/
96 def discrepancy : C →* ℂˣ := by
97   letI := source_finiteDimensional d
98   letI := source_irreducible d
99   exact Classical.choose (DiscrepancyCharacter.exists_character (sourceAction d)
100     (targetAction d) (tensorBridge d) (tensor_intertwines d) α R T hR hT)
101 
102 theorem discrepancy_law (g : C) (x : PiTensorProduct ℂ V) :
103     tensorBridge d (R g x) = (discrepancy d α R T hR hT g : ℂ) • T g (tensorBridge d x) := by
104   let := source_finiteDimensional d
105   let := source_irreducible d
106   exact Classical.choose_spec (DiscrepancyCharacter.exists_character (sourceAction d)
107     (targetAction d) (tensorBridge d) (tensor_intertwines d) α R T hR hT) g x
108 
109 /-- Arbitrary generating-set phase closure. No nonzero-trace restriction is needed
110 when the actual discrepancy values themselves are supplied and checked. -/
111 def equivOfPhase (S : Set C) (hgen : Subgroup.closure S = ⊤)
112     (hp : ∀ g ∈ S, discrepancy d α R T hR hT g = 1) :
113     Representation.Equiv
114       (CyclicBridge.semidirectRepresentation α (sourceAction d) R hR)
115       (CyclicBridge.semidirectRepresentation α (targetAction d) T hT) := by
116   refine Representation.Equiv.mk (tensorBridge d) ?_
117   have hc : ∀ g x, tensorBridge d (R g x) = T g (tensorBridge d x) := by
118     intro g x
119     simpa only [CharacterGenerators.trivial _ S hgen hp g, Units.val_one, one_smul]
120       using discrepancy_law d α R T hR hT g x
121   intro a
122   apply LinearMap.ext
123   intro x
124   exact CyclicBridge.semidirect_intertwining α
125     (CyclicBridge.semidirectRepresentation α (sourceAction d) R hR)
126     (CyclicBridge.semidirectRepresentation α (targetAction d) T hT) (tensorBridge d)
127     (by simpa only [CyclicBridge.semidirectRepresentation_inl] using tensor_intertwines d)
128     (by simpa only [CyclicBridge.semidirectRepresentation_inr] using hc) a x
129 
130 /-- The discrepancy is derived from honest lift covariance on the irreducible
131 central product. Its triviality is a test, not an assumed initial bridge. -/
132 theorem discrepancy_and_closure (S : Set C) (hgen : Subgroup.closure S = ⊤) :
133     ∃ δ : C →* ℂˣ,
134       (∀ g x, tensorBridge d (R g x) = (δ g : ℂ) • T g (tensorBridge d x)) ∧
135       ((∀ g ∈ S, δ g = 1) →
136         Nonempty (Representation.Equiv
137           (CyclicBridge.semidirectRepresentation α (sourceAction d) R hR)
138           (CyclicBridge.semidirectRepresentation α (targetAction d) T hT))) := by
139   let := source_finiteDimensional d
140   let := source_irreducible d
141   obtain ⟨δ, hd, hc⟩ := CharacterGenerators.bridge_from_actions
142     (sourceAction d) (targetAction d) (tensorBridge d) (tensor_intertwines d) α R T hR hT S hgen
143   refine ⟨δ, hd, fun hp => ⟨Representation.Equiv.mk (tensorBridge d) ?_⟩⟩
144   intro g
145   apply LinearMap.ext
146   intro x
147   exact hc hp g x
148 
149 /-- A useful directly observable phase contract: matched nonzero total traces
150 on generators close the bridge. Zero traces are deliberately not cancellable. -/
151 def equivOfTraces (S : Set C) (hgen : Subgroup.closure S = ⊤)
152     (ht : ∀ g ∈ S, LinearMap.trace ℂ (PiTensorProduct ℂ V) (R g) =
153       LinearMap.trace ℂ (PiTensorProduct ℂ W) (T g))
154     (hn : ∀ g ∈ S, LinearMap.trace ℂ (PiTensorProduct ℂ W) (T g) ≠ 0) :
155     Representation.Equiv
156       (CyclicBridge.semidirectRepresentation α (sourceAction d) R hR)
157       (CyclicBridge.semidirectRepresentation α (targetAction d) T hT) := by
158   letI := source_finiteDimensional d
159   letI := source_irreducible d
160   refine Representation.Equiv.mk (tensorBridge d) ?_
161   intro g
162   apply LinearMap.ext
163   intro x
164   exact TraceDiscrepancy.bridge_from_traces
165     (sourceAction d) (targetAction d) (tensorBridge d) (tensor_intertwines d)
166     α R T hR hT S hgen ht hn g x
167 
168 /-- The observable phase route does not change the underlying tensor map. -/
169 theorem equivOfTraces_map (S : Set C) (hgen : Subgroup.closure S = ⊤)
170     (ht : ∀ g ∈ S, LinearMap.trace ℂ (PiTensorProduct ℂ V) (R g) =
171       LinearMap.trace ℂ (PiTensorProduct ℂ W) (T g))
172     (hn : ∀ g ∈ S, LinearMap.trace ℂ (PiTensorProduct ℂ W) (T g) ≠ 0) :
173     (equivOfTraces d α R T hR hT S hgen ht hn).toLinearEquiv = tensorBridge d := rfl
174 
175 end PaperXI.FiniteBreakAssembly

Back to source controls