to_single_hom_ext — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[ext]
theorem to_single_hom_ext {K : HomologicalComplex V c} {j : ι} {A : V} {f g : K ⟶ (single V c j).obj A}
    (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_tgt

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