Realization.lean

1 import Std
2 
3 /-! Set-level realization and coherent coordinate transport.
4 The coefficients are explicitly restricted to the realizable subtype.
5 This module proves the algebraic part of P1 and the total-map statement of P2.
6 -/
7 set_option autoImplicit false
8 
9 namespace Komorebi.LSM
10 
11 universe u v w t
12 
13 /-- An observation archive with a specified left inverse. -/
14 structure Realization (X : Type u) (C : Type v) where
15   analysis : X → C
16   synthesis : C → X
17   reconstruct : ∀ x, synthesis (analysis x) = x
18 
19 namespace Realization
20 
21 variable {X : Type u} {C : Type v} {D : Type w} {E : Type t}
22 
23 /-- Coefficients fixed by analysis after synthesis are the consistent coefficients. -/
24 def projector (r : Realization X C) (c : C) : C := r.analysis (r.synthesis c)
25 
26 def Consistent (r : Realization X C) (c : C) : Prop := ∃ x, r.analysis x = c
27 
28 def Coeff (r : Realization X C) := {c : C // r.Consistent c}
29 
30 theorem analysis_injective (r : Realization X C) {x y : X}
31     (h : r.analysis x = r.analysis y) : x = y := by
32   have hs := congrArg r.synthesis h
33   simpa only [r.reconstruct] using hs
34 
35 theorem projector_idempotent (r : Realization X C) (c : C) :
36     r.projector (r.projector c) = r.projector c := by
37   simp only [projector, r.reconstruct]
38 
39 theorem projector_consistent (r : Realization X C) (c : C) :
40     r.Consistent (r.projector c) := ⟨r.synthesis c, rfl⟩
41 
42 theorem projector_fixed_iff (r : Realization X C) (c : C) :
43     r.projector c = c ↔ r.Consistent c := by
44   constructor
45   · intro h
46     exact ⟨r.synthesis c, h⟩
47   · rintro ⟨x, rfl⟩
48     exact congrArg r.analysis (r.reconstruct x)
49 
50 theorem projector_range (r : Realization X C) (c : C) :
51     (∃ d, r.projector d = c) ↔ r.Consistent c := by
52   constructor
53   · rintro ⟨d, rfl⟩
54     exact r.projector_consistent d
55   · intro h
56     exact ⟨c, (r.projector_fixed_iff c).mpr h⟩
57 
58 def encode (r : Realization X C) (x : X) : r.Coeff :=
59   ⟨r.analysis x, x, rfl⟩
60 
61 def decode (r : Realization X C) (c : r.Coeff) : X := r.synthesis c.val
62 
63 @[simp] theorem decode_encode (r : Realization X C) (x : X) :
64     r.decode (r.encode x) = x := r.reconstruct x
65 
66 @[simp] theorem encode_decode (r : Realization X C) (c : r.Coeff) :
67     r.encode (r.decode c) = c := by
68   apply Subtype.ext
69   exact (r.projector_fixed_iff c.val).mpr c.property
70 
71 /-- `transport a b` is T_ba: from the realizable coefficients of a to b. -/
72 def transport (a : Realization X C) (b : Realization X D)
73     (c : a.Coeff) : b.Coeff := b.encode (a.decode c)
74 
75 @[simp] theorem transport_self (a : Realization X C) (c : a.Coeff) :
76     transport a a c = c := a.encode_decode c
77 
78 theorem transport_comp (a : Realization X C) (b : Realization X D)
79     (d : Realization X E) (c : a.Coeff) :
80     transport b d (transport a b c) = transport a d c := by
81   simp only [transport, decode_encode]
82 
83 def realize (a : Realization X C) (F : X → X) (c : a.Coeff) : a.Coeff :=
84   a.encode (F (a.decode c))
85 
86 theorem realize_natural (a : Realization X C) (b : Realization X D)
87     (F : X → X) (c : a.Coeff) :
88     realize b F (transport a b c) = transport a b (realize a F c) := by
89   simp only [realize, transport, decode_encode]
90 
91 theorem realize_identity (a : Realization X C) (c : a.Coeff) :
92     realize a (fun x => x) c = c := a.encode_decode c
93 
94 theorem realize_composition (a : Realization X C) (F G : X → X) (c : a.Coeff) :
95     realize a (fun x => G (F x)) c = realize a G (realize a F c) := by
96   simp only [realize, decode_encode]
97 
98 theorem realize_faithful (a : Realization X C) (F G : X → X)
99     (h : ∀ c, realize a F c = realize a G c) : F = G := by
100   funext x
101   have hx := congrArg a.decode (h (a.encode x))
102   simpa only [realize, decode_encode] using hx
103 
104 end Realization
105 
106 /-- Every pairwise compatible family on a nonempty collection of charts comes
107 from exactly one operation on observations. A reference chart is supplied. -/
108 theorem coherent_family_unique_realization
109     {X : Type u} {I : Type v} {C : I → Type w}
110     (atlas : (i : I) → Realization X (C i)) (ref : I)
111     (G : (i : I) → (atlas i).Coeff → (atlas i).Coeff)
112     (coherent : ∀ i j c,
113       G j (Realization.transport (atlas i) (atlas j) c) =
114       Realization.transport (atlas i) (atlas j) (G i c)) :
115     ∃ F : X → X,
116       (∀ i c, G i c = Realization.realize (atlas i) F c) ∧
117       (∀ H : X → X,
118         (∀ i c, G i c = Realization.realize (atlas i) H c) → H = F) := by
119   let F : X → X := fun x => (atlas ref).decode (G ref ((atlas ref).encode x))
120   have hf : ∀ i c, G i c = Realization.realize (atlas i) F c := by
121     intro i c
122     have h := coherent ref i ((atlas ref).encode ((atlas i).decode c))
123     simpa only [Realization.transport, Realization.decode_encode,
124       Realization.encode_decode, Realization.realize, F] using h
125   refine ⟨F, hf, ?_⟩
126   intro H hh
127   apply Realization.realize_faithful (atlas ref)
128   intro c
129   exact (hh ref c).symm.trans (hf ref c)
130 
131 end Komorebi.LSM

Back to source controls