instIsLocallySurjectiveHomObjForgetTypeToRangeSheafify

English

Let f1: F1 → F2 and f2: F2 → F3 be morphisms of presheaves such that f2 is locally injective and f2 is locally surjective. Then f1 ≫ f2 is locally surjective iff f1 is locally surjective.

Русский

Пусть f1: F1 → F2 и f2: F2 → F3 — морфизмы прешафов, f2 локально инъективен и локально сюръективен. Тогда f1 ≫ f2 локально сюръективен тогда и только тогда, когда f1 локально сюръективен.

LaTeX

$$IsLocallyInjective_J(f2) ∧ IsLocallySurjective_J(f2) ⇒ (IsLocallySurjective_J(f1 ≫ f2) ⇔ IsLocallySurjective_J(f1))$$

Lean4

instance {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) : IsLocallySurjective J (Subpresheaf.toRangeSheafify J f) where
  imageSieve_mem
    {X} := by
    rintro ⟨s, hs⟩
    refine J.superset_covering ?_ hs
    rintro Y g ⟨t, ht⟩
    exact ⟨t, Subtype.ext ht⟩

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