hom_ext — Mathlib

English

In the category CoalgCat, two morphisms f,g: M ⟶ N are equal if their underlying CoalgHom are equal.

Русский

В категории CoalgCat два морфизма f,g: M ⟶ N равны, если их базовые CoalgHom совпадают.

LaTeX

$$$\\forall M,N: CoalgCat R,\\; f,g: M ⟶ N,\\; f.toCoalgHom = g.toCoalgHom \\Rightarrow f = g$$$

Lean4

@[ext]
theorem hom_ext {M N : CoalgCat.{v} R} (f g : M ⟶ N) (h : f.toCoalgHom = g.toCoalgHom) : f = g :=
  Hom.ext h

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