source.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiPaperIII.Transport
7 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
8 
9 /-!
10 # Reversible connections, gauge covariance, and finite holonomy blocks
11 
12 This module strengthens the minimal homogeneous connection in `Transport` to
13 a family of possibly heterogeneous fibres.  Pair transport is normalized and
14 reverses by inversion, but no cocycle law is included in the structure.
15 
16 All paths and packet resolutions in this file are finite.  The gauge results
17 are purely algebraic conjugation identities; no topology or smooth structure
18 is assumed.
19 -/
20 
21 set_option autoImplicit false
22 
23 namespace Komorebi.PaperIII.Transport
24 
25 open scoped BigOperators
26 
27 universe u v w z
28 
29 /--
30 A normalized reversible pair connection on a family of linear fibres.
31 
32 `transport a b` maps the fibre at `a` to the fibre at `b`.  Normalization and
33 reverse-edge inversion are data, while the cocycle law is deliberately not.
34 -/
35 structure ReversibleConnection
36     (R : Type u) (X : Type v) (F : X → Type w)
37     [CommRing R] [∀ a, AddCommGroup (F a)] [∀ a, Module R (F a)] where
38   transport : ∀ a b, F a ≃ₗ[R] F b
39   transport_self : ∀ a, transport a a = LinearEquiv.refl R (F a)
40   transport_reverse : ∀ a b, transport b a = (transport a b).symm
41 
42 namespace ReversibleConnection
43 
44 variable {R : Type u} {X : Type v} {F : X → Type w}
45 variable [CommRing R] [∀ a, AddCommGroup (F a)] [∀ a, Module R (F a)]
46 variable (C : ReversibleConnection R X F)
47 
48 /-- A gauge is a fibrewise family of linear automorphisms. -/
49 abbrev Gauge := ∀ a, F a ≃ₗ[R] F a
50 
51 /-- The exact pair-cocycle condition at one ordered triple. -/
52 def CocycleAt (a b c : X) : Prop :=
53   (C.transport a b).trans (C.transport b c) = C.transport a c
54 
55 /-- Algebraic flatness is the pair-cocycle condition at every triple. -/
56 def Flat : Prop := ∀ a b c, C.CocycleAt a b c
57 
58 /--
59 The additive cocycle defect from the fibre at `a` to the fibre at `c`.
60 The indices are written in traversal order `a → b → c`.
61 -/
62 def cocycleDefect (a b c : X) : F a →ₗ[R] F c :=
63   (C.transport b c).toLinearMap.comp (C.transport a b).toLinearMap -
64     (C.transport a c).toLinearMap
65 
66 /-- Triangle holonomy based at `a`, traversing `a → b → c → a`. -/
67 def triangleHolonomy (a b c : X) : F a ≃ₗ[R] F a :=
68   ((C.transport a b).trans (C.transport b c)).trans (C.transport c a)
69 
70 /-- The additive triangle obstruction `H - id` on the base fibre. -/
71 def triangleObstruction (a b c : X) : F a →ₗ[R] F a :=
72   (C.triangleHolonomy a b c).toLinearMap - LinearMap.id
73 
74 /-- Vanishing additive defect is exactly the cocycle equation at a triple. -/
75 theorem cocycleDefect_eq_zero_iff_cocycleAt (a b c : X) :
76     C.cocycleDefect a b c = 0 ↔ C.CocycleAt a b c := by
77   constructor
78   · intro h
79     apply LinearEquiv.ext
80     intro x
81     have hx := congrArg (fun L : F a →ₗ[R] F c ↦ L x) h
82     change C.transport b c (C.transport a b x) = C.transport a c x
83     change C.transport b c (C.transport a b x) - C.transport a c x = 0 at hx
84     exact sub_eq_zero.mp hx
85   · intro h
86     ext x
87     have hx := congrArg (fun e : F a ≃ₗ[R] F c ↦ e x) h
88     change C.transport b c (C.transport a b x) - C.transport a c x = 0
89     rw [sub_eq_zero]
90     simpa [CocycleAt] using hx
91 
92 /--
93 Defect--holonomy identity:
94 `H - id = transport(c,a) ∘ Δ`.
95 -/
96 theorem triangleHolonomy_sub_id (a b c : X) :
97     C.triangleObstruction a b c =
98       (C.transport c a).toLinearMap.comp (C.cocycleDefect a b c) := by
99   ext x
100   simp only [triangleObstruction, triangleHolonomy, cocycleDefect,
101     LinearMap.sub_apply, LinearMap.id_apply, LinearMap.comp_apply,
102     LinearEquiv.coe_toLinearMap, LinearEquiv.trans_apply, map_sub]
103   rw [C.transport_reverse a c]
104   simp
105 
106 /-- The triangle obstruction vanishes exactly when the additive defect does. -/
107 theorem triangleObstruction_eq_zero_iff_cocycleDefect_eq_zero (a b c : X) :
108     C.triangleObstruction a b c = 0 ↔ C.cocycleDefect a b c = 0 := by
109   rw [C.triangleHolonomy_sub_id a b c]
110   constructor
111   · intro h
112     ext x
113     apply (C.transport c a).injective
114     have hx := congrArg (fun L : F a →ₗ[R] F a ↦ L x) h
115     simpa using hx
116   · intro h
117     simp [h]
118 
119 /-- `H - id` vanishes exactly when the triangle holonomy is the identity. -/
120 theorem triangleObstruction_eq_zero_iff_triangleHolonomy_eq_refl (a b c : X) :
121     C.triangleObstruction a b c = 0 ↔
122       C.triangleHolonomy a b c = LinearEquiv.refl R (F a) := by
123   constructor
124   · intro h
125     apply LinearEquiv.ext
126     intro x
127     have hx := congrArg (fun L : F a →ₗ[R] F a ↦ L x) h
128     change C.triangleHolonomy a b c x = x
129     change C.triangleHolonomy a b c x - x = 0 at hx
130     exact sub_eq_zero.mp hx
131   · intro h
132     ext x
133     have hx := congrArg (fun e : F a ≃ₗ[R] F a ↦ e x) h
134     change C.triangleHolonomy a b c x - x = 0
135     rw [sub_eq_zero]
136     simpa using hx
137 
138 /-- Additive flatness at a triple is equivalent to identity holonomy. -/
139 theorem cocycleDefect_eq_zero_iff_triangleHolonomy_eq_refl (a b c : X) :
140     C.cocycleDefect a b c = 0 ↔
141       C.triangleHolonomy a b c = LinearEquiv.refl R (F a) := by
142   rw [← C.triangleObstruction_eq_zero_iff_cocycleDefect_eq_zero a b c,
143     C.triangleObstruction_eq_zero_iff_triangleHolonomy_eq_refl]
144 
145 /-- Flatness is equivalent to identity holonomy on every ordered triangle. -/
146 theorem flat_iff_triangleHolonomy_eq_refl :
147     C.Flat ↔ ∀ a b c,
148       C.triangleHolonomy a b c = LinearEquiv.refl R (F a) := by
149   constructor
150   · intro hflat a b c
151     rw [← C.cocycleDefect_eq_zero_iff_triangleHolonomy_eq_refl a b c,
152       C.cocycleDefect_eq_zero_iff_cocycleAt]
153     exact hflat a b c
154   · intro hhol a b c
155     rw [← C.cocycleDefect_eq_zero_iff_cocycleAt,
156       C.cocycleDefect_eq_zero_iff_triangleHolonomy_eq_refl]
157     exact hhol a b c
158 
159 /-! ## Canonical reversible transport from a family of frames -/
160 
161 variable {M : Type z} [AddCommGroup M] [Module R M]
162 
163 /-- Canonical transport from fibre `a` to fibre `b` through the ambient frame. -/
164 def canonicalTransport (frame : ∀ a, F a ≃ₗ[R] M) (a b : X) :
165     F a ≃ₗ[R] F b :=
166   (frame a).trans (frame b).symm
167 
168 /--
169 The canonical reversible connection induced by fibre-to-ambient frames.
170 -/
171 def canonicalConnection (frame : ∀ a, F a ≃ₗ[R] M) :
172     ReversibleConnection R X F where
173   transport := canonicalTransport frame
174   transport_self a := by
175     apply LinearEquiv.ext
176     intro x
177     simp [canonicalTransport]
178   transport_reverse _ _ := rfl
179 
180 /-- Canonical frame transport satisfies the pair-cocycle law. -/
181 theorem canonicalConnection_flat (frame : ∀ a, F a ≃ₗ[R] M) :
182     (canonicalConnection frame).Flat := by
183   intro a b c
184   apply LinearEquiv.ext
185   intro x
186   simp [canonicalConnection, canonicalTransport]
187 
188 /-- Canonical frame transport has zero additive connection defect. -/
189 theorem canonicalTransport_zero_connectionDefect
190     (frame : ∀ a, F a ≃ₗ[R] M) (a b c : X) :
191     (canonicalConnection frame).cocycleDefect a b c = 0 := by
192   rw [cocycleDefect_eq_zero_iff_cocycleAt]
193   exact canonicalConnection_flat frame a b c
194 
195 /-- Canonical frame transport has identity triangle holonomy. -/
196 theorem canonicalTransport_triangleHolonomy_eq_refl
197     (frame : ∀ a, F a ≃ₗ[R] M) (a b c : X) :
198     (canonicalConnection frame).triangleHolonomy a b c =
199       LinearEquiv.refl R (F a) := by
200   rw [← cocycleDefect_eq_zero_iff_triangleHolonomy_eq_refl]
201   exact canonicalTransport_zero_connectionDefect frame a b c
202 
203 /--
204 The fibrewise gauge comparing a flat connection with canonical transport,
205 based at a chosen vertex `o`.
206 -/
207 def flatGauge (frame : ∀ a, F a ≃ₗ[R] M) (o : X) :
208     Gauge (R := R) (F := F) :=
209   fun a ↦ (canonicalTransport frame a o).trans (C.transport o a)
210 
211 /--
212 Every flat normalized reversible pair connection is a gauge transform of the
213 canonical connection induced by any family of ambient frames.
214 -/
215 theorem flat_isGaugeOfCanonical
216     (hflat : C.Flat) (frame : ∀ a, F a ≃ₗ[R] M) (o a b : X) :
217     C.transport a b =
218       ((C.flatGauge frame o a).symm.trans
219         ((canonicalConnection frame).transport a b)).trans
220           (C.flatGauge frame o b) := by
221   apply LinearEquiv.ext
222   intro x
223   have hg : (C.flatGauge frame o a).symm =
224       (C.transport o a).symm.trans (canonicalTransport frame a o).symm := rfl
225   rw [hg]
226   have hcanonical_symm (p q : X) :
227       (canonicalTransport frame p q).symm = canonicalTransport frame q p := rfl
228   rw [hcanonical_symm]
229   simp only [flatGauge, canonicalConnection, LinearEquiv.trans_apply]
230   rw [show (C.transport o a).symm = C.transport a o by
231     rw [C.transport_reverse o a]]
232   simp only [canonicalTransport, LinearEquiv.trans_apply,
233     LinearEquiv.symm_apply_apply, LinearEquiv.apply_symm_apply]
234   have hao : (C.transport a o).trans (C.transport o b) = C.transport a b :=
235     hflat a o b
236   exact (congrArg (fun e : F a ≃ₗ[R] F b ↦ e x) hao).symm
237 
238 /-! ## Finite path transport -/
239 
240 /-- Transport along a finite list of successive vertices. -/
241 def pathTransport (C : ReversibleConnection R X F) (start : X) :
242     (vertices : List X) → F start ≃ₗ[R] F (pathEndpoint start vertices)
243   | [] => LinearEquiv.refl R (F start)
244   | next :: rest =>
245       (C.transport start next).trans (pathTransport C next rest)
246 
247 /-- A finite path in a flat pair connection depends only on its endpoints. -/
248 theorem pathTransport_eq_direct_of_flat
249     (hflat : C.Flat) (start : X) (vertices : List X) :
250     C.pathTransport start vertices =
251       C.transport start (pathEndpoint start vertices) := by
252   induction vertices generalizing start with
253   | nil =>
254       change LinearEquiv.refl R (F start) = C.transport start start
255       exact (C.transport_self start).symm
256   | cons next rest ih =>
257       simp only [pathTransport, pathEndpoint]
258       rw [ih (start := next)]
259       exact hflat start next (pathEndpoint next rest)
260 
261 /-- A finite vertex path indexed by its source and target. -/
262 inductive VertexPath (X : Type v) : X → X → Type v where
263   | nil (a : X) : VertexPath X a a
264   | cons (a b c : X) (rest : VertexPath X b c) : VertexPath X a c
265 
266 /-- Transport along a source-and-target-indexed finite path. -/
267 def indexedPathTransport :
268     {a b : X} → VertexPath X a b → F a ≃ₗ[R] F b
269   | _, _, .nil _ => LinearEquiv.refl R _
270   | _, _, .cons a b _ rest =>
271       (C.transport a b).trans (indexedPathTransport rest)
272 
273 /-- Indexed finite path transport in a flat connection is endpoint-only. -/
274 theorem indexedPathTransport_eq_direct_of_flat (hflat : C.Flat) :
275     ∀ {a b : X} (path : VertexPath X a b),
276       indexedPathTransport C path = C.transport a b := by
277   intro a b path
278   induction path with
279   | nil a => exact (C.transport_self a).symm
280   | cons a b c rest ih =>
281       simp only [indexedPathTransport]
282       rw [ih]
283       exact hflat a b c
284 
285 /-- Every indexed finite loop in a flat connection has identity holonomy. -/
286 theorem indexedLoopTransport_eq_refl_of_flat
287     (hflat : C.Flat) {a : X} (path : VertexPath X a a) :
288     indexedPathTransport C path = LinearEquiv.refl R (F a) := by
289   rw [indexedPathTransport_eq_direct_of_flat C hflat path, C.transport_self]
290 
291 /-! ## Gauge action and covariance -/
292 
293 /-- Gauge action: `Γᴳ(a,b) = G(b) ∘ Γ(a,b) ∘ G(a)⁻¹`. -/
294 def gauge (G : Gauge (R := R) (F := F)) : ReversibleConnection R X F where
295   transport a b := ((G a).symm.trans (C.transport a b)).trans (G b)
296   transport_self a := by
297     apply LinearEquiv.ext
298     intro x
299     rw [C.transport_self]
300     simp
301   transport_reverse a b := by
302     rw [C.transport_reverse a b]
303     apply LinearEquiv.ext
304     intro x
305     simp
306 
307 /-- The additive cocycle defect is gauge covariant. -/
308 theorem gauge_cocycleDefect
309     (G : Gauge (R := R) (F := F)) (a b c : X) :
310     (C.gauge G).cocycleDefect a b c =
311       (G c).toLinearMap.comp
312         ((C.cocycleDefect a b c).comp (G a).symm.toLinearMap) := by
313   ext x
314   simp [gauge, cocycleDefect]
315 
316 /-- Triangle holonomy transforms by conjugation at its base vertex. -/
317 theorem gauge_triangleHolonomy
318     (G : Gauge (R := R) (F := F)) (a b c : X) :
319     (C.gauge G).triangleHolonomy a b c =
320       ((G a).symm.trans (C.triangleHolonomy a b c)).trans (G a) := by
321   apply LinearEquiv.ext
322   intro x
323   simp [gauge, triangleHolonomy]
324 
325 /-- The cocycle equation at a fixed triple is gauge invariant. -/
326 theorem gauge_cocycleAt_iff
327     (G : Gauge (R := R) (F := F)) (a b c : X) :
328     (C.gauge G).CocycleAt a b c ↔ C.CocycleAt a b c := by
329   constructor
330   · intro h
331     apply LinearEquiv.ext
332     intro x
333     have hx := congrArg
334       (fun e : F a ≃ₗ[R] F c ↦ (G c).symm (e (G a x))) h
335     simpa [CocycleAt, gauge] using hx
336   · intro h
337     apply LinearEquiv.ext
338     intro x
339     have hx := congrArg
340       (fun e : F a ≃ₗ[R] F c ↦ G c (e ((G a).symm x))) h
341     simpa [CocycleAt, gauge] using hx
342 
343 /-- Algebraic flatness is gauge invariant. -/
344 theorem gauge_flat_iff (G : Gauge (R := R) (F := F)) :
345     (C.gauge G).Flat ↔ C.Flat := by
346   constructor
347   · intro hflat a b c
348     exact (C.gauge_cocycleAt_iff G a b c).mp (hflat a b c)
349   · intro hflat a b c
350     exact (C.gauge_cocycleAt_iff G a b c).mpr (hflat a b c)
351 
352 /-- Identity/nonidentity of a fixed triangle holonomy is gauge invariant. -/
353 theorem gauge_triangleHolonomy_eq_refl_iff
354     (G : Gauge (R := R) (F := F)) (a b c : X) :
355     (C.gauge G).triangleHolonomy a b c = LinearEquiv.refl R (F a) ↔
356       C.triangleHolonomy a b c = LinearEquiv.refl R (F a) := by
357   rw [← (C.gauge G).cocycleDefect_eq_zero_iff_triangleHolonomy_eq_refl,
358     ← C.cocycleDefect_eq_zero_iff_triangleHolonomy_eq_refl,
359     (C.gauge G).cocycleDefect_eq_zero_iff_cocycleAt,
360     C.cocycleDefect_eq_zero_iff_cocycleAt,
361     C.gauge_cocycleAt_iff]
362 
363 end ReversibleConnection
364 end Komorebi.PaperIII.Transport
365 
366 namespace Komorebi.PaperIII.HolonomyBlocks
367 
368 open scoped BigOperators
369 
370 universe u v w
371 
372 variable {R : Type u} {M : Type v} {I : Type w}
373 variable [CommRing R] [AddCommGroup M] [Module R M]
374 
375 /--
376 A finite complete family of idempotent packet projectors.  Orthogonality is
377 not needed for exact two-sided reconstruction, so it is not assumed here.
378 -/
379 structure PacketResolution (R : Type u) (M : Type v) (I : Type w)
380     [CommRing R] [AddCommGroup M] [Module R M] [Fintype I] where
381   projector : I → M →ₗ[R] M
382   complete : ∑ i, projector i = LinearMap.id
383   idempotent : ∀ i, (projector i).comp (projector i) = projector i
384 
385 namespace PacketResolution
386 
387 variable [Fintype I]
388 variable (P : PacketResolution R M I)
389 
390 /-- The packet block from input packet `nu` to output packet `mu`. -/
391 def block (A : M →ₗ[R] M) (mu nu : I) : M →ₗ[R] M :=
392   (P.projector mu).comp (A.comp (P.projector nu))
393 
394 /-- A complete finite packet family reconstructs every linear map by blocks. -/
395 theorem sum_blocks (A : M →ₗ[R] M) :
396     ∑ mu, ∑ nu, P.block A mu nu = A := by
397   have hcomplete (x : M) : ∑ i, P.projector i x = x := by
398     have hx := congrArg (fun L : M →ₗ[R] M ↦ L x) P.complete
399     simpa using hx
400   ext x
401   simp only [block, LinearMap.sum_apply, LinearMap.comp_apply]
402   calc
403     (∑ mu, ∑ nu, P.projector mu (A (P.projector nu x))) =
404         ∑ mu, P.projector mu (A (∑ nu, P.projector nu x)) := by
405           apply Finset.sum_congr rfl
406           intro mu _
407           calc
408             (∑ nu, P.projector mu (A (P.projector nu x))) =
409                 P.projector mu (∑ nu, A (P.projector nu x)) := by
410                   exact (map_sum (P.projector mu)
411                     (fun nu ↦ A (P.projector nu x)) Finset.univ).symm
412             _ = P.projector mu (A (∑ nu, P.projector nu x)) := by
413                   congr 1
414                   exact (map_sum A
415                     (fun nu ↦ P.projector nu x) Finset.univ).symm
416     _ = ∑ mu, P.projector mu (A x) := by rw [hcomplete x]
417     _ = A x := hcomplete (A x)
418 
419 /-- All finite packet blocks vanish exactly when the total map vanishes. -/
420 theorem blocks_zero_iff (A : M →ₗ[R] M) :
421     (∀ mu nu, P.block A mu nu = 0) ↔ A = 0 := by
422   constructor
423   · intro h
424     rw [← P.sum_blocks A]
425     simp [h]
426   · intro h mu nu
427     simp [block, h]
428 
429 /-- A nonzero block supplies a vector supported in its input packet. -/
430 theorem exists_packetWitness_of_block_ne_zero
431     (A : M →ₗ[R] M) (mu nu : I) (hne : P.block A mu nu ≠ 0) :
432     ∃ x, P.projector nu x = x ∧ P.projector mu (A x) ≠ 0 := by
433   classical
434   have hexists : ∃ y, P.block A mu nu y ≠ 0 := by
435     by_contra h
436     apply hne
437     ext y
438     by_contra hy
439     exact h ⟨y, hy⟩
440   rcases hexists with ⟨y, hy⟩
441   refine ⟨P.projector nu y, ?_, ?_⟩
442   · have hid := congrArg (fun L : M →ₗ[R] M ↦ L y) (P.idempotent nu)
443     simpa using hid
444   · simpa [block] using hy
445 
446 end PacketResolution
447 
448 variable {X : Type w} {F : X → Type v}
449 variable [∀ a, AddCommGroup (F a)] [∀ a, Module R (F a)]
450 
451 /-- Exact double-sum reconstruction of a fixed triangle obstruction. -/
452 theorem obstruction_sum_blocks
453     (C : Transport.ReversibleConnection R X F)
454     {I : Type w} [Fintype I] (a b c : X)
455     (P : PacketResolution R (F a) I) :
456     ∑ mu, ∑ nu, P.block (C.triangleObstruction a b c) mu nu =
457       C.triangleObstruction a b c :=
458   P.sum_blocks (C.triangleObstruction a b c)
459 
460 /--
461 For a fixed triangle, all holonomy-obstruction blocks vanish exactly when the
462 additive cocycle defect vanishes.
463 -/
464 theorem obstructionBlocks_zero_iff
465     (C : Transport.ReversibleConnection R X F)
466     {I : Type w} [Fintype I] (a b c : X)
467     (P : PacketResolution R (F a) I) :
468     (∀ mu nu,
469       P.block (C.triangleObstruction a b c) mu nu = 0) ↔
470       C.cocycleDefect a b c = 0 := by
471   rw [P.blocks_zero_iff,
472     C.triangleObstruction_eq_zero_iff_cocycleDefect_eq_zero]
473 
474 /--
475 The four vanishing criteria in the obstruction-packet theorem are mutually
476 equivalent: zero defect, identity holonomy, zero total obstruction, and zero
477 of every finite packet block.
478 -/
479 theorem obstructionDetection_equivalences
480     (C : Transport.ReversibleConnection R X F)
481     {I : Type w} [Fintype I] (a b c : X)
482     (P : PacketResolution R (F a) I) :
483     (C.cocycleDefect a b c = 0 ↔
484       C.triangleHolonomy a b c = LinearEquiv.refl R (F a)) ∧
485     (C.triangleHolonomy a b c = LinearEquiv.refl R (F a) ↔
486       C.triangleObstruction a b c = 0) ∧
487     (C.triangleObstruction a b c = 0 ↔
488       ∀ mu nu, P.block (C.triangleObstruction a b c) mu nu = 0) := by
489   refine ⟨C.cocycleDefect_eq_zero_iff_triangleHolonomy_eq_refl a b c, ?_⟩
490   refine ⟨(C.triangleObstruction_eq_zero_iff_triangleHolonomy_eq_refl
491     a b c).symm, ?_⟩
492   exact (P.blocks_zero_iff (C.triangleObstruction a b c)).symm
493 
494 /-- A nonzero holonomy block gives an exact packet-supported witness. -/
495 theorem exists_packetWitness_of_obstructionBlock_ne_zero
496     (C : Transport.ReversibleConnection R X F)
497     {I : Type w} [Fintype I] (a b c : X)
498     (P : PacketResolution R (F a) I) (mu nu : I)
499     (hne : P.block (C.triangleObstruction a b c) mu nu ≠ 0) :
500     ∃ x,
501       P.projector nu x = x ∧
502       P.projector mu (C.triangleObstruction a b c x) ≠ 0 :=
503   P.exists_packetWitness_of_block_ne_zero
504     (C.triangleObstruction a b c) mu nu hne
505 
506 end Komorebi.PaperIII.HolonomyBlocks

Back to source controls