HolonomyViews.lean

1 import KomorebiSpace.HolonomyRepair
2 import KomorebiSpace.ViewSections
3 
4 set_option autoImplicit false
5 
6 /-!
7 # The actual ambient view system for path-dependent transport
8 
9 A graph walk, rather than only its endpoints, is a morphism. Parallel sections
10 of this category are exactly the edge-compatible data. This retains nontrivial
11 loop operators instead of collapsing the graph to a thin comparison category.
12 -/
13 universe u v
14 noncomputable section
15 namespace KomorebiSpace
16 namespace HolonomyTransport
17 variable {V : Type u} {H : Type v}
18 variable [NormedAddCommGroup H] [NormedSpace ℝ H]
19 
20 /-- Keeping the graph as a parameter prevents a global category instance on V. -/
21 structure PathView (graph : SimpleGraph V) where
22   vertex : V
23 
24 instance pathViewCategory (graph : SimpleGraph V) : CategoryTheory.Category (PathView graph) where
25   Hom i j := graph.Walk i.vertex j.vertex
26   id _ := SimpleGraph.Walk.nil
27   comp p q := p.append q
28   id_comp := by intros; rfl
29   comp_id := by intro i j p; exact SimpleGraph.Walk.append_nil p
30   assoc := by intro i j k l p q r; exact (SimpleGraph.Walk.append_assoc p q r).symm
31 
32 namespace Connection
33 variable (T : Connection V H) (graph : SimpleGraph V)
34 
35 def pathViews : ViewSystem (PathView graph) where
36   Obj := fun _ => H
37   pull := fun f => T.walkTransport f
38   pull_id := by intros; rfl
39   pull_comp := by intro i j k f g z; exact T.walkTransport_append f g z
40 
41 def ambientValues (x : (T.pathViews graph).Ambient) : V → H := fun i => x.val ⟨i⟩
42 
43 def toAmbient (x : V → H) (hx : T.Parallel graph x) : (T.pathViews graph).Ambient :=
44   ⟨fun i => x i.vertex, fun _i _j f => T.parallel_walk x hx f⟩
45 
46 @[simp] theorem toAmbient_coordinate (x : V → H) (hx : T.Parallel graph x) (i : V) :
47     (T.toAmbient graph x hx).val ⟨i⟩ = x i := rfl
48 
49 theorem ambient_parallel (x : (T.pathViews graph).Ambient) :
50     T.Parallel graph (fun i => x.val ⟨i⟩) := by
51   intro i j hij
52   exact x.property ⟨i⟩ ⟨j⟩ (.cons hij .nil)
53 
54 /-- This is the old Ambient type with the new, actual walk restriction maps. -/
55 def ambientParallelEquiv :
56     (T.pathViews graph).Ambient ≃ {x : V → H // T.Parallel graph x} where
57   toFun x := ⟨fun i => x.val ⟨i⟩, T.ambient_parallel graph x⟩
58   invFun x := T.toAmbient graph x.val x.property
59   left_inv := by intro x; apply ViewSystem.Ambient.ext; intro i; rfl
60   right_inv := by intro x; rfl
61 
62 end Connection
63 
64 namespace Rooted
65 variable (T : Connection V H) {graph : SimpleGraph V} {o : V}
66 variable (p : OverlapTransport.Routing graph o)
67 
68 def ambientParameters : fixedSpace T p ≃ (T.pathViews graph).Ambient where
69   toFun z := T.toAmbient graph (reconstruct T p z.val)
70     ((reconstruct_parallel_iff T p z.val).mpr z.property)
71   invFun x := ⟨x.val ⟨o⟩, parallel_anchor_fixed T p (fun i => x.val ⟨i⟩)
72     (T.ambient_parallel graph x)⟩
73   left_inv := by intro z; apply Subtype.ext; exact reconstruct_anchor T p z.val
74   right_inv := by
75     intro x
76     apply ViewSystem.Ambient.ext
77     intro i
78     exact congrFun (parallel_reconstruction T p (fun j => x.val ⟨j⟩)
79       (T.ambient_parallel graph x)) i.vertex
80 
81 @[simp] theorem ambientParameters_coordinate (z : fixedSpace T p) (i : V) :
82     (ambientParameters T p z).val ⟨i⟩ = frame T p i z.val := rfl
83 
84 section Finite
85 variable [Fintype V]
86 
87 theorem quantitative_ambient_realization (U : Set V) (ho : o ∈ U) (x : V → H)
88     (hx : (problem T (graph := graph) U).obstruction x = 0) :
89     ∃ s : (T.pathViews graph).Ambient,
90       (∀ i : U, s.val ⟨i.val⟩ = x i.val) ∧
91       ‖x - T.ambientValues graph s‖ ≤ (p.radius : ℝ) * ‖T.differential graph x‖ := by
92   obtain ⟨y,hy,_⟩ := quantitative_prescribed_repair T p U ho x hx
93   exact ⟨T.toAmbient graph y hy.1, hy.2.1, hy.2.2⟩
94 
95 end Finite
96 end Rooted
97 end HolonomyTransport
98 end KomorebiSpace
99 end

Back to source controls