instIsLocallySurjectiveToSheafify

Mathlib.CategoryTheory.Sites.LocallyBijective

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

English

The map toSheafify J P is locally surjective.

Русский

Отображение toSheafify J P локально сюръективно.

LaTeX

$$[HasWeakSheafify J D] ⇒ Presheaf.IsLocallySurjective J (\mathrm{toSheafify}(J, P))$$

Lean4

instance : Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P) :=
  (J.W_toSheafify P).isLocallySurjective

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

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

Разделы

Аффилиация

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