v1.15.0 - Various additions to morphisms

Features 🧪

• Automatic deduction of special morphisms by @ScriptRaccoon in #285
• Human-readable display of implications by @ScriptRaccoon in #286
• Rename "source" to "domain", and "target" to "codomain" by @ScriptRaccoon in #287
• Add sanity check for implications by @ScriptRaccoon in #289
• Add various end-to-end tests for morphisms by @ScriptRaccoon in #295
• Show stored morphisms on category detail page by @ScriptRaccoon in #299

Database 🔋

• Add property "core-connected" and improve tags by @ScriptRaccoon in #288
• Add effective epimorphisms and related properties by @ScriptRaccoon in #291
• Add normal epimorphisms and normal monomorphisms by @ScriptRaccoon in #292
• Add strong epimorphisms and strong monomorphisms by @ScriptRaccoon in #296
• Determine some accessibilities of Met by @ykawase5048 in #297

Bugs 🐛

• Fix commands on windows by @ScriptRaccoon in #294

Full Changelog ⚙️

v1.14.0...v1.15.0

v1.14.0 - Improve architecture

Quite a lot has been improved over the last week: the morphism structure type is available, end-to-end tests have been added, and the application is better organized. This is due both to a new shared folder for utilities used by the Svelte application and the database application, and to the extraction of the admin application into its own repository. Moreover, dynamic routes have removed lots of code duplication. In addition, the database has received various updates thanks to @dschepler.

Features 🧪

• Add new structure type: morphisms by @ScriptRaccoon in #265
• Add end-to-end tests with Playwright by @ScriptRaccoon in #270
• Check that environment variables are up-to-date by @ScriptRaccoon in #274 (obsolete after #278)
• Add more end-to-end tests by @ScriptRaccoon in #276

Refactor 🧹

• Use Dynamic Routes by @ScriptRaccoon in #268
• Various refactorings by @ScriptRaccoon in #269
• Share code between database application and SvelteKit application by @ScriptRaccoon in #271
• Remove trailing commas by @ScriptRaccoon in #272
• Separate admin application by @ScriptRaccoon in #278
• Rename /databases/catdat to /database by @ScriptRaccoon in #283

Database 🔋

• Add Sierpinski topos (category of set functions and commutative squares) by @dschepler in #264
• Add category Mono of sets with a distinguished subset by @dschepler in #266
• Add quasitopos property by @dschepler in #273
• Add regular-subobject-trivial and regular-quotient-trivial properties by @dschepler in #275
• Rename "proset" to "preordered set" by @ScriptRaccoon in #284

Full Changelog ⚙️

v1.13.0...v1.14.0

v1.13.0 - Various additions to functors

Features 🧪

• Check that link targets exist by @ScriptRaccoon in #251
• Consistent clearing of deduced data by @ScriptRaccoon in #253
• Explain dual properties by @ScriptRaccoon in #255
• Support tags for properties of categories and functors by @ScriptRaccoon in #259
• Show functors on category detail page, and improve functor notation by @ScriptRaccoon in #261

Refactor 🧹

• Identify properties by ID and type by @ScriptRaccoon in #263

Bugs 🐛

• Save search after search results page loads by @ScriptRaccoon in #252

Database 🔋

• Various additions to functors by @ScriptRaccoon in #246
• Add the fundamental group functor by @ScriptRaccoon in #256
• Add various properties of the category of Banach spaces by @ScriptRaccoon in #258
• Add isomorphisms of categories by @ScriptRaccoon in #260
• Add functor properties: preserve regular epis / monos by @ScriptRaccoon in #262

Full Changelog ⚙️

v1.12.0...v1.13.0

v1.12.0 - Schema unification

The biggest change is the complete unification of categories and functors on the database level. See #242 for details.

Database 🔋

• Add the categories of filtered vector spaces and of finite-dimensional vector spaces by @ScriptRaccoon in #244

Refactor 🧹

• Schema unification by @ScriptRaccoon in #242
• Smaller fixes that were directly merged into main

Full Changelog ⚙️

v1.11.0...v1.12.0

v1.11.0 - Results on locally ringed spaces, and more

Database 🔋

• LRS does not have a small generating set by @dschepler in #225
• Schemes have no sequential colimits by @ScriptRaccoon in #226
• Add small result about cogenerating sets by @ScriptRaccoon in #228
• Add pretopos property by @dschepler in #232
• Add the forgetful functor Ring → Mon and its left adjoint by @ScriptRaccoon in #233
• Add functor properties: essentially injective / left-invertible by @ScriptRaccoon in #235
• Combine content pages about subcategories by @ScriptRaccoon in #237
• Add several negative properties of LRS_R deduced from those of Top by @dschepler in #231
• Describe epis in LRS by @ScriptRaccoon in #241

Features 🧪

• Add list page for content pages by @ScriptRaccoon in #229
• Revision of Home Page by @ScriptRaccoon in #230
• Expand page with missing data by @ScriptRaccoon in #236
• Record database downloads by @ScriptRaccoon in #239
• Extract separate proof length script by @ScriptRaccoon in #238

Refactor 🧹

• Refactor queries: avoid type casts by @ScriptRaccoon in #240

Full Changelog ⚙️

v1.10.0...v1.11.0

v1.10.0 - More Examples of Functors

The biggest change is the unification of categories and functors in the frontend (#193). Also, many more functors have been added.

Features 🧪

• Unification of categories and functors by @ScriptRaccoon in #193
• Support for adjoint functors by @ScriptRaccoon in #206
• Redundancy check for functor property assignments by @ScriptRaccoon in #207
• Improve styling of lists by @ScriptRaccoon in #208
• Make functor property labels more readable (preserves X) by @ScriptRaccoon in #213
• Automated source and target restrictions of functor properties by @ScriptRaccoon in #218
• Various UI improvements by @ScriptRaccoon in #221

Database 🔋

• Add some functors by @ScriptRaccoon in #204
• Cat does not have a regular subobject classifier by @dschepler in #209
• Add property: ℵ₁-cofiltered limits by @ScriptRaccoon in #200
• Add basic functors for the category of sets by @ScriptRaccoon in #211
• Add the Crude Monadicity Theorem by @ScriptRaccoon in #212
• Add three functors on abelian groups related to torsion by @ScriptRaccoon in #215
• Meas is not regular by @ScriptRaccoon in #216
• Sh(X) never has a generator (unless X has the indiscrete topology) by @dschepler in #210
• Add missing proofs for FinGrp, FS, Met by @ScriptRaccoon in #217
• Rename: reason -> proof by @ScriptRaccoon in #220
• Functors between monoids and groups by @ScriptRaccoon in #222

Refactor 🧹

• Refactor seed script by @ScriptRaccoon in #223

Full Changelog ⚙️

v1.9.0...v1.10.0

v1.9.0 – Filling the Gaps

Features 🧪

• Convert resources and contribution pages to content pages by @ScriptRaccoon in #192
• Handle undecidable properties as assignments by @ScriptRaccoon in #203

Refactor 🧹

• Merge category and functor deduction scripts by @ScriptRaccoon in #191

Database 🔋

All these PRs belong to #194. The number of unknown (category, property)-pairs went down from 151 to 116.

• Add property: ℵ₁-filtered colimits by @ScriptRaccoon in #179
• Small groupoids are generalized varieties and finitely accessible by @ScriptRaccoon in #195
• Decide multi-completeness for remaining categories by @ScriptRaccoon in #196
• Add criterion for sifted colimits by @ScriptRaccoon in #197
• Add new properties: ℵ₂-small products / coproducts / powers / copowers by @ScriptRaccoon in #199
• Decide some properties of FS and Rel by @ScriptRaccoon in #198
• Some coaccessibility proofs by @ScriptRaccoon in #201
• Decide all properties for the category of Hausdorff spaces by @ScriptRaccoon in #202

Full Changelog ⚙️

v1.8.0...v1.9.0

v1.8.0 - Compact spaces, Content pages

Infrastructure 💻

• Use BFS for deductions + Refactor by @ScriptRaccoon in #174
• Replace PDFs with markdown-rendered pages by @ScriptRaccoon in #184
• Replace all lemmas with markdown-generated content pages by @ScriptRaccoon in #188

Features 🧪

• Remove unused stuff by @ScriptRaccoon in #167
• Add sticky headings in long lists by @ScriptRaccoon in #168
• Display contradiction proofs on the search results page by @ScriptRaccoon in #170
• Fix cropped proofs by @ScriptRaccoon in #177
• Add help messages for new users by @ScriptRaccoon in #178
• Add focus to the given property in list of relevant implications by @ScriptRaccoon in #181
• Content pages: various improvements by @ScriptRaccoon in #189
• Show implication usage by @ScriptRaccoon in #190

Database 🔋

• Consistent category links by @ScriptRaccoon in #169
• Add the category of countable groups by @ScriptRaccoon in #171
• Assign easy properties first by @ScriptRaccoon in #173
• Add category of compact Hausdorff spaces by @dschepler in #160
• Add new property: locally finite by @ScriptRaccoon in #180
• Strengthen additive_effective_congruences_imply_normal by @dschepler in #185
• Add Barr-(co)exact properties by @dschepler in #186
• Write property instead of property_id in YAML files by @ScriptRaccoon in #183
• Small LaTeX adjustments by @ScriptRaccoon in #187

Full Changelog

v1.7.0...v1.8.0

v1.7.0 - Hello YAML

A major change to CatDat has been introduced in #164: all categorical data is now authored via YAML files. Each category now has its own YAML file, making the data much easier to maintain. The SQL database is still used for processing and querying data. See the PR description for details.

The redundancy check script developed in #155 makes it easy to determine which property assignments are actually necessary.

Features 🧪

• Add Redundancy Tests by @ScriptRaccoon in #155
• Create list page of lemmas by @ScriptRaccoon in #166

Infrastructure 💻

• Separate assignment of dual categories by @ScriptRaccoon in #157
• Fix update script by @ScriptRaccoon in #159
• Record schema changes by @ScriptRaccoon in #161
• Use IDs to order tags, special objects, and special morphisms by @ScriptRaccoon in #165
• Input all categorical data via YAML files by @ScriptRaccoon in #164

Database 🔋

• Add the category of semigroups by @ScriptRaccoon in #158

Full Changelog ⚒️

v1.6.0...v1.7.0

v1.6.0 - Three major updates

Infrastructure 💻

• Use local SQLite database by @ScriptRaccoon in #138

This is a major change. The SQLite database of CatDat is no longer hosted remotely on Turso, but is shipped directly with the application. This is possible because it is read-only at runtime. Among other things, this provides a significant performance boost for the web application (search + comparison) and simplifies the deployment process. See the PR description for details.

Features 🧪

• Support LaTeX macros by @ScriptRaccoon in #152

This makes writing LaTeX much easier.

Database 🔋

• Add the category of torsion abelian groups by @ScriptRaccoon in #150
• Has effective (co)congruences properties by @dschepler in #126

The PR on effective (co)congruences was a massive effort. It introduces many interesting results and non-trivial proofs.

Full Changelog ⚒️

v1.5.0...v1.6.0