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

• Presheaf.isLocallySurjective_toSheafify: toSheafify is locally surjective.
• Sheaf.isLocallySurjective_iff_epi: a morphism of sheaves of types is locally surjective iff it is epi

def CategoryTheory.Presheaf.imageSieve {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F 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.Presheaf.imageSieve_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F 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.Presheaf.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

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

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

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

noncomputable def CategoryTheory.Presheaf.localPreimage {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) {U : Cᵒᵖ} (s : (CategoryTheory.forget A).obj (G.obj U)) {V : C} (g : V ⟶ Opposite.unop U) (hg : (CategoryTheory.Presheaf.imageSieve f s).arrows g) : (CategoryTheory.forget A).obj (F.obj (Opposite.op V))

If a morphism g : V ⟶ U.unop belongs to the sieve imageSieve f s g, then this is choice of a preimage of G.map g.op s in F.obj (op V), see app_localPreimage.

Equations

• CategoryTheory.Presheaf.localPreimage f s g hg = Exists.choose hg

@[simp]

theorem CategoryTheory.Presheaf.app_localPreimage {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) {U : Cᵒᵖ} (s : (CategoryTheory.forget A).obj (G.obj U)) {V : C} (g : V ⟶ Opposite.unop U) (hg : (CategoryTheory.Presheaf.imageSieve f s).arrows g) : (f.app (Opposite.op V)) (CategoryTheory.Presheaf.localPreimage f s g hg) = (G.map g.op) s

class CategoryTheory.Presheaf.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 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.

• imageSieve_mem {U : C} (s : (CategoryTheory.forget A).obj (G.obj (Opposite.op U))) : CategoryTheory.Presheaf.imageSieve f s ∈ J U

theorem CategoryTheory.Presheaf.imageSieve_mem {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) [CategoryTheory.Presheaf.IsLocallySurjective J f] {U : Cᵒᵖ} (s : (CategoryTheory.forget A).obj (G.obj U)) : CategoryTheory.Presheaf.imageSieve f s ∈ J (Opposite.unop U)

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

theorem CategoryTheory.Presheaf.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 G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) : CategoryTheory.Presheaf.IsLocallySurjective J f ↔ CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J (CategoryTheory.GrothendieckTopology.imagePresheaf (CategoryTheory.whiskerRight f (CategoryTheory.forget A))) = ⊤

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

theorem CategoryTheory.Presheaf.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 G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) : CategoryTheory.Presheaf.IsLocallySurjective J f ↔ CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.whiskerRight f (CategoryTheory.forget A))

theorem CategoryTheory.Presheaf.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 G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) (H : ∀ (U : Cᵒᵖ), Function.Surjective ⇑(f.app U)) : CategoryTheory.Presheaf.IsLocallySurjective J f

instance CategoryTheory.Presheaf.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 G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) [CategoryTheory.IsIso f] : CategoryTheory.Presheaf.IsLocallySurjective J f

instance CategoryTheory.Presheaf.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₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ A} (f₁ : F₁ ⟶ F₂) (f₂ : F₂ ⟶ F₃) [CategoryTheory.Presheaf.IsLocallySurjective J f₁] [CategoryTheory.Presheaf.IsLocallySurjective J f₂] : CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.CategoryStruct.comp f₁ f₂)

theorem CategoryTheory.Presheaf.isLocallySurjective_of_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₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ A} (f₁ : F₁ ⟶ F₂) (f₂ : F₂ ⟶ F₃) [CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.CategoryStruct.comp f₁ f₂)] : CategoryTheory.Presheaf.IsLocallySurjective J f₂

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

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

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

theorem CategoryTheory.Presheaf.isLocallySurjective_of_le {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {K : CategoryTheory.GrothendieckTopology C} (hJK : J ≤ K) {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) (h : CategoryTheory.Presheaf.IsLocallySurjective J f) : CategoryTheory.Presheaf.IsLocallySurjective K f

theorem CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_of_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₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ A} (f₁ : F₁ ⟶ F₂) (f₂ : F₂ ⟶ F₃) [CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.CategoryStruct.comp f₁ f₂)] [CategoryTheory.Presheaf.IsLocallySurjective J f₁] : CategoryTheory.Presheaf.IsLocallyInjective J f₂

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

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

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

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

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

instance CategoryTheory.Presheaf.instIsLocallySurjectiveToImagePresheafSheafify {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {F₁ F₂ : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F₁ ⟶ F₂) : CategoryTheory.Presheaf.IsLocallySurjective J (J.toImagePresheafSheafify f)

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

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.

instance CategoryTheory.Presheaf.isLocallySurjective_toPlus {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) : CategoryTheory.Presheaf.IsLocallySurjective J (J.toPlus P)

instance CategoryTheory.Presheaf.isLocallySurjective_toSheafify {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) : CategoryTheory.Presheaf.IsLocallySurjective J (J.toSheafify P)

instance CategoryTheory.Presheaf.isLocallySurjective_toSheafify' {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.ConcreteCategory D] (P : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.HasWeakSheafify J D] [J.HasSheafCompose (CategoryTheory.forget D)] [J.PreservesSheafification (CategoryTheory.forget D)] : CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)

@[reducible, inline]

abbrev CategoryTheory.Sheaf.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₁ F₂ : CategoryTheory.Sheaf J A} (φ : F₁ ⟶ F₂) : Prop

If φ : F₁ ⟶ F₂ is a morphism of sheaves, this is an abbreviation for Presheaf.IsLocallySurjective J φ.val.

Equations

• CategoryTheory.Sheaf.IsLocallySurjective φ = CategoryTheory.Presheaf.IsLocallySurjective J φ.val

theorem CategoryTheory.Sheaf.isLocallySurjective_sheafToPresheaf_map_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F₁ F₂ : CategoryTheory.Sheaf J A} (φ : F₁ ⟶ F₂) : CategoryTheory.Presheaf.IsLocallySurjective J ((CategoryTheory.sheafToPresheaf J A).map φ) ↔ CategoryTheory.Sheaf.IsLocallySurjective φ

instance CategoryTheory.Sheaf.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₁ F₂ F₃ : CategoryTheory.Sheaf J A} (φ : F₁ ⟶ F₂) (ψ : F₂ ⟶ F₃) [CategoryTheory.Sheaf.IsLocallySurjective φ] [CategoryTheory.Sheaf.IsLocallySurjective ψ] : CategoryTheory.Sheaf.IsLocallySurjective (CategoryTheory.CategoryStruct.comp φ ψ)

instance CategoryTheory.Sheaf.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₁ F₂ : CategoryTheory.Sheaf J A} (φ : F₁ ⟶ F₂) [CategoryTheory.IsIso φ] : CategoryTheory.Sheaf.IsLocallySurjective φ

instance CategoryTheory.Sheaf.instIsLocallySurjectiveToImageSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F G : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ G) : CategoryTheory.Sheaf.IsLocallySurjective (CategoryTheory.GrothendieckTopology.toImageSheaf f)

instance CategoryTheory.Sheaf.instIsLocallySurjectiveMapTypeSheafComposeForget {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F₁ F₂ : CategoryTheory.Sheaf J A} (φ : F₁ ⟶ F₂) [J.HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.Sheaf.IsLocallySurjective φ] : CategoryTheory.Sheaf.IsLocallySurjective ((CategoryTheory.sheafCompose J (CategoryTheory.forget A)).map φ)

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

instance CategoryTheory.Sheaf.epi_of_isLocallySurjective' {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F₁ F₂ : CategoryTheory.Sheaf J (Type w)} (φ : F₁ ⟶ F₂) [CategoryTheory.Sheaf.IsLocallySurjective φ] : CategoryTheory.Epi φ

instance CategoryTheory.Sheaf.epi_of_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₁ F₂ : CategoryTheory.Sheaf J A} (φ : F₁ ⟶ F₂) [J.HasSheafCompose (CategoryTheory.forget A)] [CategoryTheory.Sheaf.IsLocallySurjective φ] : CategoryTheory.Epi φ

theorem CategoryTheory.Sheaf.isLocallySurjective_iff_epi {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {F G : CategoryTheory.Sheaf J (Type w)} (φ : F ⟶ G) [CategoryTheory.HasSheafify J (Type w)] : CategoryTheory.Sheaf.IsLocallySurjective φ ↔ CategoryTheory.Epi φ

noncomputable def CategoryTheory.Presieve.FamilyOfElements.localPreimage {C : Type u} [CategoryTheory.Category.{v, u} C] {R R' : CategoryTheory.Functor Cᵒᵖ (Type w)} (φ : R ⟶ R') {X : Cᵒᵖ} (r' : R'.obj X) : CategoryTheory.Presieve.FamilyOfElements R (CategoryTheory.Presheaf.imageSieve φ r').arrows

Given a morphism φ : R ⟶ R' of presheaves of types and r' : R'.obj X, this is the family of elements of R defined over the sieve Presheaf.imageSieve φ r' which sends a map in this sieve to an arbitrary choice of a preimage of the restriction of r'.

Equations

• CategoryTheory.Presieve.FamilyOfElements.localPreimage φ r' f hf = CategoryTheory.Presheaf.localPreimage φ r' f hf

theorem CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_map_localPreimage {C : Type u} [CategoryTheory.Category.{v, u} C] {R R' : CategoryTheory.Functor Cᵒᵖ (Type w)} (φ : R ⟶ R') {X : Cᵒᵖ} (r' : R'.obj X) : ((CategoryTheory.Presieve.FamilyOfElements.localPreimage φ r').map φ).IsAmalgamation r'