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) [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {FD : D → D → Type u_3} {CD : D → Type w} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] [Preregular C] {F G : Functor Cᵒᵖ D} (f : F ⟶ G) : Presheaf.IsLocallySurjective (regularTopology C) f ↔ ∀ (X : C) (y : ToType (G.obj (Opposite.op X))), ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : ToType (F.obj (Opposite.op X'))), (ConcreteCategory.hom (f.app (Opposite.op X'))) x = (ConcreteCategory.hom (G.map (Opposite.op φ))) y

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

@[deprecated CategoryTheory.extensiveTopology.surjective_of_isLocallySurjective_sheaf_of_types (since := "2024-11-26")]

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

Alias of CategoryTheory.extensiveTopology.surjective_of_isLocallySurjective_sheaf_of_types.

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

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

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

@[deprecated CategoryTheory.regularTopology.isLocallySurjective_sheaf_of_types (since := "2024-11-26")]

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

Alias of CategoryTheory.regularTopology.isLocallySurjective_sheaf_of_types.

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

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