isSeparated — Mathlib

English

If F is a presheaf IsSheaf, then it is separated.

Русский

Если F — шейф по некоторой топологии, то он разделим.

LaTeX

$$$\Presheaf.IsSheaf\, J\, F \Rightarrow \Presheaf.IsSeparated\, J\, F$$$

Lean4

theorem isSeparated {F : Cᵒᵖ ⥤ A} {FA : A → A → Type*} {CA : A → Type*} [∀ X Y, FunLike (FA X Y) (CA X) (CA Y)]
    [ConcreteCategory A FA] [J.HasSheafCompose (forget A)] (hF : Presheaf.IsSheaf J F) : Presheaf.IsSeparated J F :=
  Sheaf.isSeparated ⟨F, hF⟩

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