Locally injective morphisms of (pre)sheaves

Let C be a category equipped with a Grothendieck topology J, and let D be a concrete category. In this file, we introduce the typeclass Presheaf.IsLocallyInjective J φ for a morphism φ : F₁ ⟶ F₂ in the category Cᵒᵖ ⥤ D. This means that φ is locally injective. More precisely, if x and y are two elements of some F₁.obj U such the images of x and y in F₂.obj U coincide, then the equality x = y must hold locally, i.e. after restriction by the maps of a covering sieve.

def CategoryTheory.Presheaf.equalizerSieve {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] {F : Functor Cᵒᵖ D} {X : Cᵒᵖ} (x y : (forget D).obj (F.obj X)) : Sieve (Opposite.unop X)

If F : Cᵒᵖ ⥤ D is a presheaf with values in a concrete category, if x and y are elements in F.obj X, this is the sieve of X.unop consisting of morphisms f such that F.map f.op x = F.map f.op y.

Equations

• CategoryTheory.Presheaf.equalizerSieve x y = { arrows := fun (x_1 : C) (f : x_1 ⟶ Opposite.unop X) => (F.map f.op) x = (F.map f.op) y, downward_closed := ⋯ }

@[simp]

theorem CategoryTheory.Presheaf.equalizerSieve_apply {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] {F : Functor Cᵒᵖ D} {X : Cᵒᵖ} (x y : (forget D).obj (F.obj X)) (x✝ : C) (f : x✝ ⟶ Opposite.unop X) : (equalizerSieve x y).arrows f = ((F.map f.op) x = (F.map f.op) y)

@[simp]

theorem CategoryTheory.Presheaf.equalizerSieve_self_eq_top {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] {F : Functor Cᵒᵖ D} {X : Cᵒᵖ} (x : (forget D).obj (F.obj X)) : equalizerSieve x x = ⊤

@[simp]

theorem CategoryTheory.Presheaf.equalizerSieve_eq_top_iff {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] {F : Functor Cᵒᵖ D} {X : Cᵒᵖ} (x y : (forget D).obj (F.obj X)) : equalizerSieve x y = ⊤ ↔ x = y

class CategoryTheory.Presheaf.IsLocallyInjective {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] (J : GrothendieckTopology C) {F₁ F₂ : Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) : Prop

A morphism φ : F₁ ⟶ F₂ of presheaves Cᵒᵖ ⥤ D (with D a concrete category) is locally injective for a Grothendieck topology J on C if whenever two sections of F₁ are sent to the same section of F₂, then these two sections coincide locally.

• equalizerSieve_mem {X : Cᵒᵖ} (x y : (forget D).obj (F₁.obj X)) (h : (φ.app X) x = (φ.app X) y) : equalizerSieve x y ∈ J (Opposite.unop X)

theorem CategoryTheory.Presheaf.equalizerSieve_mem {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] (J : GrothendieckTopology C) {F₁ F₂ : Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) [IsLocallyInjective J φ] {X : Cᵒᵖ} (x y : (forget D).obj (F₁.obj X)) (h : (φ.app X) x = (φ.app X) y) : equalizerSieve x y ∈ J (Opposite.unop X)

theorem CategoryTheory.Presheaf.isLocallyInjective_of_injective {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] (J : GrothendieckTopology C) {F₁ F₂ : Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) (hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(φ.app X)) : IsLocallyInjective J φ

instance CategoryTheory.Presheaf.instIsLocallyInjectiveOfIsIsoFunctorOpposite {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] (J : GrothendieckTopology C) {F₁ F₂ : Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) [IsIso φ] : IsLocallyInjective J φ

instance CategoryTheory.Presheaf.isLocallyInjective_forget {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] (J : GrothendieckTopology C) {F₁ F₂ : Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) [IsLocallyInjective J φ] : IsLocallyInjective J (whiskerRight φ (forget D))

theorem CategoryTheory.Presheaf.isLocallyInjective_forget_iff {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] (J : GrothendieckTopology C) {F₁ F₂ : Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) : IsLocallyInjective J (whiskerRight φ (forget D)) ↔ IsLocallyInjective J φ

theorem CategoryTheory.Presheaf.isLocallyInjective_iff_equalizerSieve_mem_imp {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] (J : GrothendieckTopology C) {F₁ F₂ : Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) : IsLocallyInjective J φ ↔ ∀ ⦃X : Cᵒᵖ⦄ (x y : (forget D).obj (F₁.obj X)), equalizerSieve ((φ.app X) x) ((φ.app X) y) ∈ J (Opposite.unop X) → equalizerSieve x y ∈ J (Opposite.unop X)

theorem CategoryTheory.Presheaf.equalizerSieve_mem_of_equalizerSieve_app_mem {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] (J : GrothendieckTopology C) {F₁ F₂ : Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) {X : Cᵒᵖ} (x y : (forget D).obj (F₁.obj X)) (h : equalizerSieve ((φ.app X) x) ((φ.app X) y) ∈ J (Opposite.unop X)) [IsLocallyInjective J φ] : equalizerSieve x y ∈ J (Opposite.unop X)

instance CategoryTheory.Presheaf.isLocallyInjective_comp {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] (J : GrothendieckTopology C) {F₁ F₂ F₃ : Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) (ψ : F₂ ⟶ F₃) [IsLocallyInjective J φ] [IsLocallyInjective J ψ] : IsLocallyInjective J (CategoryStruct.comp φ ψ)

theorem CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] (J : GrothendieckTopology C) {F₁ F₂ F₃ : Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) (ψ : F₂ ⟶ F₃) [IsLocallyInjective J (CategoryStruct.comp φ ψ)] : IsLocallyInjective J φ

theorem CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_fac {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] (J : GrothendieckTopology C) {F₁ F₂ F₃ : Functor Cᵒᵖ D} {φ : F₁ ⟶ F₂} {ψ : F₂ ⟶ F₃} {φψ : F₁ ⟶ F₃} (fac : CategoryStruct.comp φ ψ = φψ) [IsLocallyInjective J φψ] : IsLocallyInjective J φ

theorem CategoryTheory.Presheaf.isLocallyInjective_iff_of_fac {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] (J : GrothendieckTopology C) {F₁ F₂ F₃ : Functor Cᵒᵖ D} {φ : F₁ ⟶ F₂} {ψ : F₂ ⟶ F₃} {φψ : F₁ ⟶ F₃} (fac : CategoryStruct.comp φ ψ = φψ) [IsLocallyInjective J ψ] : IsLocallyInjective J φψ ↔ IsLocallyInjective J φ

theorem CategoryTheory.Presheaf.isLocallyInjective_comp_iff {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] (J : GrothendieckTopology C) {F₁ F₂ F₃ : Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) (ψ : F₂ ⟶ F₃) [IsLocallyInjective J ψ] : IsLocallyInjective J (CategoryStruct.comp φ ψ) ↔ IsLocallyInjective J φ

theorem CategoryTheory.Presheaf.isLocallyInjective_iff_injective_of_separated {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] (J : GrothendieckTopology C) {F₁ F₂ : Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) (hsep : Presieve.IsSeparated J (F₁.comp (forget D))) : IsLocallyInjective J φ ↔ ∀ (X : Cᵒᵖ), Function.Injective ⇑(φ.app X)

instance CategoryTheory.Presheaf.instIsLocallyInjectiveι {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (F : Functor Cᵒᵖ (Type w)) (G : Subpresheaf F) : IsLocallyInjective J G.ι

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

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

instance CategoryTheory.Presheaf.isLocallyInjective_toSheafify' {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (J : GrothendieckTopology C) [HasForget D] (P : Functor Cᵒᵖ D) [HasWeakSheafify J D] [J.HasSheafCompose (forget D)] [J.PreservesSheafification (forget D)] : IsLocallyInjective J (toSheafify J P)

@[reducible, inline]

abbrev CategoryTheory.Sheaf.IsLocallyInjective {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] {J : GrothendieckTopology C} {F₁ F₂ : Sheaf J D} (φ : F₁ ⟶ F₂) : Prop

If φ : F₁ ⟶ F₂ is a morphism of sheaves, this is an abbreviation for Presheaf.IsLocallyInjective J φ.val. Under suitable assumptions, it is equivalent to the injectivity of all maps φ.val.app X, see isLocallyInjective_iff_injective.

Equations

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

theorem CategoryTheory.Sheaf.isLocallyInjective_sheafToPresheaf_map_iff {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] {J : GrothendieckTopology C} {F₁ F₂ : Sheaf J D} (φ : F₁ ⟶ F₂) : Presheaf.IsLocallyInjective J ((sheafToPresheaf J D).map φ) ↔ IsLocallyInjective φ

instance CategoryTheory.Sheaf.isLocallyInjective_of_iso {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] {J : GrothendieckTopology C} {F₁ F₂ : Sheaf J D} (φ : F₁ ⟶ F₂) [IsIso φ] : IsLocallyInjective φ

theorem CategoryTheory.Sheaf.mono_of_injective {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] {J : GrothendieckTopology C} {F₁ F₂ : Sheaf J D} (φ : F₁ ⟶ F₂) (hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(φ.val.app X)) : Mono φ

instance CategoryTheory.Sheaf.isLocallyInjective_forget {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] {J : GrothendieckTopology C} {F₁ F₂ : Sheaf J D} (φ : F₁ ⟶ F₂) [J.HasSheafCompose (forget D)] [IsLocallyInjective φ] : IsLocallyInjective ((sheafCompose J (forget D)).map φ)

theorem CategoryTheory.Sheaf.isLocallyInjective_iff_injective {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] {J : GrothendieckTopology C} {F₁ F₂ : Sheaf J D} (φ : F₁ ⟶ F₂) [J.HasSheafCompose (forget D)] : IsLocallyInjective φ ↔ ∀ (X : Cᵒᵖ), Function.Injective ⇑(φ.val.app X)

theorem CategoryTheory.Sheaf.mono_of_isLocallyInjective {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasForget D] {J : GrothendieckTopology C} {F₁ F₂ : Sheaf J D} (φ : F₁ ⟶ F₂) [J.HasSheafCompose (forget D)] [IsLocallyInjective φ] : Mono φ

instance CategoryTheory.Sheaf.instIsLocallyInjectiveImageι {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F G : Sheaf J (Type w)} (f : F ⟶ G) : IsLocallyInjective (imageι f)