homEquiv_eq

Mathlib.CategoryTheory.Adjunction.Parametrized

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ParametrizedAdjunction.homEquiv_eq

English

The parametrized hom-equivalence specializes to the usual hom-equivalence of the given adjunction.

Русский

Параметризованное гом-эквивалентность сводится к обычной гом-эквивалентности данного сопряжения.

LaTeX

$$$\\text{adj}_2.homEquiv = (\\text{adj}_2.adj } X_1).homEquiv X_2 X_3$$$

Lean4

theorem homEquiv_eq : adj₂.homEquiv = (adj₂.adj X₁).homEquiv X₂ X₃ :=
  rfl

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

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

Разделы

Аффилиация

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