isLocallyInjective_presheafToSheaf_map_iff

English

For presheaves P, Q valued in A and a morphism φ: P → Q, the local injectivity of φ is equivalent to the local injectivity of the corresponding map after applying presheaf-to-sheaf transformation, i.e., a map is locally injective if and only if its presheaf-to-sheaf image is locally injective.

Русский

Для презпешев P, Q и преобразования φ: P → Q локальная инъективность φ эквивалентна локальной инъективности отображения после преобразования presheaf→sheaf.

LaTeX

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

Lean4

theorem isLocallyInjective_presheafToSheaf_map_iff :
    Sheaf.IsLocallyInjective ((presheafToSheaf J A).map φ) ↔ IsLocallyInjective J φ := by
  rw [← Sheaf.isLocallyInjective_sheafToPresheaf_map_iff, ← isLocallyInjective_comp_iff J _ (toSheafify J Q), ←
    comp_isLocallyInjective_iff J (toSheafify J P), toSheafify_naturality, sheafToPresheaf_map]

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