hom_ext — Mathlib

English

If two monoid homomorphisms f,g: PushoutI φ →* K agree on all of_i and on base φ, then f = g.

Русский

Если два моноид-хомоморфизма f,g: PushoutI φ →* K совпадают на каждом of_i и на базовом φ, то они равны.

LaTeX

$$If ∀ i, f ∘ of_i = g ∘ of_i and f ∘ base φ = g ∘ base φ, then f = g$$

Lean4

@[ext 1199]
theorem hom_ext {f g : PushoutI φ →* K} (h : ∀ i, f.comp (of i : G i →* _) = g.comp (of i : G i →* _))
    (hbase : f.comp (base φ) = g.comp (base φ)) : f = g :=
  (MonoidHom.cancel_right Con.mk'_surjective).mp <| Coprod.hom_ext (CoprodI.ext_hom _ _ h) hbase

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