English
Dual Ext lemma: equality γ1 = γ2 of cochains in mapping cone is equivalent to equality after precomposing with inl φ and postcomposing with inr φ.
Русский
Двойственное лемме Ext: равенство κ1=κ2 коцепей в конусе хранения эквивалентно равенству после префиксации inl φ и постфиксации inr φ.
LaTeX
$$$\\forall i,j:\\ hij: i+1=j:\\ γ1=γ2 \\iff (inl φ).comp γ1 (show _ = i by cutsat) = (inl φ).comp γ2 (by cutsat) \\land (Cochain.ofHom (inr φ)).comp γ1 (zero_add j) = (Cochain.ofHom (inr φ)).comp γ2 (zero_add j).$$$
Lean4
theorem ext_cochain_from_iff (i j : ℤ) (hij : i + 1 = j) {K : CochainComplex C ℤ}
{γ₁ γ₂ : Cochain (mappingCone φ) K j} :
γ₁ = γ₂ ↔
(inl φ).comp γ₁ (show _ = i by cutsat) = (inl φ).comp γ₂ (by cutsat) ∧
(Cochain.ofHom (inr φ)).comp γ₁ (zero_add j) = (Cochain.ofHom (inr φ)).comp γ₂ (zero_add j) :=
by
constructor
· rintro rfl
tauto
· rintro ⟨h₁, h₂⟩
ext p q hpq
rw [ext_from_iff φ (p + 1) p rfl]
replace h₁ := Cochain.congr_v h₁ (p + 1) q (by cutsat)
replace h₂ := Cochain.congr_v h₂ p q (by cutsat)
simp only [Cochain.comp_v (inl φ) _ _ (p + 1) p q (by cutsat) hpq] at h₁
simp only [Cochain.zero_cochain_comp_v, Cochain.ofHom_v] at h₂
exact ⟨h₁, h₂⟩
