English
For two morphisms φ1, φ2: F ⟶ G, the data of a homotopy between them is equivalent to the data of a 1-cochain z with the relation φ1 = δ(-1)0 z + φ2, implemented as an additive equivalence.
Русский
Для двух морфизмов φ1, φ2: F ⟶ G данные гомотопии между ними эквивалентны данным 1-кокомпинирующего z, удовлетворяющим relation φ1 = δ(-1)0 z + φ2, образуя аддитивную эквивалентность.
LaTeX
$$$\\text{equivHomotopy}(\\phi_1,\\phi_2):\\mathrm{Homotopy}(\\phi_1,\\phi_2) \\cong \\{ z:\\mathrm{Cochain}(F,G,-1) \\mid \\mathrm{Cochain.ofHom}(\\phi_1)=\\delta(-1)0 z+\\mathrm{Cochain.ofHom}(\\phi_2) \\}.$$$
Lean4
/-- Given two morphisms of complexes `φ₁ φ₂ : F ⟶ G`, the datum of an homotopy between `φ₁` and
`φ₂` is equivalent to the datum of a `1`-cochain `z` such that `δ (-1) 0 z` is the difference
of the zero cochains associated to `φ₂` and `φ₁`. -/
@[simps]
def equivHomotopy (φ₁ φ₂ : F ⟶ G) :
Homotopy φ₁ φ₂ ≃ { z : Cochain F G (-1) // Cochain.ofHom φ₁ = δ (-1) 0 z + Cochain.ofHom φ₂ }
where
toFun ho := ⟨Cochain.ofHomotopy ho, by simp only [δ_ofHomotopy, sub_add_cancel]⟩
invFun
z :=
{ hom := fun i j => if hij : i + (-1) = j then z.1.v i j hij else 0
zero := fun i j (hij : j + 1 ≠ i) => dif_neg (fun _ => hij (by omega))
comm := fun p => by
have eq := Cochain.congr_v z.2 p p (add_zero p)
have h₁ : (ComplexShape.up ℤ).Rel (p - 1) p := by simp
have h₂ : (ComplexShape.up ℤ).Rel p (p + 1) := by simp
simp only [δ_neg_one_cochain, Cochain.ofHom_v, ComplexShape.up_Rel, Cochain.add_v,
Homotopy.nullHomotopicMap'_f h₁ h₂] at eq
rw [dNext_eq _ h₂, prevD_eq _ h₁, eq, dif_pos, dif_pos] }
left_inv := fun ho => by
ext i j
dsimp
split_ifs with h
· rfl
· rw [ho.zero i j (fun h' => h (by dsimp at h'; omega))]
right_inv := fun z => by
ext p q hpq
dsimp [Cochain.ofHomotopy]
rw [dif_pos hpq]
