isLocallyInjective_of_injective — Mathlib

English

Analogous statement for surjectivity: the local surjectivity of φ is equivalent to that of its presheaf-to-sheaf image.

Русский

Аналогично по сюръективности: локальная сюръективность φ эквивалентна локальной сюръективности образа φ после преобразования presheaf→sheaf.

LaTeX

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

Lean4

theorem isLocallyInjective_of_injective (hφ : ∀ (X : Cᵒᵖ), Function.Injective (φ.app X)) : IsLocallyInjective J φ where
  equalizerSieve_mem {X} x y
    h := by
    convert J.top_mem X.unop
    ext Y f
    simp only [equalizerSieve_apply, op_unop, Sieve.top_apply, iff_true]
    apply hφ
    simp [h]

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