You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Database schemas are formalized as sketches of various sorts (EA Sketches = finite limits + coproducts).
“The database schema is the structure of a database described in a formal language supported typically by a relational database management system (RDBMS).”
“The term "schema" refers to the organization of data as a blueprint of how the database is constructed (divided into database tables in the case of relational databases).”
“The formal definition of a database schema is a set of formulas (sentences) called integrity constraints imposed on a database.”
Claude 3 Opus:
“*In database theory, an integrity constraint is a rule that ensures the accuracy and consistency of data within a database. It defines conditions that must be satisfied for data to be valid. Here's an example of an integrity constraint:
Consider a database table named "Employees" with columns: "EmployeeID", "FirstName", "LastName", "Email", and "Age". An integrity constraint on this table could be:
SQL representation:
ALTER TABLE Employees
ADD CONSTRAINT unique_employee_id UNIQUE (EmployeeID);
SQL representation:
ALTER TABLE Employees
ADD CONSTRAINT valid_email CHECK (Email LIKE '%@%.%');
SQL representation:
ALTER TABLE Employees
ADD CONSTRAINT valid_age CHECK (Age >= 18);
These integrity constraints help maintain the accuracy and consistency of the data in the "Employees" table. They prevent invalid or inconsistent data from being inserted or updated, ensuring the reliability and integrity of the database.
Integrity constraints can be defined at the table level or the database level, and they can include various types of rules such as uniqueness, referential integrity (foreign key constraints), check constraints, and more. They play a crucial role in maintaining data quality and enforcing business rules within a database system.*”
nLab:
The notion of a sketch (Bastiani & Ehresmann 1972) is one formalisation of the notion of a theory. It is diagrammatic, and has the advantage of being very close to category theory, allowing it to very naturally express the category theoretic structure which is required to construct a model of the theory (finite products, say). On the other hand, it is not a very concise notion: as Example 3.2 illustrates, writing down the full details of a sketch even in the simplest examples takes time!
There is a precise correspondence between categories of models of sketches and accessible categories and locally presentable categories, discussed below.
The notion of a sketch generalises that of a Lawvere theory.
Definition 2.1.
A sketch is a small category equipped with a set of cones and a set of cocones.
39FC1919-F298-480B-965C-19AF45BEE564.jpg
nLab:
843E6FC9-70D5-4987-A49F-65175911BF8C.jpg
This is saying that the comma category of two functors and is ‘like’ an arrow category. An arrow category is the category whose objects are the arrows of some other category, and whose morphisms are mappings between the domain and codomain objects of each arrow, which commute with the arrows. In other words, in a category with 2 parallel arrows between and , a “morphism” in could map to , and to . These maps are not morphisms in the original category . Instead, they are “made up”, in a sense, provided they allow 2 equivalent paths from to .
Saying that, I believe this is wrong. The above arrow would describe an identity arrow in , and I believe (it being functorial) implies that . We can consider another example where .
The arrow category is isomorphic to the functor category. In order to understand how a comma category is a sub-category of the functor category (?), I need to understand why the functor category and arrow category are isomorphic.
I would like to engage with this post as I have spent a lot of time studying this paper, but I'm not sure how to. The description of the stream is "If you are looking for references, want to start a reading group, or are running a reading group, post here." This post doesn't fall clearly into any of those categories, except perhaps it is trying to start a text-based reading group for the paper? Though it doesn't say that explicitly. Or is it the "learning out loud" approach that @David Egolf is experimenting with here? Though again it doesn't say that explicitly. Right now it just seems like Julius's personal notes and hence I'm not sure how to engage with it. Maybe Julius can explain what he intended with the post, or someone with more experience than me on the forum will have some insight.
I am heavily influenced by David Egolf’s suggestion to “learn out loud” and I guess I hoped/expected people may want to suggest ideas and commentary based on what they see above. My thought was that the “reading group” channel could just have the title of a specific text in one of its streams, so it would be a place for anyone to view past notes and commentary when they wanted to read that text too.
So yeah, please engage with it freely, if you please. (That was my hope.)
I love this stuff! I've been thinking about Spivak's Ologs for like 8 years now. It's led me down many paths, mostly in higher and formal category theory and higher type theories. It seems like structure specification is a central community effort, ranging from actual implementations such as algebraic databases, to hypothetical n-theories which have been discussed here many times.
In general there is something like a sketch or schema, something like a doctrine specifying the structure of the schema, and something like a topos providing algebras for the schema, and this is how you specify structure.
I guess it could be a good idea, if there are things you particularly want people to respond to (rather than just absorb at will if they're also learning this stuff), to highlight that. It's a lot to read through for people who, say, already know this paper pretty well and would be happy to help clarify sticky points if you have them.
Sure. My goal today is to understand what sketches / EA sketches are. Which depends on me understanding things like cones, arrow categories, and comma categories. I will try to write a document showing my current take on this.
In case you haven't run across this book yet, I'd like to suggest "Notes on Category Theory" (by Perrone) as a possibly helpful reference. You can find it here: https://arxiv.org/pdf/1912.10642.pdf. For example, cones are discussed starting on page 82.
It looks really good and I will read it. That said, I learn way better by asking myself tons of questions, then reading afterwards, as it is more illuminating that way for me.
These were my thoughts this morning. Working up to thinking about cones, I spent some more time thinking about categories. I will move ahead to cones later today. Thanks.
Nice notes, there is a lot to say but for now I will just say that the example of sets with two kinds of morphisms, functions and relations, is nicely encapsulated in the double category https://www.epatters.org/wiki/algebra/relations-in-category-theory
A double category has two kinds of morphisms, vertical morphisms and horizontal morphisms, as well as 2-cells which fill squares made up of vertical and horizontal morphisms --- so the vertical and horizontal morphisms have to fit together in some kind of way to assemble into a double category, they can't just be completely independent. I'm not sure what has been done to generalize the idea of double categories to have arbitrarily many types of morphisms but it is an interesting direction for sure.
(If the types of morphisms between objects really are completely independent and have nothing to do with each other, I don't see the motivation in putting them together into a single structure rather than just allowing them to be different structures that happen to have the same objects)
Joshua Meyers said:
I'm not sure what has been done to generalize the idea of double categories to have arbitrarily many types of morphisms but it is an interesting direction for sure.
There are [[n-fold categories]] for any .
BTW, CQL contains Professor Rosebrugh's "EASIK" implementation of EA sketches, along with translation to CQL. (tools menu->EASIK)
Screenshot-2024-04-05-at-11.53.35AM.png