source.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiPaperIII.ReversibleConnections
7 
8 /-!
9 # Gauge covariance of finite holonomy blocks
10 
11 The reversible-connection module proves exact finite block reconstruction,
12 detection, and packet-supported witnesses.  This extension proves that a
13 gauge commuting with the packet projectors conjugates every block separately,
14 so the zero/nonzero pattern is preserved packet by packet.
15 -/
16 
17 set_option autoImplicit false
18 
19 namespace Komorebi.PaperIII.Transport.ReversibleConnection
20 
21 universe u v w
22 
23 variable {R : Type u} {X : Type v} {F : X → Type w}
24 variable [CommRing R] [∀ a, AddCommGroup (F a)] [∀ a, Module R (F a)]
25 
26 /-- The additive triangle obstruction transforms by conjugation at its base. -/
27 theorem gauge_triangleObstruction
28     (C : ReversibleConnection R X F) (G : Gauge (R := R) (F := F))
29     (a b c : X) :
30     (C.gauge G).triangleObstruction a b c =
31       (G a).toLinearMap.comp
32         ((C.triangleObstruction a b c).comp (G a).symm.toLinearMap) := by
33   unfold triangleObstruction
34   rw [C.gauge_triangleHolonomy]
35   ext value
36   simp only [LinearMap.sub_apply, LinearMap.id_apply, LinearMap.comp_apply,
37     LinearEquiv.coe_toLinearMap, LinearEquiv.trans_apply, map_sub,
38     LinearEquiv.apply_symm_apply]
39 
40 end Komorebi.PaperIII.Transport.ReversibleConnection
41 
42 namespace Komorebi.PaperIII.HolonomyBlocks
43 
44 universe u v w
45 
46 variable {R : Type u} {M : Type v} {I : Type w}
47 variable [CommRing R] [AddCommGroup M] [Module R M]
48 
49 namespace PacketResolution
50 
51 variable [Fintype I]
52 variable (P : PacketResolution R M I)
53 
54 /-- Conjugation of an endomorphism by a linear equivalence. -/
55 def gaugeConjugate (gauge : M ≃ₗ[R] M) (map : M →ₗ[R] M) : M →ₗ[R] M :=
56   gauge.toLinearMap.comp (map.comp gauge.symm.toLinearMap)
57 
58 /-- A gauge is packet preserving when it commutes with every packet projector. -/
59 def PacketPreserving (gauge : M ≃ₗ[R] M) : Prop :=
60   ∀ packet, gauge.toLinearMap.comp (P.projector packet) =
61     (P.projector packet).comp gauge.toLinearMap
62 
63 /-- The inverse of a packet-preserving gauge also commutes with every projector. -/
64 theorem symm_commutes_of_packetPreserving
65     (gauge : M ≃ₗ[R] M) (hpreserves : P.PacketPreserving gauge) (packet : I) :
66     gauge.symm.toLinearMap.comp (P.projector packet) =
67       (P.projector packet).comp gauge.symm.toLinearMap := by
68   ext value
69   apply gauge.injective
70   have hpoint := LinearMap.congr_fun (hpreserves packet) (gauge.symm value)
71   simpa using hpoint.symm
72 
73 /-- Packet-preserving conjugation acts on each input-output block separately. -/
74 theorem block_gauge_of_commutes
75     (gauge : M ≃ₗ[R] M) (map : M →ₗ[R] M)
76     (hpreserves : P.PacketPreserving gauge) (target source : I) :
77     P.block (gaugeConjugate gauge map) target source =
78       gaugeConjugate gauge (P.block map target source) := by
79   ext value
80   simp only [block, gaugeConjugate, LinearMap.comp_apply,
81     LinearEquiv.coe_toLinearMap]
82   have htarget (y : M) :
83       P.projector target (gauge y) = gauge (P.projector target y) :=
84     (LinearMap.congr_fun (hpreserves target) y).symm
85   have hsource :
86       gauge.symm (P.projector source value) =
87         P.projector source (gauge.symm value) :=
88     LinearMap.congr_fun
89       (P.symm_commutes_of_packetPreserving gauge hpreserves source) value
90   calc
91     P.projector target
92         (gauge (map (gauge.symm (P.projector source value)))) =
93         gauge
94           (P.projector target
95             (map (gauge.symm (P.projector source value)))) :=
96       htarget _
97     _ = gauge
98           (P.projector target
99             (map (P.projector source (gauge.symm value)))) := by
100       rw [hsource]
101 
102 /-- Conjugation by a linear equivalence preserves whether a map is zero. -/
103 theorem gaugeConjugate_eq_zero_iff
104     (gauge : M ≃ₗ[R] M) (map : M →ₗ[R] M) :
105     gaugeConjugate gauge map = 0 ↔ map = 0 := by
106   constructor
107   · intro hzero
108     ext value
109     apply gauge.injective
110     simpa [gaugeConjugate] using LinearMap.congr_fun hzero (gauge value)
111   · rintro rfl
112     simp [gaugeConjugate]
113 
114 /-- Packet-preserving conjugation preserves the zero/nonzero status of each block. -/
115 theorem block_gauge_eq_zero_iff
116     (gauge : M ≃ₗ[R] M) (map : M →ₗ[R] M)
117     (hpreserves : P.PacketPreserving gauge) (target source : I) :
118     P.block (gaugeConjugate gauge map) target source = 0 ↔
119       P.block map target source = 0 := by
120   rw [P.block_gauge_of_commutes gauge map hpreserves]
121   exact gaugeConjugate_eq_zero_iff gauge _
122 
123 end PacketResolution
124 
125 universe x y
126 
127 variable {Chart : Type x} {Fibre : Chart → Type y}
128 variable [∀ chart, AddCommGroup (Fibre chart)]
129 variable [∀ chart, Module R (Fibre chart)]
130 
131 /--
132 For a packet-preserving gauge, each holonomy-obstruction block is conjugated
133 by the gauge at the base chart.
134 -/
135 theorem obstructionBlock_gauge_of_commutes
136     (C : Transport.ReversibleConnection R Chart Fibre)
137     (G : Transport.ReversibleConnection.Gauge (R := R) (F := Fibre))
138     (a b c : Chart) {Packet : Type w} [Fintype Packet]
139     (P : PacketResolution R (Fibre a) Packet)
140     (hpreserves : P.PacketPreserving (G a)) (target source : Packet) :
141     P.block ((C.gauge G).triangleObstruction a b c) target source =
142       PacketResolution.gaugeConjugate (G a)
143         (P.block (C.triangleObstruction a b c) target source) := by
144   rw [C.gauge_triangleObstruction]
145   exact P.block_gauge_of_commutes (G a)
146     (C.triangleObstruction a b c) hpreserves target source
147 
148 /-- Packet-preserving gauges preserve each obstruction block's zero status. -/
149 theorem obstructionBlock_gauge_eq_zero_iff
150     (C : Transport.ReversibleConnection R Chart Fibre)
151     (G : Transport.ReversibleConnection.Gauge (R := R) (F := Fibre))
152     (a b c : Chart) {Packet : Type w} [Fintype Packet]
153     (P : PacketResolution R (Fibre a) Packet)
154     (hpreserves : P.PacketPreserving (G a)) (target source : Packet) :
155     P.block ((C.gauge G).triangleObstruction a b c) target source = 0 ↔
156       P.block (C.triangleObstruction a b c) target source = 0 := by
157   rw [obstructionBlock_gauge_of_commutes C G a b c P hpreserves]
158   exact PacketResolution.gaugeConjugate_eq_zero_iff (G a) _
159 
160 end Komorebi.PaperIII.HolonomyBlocks

Back to source controls