English
For cochains γ1, γ2 with γ1 = γ2, their fst and snd projections agree; conversely, equality of projections implies γ1 = γ2.
Русский
Для коцепей γ1, γ2 верно: γ1=γ2 тогда и только тогда, когда их fst- и snd-проекции совпадают.
LaTeX
$$$\\forall i,j:\\ hij: i+1=j:\\ γ1=γ2\\iff (γ1\\circ (fst φ)_{i,j,hij})=(γ2\\circ (fst φ)_{i,j,hij})\\land (γ1\\circ (snd φ)_{i,i})=(γ2\\circ (snd φ)_{i,i}).$$$
Lean4
theorem ext_cochain_to_iff (i j : ℤ) (hij : i + 1 = j) {K : CochainComplex C ℤ} {γ₁ γ₂ : Cochain K (mappingCone φ) i} :
γ₁ = γ₂ ↔
γ₁.comp (fst φ).1 hij = γ₂.comp (fst φ).1 hij ∧ γ₁.comp (snd φ) (add_zero i) = γ₂.comp (snd φ) (add_zero i) :=
by
constructor
· rintro rfl
tauto
· rintro ⟨h₁, h₂⟩
ext p q hpq
rw [ext_to_iff φ q (q + 1) rfl]
replace h₁ := Cochain.congr_v h₁ p (q + 1) (by cutsat)
replace h₂ := Cochain.congr_v h₂ p q hpq
simp only [Cochain.comp_v _ _ _ p q (q + 1) hpq rfl] at h₁
simp only [Cochain.comp_zero_cochain_v] at h₂
exact ⟨h₁, h₂⟩
