Structures · Category theory

CategoryTheory.Presheaf.IsLocallyInjective

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.

Defined in

Mathlib.CategoryTheory.Sites.LocallyInjective

Shape

2 explicit arguments · adds equalizerSieve_mem