isLocallySurjective_toSheafify' — Mathlib

English

There is a locally surjective instance for the forgetful functor from Hom-objects to RangeSheafify.

Русский

Существуют локально сюръективные структуры для функтора забывания из Hom-объектов к RangeSheafify.

LaTeX

$$IsLocallySurjective J(Subpresheaf.toRangeSheafify J f)$$

Lean4

instance isLocallySurjective_toSheafify' {D : Type*} [Category D] {FD : D → D → Type*} {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)] : IsLocallySurjective J (toSheafify J P) :=
  by
  rw [isLocallySurjective_iff_whisker_forget, ← sheafComposeIso_hom_fac, ← toSheafify_plusPlusIsoSheafify_hom]
  infer_instance

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