Detecting sheaf isomorphisms on a basis

A morphism of sheaves on a topological space is an isomorphism when its components are isomorphisms on a basis of opens. The proof completes Mathlib's basiswise injectivity result with the matching surjectivity statement, then detects the isomorphism on stalks.

These results are topological sheaf theory: their signatures require a topological space, its opens, a basis, germs, and stalk functors, but no scheme.

Main results

• TopCat.Presheaf.stalkFunctor_map_surjective_of_isBasis — surjectivity on a basis implies surjectivity on every stalk;
• TopCat.Sheaf.isIso_of_isIso_app_of_isBasis — a sheaf morphism that is an isomorphism on a basis is an isomorphism.

theorem TopCat.Presheaf.stalkFunctor_map_surjective_of_isBasis {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] {B : Set (TopologicalSpace.Opens ↑X)} (hB : TopologicalSpace.Opens.IsBasis B) {F G : Presheaf C X} {α : F ⟶ G} (hα : ∀ U ∈ B, Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op U)))) (x : ↑X) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((stalkFunctor C x).map α))

Surjectivity on stalks may be checked on a basis.

The mirror image of Mathlib's stalkFunctor_map_injective_of_isBasis: every germ is represented by a section over a basic open (germ_exist_of_isBasis), and a surjection there lifts it.

theorem TopCat.Sheaf.isIso_of_isIso_app_of_isBasis {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms] {B : Set (TopologicalSpace.Opens ↑X)} (hB : TopologicalSpace.Opens.IsBasis B) {F G : Sheaf C X} (α : F ⟶ G) (hα : ∀ U ∈ B, CategoryTheory.IsIso (α.hom.app (Opposite.op U))) : CategoryTheory.IsIso α

A morphism of sheaves that is an isomorphism on a basis is an isomorphism.

Checked on stalks: injectivity is Mathlib's stalkFunctor_map_injective_of_isBasis and surjectivity is stalkFunctor_map_surjective_of_isBasis above.

The hypotheses are written out rather than taken from a variable block: FC and CC do not appear in the statement, so variable auto-inclusion drops the ConcreteCategory and forget-preservation binders along with them.