isLocallySurjective_iff — Mathlib

English

In the extensive topology, surjectivity is controlled by local data given by sieve coverings.

Русский

В экстендитной топологии сюръективность определяется локальными данными, задаваемыми сверху рассыпи.

LaTeX

$$$\text{Surjective in extensive topology via sieve coverings}$$$

Lean4

theorem isLocallySurjective_iff [FinitaryExtensive C] {F G : Sheaf (extensiveTopology C) D} (f : F ⟶ G)
    [PreservesFiniteProducts (forget D)] : IsLocallySurjective f ↔ ∀ (X : C), Function.Surjective (f.val.app (op X)) :=
  extensiveTopology.presheafIsLocallySurjective_iff _ f.val

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