English
Under suitable preregularity assumptions, the Yoneda presheaf composed with compHausLikeToTop gives a sheaf for the coherent topology on CompHausLike P.
Русский
При подходящих предположениях preregularity конденсированная предPresheaf Yoneda вместе с compHausLikeToTop образуют Sheaf для когерентной топологии на CompHausLike P.
LaTeX
$$$\text{toSheafCompHausLike}(P) :\; \text{Sheaf}(\text{coherentTopology}(CompHausLike P), \mathrm{Type})$$$
Lean4
/-- The sheaf on `CompHausLike P` of continuous maps to a topological space.
-/
@[simps! val_obj val_map]
def toSheafCompHausLike :
have := CompHausLike.preregular hs
Sheaf (coherentTopology (CompHausLike.{u} P)) (Type (max u w))
where
val := yonedaPresheaf.{u, max u w} (CompHausLike.compHausLikeToTop.{u} P) X
cond := by
have := CompHausLike.preregular hs
rw [Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition]
refine ⟨inferInstance, ?_⟩
apply (config := { allowSynthFailures := true })
equalizerCondition_yonedaPresheaf (CompHausLike.compHausLikeToTop.{u} P) X
intro Z B π he
apply IsQuotientMap.of_surjective_continuous (hs _ he) π.hom.continuous
