hom_ext — Mathlib

English

Morphisms in the Core of a category are determined by their iso-hom component; equality of iso-homs implies equality of morphisms.

Русский

Гомоморфизмы в Core категории детерминированы по компонентам изоморфизмов; равенство гомоморфизмов отражается равенством их компонент-изоморфизмов.

LaTeX

$$$$ \forall \; {C}, \; X,Y \in \mathrm{Core}(C),\; f,g:\ X \to Y,\; f.iso.hom = g.iso.hom \Rightarrow f = g. $$$$

Lean4

@[ext]
theorem hom_ext {X Y : Core C} {f g : X ⟶ Y} (h : f.iso.hom = g.iso.hom) : f = g :=
  by
  apply CoreHom.ext
  exact Iso.ext h

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