etaIso

Mathlib.CategoryTheory.Products.Basic

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

English

The etaIso isomorphism between (X.1, X.2) and X is canonical.

Русский

Изоморфизм etaIso между (X.1, X.2) и X каноничен.

LaTeX

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

Lean4

/-- The isomorphism between `(X.1, X.2)` and `X`. -/
@[simps]
def etaIso (X : C × D) : (X.1, X.2) ≅ X where
  hom := (𝟙 _, 𝟙 _)
  inv := (𝟙 _, 𝟙 _)

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

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

Разделы

Аффилиация

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