from_single_hom_ext — Mathlib

English

Let K be a complex, j ∈ ι, A ∈ V, and f,g: (single V c j).obj A ⟶ K. If f.f j = g.f j then f = g.

Русский

Пусть K — комплекс, j ∈ ι, A ∈ V, и f,g: (single V c j).obj A ⟶ K. Если f.f j = g.f j, то f = g.

LaTeX

$$$$ f.f_j = g.f_j \Rightarrow f = g $$$$

Lean4

@[ext]
theorem from_single_hom_ext {K : HomologicalComplex V c} {j : ι} {A : V} {f g : (single V c j).obj A ⟶ K}
    (hfg : f.f j = g.f j) : f = g := by
  ext i
  by_cases h : i = j
  · subst h
    exact hfg
  · apply (isZero_single_obj_X c j A i h).eq_of_src

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