reflective

Mathlib.AlgebraicTopology.SimplicialObject.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SimplicialObject.Truncated.coskAdj.reflective

English

There is a reflective structure for coskAdj, i.e. the coskeleton adjunction is reflective.

Русский

Существует отражающая структура для coskAdj, то есть сопряжение коскелетона отражающее.

LaTeX

$$$$ \\mathrm{coskAdj}.\\mathrm{reflective} $$$$

Lean4

noncomputable instance reflective : Reflective (Truncated.cosk (C := C) n) :=
  Reflective.mk (truncation _) (coskAdj _)

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

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

Разделы

Аффилиация

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