hom_ext — Mathlib

English

If two morphisms f, g: C ⟶ D between chain complexes have identical components at every index (i.e., f.f i = g.f i for all i), then f = g.

Русский

Если два морфизма f, g: C ⟶ D между цепными комплексами имеют одинаковые компоненты на каждом индексе (то есть f.f i = g.f i для всех i), то тогда f = g.

LaTeX

$$$\\\\forall C D \\\\; (f,g : C \\\\longrightarrow D), \\\\; (\\\\forall i, f.f i = g.f i) \\\\Rightarrow f = g$$$

Lean4

@[ext]
theorem hom_ext {C D : HomologicalComplex V c} (f g : C ⟶ D) (h : ∀ i, f.f i = g.f i) : f = g :=
  by
  apply Hom.ext
  funext
  apply h

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