toCoalgHom_injective — Mathlib

English

For any R, and any V,W in CoalgCat R, the map from morphisms V ⟶ W to their internal CoalgHom representation is injective.

Русский

Для любых V,W в CoalgCat R отображение морфизмов V ⟶ W в их внутреннее представление CoalgHom инъективно.

LaTeX

$$$\\text{toCoalgHom'} : \\mathrm{Hom}(V,W) \\to _$ isInjective$$

Lean4

theorem toCoalgHom_injective (V W : CoalgCat.{v} R) : Function.Injective (Hom.toCoalgHom' : Hom V W → _) :=
  fun ⟨f⟩ ⟨g⟩ _ => by congr

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