Towers.lean

1 import Mathlib.CategoryTheory.Preadditive.Basic
2 import Mathlib.Tactic.Abel
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Sequential resolution towers and strict levelwise transports
8 
9 Bonding arrows point from finer to coarser levels. Exact transports are natural
10 levelwise maps on the fixed schedule. No identification with all pro-morphisms
11 is asserted: reindexing and eventual-equality localization are separate work.
12 -/
13 
14 universe u v
15 namespace KomorebiSpace
16 open CategoryTheory
17 
18 structure Tower (C : Type u) [Category.{v} C] where
19   obj : ℕ → C
20   down : ∀ n, obj (n + 1) ⟶ obj n
21 
22 namespace Tower
23 variable {C : Type u} [Category.{v} C]
24 
25 structure PreHom (X Y : Tower C) where
26   app : ∀ n, X.obj n ⟶ Y.obj n
27 
28 namespace PreHom
29 variable {X Y Z W : Tower C}
30 
31 @[ext] theorem ext {f g : PreHom X Y} (h : ∀ n, f.app n = g.app n) : f = g := by
32   cases f with
33   | mk f => cases g with
34     | mk g => congr; exact funext h
35 
36 def id (X : Tower C) : PreHom X X := ⟨fun n => 𝟙 (X.obj n)⟩
37 def comp (f : PreHom X Y) (g : PreHom Y Z) : PreHom X Z :=
38   ⟨fun n => f.app n ≫ g.app n⟩
39 
40 def Exact (f : PreHom X Y) : Prop :=
41   ∀ n, f.app (n + 1) ≫ Y.down n = X.down n ≫ f.app n
42 
43 @[simp] theorem id_comp (f : PreHom X Y) : comp (id X) f = f := by
44   ext n; simp [comp, id]
45 @[simp] theorem comp_id (f : PreHom X Y) : comp f (id Y) = f := by
46   ext n; simp [comp, id]
47 theorem comp_assoc (f : PreHom X Y) (g : PreHom Y Z) (h : PreHom Z W) :
48     comp (comp f g) h = comp f (comp g h) := by
49   ext n; simp [comp, Category.assoc]
50 
51 theorem exact_id (X : Tower C) : Exact (id X) := by
52   intro n; simp [id]
53 
54 theorem exact_comp {f : PreHom X Y} {g : PreHom Y Z}
55     (hf : Exact f) (hg : Exact g) : Exact (comp f g) := by
56   intro n
57   change (f.app (n+1) ≫ g.app (n+1)) ≫ Z.down n =
58     X.down n ≫ (f.app n ≫ g.app n)
59   rw [Category.assoc, hg n, ← Category.assoc, hf n, Category.assoc]
60 
61 section Additive
62 variable [Preadditive C]
63 
64 def defect (f : PreHom X Y) (n : ℕ) : X.obj (n+1) ⟶ Y.obj n :=
65   f.app (n+1) ≫ Y.down n - X.down n ≫ f.app n
66 
67 theorem exact_iff_defect_zero (f : PreHom X Y) :
68     Exact f ↔ ∀ n, defect f n = 0 := by
69   simp [Exact, defect, sub_eq_zero]
70 
71 @[simp] theorem defect_id (X : Tower C) (n : ℕ) : defect (id X) n = 0 := by
72   simp [defect, id]
73 
74 /-- The exact Leibniz law; there is no additional mixed-error term. -/
75 theorem defect_comp (f : PreHom X Y) (g : PreHom Y Z) (n : ℕ) :
76     defect (comp f g) n =
77       f.app (n+1) ≫ defect g n + defect f n ≫ g.app n := by
78   simp only [defect, comp, Preadditive.comp_sub, Preadditive.sub_comp, Category.assoc]
79   abel
80 
81 def zero (X Y : Tower C) : PreHom X Y := ⟨fun _ => 0⟩
82 
83 /-- Compatibility residual alone cannot exclude the zero transport. -/
84 theorem exact_zero (X Y : Tower C) : Exact (zero X Y) := by
85   intro n; simp [zero]
86 
87 @[simp] theorem defect_zero (X Y : Tower C) (n : ℕ) :
88     defect (zero X Y) n = 0 := by
89   simp [defect, zero]
90 
91 end Additive
92 end PreHom
93 
94 structure ExactHom (X Y : Tower C) where
95   toPreHom : PreHom X Y
96   exact : toPreHom.Exact
97 
98 namespace ExactHom
99 variable {X Y Z W : Tower C}
100 @[ext] theorem ext {f g : ExactHom X Y}
101     (h : ∀ n, f.toPreHom.app n = g.toPreHom.app n) : f = g := by
102   have hg : f.toPreHom = g.toPreHom := PreHom.ext h
103   cases f; cases g; simp_all
104 
105 def id (X : Tower C) : ExactHom X X := ⟨PreHom.id X, PreHom.exact_id X⟩
106 def comp (f : ExactHom X Y) (g : ExactHom Y Z) : ExactHom X Z :=
107   ⟨f.toPreHom.comp g.toPreHom, PreHom.exact_comp f.exact g.exact⟩
108 end ExactHom
109 
110 /-- The exact core is the category of strict natural levelwise transports. -/
111 instance : Category (Tower C) where
112   Hom := ExactHom
113   id := ExactHom.id
114   comp := ExactHom.comp
115   id_comp := by intros; ext n; simp [ExactHom.comp, ExactHom.id, PreHom.comp, PreHom.id]
116   comp_id := by intros; ext n; simp [ExactHom.comp, ExactHom.id, PreHom.comp, PreHom.id]
117   assoc := by intros; ext n; simp [ExactHom.comp, PreHom.comp, Category.assoc]
118 
119 end Tower
120 end KomorebiSpace

Back to source controls