source.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import Mathlib.Data.Fin.Basic
7 import Mathlib.Data.Rat.Defs
8 import Mathlib.Algebra.Module.Equiv.Basic
9 import Mathlib.Tactic
10 
11 /-!
12 # Exact coordinate transport and noncanonical connections
13 
14 Exact coordinate changes obtained from a single family of frames telescope.
15 Their loop transport is therefore forced to be the identity.  A separate
16 `Connection` API deliberately assumes only identity transport at equal
17 endpoints.  It may have a cocycle defect and nontrivial holonomy.
18 -/
19 
20 set_option autoImplicit false
21 
22 namespace Komorebi.PaperIII.Transport
23 
24 universe u v w
25 
26 section Exact
27 
28 variable {R : Type u} {M : Type v} {X : Type w}
29 variable [Semiring R] [AddCommMonoid M] [Module R M]
30 
31 /--
32 Canonical coordinate transport from frame `a` to frame `b`: synthesize through
33 the ambient space using `frame a`, then analyze using `frame b`.
34 -/
35 def exactTransport (frame : X → M ≃ₗ[R] M) (a b : X) : M ≃ₗ[R] M :=
36   (frame a).trans (frame b).symm
37 
38 @[simp] theorem exactTransport_apply (frame : X → M ≃ₗ[R] M)
39     (a b : X) (x : M) :
40     exactTransport frame a b x = (frame b).symm (frame a x) :=
41   rfl
42 
43 /-- Canonical transport at one frame is the identity. -/
44 @[simp] theorem exactTransport_self (frame : X → M ≃ₗ[R] M) (a : X) :
45     exactTransport frame a a = LinearEquiv.refl R M := by
46   apply LinearEquiv.ext
47   intro x
48   simp [exactTransport]
49 
50 /-- Canonical coordinate transport satisfies the exact cocycle law. -/
51 theorem exactTransport_cocycle (frame : X → M ≃ₗ[R] M) (a b c : X) :
52     (exactTransport frame a b).trans (exactTransport frame b c) =
53       exactTransport frame a c := by
54   apply LinearEquiv.ext
55   intro x
56   simp [exactTransport]
57 
58 /-- Every canonical two-edge round trip is trivial. -/
59 theorem exactTransport_roundTrip (frame : X → M ≃ₗ[R] M) (a b : X) :
60     (exactTransport frame a b).trans (exactTransport frame b a) =
61       LinearEquiv.refl R M := by
62   rw [exactTransport_cocycle, exactTransport_self]
63 
64 /-- Every canonical triangular loop is trivial. -/
65 theorem exactTransport_triangleLoop (frame : X → M ≃ₗ[R] M) (a b c : X) :
66     ((exactTransport frame a b).trans (exactTransport frame b c)).trans
67         (exactTransport frame c a) = LinearEquiv.refl R M := by
68   rw [exactTransport_cocycle, exactTransport_roundTrip]
69 
70 /-- Endpoint reached after traversing a finite list of successive vertices. -/
71 def pathEndpoint (start : X) : List X → X
72   | [] => start
73   | next :: rest => pathEndpoint next rest
74 
75 /-- Canonical transport along a finite list of successive vertices. -/
76 def exactPathTransport (frame : X → M ≃ₗ[R] M) (start : X) :
77     List X → M ≃ₗ[R] M
78   | [] => LinearEquiv.refl R M
79   | next :: rest =>
80       (exactTransport frame start next).trans
81         (exactPathTransport frame next rest)
82 
83 /-- Any finite canonical path telescopes to transport between its endpoints. -/
84 theorem exactPathTransport_eq_endpoint
85     (frame : X → M ≃ₗ[R] M) (start : X) (vertices : List X) :
86     exactPathTransport frame start vertices =
87       exactTransport frame start (pathEndpoint start vertices) := by
88   induction vertices generalizing start with
89   | nil =>
90       simp [exactPathTransport, pathEndpoint]
91   | cons next rest ih =>
92       simp only [exactPathTransport, pathEndpoint]
93       rw [ih, exactTransport_cocycle]
94 
95 /-- Every finite canonical path returning to its start has trivial holonomy. -/
96 theorem exactPathTransport_loop
97     (frame : X → M ≃ₗ[R] M) (start : X) (vertices : List X)
98     (hloop : pathEndpoint start vertices = start) :
99     exactPathTransport frame start vertices = LinearEquiv.refl R M := by
100   rw [exactPathTransport_eq_endpoint, hloop, exactTransport_self]
101 
102 end Exact
103 
104 section Connection
105 
106 variable {R : Type u} {M : Type v} {X : Type w}
107 variable [Semiring R] [AddCommMonoid M] [Module R M]
108 
109 /--
110 A noncanonical connection.  Only equal-endpoint transport is normalized;
111 neither the cocycle law nor reverse-edge inversion is assumed.
112 -/
113 structure Connection (R : Type u) (M : Type v) (X : Type w)
114     [Semiring R] [AddCommMonoid M] [Module R M] where
115   transport : X → X → M ≃ₗ[R] M
116   transport_self : ∀ x, transport x x = LinearEquiv.refl R M
117 
118 namespace Connection
119 
120 variable (C : Connection R M X)
121 
122 /-- The exact cocycle condition at one ordered triple. -/
123 def CocycleAt (a b c : X) : Prop :=
124   (C.transport a b).trans (C.transport b c) = C.transport a c
125 
126 /-- Flatness means the cocycle condition holds at every ordered triple. -/
127 def Flat : Prop := ∀ a b c, C.CocycleAt a b c
128 
129 /--
130 The cocycle defect, based at the target coordinate space.  It compares the
131 two-edge route `a → b → c` with the direct route `a → c`.
132 -/
133 def cocycleDefect (a b c : X) : M ≃ₗ[R] M :=
134   (C.transport a c).symm.trans
135     ((C.transport a b).trans (C.transport b c))
136 
137 /-- Ordered triangular holonomy: traverse `a → b → c → a`. -/
138 def triangleHolonomy (a b c : X) : M ≃ₗ[R] M :=
139   ((C.transport a b).trans (C.transport b c)).trans (C.transport c a)
140 
141 /-- A flat noncanonical connection has no triangular holonomy. -/
142 theorem triangleHolonomy_eq_refl_of_flat (hflat : C.Flat) (a b c : X) :
143     C.triangleHolonomy a b c = LinearEquiv.refl R M := by
144   rw [triangleHolonomy, hflat a b c, hflat a c a, C.transport_self]
145 
146 /-- Flatness forces the cocycle defect to be the identity. -/
147 theorem cocycleDefect_eq_refl_of_flat (hflat : C.Flat) (a b c : X) :
148     C.cocycleDefect a b c = LinearEquiv.refl R M := by
149   rw [cocycleDefect, hflat a b c]
150   apply LinearEquiv.ext
151   intro x
152   simp
153 
154 end Connection
155 end Connection
156 
157 /-! ## A concrete nontrivial loop -/
158 
159 /-- Multiplication by two as a rational linear equivalence. -/
160 def doubleEquiv : ℚ ≃ₗ[ℚ] ℚ where
161   toFun x := 2 * x
162   invFun x := x / 2
163   left_inv x := by ring
164   right_inv x := by ring
165   map_add' x y := by ring
166   map_smul' c x := by
167     simp only [smul_eq_mul, RingHom.id_apply]
168     ring
169 
170 @[simp] theorem doubleEquiv_apply (x : ℚ) : doubleEquiv x = 2 * x :=
171   rfl
172 
173 /--
174 A three-point connection with a single twisted directed transport `0 → 1`.
175 All other unequal endpoint transports are the identity.
176 -/
177 def twistedThreePointConnection : Connection ℚ ℚ (Fin 3) where
178   transport a b :=
179     if a = b then LinearEquiv.refl ℚ ℚ
180     else if a = (0 : Fin 3) ∧ b = (1 : Fin 3) then doubleEquiv
181     else LinearEquiv.refl ℚ ℚ
182   transport_self a := by simp
183 
184 /-- The loop `0 → 1 → 2 → 0` doubles the packet coordinate `1`. -/
185 theorem twisted_triangleHolonomy_apply_one :
186     twistedThreePointConnection.triangleHolonomy
187         (0 : Fin 3) (1 : Fin 3) (2 : Fin 3) (1 : ℚ) = 2 := by
188   norm_num [Connection.triangleHolonomy, twistedThreePointConnection,
189     doubleEquiv]
190 
191 /-- The separate connection API genuinely admits nontrivial holonomy. -/
192 theorem twisted_triangleHolonomy_ne_refl :
193     twistedThreePointConnection.triangleHolonomy
194         (0 : Fin 3) (1 : Fin 3) (2 : Fin 3) ≠ LinearEquiv.refl ℚ ℚ := by
195   intro h
196   have happly := congrArg (fun e : ℚ ≃ₗ[ℚ] ℚ ↦ e (1 : ℚ)) h
197   norm_num [Connection.triangleHolonomy, twistedThreePointConnection,
198     doubleEquiv] at happly
199 
200 end Komorebi.PaperIII.Transport

Back to source controls