Realization.lean

1 import Mathlib.Data.Nat.Basic
2 import Mathlib.Logic.Equiv.Basic
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Concrete inverse-limit realization
8 
9 A set-valued resolution has restriction maps for all ordered pairs of levels.
10 Its limit consists of coherent coordinates. This is an actual construction,
11 not an existence axiom for a global object.
12 -/
13 universe u v w
14 namespace KomorebiSpace
15 
16 structure Resolution where
17   Obj : ℕ → Type u
18   restrict : {i j : ℕ} → i ≤ j → Obj j → Obj i
19   restrict_refl : ∀ n (x : Obj n), restrict (Nat.le_refl n) x = x
20   restrict_trans : ∀ {i j k : ℕ} (hij : i ≤ j) (hjk : j ≤ k) (x : Obj k),
21     restrict hij (restrict hjk x) = restrict (Nat.le_trans hij hjk) x
22 
23 namespace Resolution
24 
25 def Point (X : Resolution.{u}) :=
26   {x : ∀ n, X.Obj n // ∀ i j (h : i ≤ j), X.restrict h (x j) = x i}
27 
28 @[ext] theorem Point.ext {X : Resolution.{u}} {x y : X.Point}
29     (h : ∀ n, x.val n = y.val n) : x = y := Subtype.ext (funext h)
30 
31 structure PreMap (X : Resolution.{u}) (Y : Resolution.{v}) where
32   app : ∀ n, X.Obj n → Y.Obj n
33 
34 def PreMap.Exact {X : Resolution.{u}} {Y : Resolution.{v}} (f : PreMap X Y) : Prop :=
35   ∀ i j (h : i ≤ j) (x : X.Obj j),
36     Y.restrict h (f.app j x) = f.app i (X.restrict h x)
37 
38 structure Map (X : Resolution.{u}) (Y : Resolution.{v}) extends PreMap X Y where
39   exact : toPreMap.Exact
40 
41 namespace Map
42 variable {X : Resolution.{u}} {Y : Resolution.{v}} {Z : Resolution.{w}}
43 
44 def id (X : Resolution.{u}) : Map X X where
45   app := fun _ x => x
46   exact := by intro i j h x; rfl
47 
48 def comp (f : Map X Y) (g : Map Y Z) : Map X Z where
49   app := fun n x => g.app n (f.app n x)
50   exact := by
51     intro i j h x
52     change Z.restrict h (g.app j (f.app j x)) = g.app i (f.app i (X.restrict h x))
53     rw [g.exact, f.exact]
54 
55 /-- Exact finite-level maps induce an actual map between the limits. -/
56 def onLimit (f : Map X Y) (x : X.Point) : Y.Point :=
57   ⟨fun n => f.app n (x.val n), by
58     intro i j h
59     rw [f.exact, x.property i j h]⟩
60 
61 @[simp] theorem onLimit_apply (f : Map X Y) (x : X.Point) (n : ℕ) :
62     (f.onLimit x).val n = f.app n (x.val n) := rfl
63 
64 @[simp] theorem onLimit_id (x : X.Point) : (id X).onLimit x = x := rfl
65 
66 @[simp] theorem onLimit_comp (f : Map X Y) (g : Map Y Z) (x : X.Point) :
67     (comp f g).onLimit x = g.onLimit (f.onLimit x) := rfl
68 
69 /-- Uniqueness is coordinatewise, with the coordinate specification explicit. -/
70 theorem onLimit_unique (f : Map X Y) (g : X.Point → Y.Point)
71     (hg : ∀ x n, (g x).val n = f.app n (x.val n)) : g = f.onLimit := by
72   funext x
73   exact Point.ext (hg x)
74 
75 end Map
76 
77 structure Cone (X : Resolution.{u}) (S : Type v) where
78   leg : ∀ n, S → X.Obj n
79   coherent : ∀ i j (h : i ≤ j) s, X.restrict h (leg j s) = leg i s
80 
81 namespace Cone
82 variable {X : Resolution.{u}} {S : Type v}
83 
84 def lift (c : Cone X S) (s : S) : X.Point :=
85   ⟨fun n => c.leg n s, fun i j h => c.coherent i j h s⟩
86 
87 @[simp] theorem lift_coordinate (c : Cone X S) (s : S) (n : ℕ) :
88     (c.lift s).val n = c.leg n s := rfl
89 
90 theorem lift_unique (c : Cone X S) (f : S → X.Point)
91     (hf : ∀ s n, (f s).val n = c.leg n s) : f = c.lift := by
92   funext s; exact Point.ext (hf s)
93 
94 /-- Universal property of the explicitly constructed inverse limit. -/
95 theorem exists_unique_lift (c : Cone X S) :
96     ∃! f : S → X.Point, ∀ s n, (f s).val n = c.leg n s := by
97   refine ⟨c.lift, by intro s n; rfl, ?_⟩
98   intro f hf; exact c.lift_unique f hf
99 end Cone
100 
101 /-- Realization in externally supplied objects requires explicit limit equivalences. -/
102 def realize {X : Resolution.{u}} {Y : Resolution.{v}} {S : Type u} {T : Type v}
103     (eX : S ≃ X.Point) (eY : T ≃ Y.Point) (f : Map X Y) : S → T :=
104   fun s => eY.symm (f.onLimit (eX s))
105 
106 theorem realize_coordinate {X : Resolution.{u}} {Y : Resolution.{v}}
107     {S : Type u} {T : Type v} (eX : S ≃ X.Point) (eY : T ≃ Y.Point)
108     (f : Map X Y) (s : S) (n : ℕ) :
109     (eY (realize eX eY f s)).val n = f.app n ((eX s).val n) := by
110   simp [realize]
111 
112 end Resolution
113 end KomorebiSpace

Back to source controls