Documentation

Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

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 : CategoryTheory.Functor Cᵒᵖ D} {G : CategoryTheory.Functor Cᵒᵖ D} (f : F ⟶ G) :

CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.regularTopology C) f ↔ ∀ (X : C) (y : (CategoryTheory.forget D).obj (G.obj { unop := X })), ∃ (X' : C) (φ : X' ⟶ X) (_ : CategoryTheory.EffectiveEpi φ) (x : (CategoryTheory.forget D).obj (F.obj { unop := X' })), (f.app { unop := X' }) x = (G.map { unop := φ }) y

theorem CategoryTheory.extensiveTopology.surjective_of_isLocallySurjective_sheafOfTypes {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.FinitaryPreExtensive C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {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 { unop := 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 : CategoryTheory.Functor Cᵒᵖ D} {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 { unop := 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 : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) D} {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 { unop := X })