Locally surjective morphisms of coherent sheaves

This file characterises locally surjective morphisms of presheaves for the coherent, regular and extensive topologies.

Main results

• regularTopology.isLocallySurjective_iff A morphism of presheaves f : F ⟶ G is locally surjective for the regular topology iff for every object X of C, and every y : G(X), there is an effective epimorphism φ : X' ⟶ X and an x : F(X) such that f_{X'}(x) = G(φ)(y).

• coherentTopology.isLocallySurjective_iff a morphism of sheaves for the coherent topology on a preregular finitary extensive category is locally surjective if and only if it is locally surjective for the regular topology.

• extensiveTopology.isLocallySurjective_iff a morphism of sheaves for the extensive topology on a finitary extensive category is locally surjective iff it is objectwise surjective.

theorem CategoryTheory.regularTopology.isLocallySurjective_iff {C : Type u_1} (D : Type u_2) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Preregular C] {F G : CategoryTheory.Functor Cᵒᵖ D} (f : F ⟶ G) : CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.regularTopology C) f ↔ ∀ (X : C) (y : (CategoryTheory.forget D).obj (G.obj (Opposite.op X))), ∃ (X' : C) (φ : X' ⟶ X) (_ : CategoryTheory.EffectiveEpi φ) (x : (CategoryTheory.forget D).obj (F.obj (Opposite.op X'))), (f.app (Opposite.op X')) x = (G.map (Opposite.op φ)) y

theorem CategoryTheory.extensiveTopology.surjective_of_isLocallySurjective_sheafOfTypes {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.FinitaryPreExtensive C] {F G : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F ⟶ G) [CategoryTheory.Limits.PreservesFiniteProducts F] [CategoryTheory.Limits.PreservesFiniteProducts G] (h : CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.extensiveTopology C) f) {X : C} : Function.Surjective (f.app (Opposite.op X))

theorem CategoryTheory.extensiveTopology.presheafIsLocallySurjective_iff {C : Type u_1} (D : Type u_2) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.FinitaryPreExtensive C] {F G : CategoryTheory.Functor Cᵒᵖ D} (f : F ⟶ G) [CategoryTheory.Limits.PreservesFiniteProducts F] [CategoryTheory.Limits.PreservesFiniteProducts G] [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget D)] : CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.extensiveTopology C) f ↔ ∀ (X : C), Function.Surjective ⇑(f.app (Opposite.op X))

theorem CategoryTheory.extensiveTopology.isLocallySurjective_iff {C : Type u_1} (D : Type u_2) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.FinitaryExtensive C] {F G : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) D} (f : F ⟶ G) [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget D)] : CategoryTheory.Sheaf.IsLocallySurjective f ↔ ∀ (X : C), Function.Surjective ⇑(f.val.app (Opposite.op X))

theorem CategoryTheory.regularTopology.isLocallySurjective_sheafOfTypes {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preregular C] [CategoryTheory.FinitaryPreExtensive C] {F G : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F ⟶ G) [CategoryTheory.Limits.PreservesFiniteProducts F] [CategoryTheory.Limits.PreservesFiniteProducts G] (h : CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.coherentTopology C) f) : CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.regularTopology C) f

theorem CategoryTheory.coherentTopology.presheafIsLocallySurjective_iff {C : Type u_1} (D : Type u_2) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.ConcreteCategory D] {F G : CategoryTheory.Functor Cᵒᵖ D} (f : F ⟶ G) [CategoryTheory.Preregular C] [CategoryTheory.FinitaryPreExtensive C] [CategoryTheory.Limits.PreservesFiniteProducts F] [CategoryTheory.Limits.PreservesFiniteProducts G] [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget D)] : CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.coherentTopology C) f ↔ CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.regularTopology C) f

theorem CategoryTheory.coherentTopology.isLocallySurjective_iff {C : Type u_1} (D : Type u_2) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Preregular C] [CategoryTheory.FinitaryExtensive C] {F G : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) D} (f : F ⟶ G) [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget D)] : CategoryTheory.Sheaf.IsLocallySurjective f ↔ CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.regularTopology C) f.val