hom — Mathlib

English

The property IsSheafFor holds for presheafHom with sieve S.arrows under the assumed hG condition.

Русский

Для presheafHom выполняется IsSheafFor при сетке S.arrows при условии hG.

LaTeX

$$Presieve.IsSheafFor(presheafHom F G, S.arrows)$$

Lean4

theorem hom (hG : Presheaf.IsSheaf J G) : Presheaf.IsSheaf J (presheafHom F G) :=
  by
  rw [isSheaf_iff_isSheaf_of_type]
  intro X S hS
  exact
    presheafHom_isSheafFor F G S (fun _ _ => ((Presheaf.isSheaf_iff_isLimit J G).1 hG _ (J.pullback_stable _ hS)).some)

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