TowerCorrection.lean

1 import KomorebiSpace.Towers
2 import KomorebiSpace.Correction
3 
4 set_option autoImplicit false
5 
6 /-!
7 # The obstruction quotient for actual resolution-tower defects
8 
9 This module connects the categorical and additive cores. The residual operator
10 is constructed from the bonding arrows, not supplied as an unrelated map.
11 A semantic observable restricts corrections and prevents trivial zero-map repair.
12 -/
13 universe u v w
14 namespace KomorebiSpace
15 namespace TowerCorrection
16 open CategoryTheory
17 variable {C : Type u} [Category.{v} C] [Preadditive C]
18 
19 abbrev Candidates (X Y : Tower C) := ∀ n, X.obj n ⟶ Y.obj n
20 abbrev Residuals (X Y : Tower C) := ∀ n, X.obj (n+1) ⟶ Y.obj n
21 
22 def asPreHom {X Y : Tower C} (f : Candidates X Y) : Tower.PreHom X Y := ⟨f⟩
23 
24 /-- The linear naturality differential on a fixed resolution schedule. -/
25 def differential (X Y : Tower C) : Candidates X Y →+ Residuals X Y where
26   toFun f n := f (n+1) ≫ Y.down n - X.down n ≫ f n
27   map_zero' := by
28     funext n
29     simp
30   map_add' := by
31     intro f g
32     funext n
33     simp only [Pi.add_apply, Preadditive.add_comp, Preadditive.comp_add]
34     abel
35 
36 @[simp] theorem differential_apply (X Y : Tower C) (f : Candidates X Y) (n : ℕ) :
37     differential X Y f n = Tower.PreHom.defect (asPreHom f) n := rfl
38 
39 theorem exact_iff_differential_zero (X Y : Tower C) (f : Candidates X Y) :
40     (asPreHom f).Exact ↔ differential X Y f = 0 := by
41   rw [Tower.PreHom.exact_iff_defect_zero]
42   constructor
43   · intro h
44     funext n
45     exact h n
46   · intro h n
47     exact congrFun h n
48 
49 variable {S : Type w} [AddCommGroup S]
50 
51 def problem (X Y : Tower C) (p : Candidates X Y →+ S) :
52     CorrectionProblem (Candidates X Y) (Residuals X Y) S :=
53   ⟨differential X Y, p⟩
54 
55 /-- A genuine obstruction criterion for semantic-preserving tower repair. -/
56 theorem obstruction_zero_iff_exact (X Y : Tower C) (p : Candidates X Y →+ S)
57     (f : Candidates X Y) :
58     (problem X Y p).obstruction f = 0 ↔
59       ∃ g : Candidates X Y, (asPreHom g).Exact ∧ p g = p f := by
60   rw [(problem X Y p).flatten_iff]
61   constructor
62   · rintro ⟨g, hd, hp⟩
63     exact ⟨g, (exact_iff_differential_zero X Y g).2 hd, hp⟩
64   · rintro ⟨g, hg, hp⟩
65     exact ⟨g, (exact_iff_differential_zero X Y g).1 hg, hp⟩
66 
67 /-- Exact repair descends to a real map on inverse-limit points in a realization model;
68 this theorem packages the categorical exact transport itself, before realization. -/
69 theorem obstruction_zero_iff_exactHom (X Y : Tower C) (p : Candidates X Y →+ S)
70     (f : Candidates X Y) :
71     (problem X Y p).obstruction f = 0 ↔
72       ∃ g : Tower.ExactHom X Y, p g.toPreHom.app = p f := by
73   rw [obstruction_zero_iff_exact]
74   constructor
75   · rintro ⟨g, hg, hp⟩
76     exact ⟨⟨asPreHom g, hg⟩, hp⟩
77   · rintro ⟨g, hp⟩
78     exact ⟨g.toPreHom.app, g.exact, hp⟩
79 
80 end TowerCorrection
81 end KomorebiSpace

Back to source controls