hom_ext

Mathlib.CategoryTheory.Galois.Prorepresentability

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreGaloisCategory.PointedGaloisObject.hom_ext

English

Morphisms between pointed Galois objects are determined by their underlying values.

Русский

Опорные морфизмы между отмеченными Галуа-объектами определяются по их значениям.

LaTeX

$$$f.val = g.val \\Rightarrow f = g$$$

Lean4

@[ext]
theorem hom_ext {A B : PointedGaloisObject F} {f g : A ⟶ B} (h : f.val = g.val) : f = g :=
  Hom.ext h

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

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

Разделы

Аффилиация

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