isSeparated — Mathlib

English

If F is a sheaf on J, then its underlying presheaf is separated.

Русский

Если F является шейфом по J, то содержащийся у него прешеф является разделимым.

LaTeX

$$$Presheaf.IsSeparated\, J\, F.val$$$

Lean4

theorem isSeparated {FA : A → A → Type*} {CA : A → Type*} [∀ X Y, FunLike (FA X Y) (CA X) (CA Y)]
    [ConcreteCategory A FA] [J.HasSheafCompose (forget A)] (F : Sheaf J A) : Presheaf.IsSeparated J F.val :=
  by
  rintro X S hS x y h
  exact
    (((isSheaf_iff_isSheaf_of_type _ _).1 ((sheafCompose J (forget A)).obj F).2).isSeparated S hS).ext
      (fun _ _ hf => h _ _ hf)

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