ViewSections.lean

1 import Mathlib.CategoryTheory.Category.Basic
2 import Mathlib.Data.Set.Basic
3 import Mathlib.Logic.Equiv.Basic
4 
5 set_option autoImplicit false
6 
7 /-!
8 # Set-valued views and coherent ambient sections
9 
10 This is the strict, set-valued layer of the proposed indexed realization system.
11 It does not assert a higher category or a stack. Arrows point from a restricted
12 view to a larger view; restriction of data is contravariant.
13 -/
14 universe u v w z t
15 namespace KomorebiSpace
16 open CategoryTheory
17 
18 structure ViewSystem (V : Type u) [Category.{v} V] where
19   Obj : V → Type w
20   pull : {a b : V} → (a ⟶ b) → Obj b → Obj a
21   pull_id : ∀ a (x : Obj a), pull (𝟙 a) x = x
22   pull_comp : ∀ {a b c : V} (f : a ⟶ b) (g : b ⟶ c) (x : Obj c),
23     pull (f ≫ g) x = pull f (pull g x)
24 
25 namespace ViewSystem
26 variable {V : Type u} [Category.{v} V]
27 
28 /-- Coherent data at every view, not a choice of one preferred view. -/
29 def Ambient (F : ViewSystem.{u,v,w} V) :=
30   {x : ∀ a, F.Obj a // ∀ a b (f : a ⟶ b), F.pull f (x b) = x a}
31 
32 @[ext] theorem Ambient.ext {F : ViewSystem.{u,v,w} V} {x y : F.Ambient}
33     (h : ∀ a, x.val a = y.val a) : x = y := Subtype.ext (funext h)
34 
35 /-- Evaluation need not be individually injective or surjective. -/
36 def evaluate (F : ViewSystem.{u,v,w} V) (a : V) : F.Ambient → F.Obj a :=
37   fun x => x.val a
38 
39 theorem evaluations_jointly_injective (F : ViewSystem.{u,v,w} V)
40     {x y : F.Ambient} (h : ∀ a, F.evaluate a x = F.evaluate a y) : x = y :=
41   Ambient.ext h
42 
43 @[simp] theorem evaluation_coherent (F : ViewSystem.{u,v,w} V)
44     (x : F.Ambient) {a b : V} (f : a ⟶ b) :
45     F.pull f (F.evaluate b x) = F.evaluate a x := x.property a b f
46 
47 /-- A family of maps which commutes with restriction. -/
48 structure Morphism (F : ViewSystem.{u,v,w} V) (G : ViewSystem.{u,v,z} V) where
49   app : ∀ a, F.Obj a → G.Obj a
50   natural : ∀ {a b : V} (f : a ⟶ b) (x : F.Obj b),
51     G.pull f (app b x) = app a (F.pull f x)
52 
53 namespace Morphism
54 variable {F : ViewSystem.{u,v,w} V} {G : ViewSystem.{u,v,z} V}
55 
56 def onAmbient (f : Morphism F G) (x : F.Ambient) : G.Ambient :=
57   ⟨fun a => f.app a (x.val a), by
58     intro a b e
59     rw [f.natural, x.property a b e]⟩
60 
61 @[simp] theorem onAmbient_evaluate (f : Morphism F G) (x : F.Ambient) (a : V) :
62     G.evaluate a (f.onAmbient x) = f.app a (F.evaluate a x) := rfl
63 
64 def id (F : ViewSystem.{u,v,w} V) : Morphism F F where
65   app := fun _ x => x
66   natural := by intros; rfl
67 
68 def comp {H : ViewSystem.{u,v,t} V} (f : Morphism F G) (g : Morphism G H) :
69     Morphism F H where
70   app := fun a x => g.app a (f.app a x)
71   natural := by intros; rw [g.natural, f.natural]
72 
73 @[simp] theorem onAmbient_id (x : F.Ambient) : (id F).onAmbient x = x := rfl
74 
75 @[simp] theorem onAmbient_comp {H : ViewSystem.{u,v,t} V}
76     (f : Morphism F G) (g : Morphism G H) (x : F.Ambient) :
77     (comp f g).onAmbient x = g.onAmbient (f.onAmbient x) := rfl
78 end Morphism
79 
80 /-- The usual set-level limit universal property, with legs and coherence explicit. -/
81 structure Cone (F : ViewSystem.{u,v,w} V) (T : Type z) where
82   leg : ∀ a, T → F.Obj a
83   coherent : ∀ a b (f : a ⟶ b) x, F.pull f (leg b x) = leg a x
84 
85 namespace Cone
86 variable {F : ViewSystem.{u,v,w} V} {T : Type z}
87 
88 def lift (c : Cone F T) (x : T) : F.Ambient :=
89   ⟨fun a => c.leg a x, fun a b f => c.coherent a b f x⟩
90 
91 @[simp] theorem lift_evaluate (c : Cone F T) (x : T) (a : V) :
92     F.evaluate a (c.lift x) = c.leg a x := rfl
93 
94 theorem lift_unique (c : Cone F T) (g : T → F.Ambient)
95     (h : ∀ x a, F.evaluate a (g x) = c.leg a x) : g = c.lift := by
96   funext x
97   exact Ambient.ext (h x)
98 
99 theorem exists_unique_lift (c : Cone F T) :
100     ∃! g : T → F.Ambient, ∀ x a, F.evaluate a (g x) = c.leg a x := by
101   refine ⟨c.lift, by intro x a; rfl, ?_⟩
102   intro g h
103   exact c.lift_unique g h
104 end Cone
105 
106 /-- A partial section includes every transition with both endpoints in its domain. -/
107 def Partial (F : ViewSystem.{u,v,w} V) (U : Set V) :=
108   {x : ∀ a : U, F.Obj a.val //
109     ∀ (a b : U) (f : a.val ⟶ b.val), F.pull f (x b) = x a}
110 
111 @[ext] theorem Partial.ext {F : ViewSystem.{u,v,w} V} {U : Set V}
112     {x y : F.Partial U} (h : ∀ a, x.val a = y.val a) : x = y :=
113   Subtype.ext (funext h)
114 
115 def restrict (F : ViewSystem.{u,v,w} V) (U : Set V) (x : F.Ambient) : F.Partial U :=
116   ⟨fun a => x.val a.val, fun a b f => x.property a.val b.val f⟩
117 
118 def restrictPartial (F : ViewSystem.{u,v,w} V) {U W : Set V} (h : U ⊆ W)
119     (x : F.Partial W) : F.Partial U :=
120   ⟨fun a => x.val ⟨a.val, h a.property⟩, fun a b f => x.property ⟨a.val, h a.property⟩ ⟨b.val, h b.property⟩ f⟩
121 
122 @[simp] theorem restrictPartial_refl (F : ViewSystem.{u,v,w} V) (U : Set V)
123     (x : F.Partial U) : F.restrictPartial (Set.Subset.refl U) x = x := rfl
124 
125 @[simp] theorem restrictPartial_comp (F : ViewSystem.{u,v,w} V)
126     {U W Z : Set V} (h : U ⊆ W) (k : W ⊆ Z) (x : F.Partial Z) :
127     F.restrictPartial h (F.restrictPartial k x) = F.restrictPartial (h.trans k) x := rfl
128 
129 /-- The extension space can be empty, singleton, or contain multiple choices. -/
130 def Extensions (F : ViewSystem.{u,v,w} V) (U : Set V) (x : F.Partial U) :=
131   {s : F.Ambient // F.restrict U s = x}
132 
133 theorem extension_nonempty_iff (F : ViewSystem.{u,v,w} V) (U : Set V)
134     (x : F.Partial U) :
135     Nonempty (F.Extensions U x) ↔ ∃ s : F.Ambient, F.restrict U s = x := by
136   constructor
137   · rintro ⟨⟨s, h⟩⟩; exact ⟨s, h⟩
138   · rintro ⟨s, h⟩; exact ⟨⟨s, h⟩⟩
139 
140 /-- Including a terminal global view makes evaluation at that view an equivalence.
141 This does not prove that observations on a smaller view domain extend to it. -/
142 def terminalEvaluationEquiv (F : ViewSystem.{u,v,w} V) (t : V)
143     (toTop : ∀ a, a ⟶ t) (ht : toTop t = 𝟙 t)
144     (hn : ∀ a b (f : a ⟶ b), f ≫ toTop b = toTop a) :
145     F.Ambient ≃ F.Obj t where
146   toFun := F.evaluate t
147   invFun := fun x => ⟨fun a => F.pull (toTop a) x, by
148     intro a b f
149     rw [← F.pull_comp, hn]⟩
150   left_inv := by
151     intro x
152     apply Ambient.ext
153     intro a
154     exact x.property a t (toTop a)
155   right_inv := by
156     intro x
157     change F.pull (toTop t) x = x
158     rw [ht, F.pull_id]
159 
160 @[simp] theorem terminalEvaluation_coordinate (F : ViewSystem.{u,v,w} V) (t : V)
161     (toTop : ∀ a, a ⟶ t) (ht : toTop t = 𝟙 t)
162     (hn : ∀ a b (f : a ⟶ b), f ≫ toTop b = toTop a) (x : F.Obj t) (a : V) :
163     ((F.terminalEvaluationEquiv t toTop ht hn).symm x).val a = F.pull (toTop a) x := rfl
164 
165 /-- The constant view system is useful for explicit boundary examples. -/
166 def constant (V : Type u) [Category.{v} V] (T : Type w) : ViewSystem V where
167   Obj := fun _ => T
168   pull := fun _ x => x
169   pull_id := by intros; rfl
170   pull_comp := by intros; rfl
171 
172 def constantSection (V : Type u) [Category.{v} V] {T : Type w} (x : T) :
173     (constant V T).Ambient := ⟨fun _ => x, by intros; rfl⟩
174 
175 end ViewSystem
176 end KomorebiSpace

Back to source controls