isLocallySurjective_of_le — Mathlib

English

Let J and K be Grothendieck topologies on a category C with J ≤ K. If a morphism f of presheaves F → G is locally surjective with respect to J, then f is locally surjective with respect to K.

Русский

Пусть J и K — топологии Гротендик на категорию C such that J ≤ K. Если морфизм f между прешафами F → G локально сюръективен по J, то он локально сюръективен по K.

LaTeX

$$$J \le K \Rightarrow IsLocallySurjective_J(f) \Rightarrow IsLocallySurjective_K(f)$$$

Lean4

theorem isLocallySurjective_of_le {K : GrothendieckTopology C} (hJK : J ≤ K) {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G)
    (h : IsLocallySurjective J f) : IsLocallySurjective K f where imageSieve_mem s := by apply hJK; exact h.1 _

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