hom_ext — Mathlib

English

If two maps from the direct limit to P agree on all injections, then they are equal.

Русский

Если два отображения из прямого предела в P совпадают на всех инъекциях, то они равны.

LaTeX

$$$F_1|_{\iota_i(G_i)} = F_2|_{\iota_i(G_i)} \text{ for all } i \Rightarrow F_1=F_2$$$

Lean4

@[ext]
theorem hom_ext {g₁ g₂ : DirectLimit G f →+ P} (h : ∀ i, g₁.comp (of G f i) = g₂.comp (of G f i)) : g₁ = g₂ :=
  AddCon.hom_ext <| DirectSum.addHom_ext' h

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