isLocallySurjective_toSheafify — Mathlib

English

If P is a presheaf and J is a Grothendieck topology, then P under sheafification is locally surjective.

Русский

Пусть P — прешаф, J — топология Гротендик; переход к шейфайфикации сохраняет локальную сюръективность.

LaTeX

$$IsLocallySurjective_J(J.toSheafify P)$$

Lean4

instance isLocallySurjective_toSheafify (P : Cᵒᵖ ⥤ Type max u v) : IsLocallySurjective J (J.toSheafify P) :=
  by
  dsimp [GrothendieckTopology.toSheafify]
  rw [GrothendieckTopology.plusMap_toPlus]
  infer_instance

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