English
For a condensed object X in A, there is a sheaf condition on Profinite with respect to the coherent topology: the corresponding presheaf is a sheaf on Profinite.
Русский
Для конденсированного объекта X в A выполняется условие sheaf для Profinite при когерентной топологии: соответствующий предсешеп является sheaf на Profinite.
LaTeX
$$$$\mathrm{Presheaf.IsSheaf}(\mathrm{coherentTopology\;Profinite})(\mathrm{profiniteToCompHaus}^{\mathrm{op}} \circ X).$$$$
Lean4
theorem isSheafProfinite [∀ Y, HasLimitsOfShape (StructuredArrow Y profiniteToCompHaus.{u}.op) A] :
Presheaf.IsSheaf (coherentTopology Profinite) (profiniteToCompHaus.op ⋙ X.val) :=
((ProfiniteCompHaus.equivalence A).inverse.obj X).cond
