Theorems · Definition · category theory

CategoryTheory.Sheaf.IsLocallyInjective

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {FD : D → D → Type u_1} →
          {CD : D → Type w} →
            [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
              [CategoryTheory.ConcreteCategory D FD] →
                {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.

Defined in

Mathlib.CategoryTheory.Sites.LocallyInjective

Cited by

7 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategory