PacketCohomology.lean

1 import PaperX.Cohomology
2 
3 /-!
4 Paper X 4.2: a finite family of commuting chain projectors yields an actual
5 linear equivalence between cohomology and the direct sum of packet cohomologies.
6 The packet terms are ranges of the stated projectors; their boundaries are
7 computed from their own incoming differentials. No dimension equality is assumed.
8 -/
9 set_option autoImplicit false
10 namespace PaperX.PacketCohomology
11 
12 open PaperX.Cohomology
13 open scoped BigOperators DirectSum
14 
15 universe u v w
16 variable {R : Type u} [CommRing R]
17 
18 /-- Restrict a commuting linear map to the actual image submodules. -/
19 def rangeMap {V W : Type v} [AddCommGroup V] [AddCommGroup W]
20     [Module R V] [Module R W]
21     (f : V →ₗ[R] W) (p : V →ₗ[R] V) (q : W →ₗ[R] W)
22     (h : f.comp p = q.comp f) : LinearMap.range p →ₗ[R] LinearMap.range q :=
23   (f.comp (LinearMap.range p).subtype).codRestrict (LinearMap.range q) (by
24     rintro ⟨x, y, hy⟩
25     exact ⟨f y, by
26       change q (f y) = f x
27       rw [← hy]
28       exact (LinearMap.congr_fun h y).symm⟩)
29 
30 @[simp] theorem rangeMap_val {V W : Type v} [AddCommGroup V] [AddCommGroup W]
31     [Module R V] [Module R W]
32     (f : V →ₗ[R] W) (p : V →ₗ[R] V) (q : W →ₗ[R] W)
33     (h : f.comp p = q.comp f) (x : LinearMap.range p) :
34     (rangeMap f p q h x).val = f x.val := rfl
35 
36 variable {C D : Triple.{u,v} R}
37 
38 /-- The genuine packet subcomplex: range(P) in each of three consecutive degrees. -/
39 def packet (p : ChainMap C C) : Triple.{u,v} R where
40   X₀ := LinearMap.range p.left
41   X₁ := LinearMap.range p.middle
42   X₂ := LinearMap.range p.right
43   d₀ := rangeMap C.d₀ p.left p.middle p.comm₀
44   d₁ := rangeMap C.d₁ p.middle p.right p.comm₁
45   square := by
46     ext x
47     exact LinearMap.congr_fun C.square x.val
48 
49 def inclusion (p : ChainMap C C) : ChainMap (packet p) C where
50   left := (LinearMap.range p.left).subtype
51   middle := (LinearMap.range p.middle).subtype
52   right := (LinearMap.range p.right).subtype
53   comm₀ := by ext x; rfl
54   comm₁ := by ext x; rfl
55 
56 def projection (p : ChainMap C C) : ChainMap C (packet p) where
57   left := p.left.rangeRestrict
58   middle := p.middle.rangeRestrict
59   right := p.right.rangeRestrict
60   comm₀ := by
61     ext x
62     apply Subtype.ext
63     exact LinearMap.congr_fun p.comm₀ x
64   comm₁ := by
65     ext x
66     apply Subtype.ext
67     exact LinearMap.congr_fun p.comm₁ x
68 
69 /-- Inclusion of a packet cocycle really is a total cocycle. -/
70 theorem packet_cycle_is_cycle (p : ChainMap C C) (x : Cycles (packet p)) :
71     C.d₁ x.val.val = 0 := by
72   exact congrArg Subtype.val x.property
73 
74 /-- The incoming packet boundary is obtained from an incoming element in range(P). -/
75 theorem packet_boundary_is_boundary (p : ChainMap C C) (x : (packet p).X₀) :
76     C.d₀ x.val = ((packet p).d₀ x).val := rfl
77 
78 /-- A retraction on the quotient, proved using actual packet representatives. -/
79 theorem h_retract (p : ChainMap C C) (hp : p.middle.comp p.middle = p.middle)
80     (z : H (packet p)) : hmap (projection p) (hmap (inclusion p) z) = z := by
81   obtain ⟨x, rfl⟩ := classOf_surjective (packet p) z
82   rw [hmap_classOf, hmap_classOf]
83   congr 1
84   apply Subtype.ext
85   apply Subtype.ext
86   change p.middle x.val.val = x.val.val
87   obtain ⟨y, hy⟩ := x.val.property
88   rw [← hy]
89   exact LinearMap.congr_fun hp y
90 
91 /-- Orthogonal packets vanish under the other packet's quotient projection. -/
92 theorem h_cross_zero (p q : ChainMap C C)
93     (hpq : p.middle.comp q.middle = 0) (z : H (packet q)) :
94     hmap (projection p) (hmap (inclusion q) z) = 0 := by
95   obtain ⟨x, rfl⟩ := classOf_surjective (packet q) z
96   rw [hmap_classOf, hmap_classOf]
97   have hx : cyclesMap (projection p) (cyclesMap (inclusion q) x) = 0 := by
98     apply Subtype.ext
99     apply Subtype.ext
100     change p.middle x.val.val = 0
101     obtain ⟨y, hy⟩ := x.val.property
102     rw [← hy]
103     exact LinearMap.congr_fun hpq y
104   rw [hx, map_zero]
105 
106 /-- Only the middle-degree orthogonality and completeness are needed for H in
107 that degree; a full chain-projector resolution in the manuscript implies them. -/
108 structure Resolution (C : Triple.{u,v} R) (ι : Type w) [Fintype ι] where
109   projectors : ι → ChainMap C C
110   idempotent : ∀ i, (projectors i).middle.comp (projectors i).middle = (projectors i).middle
111   orthogonal : ∀ i j, i ≠ j → (projectors i).middle.comp (projectors j).middle = 0
112   complete : ∑ i, (projectors i).middle = LinearMap.id
113 
114 variable {ι : Type w} [Fintype ι]
115 
116 theorem h_reconstruct (P : Resolution C ι) (z : H C) :
117     ∑ i, hmap (inclusion (P.projectors i)) (hmap (projection (P.projectors i)) z) = z := by
118   obtain ⟨x, rfl⟩ := classOf_surjective C z
119   simp only [hmap_classOf]
120   rw [← map_sum]
121   congr 1
122   apply Subtype.ext
123   simp only [Submodule.coe_sum]
124   change (∑ i, (P.projectors i).middle x.val) = x.val
125   simpa only [LinearMap.sum_apply, LinearMap.id_apply] using
126     LinearMap.congr_fun P.complete x.val
127 
128 /-- The main splitting as a linear equivalence with the finite product. -/
129 noncomputable def cohomologyPiEquiv (P : Resolution C ι) :
130     H C ≃ₗ[R] (∀ i, H (packet (P.projectors i))) := by
131   classical
132   refine
133     { LinearMap.pi (fun i => hmap (projection (P.projectors i))) with
134       invFun := fun z => ∑ i, hmap (inclusion (P.projectors i)) (z i)
135       left_inv := fun z => h_reconstruct P z
136       right_inv := ?_ }
137   intro z
138   funext i
139   change hmap (projection (P.projectors i)) (∑ j, hmap (inclusion (P.projectors j)) (z j)) = z i
140   rw [map_sum, Finset.sum_eq_single i]
141   · exact h_retract _ (P.idempotent i) (z i)
142   · intro j _ hj
143     exact h_cross_zero _ _ (P.orthogonal i j (Ne.symm hj)) (z j)
144   · intro hi
145     exact (hi (Finset.mem_univ i)).elim
146 
147 /-- Paper X 4.2 in literal direct-sum notation. Valid over every commutative ring. -/
148 noncomputable def cohomologyPacketEquiv (P : Resolution C ι) :
149     H C ≃ₗ[R] ⨁ i, H (packet (P.projectors i)) :=
150   (cohomologyPiEquiv P).trans
151     (DirectSum.linearEquivFunOnFintype R ι (fun i => H (packet (P.projectors i)))).symm
152 
153 /-- The forward map is exactly projection of a cocycle's class. -/
154 theorem decompose_class (P : Resolution C ι) (x : Cycles C) (i : ι) :
155     cohomologyPiEquiv P (classOf C x) i =
156       classOf (packet (P.projectors i)) (cyclesMap (projection (P.projectors i)) x) := rfl
157 
158 /-- Its inverse is precisely the finite sum of included packet classes. -/
159 theorem recompose_classes (P : Resolution C ι) (z : ∀ i, H (packet (P.projectors i))) :
160     (cohomologyPiEquiv P).symm z =
161       ∑ i, hmap (inclusion (P.projectors i)) (z i) := rfl
162 
163 /-- Being a total boundary is equivalent to every projected cocycle being a
164 boundary inside its own packet, not merely vanishing in the ambient module. -/
165 theorem boundary_iff_packet_boundaries (P : Resolution C ι) (x : Cycles C) :
166     classOf C x = 0 ↔
167       ∀ i, ∃ y : (packet (P.projectors i)).X₀,
168         (packet (P.projectors i)).d₀ y = (projection (P.projectors i)).middle x.val := by
169   constructor
170   · intro hx i
171     have h := congrArg (fun z => cohomologyPiEquiv P z i) hx
172     simpa only [decompose_class, map_zero, Pi.zero_apply, classOf_eq_zero_iff,
173       cyclesMap_val] using h
174   · intro hx
175     apply (cohomologyPiEquiv P).injective
176     ext i
177     rw [map_zero, Pi.zero_apply, decompose_class, classOf_eq_zero_iff]
178     exact hx i
179 
180 
181 /-- Splitting detects vanishing but cannot force it: total cohomology vanishes
182 if and only if every packet cohomology vanishes. -/
183 theorem vanishing_iff (P : Resolution C ι) :
184     Subsingleton (H C) ↔ ∀ i, Subsingleton (H (packet (P.projectors i))) := by
185   constructor
186   · intro h i
187     let _ := h
188     constructor
189     intro x y
190     calc
191       x = hmap (projection (P.projectors i)) (hmap (inclusion (P.projectors i)) x) :=
192         (h_retract _ (P.idempotent i) x).symm
193       _ = hmap (projection (P.projectors i)) (hmap (inclusion (P.projectors i)) y) :=
194         congrArg (hmap (projection (P.projectors i))) (Subsingleton.elim _ _)
195       _ = y := h_retract _ (P.idempotent i) y
196   · intro h
197     constructor
198     intro x y
199     apply (cohomologyPiEquiv P).injective
200     funext i
201     exact (h i).elim _ _
202 
203 end PaperX.PacketCohomology

Back to source controls