Locally surjective morphisms

Main definitions

• IsLocallySurjective : A morphism of presheaves valued in a concrete category is locally surjective with respect to a grothendieck topology if every section in the target is locally in the set-theoretic image, i.e. the image sheaf coincides with the target.

Main results

• toSheafify_isLocallySurjective : toSheafify is locally surjective.

theorem CategoryTheory.imageSieve_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F : CategoryTheory.Functor Cᵒᵖ A} {G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) {U : C} (s : (CategoryTheory.forget A).obj (G.obj (Opposite.op U))) (V : C) (i : V ⟶ U) : (CategoryTheory.imageSieve f s).arrows i = ∃ (t : (CategoryTheory.forget A).obj (F.obj (Opposite.op V))), (f.app (Opposite.op V)) t = (G.map i.op) s

def CategoryTheory.imageSieve {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F : CategoryTheory.Functor Cᵒᵖ A} {G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) {U : C} (s : (CategoryTheory.forget A).obj (G.obj (Opposite.op U))) : CategoryTheory.Sieve U

Given f : F ⟶ G, a morphism between presieves, and s : G.obj (op U), this is the sieve of U consisting of the i : V ⟶ U such that s restricted along i is in the image of f.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.imageSieve_eq_sieveOfSection {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F : CategoryTheory.Functor Cᵒᵖ A} {G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) {U : C} (s : (CategoryTheory.forget A).obj (G.obj (Opposite.op U))) : CategoryTheory.imageSieve f s = CategoryTheory.GrothendieckTopology.Subpresheaf.sieveOfSection (CategoryTheory.GrothendieckTopology.imagePresheaf (CategoryTheory.whiskerRight f (CategoryTheory.forget A))) s

theorem CategoryTheory.imageSieve_whisker_forget {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F : CategoryTheory.Functor Cᵒᵖ A} {G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) {U : C} (s : (CategoryTheory.forget A).obj (G.obj (Opposite.op U))) : CategoryTheory.imageSieve (CategoryTheory.whiskerRight f (CategoryTheory.forget A)) s = CategoryTheory.imageSieve f s

theorem CategoryTheory.imageSieve_app {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F : CategoryTheory.Functor Cᵒᵖ A} {G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) {U : C} (s : (CategoryTheory.forget A).obj (F.obj (Opposite.op U))) : CategoryTheory.imageSieve f ((f.app (Opposite.op U)) s) = ⊤

def CategoryTheory.IsLocallySurjective {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F : CategoryTheory.Functor Cᵒᵖ A} {G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) : Prop

A morphism of presheaves f : F ⟶ G is locally surjective with respect to a grothendieck topology if every section of G is locally in the image of f.

Equations

• CategoryTheory.IsLocallySurjective J f = ∀ (U : C) (s : (CategoryTheory.forget A).obj (G.obj (Opposite.op U))), CategoryTheory.imageSieve f s ∈ J.sieves U

theorem CategoryTheory.isLocallySurjective_iff_imagePresheaf_sheafify_eq_top {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F : CategoryTheory.Functor Cᵒᵖ A} {G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) : CategoryTheory.IsLocallySurjective J f ↔ CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J (CategoryTheory.GrothendieckTopology.imagePresheaf (CategoryTheory.whiskerRight f (CategoryTheory.forget A))) = ⊤

theorem CategoryTheory.isLocallySurjective_iff_imagePresheaf_sheafify_eq_top' {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {G : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F ⟶ G) : CategoryTheory.IsLocallySurjective J f ↔ CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J (CategoryTheory.GrothendieckTopology.imagePresheaf f) = ⊤

theorem CategoryTheory.isLocallySurjective_iff_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {F : CategoryTheory.Sheaf J (Type w)} {G : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ G) : CategoryTheory.IsLocallySurjective J f.val ↔ CategoryTheory.IsIso (CategoryTheory.GrothendieckTopology.imageSheafι f)

theorem CategoryTheory.isLocallySurjective_iff_whisker_forget {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F : CategoryTheory.Functor Cᵒᵖ A} {G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) : CategoryTheory.IsLocallySurjective J f ↔ CategoryTheory.IsLocallySurjective J (CategoryTheory.whiskerRight f (CategoryTheory.forget A))

theorem CategoryTheory.isLocallySurjective_of_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F : CategoryTheory.Functor Cᵒᵖ A} {G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) (H : ∀ (U : Cᵒᵖ), Function.Surjective ⇑(f.app U)) : CategoryTheory.IsLocallySurjective J f

theorem CategoryTheory.isLocallySurjective_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F : CategoryTheory.Functor Cᵒᵖ A} {G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) [CategoryTheory.IsIso f] : CategoryTheory.IsLocallySurjective J f

theorem CategoryTheory.IsLocallySurjective.comp {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F₁ : CategoryTheory.Functor Cᵒᵖ A} {F₂ : CategoryTheory.Functor Cᵒᵖ A} {F₃ : CategoryTheory.Functor Cᵒᵖ A} {f₁ : F₁ ⟶ F₂} {f₂ : F₂ ⟶ F₃} (h₁ : CategoryTheory.IsLocallySurjective J f₁) (h₂ : CategoryTheory.IsLocallySurjective J f₂) : CategoryTheory.IsLocallySurjective J (CategoryTheory.CategoryStruct.comp f₁ f₂)

noncomputable def CategoryTheory.sheafificationIsoImagePresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) : CategoryTheory.GrothendieckTopology.sheafify J F ≅ CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf (CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J (CategoryTheory.GrothendieckTopology.imagePresheaf (CategoryTheory.GrothendieckTopology.toSheafify J F)))

The image of F in J.sheafify F is isomorphic to the sheafification.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.toSheafify_isLocallySurjective {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {B : Type w} [CategoryTheory.Category.{max u v, w} B] [CategoryTheory.ConcreteCategory B] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ B] [∀ (P : CategoryTheory.Functor Cᵒᵖ B) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [(X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ B) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) (CategoryTheory.forget B)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget B)] [∀ (α β : Type (max u v)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) B] (F : CategoryTheory.Functor Cᵒᵖ B) : CategoryTheory.IsLocallySurjective J (CategoryTheory.GrothendieckTopology.toSheafify J F)