isLocallySurjective_toPlus — Mathlib

English

For presheaves F1 → F2 valued in Type w, the map toRangeSheafify J f is locally surjective.

Русский

Для прешафов F1 → F2 величиной в Type w отображение toRangeSheafify J f локально сюръективно.

LaTeX

$$IsLocallySurjective_J(Subpresheaf.toRangeSheafify J f)$$

Lean4

instance isLocallySurjective_toPlus (P : Cᵒᵖ ⥤ Type max u v) : IsLocallySurjective J (J.toPlus P) where
  imageSieve_mem
    x := by
    obtain ⟨S, x, rfl⟩ := exists_rep x
    refine J.superset_covering (fun Y f hf => ⟨x.1 ⟨Y, f, hf⟩, ?_⟩) S.2
    dsimp
    rw [toPlus_eq_mk, res_mk_eq_mk_pullback, eq_mk_iff_exists]
    refine ⟨S.pullback f, homOfLE le_top, 𝟙 _, ?_⟩
    ext ⟨Z, g, hg⟩
    simpa using x.2 { fst.hf := hf, snd.hf := S.1.downward_closed hf g, r.g₁ := g, r.g₂ := 𝟙 Z, .. }

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