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} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.ConcreteCategory D] {F : CategoryTheory.Functor Cᵒᵖ D} {X : Cᵒᵖ} (x y : (CategoryTheory.forget D).obj (F.obj X)) : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.ConcreteCategory D] {F : CategoryTheory.Functor Cᵒᵖ D} {X : Cᵒᵖ} (x y : (CategoryTheory.forget D).obj (F.obj X)) (x✝ : C) (f : x✝ ⟶ Opposite.unop X) : (CategoryTheory.Presheaf.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} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.ConcreteCategory D] {F : CategoryTheory.Functor Cᵒᵖ D} {X : Cᵒᵖ} (x : (CategoryTheory.forget D).obj (F.obj X)) : CategoryTheory.Presheaf.equalizerSieve x x = ⊤

@[simp]

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

class CategoryTheory.Presheaf.IsLocallyInjective {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.ConcreteCategory D] (J : CategoryTheory.GrothendieckTopology C) {F₁ F₂ : CategoryTheory.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 : (CategoryTheory.forget D).obj (F₁.obj X)), (φ.app X) x = (φ.app X) y → CategoryTheory.Presheaf.equalizerSieve x y ∈ J (Opposite.unop X)

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

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

Equations

• ⋯ = ⋯

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

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

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

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev CategoryTheory.Sheaf.IsLocallyInjective {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.ConcreteCategory D] {J : CategoryTheory.GrothendieckTopology C} {F₁ F₂ : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.ConcreteCategory D] {J : CategoryTheory.GrothendieckTopology C} {F₁ F₂ : CategoryTheory.Sheaf J D} (φ : F₁ ⟶ F₂) : CategoryTheory.Presheaf.IsLocallyInjective J ((CategoryTheory.sheafToPresheaf J D).map φ) ↔ CategoryTheory.Sheaf.IsLocallyInjective φ

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• ⋯ = ⋯