isLocallyInjective_toSheafify' — Mathlib

English

An isLocallyInjective structure on a presheaf extends to the toSheafify construction.

Русский

Структура локальной инъективности на предрассехе переносится на конструкцию toSheafify.

LaTeX

$$$\\text{IsLocallyInjective } J (\\text{toSheafify } J P)$$$

Lean4

instance isLocallyInjective_toSheafify' {CD : D → Type (max u v)} [∀ X Y, FunLike (FD X Y) (CD X) (CD Y)]
    [ConcreteCategory.{max u v} D FD] (P : Cᵒᵖ ⥤ D) [HasWeakSheafify J D] [J.HasSheafCompose (forget D)]
    [J.PreservesSheafification (forget D)] : IsLocallyInjective J (toSheafify J P) :=
  by
  rw [← isLocallyInjective_forget_iff, ← sheafComposeIso_hom_fac, ← toSheafify_plusPlusIsoSheafify_hom]
  infer_instance

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