instSubcanonicalCanonicalTopology

Mathlib.CategoryTheory.Sites.Canonical

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.instSubcanonicalCanonicalTopology

English

If J is subcanonical, then every representable functor is a J-sheaf.

Русский

Если J субканонична, то любой представимый функтор является J-шейфом.

LaTeX

$$$\\text{Subcanonical}(J) \\Rightarrow \\mathrm{IsSheaf}(J, P)$ для каждого P, representable$$

Lean4

instance : (canonicalTopology C).Subcanonical where le_canonical := le_rfl

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

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

Разделы

Аффилиация

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