SectionExactSequence.lean

1 import KomorebiSpace.SectionExtensionFibers
2 
3 set_option autoImplicit false
4 
5 /-!
6 # An exact sequence for partial ambient observations
7 
8 The connecting map is an actual additive homomorphism into the existing
9 relative obstruction quotient. Exactness is proved as equality of subgroups.
10 There is no asserted surjectivity onto all arrow-indexed residual classes.
11 -/
12 universe u v w
13 namespace KomorebiSpace
14 open CategoryTheory
15 namespace AdditiveViewSystem
16 variable {V : Type u} [Category.{v} V]
17 variable {A : V → Type w} [∀ a, AddCommGroup (A a)]
18 variable (F : AdditiveViewSystem V A)
19 
20 /-- The group of all coherent ambient families. -/
21 def sectionGroup : AddSubgroup (∀ a, A a) := F.differential.ker
22 
23 /-- Coherent partial families, with their inherited additive structure. -/
24 def partialGroup (U : Set V) : AddSubgroup (∀ a : U, A a.val) where
25   carrier := {x | ∀ (a b : U) (f : a.val ⟶ b.val), F.pull f (x b) = x a}
26   zero_mem' := by intro a b f; exact map_zero _
27   add_mem' := by
28     intro x y hx hy a b f
29     change F.pull f (x b + y b) = x a + y a
30     rw [map_add, hx, hy]
31   neg_mem' := by
32     intro x hx a b f
33     change F.pull f (-x b) = -x a
34     rw [map_neg, hx]
35 
36 def sectionGroupEquiv : F.sectionGroup ≃ F.views.Ambient where
37   toFun x := ⟨x.val,(F.differential_zero_iff _).mp x.property⟩
38   invFun x := ⟨x.val,(F.differential_zero_iff _).mpr x.property⟩
39   left_inv _ := rfl
40   right_inv _ := rfl
41 
42 def partialGroupEquiv (U : Set V) : F.partialGroup U ≃ F.views.Partial U where
43   toFun x := ⟨x.val,x.property⟩
44   invFun x := ⟨x.val,x.property⟩
45   left_inv _ := rfl
46   right_inv _ := rfl
47 
48 /-- Extension by zero is additive but generally not coherent. -/
49 noncomputable def rawLift (_F : AdditiveViewSystem V A) (U : Set V) : (∀ a : U, A a.val) →+ (∀ a, A a) := by
50   classical
51   exact {
52     toFun := fun x a => if h : a ∈ U then x ⟨a,h⟩ else 0
53     map_zero' := by funext a; split_ifs <;> rfl
54     map_add' := by
55       intro x y
56       funext a
57       by_cases h : a ∈ U <;> simp [h]
58   }
59 
60 @[simp] theorem rawLift_observed (U : Set V) (x : ∀ a : U, A a.val) :
61     F.observation U (F.rawLift U x) = x := by
62   classical
63   funext a
64   simp [observation,rawLift,a.property]
65 
66 /-- The independently defined obstruction map on prescribed raw observations. -/
67 noncomputable def obstructionOfData (U : Set V) :
68     (∀ a : U, A a.val) →+ (F.problem U).Obstruction :=
69   (QuotientAddGroup.mk' (F.problem U).boundaries).comp
70     (F.differential.comp (F.rawLift U))
71 
72 @[simp] theorem obstructionOfData_apply (U : Set V) (x : ∀ a : U, A a.val) :
73     F.obstructionOfData U x = (F.problem U).obstruction (F.rawLift U x) := rfl
74 
75 /-- Actual restriction on the additive groups of coherent sections. -/
76 def restrictionHom (U : Set V) : F.sectionGroup →+ F.partialGroup U where
77   toFun x := ⟨F.observation U x.val, by
78     intro a b f
79     exact (F.differential_zero_iff _).mp x.property a.val b.val f⟩
80   map_zero' := rfl
81   map_add' := by intros; rfl
82 
83 noncomputable def connectingHom (U : Set V) :
84     F.partialGroup U →+ (F.problem U).Obstruction :=
85   (F.obstructionOfData U).comp (F.partialGroup U).subtype
86 
87 @[simp] theorem connecting_eq_extensionClass (U : Set V) (x : F.partialGroup U) :
88     F.connectingHom U x = F.extensionClass U (F.partialGroupEquiv U x) := by
89   apply F.extensionClass_independent
90   intro a
91   exact congrFun (F.rawLift_observed U x.val) a
92 
93 /-- Exactness at partial sections: the obstruction kernel is the restriction image. -/
94 theorem connecting_zero_iff_lift (U : Set V) (x : F.partialGroup U) :
95     F.connectingHom U x = 0 ↔ ∃ y : F.sectionGroup, F.restrictionHom U y = x := by
96   rw [F.connecting_eq_extensionClass, F.extensionClass_zero_iff]
97   constructor
98   · rintro ⟨⟨y,hy⟩⟩
99     refine ⟨(F.sectionGroupEquiv).symm y, ?_⟩
100     apply Subtype.ext
101     exact congrArg Subtype.val hy
102   · rintro ⟨y,hy⟩
103     refine ⟨⟨F.sectionGroupEquiv y, ?_⟩⟩
104     apply ViewSystem.Partial.ext
105     intro a
106     exact congrFun (congrArg Subtype.val hy) a
107 
108 theorem connecting_kernel_eq_range (U : Set V) :
109     (F.connectingHom U).ker = (F.restrictionHom U).range := by
110   ext x
111   exact F.connecting_zero_iff_lift U x
112 
113 @[simp] theorem connecting_restriction_zero (U : Set V) (x : F.sectionGroup) :
114     F.connectingHom U (F.restrictionHom U x) = 0 :=
115   (F.connecting_zero_iff_lift U _).mpr ⟨x,rfl⟩
116 
117 /-- The earlier extension class is the value of the same additive connecting map. -/
118 theorem extensionClass_as_hom (U : Set V) (s : F.views.Partial U) :
119     F.extensionClass U s = F.connectingHom U ((F.partialGroupEquiv U).symm s) :=
120   (F.connecting_eq_extensionClass U _).symm
121 
122 /-- Forgetting coherence proofs does not change the homogeneous kernel. -/
123 theorem restriction_kernel_characterization (U : Set V) (x : F.sectionGroup) :
124     F.restrictionHom U x = 0 ↔ x.val ∈ F.ambiguity U := by
125   constructor
126   · intro h
127     exact ⟨x.property, congrArg Subtype.val h⟩
128   · intro h
129     exact Subtype.ext h.2
130 
131 /-- Universal extension is vanishing of the connecting homomorphism, not automatic. -/
132 theorem restriction_surjective_iff_connecting_zero (U : Set V) :
133     Function.Surjective (F.restrictionHom U) ↔ F.connectingHom U = 0 := by
134   constructor
135   · intro hs
136     ext x
137     obtain ⟨y,rfl⟩ := hs x
138     exact F.connecting_restriction_zero U y
139   · intro h x
140     apply (F.connecting_zero_iff_lift U x).mp
141     rw [h]
142     rfl
143 
144 /-- The obstruction carried by partial sections, without irrelevant residual classes. -/
145 noncomputable def partialObstructionEquiv (U : Set V) :
146     F.partialGroup U ⧸ (F.restrictionHom U).range ≃+
147       (F.connectingHom U).range :=
148   (QuotientAddGroup.quotientAddEquivOfEq (F.connecting_kernel_eq_range U).symm).trans
149     (QuotientAddGroup.quotientKerEquivRange (F.connectingHom U))
150 
151 @[simp] theorem partialObstructionEquiv_class (U : Set V) (s : F.partialGroup U) :
152     (F.partialObstructionEquiv U
153       (s : F.partialGroup U ⧸ (F.restrictionHom U).range)).val =
154         F.connectingHom U s := rfl
155 
156 end AdditiveViewSystem
157 end KomorebiSpace

Back to source controls