FiniteObservation.lean

1 import KomorebiSpace.RealizationFaithfulness
2 
3 set_option autoImplicit false
4 
5 /-!
6 # The exact image of realization for projection-surjective sources
7 
8 An output level must factor through some finite input level. The input level
9 may depend on the output level. A common monotone schedule is constructed.
10 No topology or numerical complexity bound is implicit in this condition.
11 -/
12 
13 universe u v
14 namespace KomorebiSpace
15 namespace Resolution
16 variable {X : Resolution.{u}} {Y : Resolution.{v}}
17 
18 /-- Finite-level factorization for every output coordinate. -/
19 def FinitelyObserved (F : X.Point → Y.Point) : Prop :=
20   ∀ n, ∃ k, ∃ a : X.Obj k → Y.Obj n,
21     ∀ x : X.Point, (F x).val n = a (x.val k)
22 
23 def levelEnvelope (k : ℕ → ℕ) : ℕ → ℕ
24   | 0 => k 0
25   | n+1 => max (levelEnvelope k n) (k (n+1))
26 
27 theorem levelEnvelope_ge (k : ℕ → ℕ) (n : ℕ) : k n ≤ levelEnvelope k n := by
28   cases n with
29   | zero => exact le_refl _
30   | succ n => exact Nat.le_max_right _ _
31 
32 theorem levelEnvelope_monotone (k : ℕ → ℕ) : Monotone (levelEnvelope k) := by
33   intro i j h
34   induction j, h using Nat.le_induction with
35   | base => exact le_refl _
36   | succ j hj ih => exact ih.trans (Nat.le_max_left _ _)
37 
38 def observedApp (k : ℕ → ℕ) (a : ∀ n, X.Obj (k n) → Y.Obj n) (n : ℕ) :
39     X.Obj (levelEnvelope k n) → Y.Obj n :=
40   fun x => a n (X.restrict (levelEnvelope_ge k n) x)
41 
42 theorem observedApp_on_point (F : X.Point → Y.Point) (k : ℕ → ℕ)
43     (a : ∀ n, X.Obj (k n) → Y.Obj n)
44     (ha : ∀ n x, (F x).val n = a n (x.val (k n))) (n : ℕ) (x : X.Point) :
45     observedApp k a n (x.val (levelEnvelope k n)) = (F x).val n := by
46   exact (congrArg (a n) (x.property (k n) (levelEnvelope k n)
47     (levelEnvelope_ge k n))).trans (ha n x).symm
48 
49 /-- Compatibility is derived from the realized output and source projection surjectivity. -/
50 def observedPresentation (hX : ProjectionSurjective X) (F : X.Point → Y.Point)
51     (k : ℕ → ℕ) (a : ∀ n, X.Obj (k n) → Y.Obj n)
52     (ha : ∀ n x, (F x).val n = a n (x.val (k n))) : ReindexedMap X Y where
53   level := levelEnvelope k
54   monotone := levelEnvelope_monotone k
55   app := observedApp k a
56   naturality := by
57     intro i j hij y
58     obtain ⟨x, hx⟩ := hX (levelEnvelope k j) y
59     change x.val (levelEnvelope k j) = y at hx
60     subst y
61     rw [observedApp_on_point F k a ha j x, (F x).property i j hij,
62       x.property _ _ (levelEnvelope_monotone k hij), observedApp_on_point F k a ha i x]
63 
64 theorem observedPresentation_onLimit (hX : ProjectionSurjective X)
65     (F : X.Point → Y.Point) (k : ℕ → ℕ) (a : ∀ n, X.Obj (k n) → Y.Obj n)
66     (ha : ∀ n x, (F x).val n = a n (x.val (k n))) :
67     (observedPresentation hX F k a ha).onLimit = F := by
68   funext x
69   exact Point.ext (fun n => observedApp_on_point F k a ha n x)
70 
71 theorem exists_presentation_of_finitelyObserved (hX : ProjectionSurjective X)
72     (F : X.Point → Y.Point) (hF : FinitelyObserved F) :
73     ∃ f : ReindexedMap X Y, f.onLimit = F := by
74   classical
75   let k : ℕ → ℕ := fun n => Classical.choose (hF n)
76   let a : ∀ n, X.Obj (k n) → Y.Obj n :=
77     fun n => Classical.choose (Classical.choose_spec (hF n))
78   have ha : ∀ n x, (F x).val n = a n (x.val (k n)) :=
79     fun n => Classical.choose_spec (Classical.choose_spec (hF n))
80   exact ⟨observedPresentation hX F k a ha, observedPresentation_onLimit hX F k a ha⟩
81 
82 theorem reindexed_finitelyObserved (f : ReindexedMap X Y) :
83     FinitelyObserved f.onLimit := by
84   intro n
85   exact ⟨f.level n, f.app n, fun _ => rfl⟩
86 
87 theorem eventual_finitelyObserved (f : EventualHom X Y) :
88     FinitelyObserved f.onLimit := by
89   induction f using Quotient.inductionOn with
90   | _ f => exact reindexed_finitelyObserved f
91 
92 theorem realization_image_iff (hX : ProjectionSurjective X) (F : X.Point → Y.Point) :
93     (∃ f : EventualHom X Y, f.onLimit = F) ↔ FinitelyObserved F := by
94   constructor
95   · rintro ⟨f, rfl⟩; exact eventual_finitelyObserved f
96   · intro hF
97     obtain ⟨f, hf⟩ := exists_presentation_of_finitelyObserved hX F hF
98     exact ⟨EventualHom.mk f, hf⟩
99 
100 /-- Presentation-independent coordinates on the morphism set, under an explicit hypothesis. -/
101 noncomputable def finiteObservationEquiv (hX : ProjectionSurjective X) :
102     EventualHom X Y ≃ {F : X.Point → Y.Point // FinitelyObserved F} :=
103   Equiv.ofBijective (fun f => ⟨f.onLimit, eventual_finitelyObserved f⟩)
104     ⟨by
105       intro f g h
106       exact EventualHom.onLimit_injective hX (congrArg Subtype.val h),
107      by
108       intro F
109       obtain ⟨f, hf⟩ := (realization_image_iff hX F.val).mpr F.property
110       exact ⟨f, Subtype.ext hf⟩⟩
111 
112 @[simp] theorem finiteObservationEquiv_apply (hX : ProjectionSurjective X)
113     (f : EventualHom X Y) : (finiteObservationEquiv hX f).val = f.onLimit := rfl
114 
115 end Resolution
116 end KomorebiSpace

Back to source controls