isTerminal_of_isSheafFor_empty_presieve

English

If F is a presheaf that satisfies the sheaf condition for the empty presieve on the initial object, then F(n(op I)) is a terminal object, i.e., F preserves the terminal object along the initial op.

Русский

Если F — преснив и удовлетворяет условию шейфа для пустого пресивера на начальном объекте, то F(опposite I) является терм-объектом; F сохраняет тождественный предел на начальном объекте.

LaTeX

$$$ IsTerminal (F.obj (op I)) $$$

Lean4

/-- If `F` is a presheaf which satisfies the sheaf condition with respect to the empty presieve on any
object, then `F` takes that object to the terminal object.
-/
noncomputable def isTerminal_of_isSheafFor_empty_presieve : IsTerminal (F.obj (op I)) :=
  by
  refine @IsTerminal.ofUnique _ _ _ fun Y ↦ ?_
  choose t h using hF (by tauto) (by tauto)
  exact ⟨⟨fun _ ↦ t⟩, fun a ↦ by ext; exact h.2 _ (by tauto)⟩

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