sheafification_reflective

Mathlib.CategoryTheory.Sites.Sheafification

URI: https://scilib.ai/kg/mathlib#CategoryTheory.sheafification_reflective

English

The counit of the sheafification adjunction is a natural isomorphism.

Русский

Каунит adjunction кsheafification образует естественный изоморфизм.

LaTeX

$$$\\text{IsIso}\\left(\\mathrm{sheafificationAdjunction} J D\\right).\\mathrm{counit}$$$

Lean4

instance sheafification_reflective : IsIso (sheafificationAdjunction J D).counit :=
  NatIso.isIso_of_isIso_app _

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

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

Разделы

Аффилиация

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