hom_f_injective — Mathlib

English

The map that sends a chain map f: K ⟶ L to its family of components (f.f i) is injective; equivalently, if f.f i = g.f i for all i, then f = g.

Русский

Отображение, отправляющее цепной отображатель f: K ⟶ L в его семейство компонент (f.f i), инъективно; эквивалентно, если f.f i = g.f i для всех i, то f = g.

LaTeX

$$$\\\\forall {K L} \\\\; (f,g : K \\\\longrightarrow L), \\\\; (\\\\forall i, f.f i = g.f i) \\\\Rightarrow f = g$$$

Lean4

theorem hom_f_injective {C₁ C₂ : HomologicalComplex V c} : Function.Injective fun f : Hom C₁ C₂ => f.f := by cat_disch

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