FiniteRealizationExistence.lean

1 import KomorebiSpace.ResolutionViews
2 import Mathlib.CategoryTheory.CofilteredSystem
3 
4 set_option autoImplicit false
5 
6 /-!
7 # KS58: finite-fiber realization and persistent images
8 
9 The finite cofiltered-system theorem from the pinned mathlib is applied to an
10 explicit functor made from the original Resolution. An actual coordinatewise
11 equivalence connects its sections to Resolution.Point. The evaluation image
12 is identified with the intersection of the later restriction images.
13 -/
14 universe u
15 noncomputable section
16 namespace KomorebiSpace.Resolution.FiniteExistence
17 open CategoryTheory Opposite
18 variable (X : Resolution.{u})
19 
20 def diagram : ℕᵒᵖ ⥤ Type u where
21   obj n := X.Obj n.unop
22   map f := TypeCat.ofHom (X.restrict (leOfHom f.unop))
23   map_id n := by ext x; exact X.restrict_refl n.unop x
24   map_comp f g := by
25     ext x
26     exact (X.restrict_trans (leOfHom g.unop) (leOfHom f.unop) x).symm
27 
28 def pointEquivSections : X.Point ≃ (diagram X).sections where
29   toFun s := ⟨fun n => s.val n.unop, fun f => s.property _ _ (leOfHom f.unop)⟩
30   invFun s := ⟨fun n => s.val (op n), fun _ _ h => s.property (homOfLE h).op⟩
31   left_inv _ := rfl
32   right_inv _ := rfl
33 
34 @[simp] theorem sections_coordinate (s : X.Point) (n : ℕ) :
35     (pointEquivSections X s).val (op n) = s.val n := rfl
36 
37 /-- Persistent values are defined by actual later images, not by extendability. -/
38 def persistentImage (n : ℕ) : Set (X.Obj n) :=
39   {x | ∀ (m : ℕ) (h : n ≤ m), x ∈ Set.range (X.restrict h)}
40 
41 theorem persistent_iff_eventual (n : ℕ) (x : X.Obj n) :
42     x ∈ persistentImage X n ↔ x ∈ (diagram X).eventualRange (op n) := by
43   constructor
44   · intro h
45     exact (diagram X).mem_eventualRange_iff.mpr (fun {j} f => h j.unop (leOfHom f.unop))
46   · intro h m hnm
47     exact ((diagram X).mem_eventualRange_iff.mp h) (homOfLE hnm).op
48 
49 variable [∀ n, Finite (X.Obj n)] [∀ n, Nonempty (X.Obj n)]
50 
51 instance diagram_finite : ∀ n, Finite ((diagram X).obj n) :=
52   fun n => inferInstanceAs (Finite (X.Obj n.unop))
53 instance diagram_nonempty : ∀ n, Nonempty ((diagram X).obj n) :=
54   fun n => inferInstanceAs (Nonempty (X.Obj n.unop))
55 
56 theorem nonempty_point : Nonempty X.Point := by
57   obtain ⟨s, hs⟩ := nonempty_sections_of_finite_inverse_system (diagram X)
58   exact ⟨(pointEquivSections X).symm ⟨s, hs⟩⟩
59 
60 theorem nonempty_ambient : Nonempty X.views.Ambient := by
61   obtain ⟨s⟩ := nonempty_point X
62   exact ⟨X.ambientEquiv.symm s⟩
63 
64 omit [∀ n, Nonempty (X.Obj n)] in
65 theorem mittagLeffler : (diagram X).IsMittagLeffler :=
66   (diagram X).isMittagLeffler_of_exists_finite_range
67     (fun j => ⟨j, 𝟙 j, Set.toFinite _⟩)
68 
69 /-- The range of actual evaluation is exactly the persistent image. -/
70 theorem evaluation_range (n : ℕ) :
71     Set.range (fun s : X.Point => s.val n) = persistentImage X n := by
72   ext x
73   constructor
74   · rintro ⟨s, rfl⟩ m h
75     exact ⟨s.val m, s.property n m h⟩
76   · intro hx
77     let F := diagram X
78     have hm : F.IsMittagLeffler := mittagLeffler X
79     have : ∀ j, Nonempty (F.toEventualRanges.obj j) := F.toEventualRanges_nonempty hm
80     let y : F.toEventualRanges.obj (op n) :=
81       ⟨x, (persistent_iff_eventual X n x).mp hx⟩
82     obtain ⟨s, hs⟩ := F.toEventualRanges.eval_section_surjective_of_surjective
83       (F.surjective_toEventualRanges hm) (op n) y
84     refine ⟨(pointEquivSections X).symm (F.toEventualRangesSectionsEquiv s), ?_⟩
85     exact congrArg Subtype.val hs
86 
87 theorem extension_iff_persistent (n : ℕ) (x : X.Obj n) :
88     (∃ s : X.Point, s.val n = x) ↔
89       ∀ (m : ℕ) (h : n ≤ m), ∃ z : X.Obj m, X.restrict h z = x := by
90   change x ∈ Set.range (fun s : X.Point => s.val n) ↔ x ∈ persistentImage X n
91   rw [evaluation_range]
92 
93 theorem persistent_nonempty (n : ℕ) : (persistentImage X n).Nonempty := by
94   obtain ⟨s⟩ := nonempty_point X
95   rw [← evaluation_range]
96   exact ⟨s.val n, ⟨s, rfl⟩⟩
97 
98 end KomorebiSpace.Resolution.FiniteExistence
99 end

Back to source controls