instIsLocallyInjectiveHomObjForgetTypeι

English

If F is a presheaf valued in Type and G is a subpresheaf of F, then the inclusion G ⟶ F is locally injective with respect to J.

Русский

Пусть F — прешаф, значения которого являются Type, и G — подпресшаф F. Тогда включение G ⟶ F локально инъективно по J.

LaTeX

$$$G\hookrightarrow F\quad\text{is locally injective with respect to } J.$$$

Lean4

instance (F : Cᵒᵖ ⥤ Type w) (G : Subpresheaf F) : IsLocallyInjective J G.ι :=
  isLocallyInjective_of_injective _ _
    (fun X => by
      intro ⟨x, _⟩ ⟨y, _⟩ h
      exact Subtype.ext h)

Похожие утверждения