CoordinateNaturality.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import Mathlib.Logic.Equiv.Basic
7 
8 /-!
9 # Exact coordinate naturality for arbitrary maps
10 
11 An exact coordinate system is represented by an equivalence from an ambient
12 type to a coordinate type.  No linear, topological, or differentiable
13 structure is needed.  Coordinate transport and coordinate representation are
14 therefore functorial for arbitrary functions.
15 -/
16 
17 set_option autoImplicit false
18 
19 namespace Komorebi.PaperIII.Transport
20 
21 universe u v w x y z
22 
23 /-- Exact change of coordinates from `source` coordinates to `target` coordinates. -/
24 def exactCoordinateTransport
25     {X : Type u} {Source : Type v} {Target : Type w}
26     (source : X ≃ Source) (target : X ≃ Target) : Source ≃ Target :=
27   source.symm.trans target
28 
29 @[simp] theorem exactCoordinateTransport_apply
30     {X : Type u} {Source : Type v} {Target : Type w}
31     (source : X ≃ Source) (target : X ≃ Target) (value : Source) :
32     exactCoordinateTransport source target value = target (source.symm value) :=
33   rfl
34 
35 /-- Exact transport from one coordinate system to itself is the identity. -/
36 @[simp] theorem exactCoordinateTransport_self
37     {X : Type u} {Coordinate : Type v} (coordinate : X ≃ Coordinate) :
38     exactCoordinateTransport coordinate coordinate = Equiv.refl Coordinate := by
39   ext value
40   simp [exactCoordinateTransport]
41 
42 /-- Reversing an exact coordinate transport gives its inverse. -/
43 theorem exactCoordinateTransport_symm
44     {X : Type u} {Source : Type v} {Target : Type w}
45     (source : X ≃ Source) (target : X ≃ Target) :
46     (exactCoordinateTransport source target).symm =
47       exactCoordinateTransport target source := by
48   ext value
49   simp [exactCoordinateTransport]
50 
51 /-- Exact coordinate transports satisfy the cocycle law across heterogeneous coordinate types. -/
52 theorem exactCoordinateTransport_cocycle
53     {X : Type u} {A : Type v} {B : Type w} {C : Type x}
54     (a : X ≃ A) (b : X ≃ B) (c : X ≃ C) :
55     (exactCoordinateTransport a b).trans (exactCoordinateTransport b c) =
56       exactCoordinateTransport a c := by
57   ext value
58   simp [exactCoordinateTransport]
59 
60 /-- Every exact coordinate triangle has trivial holonomy. -/
61 theorem exactCoordinateTransport_triangle
62     {X : Type u} {A : Type v} {B : Type w} {C : Type x}
63     (a : X ≃ A) (b : X ≃ B) (c : X ≃ C) :
64     ((exactCoordinateTransport a b).trans
65       (exactCoordinateTransport b c)).trans
66         (exactCoordinateTransport c a) = Equiv.refl A := by
67   ext value
68   simp [exactCoordinateTransport]
69 
70 /-- Represent an arbitrary function between two exact coordinate systems. -/
71 def exactCoordinateMap
72     {X : Type u} {Y : Type v} {Source : Type w} {Target : Type x}
73     (source : X ≃ Source) (target : Y ≃ Target) (map : X → Y) :
74     Source → Target :=
75   fun value ↦ target (map (source.symm value))
76 
77 @[simp] theorem exactCoordinateMap_apply
78     {X : Type u} {Y : Type v} {Source : Type w} {Target : Type x}
79     (source : X ≃ Source) (target : Y ≃ Target) (map : X → Y)
80     (value : Source) :
81     exactCoordinateMap source target map value =
82       target (map (source.symm value)) :=
83   rfl
84 
85 /-- Exact coordinate representation preserves identities. -/
86 theorem exactCoordinateMap_id
87     {X : Type u} {Coordinate : Type v} (coordinate : X ≃ Coordinate) :
88     exactCoordinateMap coordinate coordinate id = id := by
89   funext value
90   simp [exactCoordinateMap]
91 
92 /-- Exact coordinate representation preserves composition of arbitrary functions. -/
93 theorem exactCoordinateMap_comp
94     {X : Type u} {Y : Type v} {Z : Type w}
95     {CX : Type x} {CY : Type y} {CZ : Type z}
96     (xCoordinate : X ≃ CX) (yCoordinate : Y ≃ CY)
97     (zCoordinate : Z ≃ CZ) (first : X → Y) (second : Y → Z) :
98     exactCoordinateMap xCoordinate zCoordinate (second ∘ first) =
99       exactCoordinateMap yCoordinate zCoordinate second ∘
100         exactCoordinateMap xCoordinate yCoordinate first := by
101   funext value
102   simp [exactCoordinateMap]
103 
104 /--
105 Changing exact source and target coordinates commutes with representing any
106 function.  This is set-level naturality and assumes neither linearity nor
107 differentiability.
108 -/
109 theorem exactCoordinateMap_naturality
110     {X : Type u} {Y : Type v}
111     {XA : Type w} {XB : Type x} {YR : Type y} {YS : Type z}
112     (sourceA : X ≃ XA) (sourceB : X ≃ XB)
113     (targetR : Y ≃ YR) (targetS : Y ≃ YS) (map : X → Y) :
114     exactCoordinateTransport targetR targetS ∘
115         exactCoordinateMap sourceA targetR map =
116       exactCoordinateMap sourceB targetS map ∘
117         exactCoordinateTransport sourceA sourceB := by
118   funext value
119   simp [exactCoordinateTransport, exactCoordinateMap, Function.comp_def]
120 
121 end Komorebi.PaperIII.Transport

Back to source controls