hom_ext

Mathlib.CategoryTheory.Products.Basic

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

English

There is a canonical isomorphism between any pair (X.fst, X.snd) and X in a product category.

Русский

В произведении существует каноническое изоморфизм между парой (X.fst, X.snd) и X.

LaTeX

$$$\eta\mathrm{Iso}(X): (X.1,X.2) \cong X$$$

Lean4

@[ext]
theorem hom_ext {X Y : C × D} {f g : X ⟶ Y} (h₁ : f.1 = g.1) (h₂ : f.2 = g.2) : f = g :=
  by
  dsimp
  ext <;> assumption

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

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

Разделы

Аффилиация

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