CommonQuotientInterface.lean

1 import MachineTheory.CommonQuotient
2 
3 /-!
4 # Actual common quotient data and its universal factorization
5 
6 The source's third condition quantifies over a carrier, a surjective linear
7 projection, shared linear updates and a readout. It is not replaced by an assumed
8 commuting quotient. The canonical witness is V/E. Arbitrary common data imply
9 the original all-vector observable condition, and their projections factor
10 uniquely through V/E. The canonical quotient need not be a minimal predictor.
11 -/
12 namespace Komorebi.MachineTheory.CommonQuotient
13 
14 noncomputable section
15 
16 universe uK uV uY uA uT uZ
17 variable {K : Type uK} {V : Type uV} {Y : Type uY} {A : Type uA} {Θ : Type uT}
18 variable [Field K] [AddCommGroup V] [Module K V] [AddCommGroup Y] [Module K Y]
19 
20 /-- The full existential data of the source's common linear realization. -/
21 structure CommonModel (T : Θ → A → V →ₗ[K] V) (Q : V →ₗ[K] Y) where
22   Carrier : Type uV
23   [addGroup : AddCommGroup Carrier]
24   [module : Module K Carrier]
25   projection : V →ₗ[K] Carrier
26   onto : Function.Surjective projection
27   update : A → Carrier →ₗ[K] Carrier
28   readout : Carrier →ₗ[K] Y
29   intertwines : ∀ θ a, projection.comp (T θ a) = (update a).comp projection
30   reads : Q = readout.comp projection
31 
32 attribute [instance] CommonModel.addGroup CommonModel.module
33 
34 /-- Arbitrary linear intertwining extends to every left-to-right word. -/
35 theorem factor_word {Z : Type uZ} [AddCommGroup Z] [Module K Z]
36     (T : Θ → A → V →ₗ[K] V) (r : V →ₗ[K] Z) (G : A → Z →ₗ[K] Z)
37     (h : ∀ θ a, r.comp (T θ a) = (G a).comp r) (θ : Θ) (w : List A) :
38     r.comp (wordMap (T θ) w) = (wordMap G w).comp r := by
39   induction w with
40   | nil => rfl
41   | cons a w ih =>
42     ext v
43     change r (wordMap (T θ) w (T θ a v)) = wordMap G w (G a (r v))
44     have hw := LinearMap.congr_fun ih (T θ a v)
45     change r (wordMap (T θ) w (T θ a v)) = wordMap G w (r (T θ a v)) at hw
46     rw [hw]
47     exact congrArg (wordMap G w) (LinearMap.congr_fun (h θ a) v)
48 
49 /-- Any common projection, even before a readout is selected, kills all discrepancies. -/
50 theorem discrepancy_le_kernel_of_factor {Z : Type uZ} [AddCommGroup Z] [Module K Z]
51     (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) (r : V →ₗ[K] Z) (G : A → Z →ₗ[K] Z)
52     (h : ∀ θ a, r.comp (T θ a) = (G a).comp r) :
53     discrepancy T θ₀ ≤ LinearMap.ker r := by
54   apply discrepancy_invisible_of_agreement T θ₀ r
55   intro θ w
56   rw [factor_word T r G h θ w, factor_word T r G h θ₀ w]
57 
58 /-- A common projection and matched readout imply observable agreement.
59 Surjectivity is unnecessary for this direction, and the target universe is unrestricted. -/
60 theorem agreement_of_factor {Z : Type uZ} [AddCommGroup Z] [Module K Z]
61     (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) (Q : V →ₗ[K] Y)
62     (r : V →ₗ[K] Z) (G : A → Z →ₗ[K] Z) (q : Z →ₗ[K] Y)
63     (h : ∀ θ a, r.comp (T θ a) = (G a).comp r) (hq : Q = q.comp r) :
64     ObservableAgreement T θ₀ Q := by
65   intro θ w
66   ext v
67   change Q (wordMap (T θ) w v) = Q (wordMap (T θ₀) w v)
68   have hl := LinearMap.congr_fun (factor_word T r G h θ w) v
69   have hr := LinearMap.congr_fun (factor_word T r G h θ₀ w) v
70   change r (wordMap (T θ) w v) = wordMap G w (r v) at hl
71   change r (wordMap (T θ₀) w v) = wordMap G w (r v) at hr
72   simp only [hq, LinearMap.comp_apply, hl, hr]
73 
74 /-- Even untyped function updates and readouts suffice for the necessary direction.
75 This covers a reading of the source in which their linearity is not stated separately. -/
76 theorem agreement_of_function_factor {Z : Type uZ}
77     (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) (Q : V →ₗ[K] Y)
78     (r : V → Z) (G : A → Z → Z) (q : Z → Y)
79     (h : ∀ θ a v, r (T θ a v) = G a (r v)) (hq : ∀ v, Q v = q (r v)) :
80     ObservableAgreement T θ₀ Q := by
81   intro θ w
82   ext v
83   change Q (wordMap (T θ) w v) = Q (wordMap (T θ₀) w v)
84   rw [wordMap_eq_run, wordMap_eq_run]
85   have hθ := Komorebi.MachineTheory.forward_output (fun a => T θ a) G r id Q q
86     (h θ) hq w v
87   have h₀ := Komorebi.MachineTheory.forward_output (fun a => T θ₀ a) G r id Q q
88     (h θ₀) hq w v
89   exact hθ.trans h₀.symm
90 
91 /-- Explicit common data give the source agreement, using the distinguished reference. -/
92 theorem commonModel_agreement (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ)
93     (Q : V →ₗ[K] Y) (M : CommonModel T Q) : ObservableAgreement T θ₀ Q :=
94   agreement_of_factor T θ₀ Q M.projection M.update M.readout M.intertwines M.reads
95 
96 /-- Construct the quotient carrier, projection, updates and readout from invisibility. -/
97 def canonicalModel (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) (Q : V →ₗ[K] Y)
98     (h : discrepancy T θ₀ ≤ LinearMap.ker Q) : CommonModel T Q where
99   Carrier := V ⧸ discrepancy T θ₀
100   addGroup := inferInstance
101   module := inferInstance
102   projection := (discrepancy T θ₀).mkQ
103   onto := (discrepancy T θ₀).mkQ_surjective
104   update := quotientUpdate T θ₀
105   readout := quotientReadout T θ₀ Q h
106   intertwines := by
107     intro θ a
108     ext v
109     exact quotientUpdate_candidate T θ₀ θ a v
110   reads := ((discrepancy T θ₀).liftQ_mkQ Q h).symm
111 
112 /-- Source condition three is equivalent to the constructed obstruction being invisible. -/
113 theorem commonModel_iff_invisible (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) (Q : V →ₗ[K] Y) :
114     Nonempty (CommonModel T Q) ↔ discrepancy T θ₀ ≤ LinearMap.ker Q := by
115   constructor
116   · rintro ⟨M⟩
117     exact discrepancy_invisible_of_agreement T θ₀ Q (commonModel_agreement T θ₀ Q M)
118   · intro h
119     exact ⟨canonicalModel T θ₀ Q h⟩
120 
121 /-- An exact statement of equivalence between the source's first and third conditions. -/
122 theorem agreement_iff_commonModel (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) (Q : V →ₗ[K] Y) :
123     ObservableAgreement T θ₀ Q ↔ Nonempty (CommonModel T Q) := by
124   rw [agreement_iff_invisible, commonModel_iff_invisible]
125 
126 /-- Any other common projection factors through the constructed discrepancy quotient. -/
127 def comparisonMap (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ)
128     (Q : V →ₗ[K] Y) (M : CommonModel T Q) : (V ⧸ discrepancy T θ₀) →ₗ[K] M.Carrier :=
129   (discrepancy T θ₀).liftQ M.projection
130     (discrepancy_le_kernel_of_factor T θ₀ M.projection M.update M.intertwines)
131 
132 @[simp] theorem comparisonMap_mk (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ)
133     (Q : V →ₗ[K] Y) (M : CommonModel T Q) (v : V) :
134     comparisonMap T θ₀ Q M ((discrepancy T θ₀).mkQ v) = M.projection v := rfl
135 
136 /-- Uniqueness is on the entire quotient, because every quotient value is attained. -/
137 theorem comparisonMap_unique (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ)
138     (Q : V →ₗ[K] Y) (M : CommonModel T Q)
139     (f : (V ⧸ discrepancy T θ₀) →ₗ[K] M.Carrier)
140     (hf : f.comp (discrepancy T θ₀).mkQ = M.projection) :
141     f = comparisonMap T θ₀ Q M := by
142   apply LinearMap.ext
143   intro z
144   obtain ⟨v, rfl⟩ := (discrepancy T θ₀).mkQ_surjective z
145   exact LinearMap.congr_fun hf v
146 
147 /-- The universal comparison is itself onto. -/
148 theorem comparisonMap_surjective (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ)
149     (Q : V →ₗ[K] Y) (M : CommonModel T Q) : Function.Surjective (comparisonMap T θ₀ Q M) := by
150   intro z
151   obtain ⟨v, hv⟩ := M.onto z
152   exact ⟨(discrepancy T θ₀).mkQ v, hv⟩
153 
154 /-- The universal comparison preserves the common actions. -/
155 theorem comparisonMap_intertwines (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ)
156     (Q : V →ₗ[K] Y) (M : CommonModel T Q) (a : A) :
157     (comparisonMap T θ₀ Q M).comp (quotientUpdate T θ₀ a) =
158       (M.update a).comp (comparisonMap T θ₀ Q M) := by
159   apply LinearMap.ext
160   intro z
161   obtain ⟨v, rfl⟩ := (discrepancy T θ₀).mkQ_surjective z
162   simpa only [LinearMap.comp_apply, quotientUpdate_mk, comparisonMap_mk] using
163     LinearMap.congr_fun (M.intertwines θ₀ a) v
164 
165 /-- An annihilated generator calculation does not depend on which candidate is reference. -/
166 theorem discrepancy_reference_le (T : Θ → A → V →ₗ[K] V) (θ₀ θ₁ : Θ) :
167     discrepancy T θ₁ ≤ discrepancy T θ₀ := by
168   apply discrepancy_le T θ₁
169   · intro θ a v
170     have h := (discrepancy T θ₀).sub_mem (difference_mem T θ₀ a θ v)
171       (difference_mem T θ₀ a θ₁ v)
172     simpa only [LinearMap.sub_apply, sub_sub_sub_cancel_right] using h
173   · intro a x hx
174     exact candidate_invariant T θ₀ θ₁ a hx
175 
176 /-- Distinguished reference candidates produce exactly the same discrepancy submodule. -/
177 theorem discrepancy_reference_independent (T : Θ → A → V →ₗ[K] V) (θ₀ θ₁ : Θ) :
178     discrepancy T θ₀ = discrepancy T θ₁ :=
179   le_antisymm (discrepancy_reference_le T θ₁ θ₀) (discrepancy_reference_le T θ₀ θ₁)
180 
181 end
182 end Komorebi.MachineTheory.CommonQuotient

Back to source controls