English
For any C and X, applying the inverse of the correspondence from fromSingle₀Equiv to a morphism f with the property hf (f ≫ d0 1 = 0) yields a 0-component equal to f.
Русский
Пусть C и X заданы; применение обращения соответствия fromSingle₀Equiv к f, удовлетворяющему hf, даёт нулевой компонент, равный f.
LaTeX
$$$((\\mathrm{fromSingle}_0^{\\mathrm{Equiv}} C X)^{-1} \\langle f, hf \\rangle)_0 = f$$$
Lean4
/-- Morphisms from a single object cochain complex with `X` concentrated in degree 0
to an `ℕ`-indexed cochain complex `C`
are the same as morphisms `f : X ⟶ C.X 0` such that `f ≫ C.d 0 1 = 0`. -/
@[simps apply_coe]
noncomputable def fromSingle₀Equiv (C : CochainComplex V ℕ) (X : V) :
((single₀ V).obj X ⟶ C) ≃ { f : X ⟶ C.X 0 // f ≫ C.d 0 1 = 0 }
where
toFun φ := ⟨φ.f 0, by rw [φ.comm 0 1, HomologicalComplex.single_obj_d, zero_comp]⟩
invFun
f :=
HomologicalComplex.mkHomFromSingle f.1
(fun i hi => by
obtain rfl : i = 1 := by simpa using hi.symm
exact f.2)
left_inv φ := by cat_disch
right_inv := by cat_disch
