English
If X has an upper-set topology from a preorder, then the right Kan extension along principals is a sheaf.
Русский
Если X имеет топологию верхних множеств, полученную от предорядка, то правое кан-расширение вдоль princip als является шейфом.
LaTeX
$$$\text{IsSheaf}(\mathrm{Opens.grothendieckTopology}(X), \mathrm{principalsKanExtension}(F))$$$
Lean4
/-- The main theorem of this file.
If `X` is a topological space and preorder whose topology is the `UpperSet` topology associated
with the preorder, `F : X ⥤ C` is a functor into a complete category from the preorder category,
and `P : (Opens X)ᵒᵖ ⥤ C` denotes the right Kan extension of `F` along the
functor `X ⥤ (Open X)ᵒᵖ` which sends `x : X` to `{y | x ≤ y}`, then `P` is a sheaf.
-/
theorem isSheaf_of_isRightKanExtension (P : (Opens X)ᵒᵖ ⥤ C) (η : Alexandrov.principals X ⋙ P ⟶ F)
[P.IsRightKanExtension η] : Presheaf.IsSheaf (Opens.grothendieckTopology X) P :=
by
let γ : principals X ⋙ principalsKanExtension F ⟶ F := (principals X).pointwiseRightKanExtensionCounit F
let _ : (principalsKanExtension F).IsRightKanExtension γ := inferInstance
have : P ≅ principalsKanExtension F :=
@rightKanExtensionUnique _ _ _ _ _ _ _ _ _ _ (by assumption) _ _ (by assumption)
change TopCat.Presheaf.IsSheaf (X := TopCat.of X) P
rw [isSheaf_iso_iff this]
let _ : Preorder (TopCat.of X) := inferInstanceAs <| Preorder X
have _ : Topology.IsUpperSet (TopCat.of X) := inferInstanceAs <| Topology.IsUpperSet X
exact isSheaf_principalsKanExtension (X := TopCat.of X) F
