isLocallyInjective_toPlus — Mathlib

English

For any presheaf P, the functor J.toPlus sends P to a presheaf that is locally injective with respect to J.

Русский

Для каждого прешефа P сохраняющееся через J.toPlus даёт прешаф, локально инъективный по J.

LaTeX

$$$\mathrm{IsLocallyInjective}(J, J^{+}P)$$$

Lean4

instance isLocallyInjective_toPlus (P : Cᵒᵖ ⥤ Type max u v) : IsLocallyInjective J (J.toPlus P) where
  equalizerSieve_mem {X} x y
    h := by
    rw [toPlus_eq_mk, toPlus_eq_mk, eq_mk_iff_exists] at h
    obtain ⟨W, h₁, h₂, eq⟩ := h
    exact J.superset_covering (fun Y f hf => congr_fun (congr_arg Subtype.val eq) ⟨Y, f, hf⟩) W.2

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