fromSingle₀Equiv_symm_apply_f_zero

English

In the nat-indexed setting, the 0th component of the inverse image under the equivalence yields f.

Русский

В nat-индексированной настройке нулевая компонента образа под обратным отображением эквивалентности возвращает f.

LaTeX

$$$((\\mathrm{fromSingle}_0^{\\mathrm{Equiv}} C X)^{-1} f)_0 = f$$$

Lean4

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

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