ResolutionViews.lean

1 import KomorebiSpace.SectionGluing
2 import KomorebiSpace.Cofinal
3 import KomorebiSpace.AdjacentResolution
4 import Mathlib.CategoryTheory.Category.Preorder
5 
6 set_option autoImplicit false
7 
8 /-!
9 # Existing resolution points are coherent view sections
10 
11 This connects the new language to the existing all-pairs resolution and its
12 cofinal equivalence. No original mathematical object is identified with the
13 section space without a separate realization theorem.
14 -/
15 universe u v
16 namespace KomorebiSpace
17 open CategoryTheory
18 namespace Resolution
19 
20 def views (X : Resolution.{u}) : ViewSystem ℕ where
21   Obj := X.Obj
22   pull := fun f => X.restrict (leOfHom f)
23   pull_id := X.restrict_refl
24   pull_comp := fun f g x => (X.restrict_trans (leOfHom f) (leOfHom g) x).symm
25 
26 /-- A literal bridge to the previously checked inverse-limit point type. -/
27 def ambientEquiv (X : Resolution.{u}) : X.views.Ambient ≃ X.Point where
28   toFun := fun x => ⟨x.val, fun i j h => x.property i j (homOfLE h)⟩
29   invFun := fun x => ⟨x.val, fun i j f => x.property i j (leOfHom f)⟩
30   left_inv := by intro x; rfl
31   right_inv := by intro x; rfl
32 
33 @[simp] theorem ambientEquiv_coordinate (X : Resolution.{u})
34     (x : X.views.Ambient) (n : ℕ) : (X.ambientEquiv x).val n = x.val n := rfl
35 
36 def Map.viewMorphism {X : Resolution.{u}} {Y : Resolution.{v}} (f : Map X Y) :
37     ViewSystem.Morphism X.views Y.views where
38   app := f.app
39   natural := fun e x => f.exact _ _ (leOfHom e) x
40 
41 @[simp] theorem Map.viewMorphism_onAmbient {X : Resolution.{u}} {Y : Resolution.{v}}
42     (f : Map X Y) (x : X.views.Ambient) :
43     Y.ambientEquiv (f.viewMorphism.onAmbient x) = f.onLimit (X.ambientEquiv x) := rfl
44 
45 noncomputable def cofinalAmbientEquiv (X : Resolution.{u})
46     (φ : ℕ → ℕ) (hφ : Monotone φ) (hcof : UnboundedSchedule φ) :
47     X.views.Ambient ≃ (X.reindex φ hφ).views.Ambient :=
48   X.ambientEquiv.trans ((cofinalEquiv X φ hφ hcof).trans
49     (X.reindex φ hφ).ambientEquiv.symm)
50 
51 @[simp] theorem cofinalAmbient_coordinate (X : Resolution.{u})
52     (φ : ℕ → ℕ) (hφ : Monotone φ) (hcof : UnboundedSchedule φ)
53     (x : X.views.Ambient) (n : ℕ) :
54     (cofinalAmbientEquiv X φ hφ hcof x).val n = x.val (φ n) := rfl
55 
56 /-- These patches include every transition, not only every natural-number view. -/
57 def prefixViews (N : ℕ) : Set ℕ := {n | n ≤ N}
58 
59 theorem prefixViews_transitionCover : ViewSystem.TransitionCover prefixViews := by
60   intro a b f
61   exact ⟨b, leOfHom f, Nat.le_refl b⟩
62 
63 /-- A global section is equivalent to a matching family of finite-prefix sections. -/
64 noncomputable def prefixSectionEquiv (X : Resolution.{u}) :
65     X.views.Ambient ≃ ViewSystem.Matching X.views prefixViews :=
66   X.views.gluingEquiv prefixViews prefixViews_transitionCover
67 
68 theorem prefixes_determine_point (X : Resolution.{u}) {x y : X.Point}
69     (h : ∀ N, X.views.restrict (prefixViews N) (X.ambientEquiv.symm x) =
70       X.views.restrict (prefixViews N) (X.ambientEquiv.symm y)) : x = y := by
71   have he := X.views.restrict_jointly_injective prefixViews
72     (ViewSystem.TransitionCover.objectCover prefixViews prefixViews_transitionCover) h
73   have hh := congrArg X.ambientEquiv he
74   simpa only [Equiv.apply_symm_apply] using hh
75 
76 end Resolution
77 end KomorebiSpace

Back to source controls