CohomologyExamples.lean

1 import PaperX.ComplexCohomology
2 import PaperX.PacketNaturality
3 import Mathlib.Data.ZMod.Basic
4 
5 /-!
6 Concrete nonzero-differential examples and negative-boundary witnesses.
7 The example is supplied here, not claimed to be the unretrieved original script.
8 -/
9 set_option autoImplicit false
10 namespace PaperX.CohomologyExamples
11 
12 open PaperX.Cohomology PaperX.PacketCohomology PaperX.ComplexCohomology
13 open scoped BigOperators
14 
15 instance primeFive : Fact (Nat.Prime 5) := ⟨by decide⟩
16 
17 variable (R : Type*) [CommRing R]
18 
19 /-- The first summand of R x R. -/
20 def firstPair : (R × R) →ₗ[R] R × R := (LinearMap.fst R R R).prod 0
21 
22 def lastPair : (R × R) →ₗ[R] R × R := (0 : (R × R) →ₗ[R] R).prod (LinearMap.snd R R R)
23 
24 /-- One exact packet R -> R^2 -> R and one zero-differential packet of sizes (1,2,1). -/
25 abbrev exampleComplex : Triple R where
26   X₀ := R × R
27   X₁ := (R × R) × (R × R)
28   X₂ := R × R
29   d₀ := (firstPair R).prod 0
30   d₁ := ((LinearMap.snd R R R).comp (LinearMap.fst R (R × R) (R × R))).prod 0
31   square := by apply LinearMap.ext; intro x; rfl
32 
33 def firstPacket : ChainMap (exampleComplex R) (exampleComplex R) where
34   left := firstPair R
35   middle := (LinearMap.fst R (R × R) (R × R)).prod 0
36   right := firstPair R
37   comm₀ := by apply LinearMap.ext; intro x; rfl
38   comm₁ := by apply LinearMap.ext; intro x; rfl
39 
40 def lastPacket : ChainMap (exampleComplex R) (exampleComplex R) where
41   left := lastPair R
42   middle := (0 : ((R × R) × (R × R)) →ₗ[R] R × R).prod (LinearMap.snd R (R × R) (R × R))
43   right := lastPair R
44   comm₀ := by apply LinearMap.ext; intro x; rfl
45   comm₁ := by apply LinearMap.ext; intro x; rfl
46 
47 def exampleResolution : Resolution (exampleComplex R) Bool where
48   projectors := fun b => if b then lastPacket R else firstPacket R
49   idempotent := by
50     intro i
51     cases i <;> apply LinearMap.ext <;> intro x <;> rfl
52   orthogonal := by
53     intro i j h
54     cases i <;> cases j <;> try contradiction
55     all_goals apply LinearMap.ext; intro x; rfl
56   complete := by
57     apply LinearMap.ext
58     intro x
59     change (∑ b : Bool, ((if b then lastPacket R else firstPacket R).middle)) x = x
60     simp only [Fintype.sum_bool, Bool.false_eq_true, ite_false, ite_true]
61     change ((0,0),x.2) + (x.1,(0,0)) = x
62     exact Prod.ext (by simp) (by simp)
63 
64 /-- A literal kernel cocycle with free coordinates (a,b). -/
65 def freeCycle (x : R × R) : Cycles (exampleComplex R) := ⟨((0,0),x), rfl⟩
66 
67 def freeCycles : (R × R) →ₗ[R] Cycles (exampleComplex R) where
68   toFun := freeCycle R
69   map_add' := by
70     intro x y
71     apply Subtype.ext
72     change ((0,0),x+y) = ((0,0),x) + ((0,0),y)
73     simp
74   map_smul' := by
75     intro a x
76     apply Subtype.ext
77     change ((0,0),a • x) = a • ((0,0),x)
78     simp
79 
80 def readCycle : Cycles (exampleComplex R) →ₗ[R] R × R :=
81   (LinearMap.snd R (R × R) (R × R)).comp (Cycles (exampleComplex R)).subtype
82 
83 def readCohomology : H (exampleComplex R) →ₗ[R] R × R :=
84   (boundaries (exampleComplex R)).liftQ (readCycle R) (by
85     rintro x ⟨y,rfl⟩
86     rfl)
87 
88 /-- This explicit quotient isomorphism checks a genuinely nonzero cohomology example. -/
89 def exampleCohomologyEquiv : H (exampleComplex R) ≃ₗ[R] R × R where
90   toLinearMap := readCohomology R
91   invFun := fun x => classOf (exampleComplex R) (freeCycle R x)
92   left_inv := by
93     intro z
94     obtain ⟨x,rfl⟩ := classOf_surjective (exampleComplex R) z
95     change classOf (exampleComplex R) (freeCycle R x.val.2) = classOf (exampleComplex R) x
96     apply sub_eq_zero.mp
97     rw [← map_sub, classOf_eq_zero_iff]
98     refine ⟨(-x.val.1.1,0), ?_⟩
99     have hx : x.val.1.2 = 0 := congrArg Prod.fst x.property
100     change ((-x.val.1.1,0),(0,0)) = ((0,0),x.val.2) - x.val
101     ext <;> simp [hx]
102   right_inv := by intro x; rfl
103 
104 /-- The displayed middle cohomology has dimension two over F_5. -/
105 theorem example_h1_dimension :
106     Module.finrank (ZMod 5) (H (exampleComplex (ZMod 5))) = 2 := by
107   rw [(exampleCohomologyEquiv (ZMod 5)).finrank_eq]
108   rw [Module.finrank_prod]
109   simp
110 
111 /-- An obstruction coordinate is not removed by the fact that decomposition exists. -/
112 theorem example_class_nonzero :
113     classOf (exampleComplex (ZMod 5)) (freeCycle (ZMod 5) (1,0)) ≠ 0 := by
114   intro h
115   have hh := congrArg (readCohomology (ZMod 5)) h
116   change (1,0) = ((0,0) : ZMod 5 × ZMod 5) at hh
117   have hz := congrArg Prod.fst hh
118   exact one_ne_zero hz
119 
120 /-- Complementary idempotents that do not preserve the differential can destroy cocycles. -/
121 def badProjector : (ZMod 5 × ZMod 5) →ₗ[ZMod 5] ZMod 5 × ZMod 5 :=
122   (LinearMap.fst (ZMod 5) (ZMod 5) (ZMod 5)).prod (LinearMap.fst (ZMod 5) (ZMod 5) (ZMod 5))
123 
124 theorem badProjector_idempotent : badProjector.comp badProjector = badProjector := by
125   apply LinearMap.ext
126   intro x
127   rfl
128 
129 theorem badProjector_complement : badProjector + (LinearMap.id - badProjector) = LinearMap.id := by
130   abel
131 
132 theorem badProjector_orthogonal : badProjector.comp (LinearMap.id - badProjector) = 0 := by
133   rw [LinearMap.comp_sub, LinearMap.comp_id, badProjector_idempotent, sub_self]
134 
135 theorem badProjector_breaks_cycle :
136     (LinearMap.snd (ZMod 5) (ZMod 5) (ZMod 5)) (1,0) = 0 ∧
137     (LinearMap.snd (ZMod 5) (ZMod 5) (ZMod 5)) (badProjector (1,0)) ≠ 0 := by
138   constructor
139   · rfl
140   · change (1 : ZMod 5) ≠ 0
141     decide
142 
143 /-- With outgoing differential zero, the same projector can instead destroy boundaries. -/
144 theorem badProjector_breaks_boundary :
145     ((1,0) : ZMod 5 × ZMod 5) ∈ LinearMap.range (firstPair (ZMod 5)) ∧
146     badProjector (1,0) ∉ LinearMap.range (firstPair (ZMod 5)) := by
147   constructor
148   · exact ⟨(1,0),rfl⟩
149   · rintro ⟨x,hx⟩
150     have hz := congrArg Prod.snd hx
151     change (0 : ZMod 5) = 1 at hz
152     exact zero_ne_one hz
153 
154 end PaperX.CohomologyExamples

Back to source controls