isLocallySurjective_of_surjective

English

If for every object U, the map f.app U is surjective, then f is locally surjective with respect to J.

Русский

Если для каждого объекта U отображение f.app U сюрьективно, то f локально сюрьективно относительно J.

LaTeX

$$$\forall U, \mathrm{Surjective}(f_{\mathrm{app} U}) \Rightarrow \text{IsLocallySurjective}_J(f)$$$

Lean4

theorem isLocallySurjective_of_surjective {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) (H : ∀ U, Function.Surjective (f.app U)) :
    IsLocallySurjective J f where
  imageSieve_mem {U}
    s := by
    obtain ⟨t, rfl⟩ := H _ s
    rw [imageSieve_app]
    exact J.top_mem _

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