EventualCategory.lean

1 import KomorebiSpace.ReindexedTransports
2 import Mathlib.CategoryTheory.Types.Basic
3 
4 set_option autoImplicit false
5 
6 /-!
7 # A category of sequential resolutions modulo eventual equality
8 
9 The quotient is defined by finite-stage agreement, not by equality after
10 realization. No equivalence with the full pro-category has yet been proved.
11 -/
12 
13 universe u v w z
14 namespace KomorebiSpace
15 namespace Resolution
16 
17 abbrev EventualHom (X : Resolution.{u}) (Y : Resolution.{v}) :=
18   Quotient (ReindexedMap.eventualSetoid X Y)
19 
20 namespace EventualHom
21 variable {X : Resolution.{u}} {Y : Resolution.{v}}
22     {Z : Resolution.{w}} {W : Resolution.{z}}
23 
24 def mk (f : ReindexedMap X Y) : EventualHom X Y := Quotient.mk' f
25 
26 theorem mk_eq_iff (f g : ReindexedMap X Y) :
27     mk f = mk g ↔ ReindexedMap.EventuallyEq f g := Quotient.eq
28 
29 def id (X : Resolution.{u}) : EventualHom X X := mk (ReindexedMap.id X)
30 
31 def comp (f : EventualHom X Y) (g : EventualHom Y Z) : EventualHom X Z :=
32   Quotient.liftOn₂ f g (fun a b => mk (ReindexedMap.comp a b))
33     (by intro a a' b b' ha hb; exact Quotient.sound (ReindexedMap.comp_congr ha hb))
34 
35 @[simp] theorem mk_comp (f : ReindexedMap X Y) (g : ReindexedMap Y Z) :
36     comp (mk f) (mk g) = mk (ReindexedMap.comp f g) := rfl
37 
38 @[simp] theorem id_comp (f : EventualHom X Y) : comp (id X) f = f := by
39   induction f using Quotient.inductionOn with
40   | _ f => change mk (ReindexedMap.comp (ReindexedMap.id X) f) = mk f
41            rw [ReindexedMap.id_comp]
42 
43 @[simp] theorem comp_id (f : EventualHom X Y) : comp f (id Y) = f := by
44   induction f using Quotient.inductionOn with
45   | _ f => change mk (ReindexedMap.comp f (ReindexedMap.id Y)) = mk f
46            rw [ReindexedMap.comp_id]
47 
48 theorem comp_assoc (f : EventualHom X Y) (g : EventualHom Y Z)
49     (h : EventualHom Z W) : comp (comp f g) h = comp f (comp g h) := by
50   induction f using Quotient.inductionOn with
51   | _ f => induction g using Quotient.inductionOn with
52     | _ g => induction h using Quotient.inductionOn with
53       | _ h => rfl
54 
55 def onLimit (f : EventualHom X Y) : X.Point → Y.Point :=
56   Quotient.liftOn f ReindexedMap.onLimit
57     (by intro a b h; exact ReindexedMap.onLimit_congr h)
58 
59 @[simp] theorem onLimit_mk (f : ReindexedMap X Y) :
60     (mk f).onLimit = f.onLimit := rfl
61 
62 @[simp] theorem onLimit_id (x : X.Point) : (id X).onLimit x = x := rfl
63 
64 @[simp] theorem onLimit_comp (f : EventualHom X Y) (g : EventualHom Y Z)
65     (x : X.Point) : (comp f g).onLimit x = g.onLimit (f.onLimit x) := by
66   induction f using Quotient.inductionOn with
67   | _ f => induction g using Quotient.inductionOn with
68     | _ g => rfl
69 
70 def ofMap (f : Map X Y) : EventualHom X Y := mk (ReindexedMap.ofMap f)
71 
72 @[simp] theorem onLimit_ofMap (f : Map X Y) : (ofMap f).onLimit = f.onLimit := rfl
73 
74 @[simp] theorem ofMap_id : ofMap (Map.id X) = id X := rfl
75 
76 @[simp] theorem ofMap_comp (f : Map X Y) (g : Map Y Z) :
77     ofMap (Map.comp f g) = comp (ofMap f) (ofMap g) := rfl
78 
79 end EventualHom
80 
81 /-- Same objects as the concrete resolutions; arrows are eventual classes. -/
82 instance : CategoryTheory.Category.{u} Resolution.{u} where
83   Hom := EventualHom
84   id := EventualHom.id
85   comp := EventualHom.comp
86   id_comp := EventualHom.id_comp
87   comp_id := EventualHom.comp_id
88   assoc := EventualHom.comp_assoc
89 
90 open CategoryTheory
91 
92 /-- Realization is a functor, without a claim that it is faithful or full. -/
93 def realizationFunctor : Resolution.{u} ⥤ Type u where
94   obj := Point
95   map := fun f => ↾f.onLimit
96   map_id := by intro X; rfl
97   map_comp := by
98     intro X Y Z f g
99     apply ConcreteCategory.hom_ext
100     intro x
101     exact EventualHom.onLimit_comp f g x
102 
103 end Resolution
104 end KomorebiSpace

Back to source controls