Condensed mathematics, developed by Clausen and Scholze over the last few years, proposes a generalization of topology with better categorical properties. It replaces the concept of a topological space by that of a condensed set, which can be defined as a sheaf for the coherent topology on a certain category of compact Hausdorff spaces. In this case, the sheaf condition has a fairly simple explicit description, which arises from studying the relationship between the coherent, regular and extensive topologies. In this paper, we establish this relationship under minimal assumptions on the category, going beyond the case of compact Hausdorff spaces. Along the way, we also provide a characterization of sheaves and covering sieves for these categories. All results in this paper have been fully formalized in the Lean proof assistant.
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined in a non-algebraic and space-based style, as well as models of higher-order theories such as topological spaces. In particular, we formulate a general definition of indiscernibility for objects of any such structure, and a corresponding univalence condition that generalizes Rezk's completeness condition for Segal spaces and ensures that all equivalences of struc…
Northeastern University（东北大学）；Australian National University（澳大利亚国立大学）
Category theory has been successfully applied in various domains of science, shedding light on universal principles unifying diverse phenomena and thereby enabling knowledge transfer between them. Applications to machine learning have been pursued recently, and yet there is still a gap between abstract mathematical foundations and concrete applications to machine learning tasks. In this paper we introduce DisCoPyro as a categorical structure learning framework, which combines categorical structures (such as symmetric monoidal categories and operads) with amortized variational inference, and ca…
