ComplexCohomology.lean

1 import PaperX.PacketCohomology
2 import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
3 import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
4 import Mathlib.LinearAlgebra.Dimension.Constructions
5 
6 /-!
7 Explicit bridge from the quotient used in this release to Mathlib's categorical
8 homology, including windows of arbitrary homological/cochain complexes.
9 -/
10 set_option autoImplicit false
11 namespace PaperX.ComplexCohomology
12 
13 open CategoryTheory
14 open PaperX.Cohomology PaperX.PacketCohomology
15 open scoped DirectSum BigOperators
16 universe u v w
17 variable {R : Type u} [CommRing R]
18 
19 def ofShortComplex (S : ShortComplex (ModuleCat.{v} R)) : Triple.{u,v} R where
20   X₀ := S.X₁
21   X₁ := S.X₂
22   X₂ := S.X₃
23   d₀ := S.f.hom
24   d₁ := S.g.hom
25   square := ModuleCat.hom_ext_iff.mp S.zero
26 
27 def toShortComplex (C : Triple.{u,v} R) : ShortComplex (ModuleCat.{v} R) :=
28   ShortComplex.moduleCatMk C.d₀ C.d₁ C.square
29 
30 /-- Our explicit quotient agrees with the standard ModuleCat homology object. -/
31 noncomputable def standardHomologyEquiv (S : ShortComplex (ModuleCat.{v} R)) :
32     S.homology ≃ₗ[R] H (ofShortComplex S) :=
33   S.moduleCatHomologyIso.toLinearEquiv
34 
35 noncomputable def quotientHomologyEquiv (C : Triple.{u,v} R) :
36     (toShortComplex C).homology ≃ₗ[R] H C :=
37   (toShortComplex C).moduleCatHomologyIso.toLinearEquiv
38 
39 /-- The decomposition also applies to Mathlib's standard short-complex homology. -/
40 noncomputable def standardPacketEquiv {ι : Type w} [Fintype ι]
41     (C : Triple.{u,v} R) (P : Resolution C ι) :
42     (toShortComplex C).homology ≃ₗ[R] ⨁ i, H (packet (P.projectors i)) :=
43   (quotientHomologyEquiv C).trans (cohomologyPacketEquiv P)
44 
45 /-- A window from a genuine graded complex, with the library's endpoint convention. -/
46 noncomputable def window {κ : Type w} {c : ComplexShape κ}
47     (K : HomologicalComplex (ModuleCat.{v} R) c) (r : κ) : Triple.{u,v} R :=
48   ofShortComplex (K.sc r)
49 
50 /-- This checks the meaning of H^r for arbitrary shapes, including degrees 0,1,2. -/
51 noncomputable def gradedHomologyEquiv {κ : Type w} {c : ComplexShape κ}
52     (K : HomologicalComplex (ModuleCat.{v} R) c) (r : κ) :
53     K.homology r ≃ₗ[R] H (window K r) :=
54   standardHomologyEquiv (K.sc r)
55 
56 noncomputable def gradedPacketEquiv {κ ι : Type w} {c : ComplexShape κ} [Fintype ι]
57     (K : HomologicalComplex (ModuleCat.{v} R) c) (r : κ)
58     (P : Resolution (window K r) ι) :
59     K.homology r ≃ₗ[R] ⨁ i, H (packet (P.projectors i)) :=
60   (gradedHomologyEquiv K r).trans (cohomologyPacketEquiv P)
61 
62 /-- Over a field, finite-dimensional cohomologies have the expected sum of dimensions.
63 This is derived from the equivalence, not assumed as a substitute for it. -/
64 theorem dimension_sum {F : Type u} [Field F] {ι : Type w} [Fintype ι]
65     (C : Triple.{u,v} F) (P : Resolution C ι)
66     [∀ i, FiniteDimensional F (H (packet (P.projectors i)))] :
67     Module.finrank F (H C) = ∑ i, Module.finrank F (H (packet (P.projectors i))) := by
68   rw [(cohomologyPiEquiv P).finrank_eq, Module.finrank_pi_fintype]
69 
70 
71 /-- A morphism of genuine short complexes yields the corresponding cochain map. -/
72 def ofShortMap {S T : ShortComplex (ModuleCat.{v} R)} (f : S ⟶ T) :
73     ChainMap (ofShortComplex S) (ofShortComplex T) where
74   left := f.τ₁.hom
75   middle := f.τ₂.hom
76   right := f.τ₃.hom
77   comm₀ := ModuleCat.hom_ext_iff.mp f.comm₁₂
78   comm₁ := ModuleCat.hom_ext_iff.mp f.comm₂₃
79 
80 /-- Restrict a genuine chain endomorphism to the selected window. -/
81 noncomputable def windowMap {κ : Type w} {c : ComplexShape κ}
82     (K : HomologicalComplex (ModuleCat.{v} R) c) (r : κ) (p : K ⟶ K) :
83     ChainMap (window K r) (window K r) :=
84   ofShortMap ((HomologicalComplex.shortComplexFunctor _ c r).map p)
85 
86 /-- The image at every degree, with its restricted differential, is a genuine
87 Mathlib HomologicalComplex, not only a three-term stand-in. -/
88 def imageComplex {κ : Type w} {c : ComplexShape κ}
89     (K : HomologicalComplex (ModuleCat.{v} R) c) (p : K ⟶ K) :
90     HomologicalComplex (ModuleCat.{v} R) c where
91   X i := ModuleCat.of R (LinearMap.range (p.f i).hom)
92   d i j := ModuleCat.ofHom (rangeMap (K.d i j).hom (p.f i).hom (p.f j).hom
93     (ModuleCat.hom_ext_iff.mp (p.comm i j)))
94   shape := by
95     intro i j hij
96     apply ModuleCat.hom_ext
97     apply LinearMap.ext
98     intro x
99     apply Subtype.ext
100     change (K.d i j).hom x.val = 0
101     rw [K.shape i j hij]
102     rfl
103   d_comp_d' := by
104     intro i j k _ _
105     apply ModuleCat.hom_ext
106     apply LinearMap.ext
107     intro x
108     apply Subtype.ext
109     exact LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (K.d_comp_d i j k)) x.val
110 
111 noncomputable def imageHomologyEquiv {κ : Type w} {c : ComplexShape κ}
112     (K : HomologicalComplex (ModuleCat.{v} R) c) (r : κ) (p : K ⟶ K) :
113     (imageComplex K p).homology r ≃ₗ[R] H (packet (windowMap K r p)) :=
114   standardHomologyEquiv ((imageComplex K p).sc r)
115 
116 /-- Build the window resolution directly from actual chain endomorphisms. -/
117 noncomputable def chainResolution {κ ι : Type w} {c : ComplexShape κ} [Fintype ι]
118     (K : HomologicalComplex (ModuleCat.{v} R) c) (r : κ) (P : ι → (K ⟶ K))
119     (hid : ∀ i, ((P i).f r).hom.comp ((P i).f r).hom = ((P i).f r).hom)
120     (hort : ∀ i j, i ≠ j → ((P i).f r).hom.comp ((P j).f r).hom = 0)
121     (hsum : ∑ i, ((P i).f r).hom = LinearMap.id) : Resolution (window K r) ι where
122   projectors i := windowMap K r (P i)
123   idempotent := hid
124   orthogonal := hort
125   complete := hsum
126 
127 /-- The literal manuscript statement using Mathlib's genuine graded complexes
128 and its standard homology objects on BOTH sides. -/
129 noncomputable def chainCohomologyPacketEquiv {κ ι : Type w} {c : ComplexShape κ} [Fintype ι]
130     (K : HomologicalComplex (ModuleCat.{v} R) c) (r : κ) (P : ι → (K ⟶ K))
131     (hid : ∀ i, ((P i).f r).hom.comp ((P i).f r).hom = ((P i).f r).hom)
132     (hort : ∀ i j, i ≠ j → ((P i).f r).hom.comp ((P j).f r).hom = 0)
133     (hsum : ∑ i, ((P i).f r).hom = LinearMap.id) :
134     K.homology r ≃ₗ[R] ⨁ i, (imageComplex K (P i)).homology r :=
135   (gradedHomologyEquiv K r).trans
136     ((cohomologyPiEquiv (chainResolution K r P hid hort hsum)).trans
137       ((LinearEquiv.piCongrRight (fun i => (imageHomologyEquiv K r (P i)).symm)).trans
138         (DirectSum.linearEquivFunOnFintype R ι
139           (fun i => (imageComplex K (P i)).homology r)).symm))
140 
141 end PaperX.ComplexCohomology

Back to source controls