instIsLocallyInjectiveToSheafify

Mathlib.CategoryTheory.Sites.LocallyBijective

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

English

The map toSheafify J P is locally injective.

Русский

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

LaTeX

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

Lean4

instance : Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P) :=
  (J.W_toSheafify P).isLocallyInjective

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

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

Разделы

Аффилиация

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