hom_ext

Mathlib.Algebra.Category.ModuleCat.Sheaf

URI: https://scilib.ai/kg/mathlib#SheafOfModules.hom_ext

English

Extensionality for morphisms in SheafOfModules: a morphism is determined by its values.

Русский

Расширение гомоморфизмов: морфизм задаётся значениями.

LaTeX

$$$\operatorname{ext}\;\mathrm{Hom} = \mathrm{Hom}$$$

Lean4

@[ext]
theorem hom_ext {X Y : SheafOfModules.{v} R} {f g : X ⟶ Y} (h : f.val = g.val) : f = g :=
  Hom.ext h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru