isLocallySurjective_presheafToSheaf_map_iff

English

Analogous to injectivity, the local surjectivity of a presheaf morphism φ: P → Q is equivalent to the local surjectivity of its image under presheaf-to-sheaf transformation.

Русский

Аналогично локальной сюръективности, локальная сюръективность отображения презпеша φ: P → Q эквивалентна локальной сюръективности после преобразованияPresheaf→Sheaf.

LaTeX

$$$\text{Presheaf.IsLocallySurjective}(J,φ) \iff \text{Sheaf.IsLocallySurjective}((presheafToSheaf\,J\,A).map\,φ)$$$

Lean4

theorem isLocallySurjective_presheafToSheaf_map_iff :
    Sheaf.IsLocallySurjective ((presheafToSheaf J A).map φ) ↔ IsLocallySurjective J φ := by
  rw [← Sheaf.isLocallySurjective_sheafToPresheaf_map_iff, ← isLocallySurjective_comp_iff J _ (toSheafify J Q), ←
    comp_isLocallySurjective_iff J (toSheafify J P), toSheafify_naturality, sheafToPresheaf_map]

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