English
For a fixed coherent topology determined by a class of compact Hausdorff-like objects, there is a functor from the category of topological spaces to the category of Type-valued sheaves on that topology. This functor sends a space X to the coherent-sheaf associated to X (constructed via X.toSheafCompHausLike with the preregular hypothesis hs) and a continuous map to the corresponding morphism of such sheaves.
Русский
Для заданной когерентной топологии, задаваемой классом объектов CompHausLike, существует функтор от категории топологических пространств кCategory теории касательных (sheaf) над этой топологией значений в Type. Этот функтор отправляет пространство X в соответствующий шелев-подобный объект X.toSheafCompHausLike P hs и непрерывное отображение f:X→Y в соответствующий морфизм шелфов.
LaTeX
$$$F:\\mathbf{TopCat}\\to \\mathbf{Sheaf}(\\operatorname{coherentTopology}(\\operatorname{CompHausLike}(P))(\\mathrm{Type}(\\max u w)))\\,,$ with $F(X)=X^{toSheafCompHausLike} P hs$ and $F(f)$ the induced morphism of sheaves.$$
Lean4
/-- `TopCat.toSheafCompHausLike` yields a functor from `TopCat.{max u w}` to
`Sheaf (coherentTopology (CompHausLike.{u} P)) (Type (max u w))`.
-/
@[simps]
noncomputable def topCatToSheafCompHausLike :
have := CompHausLike.preregular hs
TopCat.{max u w} ⥤ Sheaf (coherentTopology (CompHausLike.{u} P)) (Type (max u w))
where
obj X := X.toSheafCompHausLike P hs
map f := ⟨⟨fun _ g ↦ f.hom.comp g, by aesop⟩⟩
