Documentation

Mathlib.CategoryTheory.Sites.LocallyInjective

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.

@[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 : (CategoryTheory.forget D).obj (F.obj X)) (y : (CategoryTheory.forget D).obj (F.obj X)) :
∀ (x_1 : C) (f : x_1 Opposite.unop X), (CategoryTheory.Presheaf.equalizerSieve x y).arrows f = ((F.map f.op) x = (F.map f.op) y)

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
Instances For

    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.

    Instances
      @[reducible, inline]

      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
      Instances For