uniq

Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.StructuredArrow.IsUniversal.uniq

English

There exists a unique morphism η making f.hom ≫ T.map η = g.hom, given an IsUniversal f.

Русский

Существуют единственные такие морфизмы η, что f.hom ≫ T.map η = g.hom, если f является универсальным.

LaTeX

$$$\\exists!\\eta: f.right \\to g.right,\\ f.hom \\circ T.map\\eta = g.hom$$$

Lean4

theorem uniq (h : IsUniversal f) (η : f ⟶ g) : η = h.to g :=
  h.hom_ext η (h.to g)

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

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

Разделы

Аффилиация

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