Paper X · Lean source
PacketNaturality.lean
Declared contract recorded Coverage and evidence
The cited release explicitly reports completion of its registered formal contract, under its exact hypotheses.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
Local imports (1)
PaperX/PacketNaturality.lean55 lines
Original source path
current_continuation/lean/PaperX/PacketNaturality.leanSkip declarations and read code
1 import PaperX.PacketCohomology
2
3 /-! The decomposition is compatible with maps intertwining the supplied projectors. -/
4 set_option autoImplicit false
5 namespace PaperX.PacketNaturality
6
7 open PaperX.Cohomology PaperX.PacketCohomology
8 open scoped BigOperators
9 universe u v w
10 variable {R : Type u} [CommRing R] {C D : Triple.{u,v} R}
11
12 /-- A cochain map preserving the projectors restricts to their actual image complexes. -/
13 def transport (f : ChainMap C D) (p : ChainMap C C) (q : ChainMap D D)
14 (h₀ : f.left.comp p.left = q.left.comp f.left)
15 (h₁ : f.middle.comp p.middle = q.middle.comp f.middle)
16 (h₂ : f.right.comp p.right = q.right.comp f.right) :
17 ChainMap (packet p) (packet q) where
18 left := rangeMap f.left p.left q.left h₀
19 middle := rangeMap f.middle p.middle q.middle h₁
20 right := rangeMap f.right p.right q.right h₂
21 comm₀ := by
22 ext x
23 apply Subtype.ext
24 exact LinearMap.congr_fun f.comm₀ x.val
25 comm₁ := by
26 ext x
27 apply Subtype.ext
28 exact LinearMap.congr_fun f.comm₁ x.val
29
30 theorem projection_natural (f : ChainMap C D) (p : ChainMap C C) (q : ChainMap D D)
31 (h₀ : f.left.comp p.left = q.left.comp f.left)
32 (h₁ : f.middle.comp p.middle = q.middle.comp f.middle)
33 (h₂ : f.right.comp p.right = q.right.comp f.right) (z : H C) :
34 hmap (projection q) (hmap f z) =
35 hmap (transport f p q h₀ h₁ h₂) (hmap (projection p) z) := by
36 obtain ⟨x, rfl⟩ := classOf_surjective C z
37 simp only [hmap_classOf]
38 congr 1
39 apply Subtype.ext
40 apply Subtype.ext
41 exact (LinearMap.congr_fun h₁ x.val).symm
42
43 /-- The square between total cohomology and all packet cohomologies commutes. -/
44 theorem decomposition_natural {ι : Type w} [Fintype ι]
45 (P : Resolution C ι) (Q : Resolution D ι) (f : ChainMap C D)
46 (h₀ : ∀ i, f.left.comp (P.projectors i).left = (Q.projectors i).left.comp f.left)
47 (h₁ : ∀ i, f.middle.comp (P.projectors i).middle = (Q.projectors i).middle.comp f.middle)
48 (h₂ : ∀ i, f.right.comp (P.projectors i).right = (Q.projectors i).right.comp f.right)
49 (z : H C) (i : ι) :
50 cohomologyPiEquiv Q (hmap f z) i =
51 hmap (transport f (P.projectors i) (Q.projectors i) (h₀ i) (h₁ i) (h₂ i))
52 (cohomologyPiEquiv P z i) :=
53 projection_natural f _ _ (h₀ i) (h₁ i) (h₂ i) z
54
55 end PaperX.PacketNaturality
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: b6ad9b1b6c8cc5d35b9fb31bc15ce0e3f363d8b1d9e48a883dcadd16bd6e8855
Back to Paper X: Universal Residual Seeds and Conditional Occupied-System Completion