source.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIII.PacketCoordinates
6 import KomorebiPaperIII.CoordinateNaturality
7 import Mathlib.Logic.Function.Iterate
8 
9 /-!
10 # Nonlinear maps in constructed packet coordinates
11 
12 Paper III, Definition 16.1, Theorem 16.2, Corollary 16.3 and Proposition 16.4.
13 Every coordinate equivalence here is obtained from actual projector ranges by
14 `PacketCoordinates.System.coordinateEquiv`. The ambient maps are arbitrary
15 functions and may couple every input packet to every output packet.
16 -/
17 set_option autoImplicit false
18 noncomputable section
19 
20 namespace Komorebi.PaperIII.PacketCoordinates
21 universe u v w x y z t
22 variable {R : Type u} [Semiring R]
23 variable {M : Type v} {N : Type w} {O : Type x}
24 variable [AddCommMonoid M] [Module R M]
25 variable [AddCommMonoid N] [Module R N]
26 variable [AddCommMonoid O] [Module R O]
27 variable {I : Type y} {J : Type z} {K : Type t}
28 variable [Fintype I] [Fintype J] [Fintype K]
29 
30 /-- Exact packet representation: analyze the output after applying the map to the full sum. -/
31 def coordinateMap (P : System R M I) (Q : System R N J) (f : M → N) :
32     P.Coordinates → Q.Coordinates := fun x => Q.analysis (f (P.synthesis x))
33 
34 @[simp] theorem coordinateMap_analysis (P : System R M I) (Q : System R N J)
35     (f : M → N) (x : M) : coordinateMap P Q f (P.analysis x) = Q.analysis (f x) := by
36   simp only [coordinateMap, P.synthesis_analysis]
37 
38 /-- The new construction instantiates the existing arbitrary-equivalence API literally. -/
39 theorem coordinateMap_eq_existing (P : System R M I) (Q : System R N J) (f : M → N) :
40     coordinateMap P Q f = Transport.exactCoordinateMap
41       P.coordinateEquiv.toEquiv Q.coordinateEquiv.toEquiv f := rfl
42 
43 /-- Theorem 16.2, first identity: reconstruct the original arbitrary map. -/
44 theorem coordinateMap_reconstruction (P : System R M I) (Q : System R N J) (f : M → N) :
45     Q.synthesis ∘ coordinateMap P Q f ∘ P.analysis = f := by
46   funext x
47   simp only [Function.comp_apply, coordinateMap_analysis, Q.synthesis_analysis]
48 
49 /-- Theorem 16.2, second identity: exact representation preserves composition. -/
50 theorem coordinateMap_comp (P : System R M I) (Q : System R N J) (S : System R O K)
51     (f : M → N) (g : N → O) :
52     coordinateMap P S (g ∘ f) = coordinateMap Q S g ∘ coordinateMap P Q f := by
53   funext x
54   simp only [coordinateMap, Function.comp_apply, Q.synthesis_analysis]
55 
56 /-- Exact representation preserves the identity function. -/
57 @[simp] theorem coordinateMap_id (P : System R M I) : coordinateMap P P id = id := by
58   funext x
59   exact P.analysis_synthesis x
60 
61 /-- No two distinct ambient maps become equal after exact packet representation. -/
62 theorem coordinateMap_injective (P : System R M I) (Q : System R N J) :
63     Function.Injective (coordinateMap P Q) := by
64   intro f g h
65   have hh := congrArg (fun k => Q.synthesis ∘ k ∘ P.analysis) h
66   simpa only [coordinateMap_reconstruction] using hh
67 
68 /-- Corollary 16.3: injectivity of the underlying map is preserved and reflected. -/
69 theorem injective_iff (P : System R M I) (Q : System R N J) (f : M → N) :
70     Function.Injective (coordinateMap P Q f) ↔ Function.Injective f := by
71   constructor
72   · intro h x y hxy
73     apply P.analysis_injective
74     apply h
75     simpa only [coordinateMap_analysis] using congrArg Q.analysis hxy
76   · intro h x y hxy
77     apply P.coordinateEquiv.symm.injective
78     exact h (Q.analysis_injective hxy)
79 
80 /-- Corollary 16.3: surjectivity of the underlying map is preserved and reflected. -/
81 theorem surjective_iff (P : System R M I) (Q : System R N J) (f : M → N) :
82     Function.Surjective (coordinateMap P Q f) ↔ Function.Surjective f := by
83   constructor
84   · intro h y
85     rcases h (Q.analysis y) with ⟨x, hx⟩
86     exact ⟨P.synthesis x, Q.analysis_injective hx⟩
87   · intro h y
88     rcases h (Q.synthesis y) with ⟨x, hx⟩
89     refine ⟨P.analysis x, ?_⟩
90     rw [coordinateMap_analysis, hx, Q.analysis_synthesis]
91 
92 /-- Corollary 16.3: bijectivity is preserved and reflected. -/
93 theorem bijective_iff (P : System R M I) (Q : System R N J) (f : M → N) :
94     Function.Bijective (coordinateMap P Q f) ↔ Function.Bijective f := by
95   exact and_congr (injective_iff P Q f) (surjective_iff P Q f)
96 
97 /-- The actual proposed inverse is transported, not merely its existence. -/
98 theorem leftInverse_iff (P : System R M I) (Q : System R N J)
99     (f : M → N) (g : N → M) :
100     Function.LeftInverse (coordinateMap Q P g) (coordinateMap P Q f) ↔
101       Function.LeftInverse g f := by
102   constructor
103   · intro h x
104     apply P.analysis_injective
105     simpa only [coordinateMap_analysis] using h (P.analysis x)
106   · intro h x
107     change P.analysis (g (Q.synthesis (Q.analysis (f (P.synthesis x))))) = x
108     rw [Q.synthesis_analysis, h, P.analysis_synthesis]
109 
110 /-- Right inverses obey the same exact transport law. -/
111 theorem rightInverse_iff (P : System R M I) (Q : System R N J)
112     (f : M → N) (g : N → M) :
113     Function.RightInverse (coordinateMap Q P g) (coordinateMap P Q f) ↔
114       Function.RightInverse g f := leftInverse_iff Q P g f
115 
116 /-- Corollary 16.3, displayed fixed-point equivalence. -/
117 theorem fixedPoint_iff (P : System R M I) (f : M → M) (x : M) :
118     coordinateMap P P f (P.analysis x) = P.analysis x ↔ f x = x := by
119   rw [coordinateMap_analysis]
120   exact P.analysis_injective.eq_iff
121 
122 /-- All finite iterates, including the zero iterate, are exactly conjugate. -/
123 theorem iterate_analysis (P : System R M I) (f : M → M) (n : Nat) (x : M) :
124     (coordinateMap P P f)^[n] (P.analysis x) = P.analysis ((f^[n]) x) := by
125   induction n with
126   | zero => rfl
127   | succ n ih =>
128       rw [Function.iterate_succ_apply', Function.iterate_succ_apply', ih,
129         coordinateMap_analysis]
130 
131 /-- A point returns after exactly the same prescribed numbers of steps in either description. -/
132 theorem periodicPoint_iff (P : System R M I) (f : M → M) (n : Nat) (x : M) :
133     (coordinateMap P P f)^[n] (P.analysis x) = P.analysis x ↔ (f^[n]) x = x := by
134   rw [iterate_analysis]
135   exact P.analysis_injective.eq_iff
136 
137 /-- The entire set of return times is preserved; this also identifies least positive periods. -/
138 theorem returnTimes_eq (P : System R M I) (f : M → M) (x : M) :
139     {n : Nat | (coordinateMap P P f)^[n] (P.analysis x) = P.analysis x} =
140       {n : Nat | (f^[n]) x = x} := by
141   ext n
142   exact periodicPoint_iff P f n x
143 
144 /-- Actual change between two projector coordinate systems on one ambient module. -/
145 def coordinateTransport (P : System R M I) (Q : System R M J) :
146     P.Coordinates ≃ₗ[R] Q.Coordinates := P.coordinateEquiv.symm.trans Q.coordinateEquiv
147 
148 @[simp] theorem coordinateTransport_apply (P : System R M I) (Q : System R M J)
149     (x : P.Coordinates) : coordinateTransport P Q x = Q.analysis (P.synthesis x) := rfl
150 
151 /-- Actual projector coordinate changes satisfy the cocycle law. -/
152 theorem coordinateTransport_cocycle (P : System R M I) (Q : System R M J)
153     (S : System R M K) :
154     (coordinateTransport P Q).trans (coordinateTransport Q S) = coordinateTransport P S := by
155   ext x
156   simp only [LinearEquiv.trans_apply, coordinateTransport_apply, Q.synthesis_analysis]
157 
158 /-- Actual projector coordinate loops are identities. This does not assert flatness of a connection. -/
159 theorem coordinateTransport_triangle (P : System R M I) (Q : System R M J)
160     (S : System R M K) :
161     ((coordinateTransport P Q).trans (coordinateTransport Q S)).trans
162       (coordinateTransport S P) = LinearEquiv.refl R P.Coordinates := by
163   ext x
164   simp only [LinearEquiv.trans_apply, coordinateTransport_apply, Q.synthesis_analysis,
165     S.synthesis_analysis, P.analysis_synthesis, LinearEquiv.refl_apply]
166 
167 universe s r
168 variable {I' : Type s} {J' : Type r} [Fintype I'] [Fintype J']
169 
170 /-- Proposition 16.4: changes of both input and output packet systems commute with arbitrary maps. -/
171 theorem change_coordinates (P : System R M I) (P' : System R M I')
172     (Q : System R N J) (Q' : System R N J') (f : M → N) :
173     coordinateMap P' Q' f = coordinateTransport Q Q' ∘ coordinateMap P Q f ∘
174       coordinateTransport P' P := by
175   funext x
176   simp only [Function.comp_apply, coordinateMap, coordinateTransport_apply,
177     P.synthesis_analysis, Q.synthesis_analysis]
178 
179 end Komorebi.PaperIII.PacketCoordinates

Back to source controls