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.
When I want to model a scenario, I find ordered pairs to be paramount.
In a system to be modeled, one often has some entities, and some relationships between them. Perhaps the relationships are functions, or maybe they don't meet the criteria of a function, in which case they are relations; and relations are defined in terms of products. It seems like all of our modeling needs can be reduced to having "a category with products".
However, it seems like products have a kind of arbitariness. In modeling a system, the real reason we use ordered pairs is to track associations or correspondences. For example, let there be a collection of commodities and a collection of people. Each person owns some quantity of some commodities.
I can model this in equivalent ways. I can form ordered pairs of commodities and quantities. A collection of such ordered pairs can represent a person who owns those commodities in those quantities. In this choice of modeling approach, we do not have a set of primitive elements called "people". We associate a person with what they own: . The "representation of people" is because we choose to name a set with the name of a person.
We can also include people as primitive elements. We can form ordered triples associating a person with a commodity and with a quantity: . Or, we could have chosen to first group commodities with quantities, then people with commodity-quantities: . Or, we could have represented ownership as a function, .
None of this matters, because all of the above representations have the same information. From the perspective of category theory, it seems like we are just forming products, . Regarding universal properties, it seems like category theory helps us clear away surface details and find a canonical representation of structures.
However, it makes me feel like we are using the fact that products form an order of elements as a heuristic to track correspondences. What I truly want is to preserve the information that "Melissa owns 3 Bitcoins". If my model represents ownership as a triple , then I have a standard format by which I can extract information from any ordered triple that comes my way. But the order of the elements was never the point. I could model the same information as .
Is there an even better "universal" way to model this?
My only idea has been to tag the type of the elements and define functions that seek out an element of that type, in an unordered set, as their argument. For example, consider a transaction to be changing the "person" element in an ownership-triple: . Specifying a giver, a receiver, and a commodity, you receive a new ownership triple for the new owner. Instead of relying on the order of elements in the tuples, we can tell the function what to do with the input data based on each element's type: . I may also use spans as generalized relations.
perhaps you are looking for so-called "indexed products", where the projections of an n-ary, unordered tuple are labelled by elements from an arbitrary set, rather than "first" and "second"?
It's worth noting that your modeling alternatives are not all equivalent. If we say that P=People is a subset of CxQ (Commodity x Quantity), then we can't have two people with the same ownership profile, whereas taking a set of triples will allow this.
Of course, taking spans rather than relations addresses this issue
You may get some insight from looking at the way that undirected graphs are modeled as presheaves. Instead of getting rid of directed edges (as in the graph schema ), we associate an undirected edge with a pair of directed edges, related by an involution. This trick of adding in all (ordered) permutations to represent an unordered structure is pretty common.
You can try the AlgebraicJulia blog for a discussion of this approach.
Ryan Wisnesky said:
perhaps you are looking for so-called "indexed products", where the projections of an n-ary, unordered tuple are labelled by elements from an arbitrary set, rather than "first" and "second"?
Would you have a formal definition on hand?
Mendelson gives one standard definition of indexed products here on Math Stackexchange.
Given a set , and a set for each , an element of the product
is a function that maps each to some element .
See the answer to the original question on Math Stackexchange for more.
This is all very interesting and I will be thinking about how to use the above ideas in my mathematical models.
Ok, so in a category, instead of having a product whose projection morphisms are numbered, we have projection morphisms that are indexed by any set. It looks like this is discussed in the article [[family of sets]], and generalized in [[dependent product]].
Does anyone have an exercise or proof that can help me learn more about dependent products?
I'm not so good at this stuff, but you can prove that if you have a category C that has finite products whose projections morphisms are numbered, then C also has finite products whose projection morphisms that are indexed by any finite set.
(I'm putting a finiteness restriction in here just to make the problem easier to think about. It's not necessary, but the concept of 'numbered' for infinite products requires using numbers that aren't finite, e.g. infinite ordinals, which is a distraction here, I think.)