toSingle₀Equiv_symm_apply_f_zero

English

If f: C.X 0 → X satisfies the zero compatibility C.d 1 0 ≫ f = 0, then the 0th component of the inverse image of ⟨f, hf⟩ under the equivalence is exactly f.

Русский

Пусть f: C.X 0 → X удовлетворяет условию нулевого композиирования; тогда нулевой компонент образа через обратное отображение эквивалентности равен именно f.

LaTeX

$$$\left( (\mathrm{toSingle}_0\mathrm{Equiv}(C,X))^{-1} \langle f, hf\rangle \right)_{0} = f$$$

Lean4

@[simp]
theorem toSingle₀Equiv_symm_apply_f_zero {C : ChainComplex V ℕ} {X : V} (f : C.X 0 ⟶ X) (hf : C.d 1 0 ≫ f = 0) :
    ((toSingle₀Equiv C X).symm ⟨f, hf⟩).f 0 = f := by simp [toSingle₀Equiv]

Похожие утверждения