hom_ext — Mathlib

English

If two morphisms f and g have the same underlying hom, then f = g; i.e., morphisms in SemiRingCat are determined by their hom components.

Русский

Если два морфизма f и g имеют одинаковый базовый гомоморфизм, то f = g; то есть морфизмы в SemiRingCat определяются по их компонентам гомоморфизма.

LaTeX

$$$ f.\mathrm{hom} = g.\mathrm{hom} \Rightarrow f = g. $$$

Lean4

@[ext]
theorem hom_ext {R S : SemiRingCat} {f g : R ⟶ S} (hf : f.hom = g.hom) : f = g :=
  Hom.ext hf

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