Category Theory
Zulip Server
Archive

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.

Stream: learning: questions

Topic: Quick Question on Yoneda Structures

John Onstead (Apr 17 2024 at 14:08):

When first learning category theory, we learn about the Yoneda Lemma and how to prove it. There's an entire proof involving clever uses of the identity morphism (these proofs can be found anywhere). It's then said that category theory is "the set of consequences of the Yoneda Lemma". I'm not sure how hyperbolic that statement is, but clearly the Yoneda lemma is a key first step in many proofs within category theory, thus making its own proof even more important to understand.
However, later on we learn about formal category theory and the concept of a Yoneda Structure. In a Yoneda Structure, instead of the Yoneda Lemma, we have "Yoneda Axioms" that define the Yoneda Structure. These are meant to specialize to the Yoneda Lemma in the case of Cat, but can be generalized to other structures than typical categories. So here's my question: if the Yoneda Lemma is really a "Yoneda Axiom" in the Yoneda Structure on Cat, then what exactly are we proving in the standard proof of the Yoneda Lemma? That is, if the Yoneda Lemma is actually an axiom, then why need to prove anything at all, since axioms are just presupposed to be true? Is this related in any way to claims that the Yoneda Lemma is trivial or tautologous that some category theorists make?

John Baez (Apr 17 2024 at 14:30):

Of course it's common math to take what began life as a theorem in one context and generalize it to a definition; for example the proof that every complex polynomial can be factored into linear factors - which actually uses analysis - gets generalized into the definition of "algebraically closed field".

Doing this doesn't eliminate the need to prove things, since we still need to prove that the complex numbers are an algebraically closed field. Similarly, we still need to prove that the usual Yoneda structure on Cat actually obeys the Yoneda axioms.

John Baez (Apr 17 2024 at 14:32):

The advantage of proceeding this way is that it saves us from repeating work. After someone has proved a lot of theorems about algebraically closed fields, as soon as we check that a field is algebraically closed, we instantly know all these theorems apply. Similarly, after someone has proved a lot of theorems about Yoneda structures, as soon as we check that a category has a Yoneda structure we instantly know all these theorems apply.

Jean-Baptiste Vienney (Apr 17 2024 at 14:34):

I was writing at the same time, so there should be a bit of overlapping with my answer, but it's probably not exactly the same one.

I think that the sense of the word axiom in mathematics has changed since Euclide. Nowadays, for most mathematicians an axiom is an identity or more generally a proposition that is required to be verified for an object to verify a definition.

For instance, I can say that one of the axioms of a ring is the distributivity of the multiplication over the addition. I don't think many people would be shocked by such a terminology. Probably the word axiom is even more used when such a requirement is something a bit more complex than a simple identity such as this Yoneda axiom. I feel that the word axiom is somehow linked to the idea of synthetic mathematics i.e. when you list all the basic facts which should be verified in some mathematical theory and start with these basic facts. For instance, in synthetic differential geometry.

But these are not exactly axioms in the sense of a fact that we assume to be true because it is obvious. Formally, these are still axioms in the sense of a part of a definition.

Noah Chrein (Apr 17 2024 at 17:15):

Axioms are "presupposed to be true", but theorems make them relevant.

Perhaps someone could have randomly guessed the yoneda structure axioms on a 2 category before knowing what a category was, but it would still be a theorem that categories form a yoneda structure.

Noah Chrein (Apr 17 2024 at 17:19):

There's an ability to guess axioms in formal category theory by scribbling diagrams, but most scribbles are irrelevant until you prove a theorem that connects it to an important idea.

fosco (Apr 17 2024 at 19:31):

The way I see it is a bit different: proving that $Cat$ has a yoneda structure, each time you will conclude that "axiom n is true because yoneda lemma holds in $Cat$"; so, all properties of a yoneda structure hold because yoneda lemma is true. Each axiom is a different thing that in an abstract 2-category we'd like to do, and which in $Cat$ is the yoneda lemma.

fosco (Apr 17 2024 at 19:35):

The fact that the axioms of a yoneda structure are mostly independent from one another (they predicate a property about a certain diagram, and then another, and then another) witnesses how many different things "are" the equivalence of which we take for granted in $Cat$: for example, in a certain sense, the yoneda lemma says that presheaves are colimits of representables, and that every functor has a [relative] left adjoint.

fosco (Apr 17 2024 at 19:38):

I see the situation much like many other settings where an axiomatics on a category is fixed in order to "calculate" in that category as if it was a concrete, paradigmatic example of the class you're axiomatizing: abelian categories, and toposes, for example. And the work of Weber on 2-toposes explains in great detail how after all, a topos and a 2category with a yoneda structure are close siblings.

John Onstead (Apr 17 2024 at 19:50):

Thanks for the insight, this makes sense. So it seems that when moving into more "synthetic mathematics", like going from category theory to formal category theory, you move from proving something satisfies some property to proving that something is an element of some class of thing defined by axioms that encode this property, which then satisfies the original proof by default. So it just shifts what exactly you need to prove, rather than removes the need to prove things altogether.

Part of me wonders if this can be adapted into a valid proof method. For instance, if there's a difficult open problem in mathematics that asks to prove if something has some property, you instead axiomatize this property and assume there is a class of structures that are defined by such an axiomatization. Then you try to prove your original thing is an element of this class. I'm not sure if this is ever used since it is not one of the standard proof methods I've learned about (direct proof, proof by contradiction, proof by induction, etc.) but maybe this shift in perspective could result in some problems being simplified?

Peva Blanchard (Apr 17 2024 at 20:24):

I would say this is a quite old technique. It reminds me of how Al Khwarizmi introduced the "thing" (unknown solution "x" to an equation). To solve an equation, assume that the thing exists, and, by manipulations (adjustment, balancing, etc.), derive enough constraints about it so that its value is determined (I would add: or a contradiction is found).

fosco (Apr 17 2024 at 20:48):

Again, I see it slightly differently: when giving the axioms of topos, abcat, or of yoneda structure you specify properties that are enjoyed by a category as a postulate because they give you a framework to deduce with calculations, formally analogous to the ones you performed if you had concrete sets, ab groups, or categories. These axioms are sensible because they are nonempty (there is a model).

Calculi (in a semi-formal sense) attached to these theories are different, but the idea is the same, indeed to be calculation rules to deduce true facts from axioms.

I have more than one idea on how and why formal category theory is a syntax... we all do (and I consider myself the dumbest of the crowd :grinning:). Somehow making this precise in a satisfactory way is a holy grail of formal ct.

Noah Chrein (Apr 17 2024 at 21:50):

Agree about the holy grail (but not about the dumbest in the crowd). Its like we want to make all structural specification into a purely syntax calculus.

W.r.t. yoneda structures, its not just a generalization for the sake of it, it allows us to do all the cool yoneda calculus in more difficult settings like enriched categories.

John Baez (Apr 18 2024 at 08:32):

John Onstead said:

Part of me wonders if this can be adapted into a valid proof method. For instance, if there's a difficult open problem in mathematics that asks to prove if something has some property, you instead axiomatize this property and assume there is a class of structures that are defined by such an axiomatization. Then you try to prove your original thing is an element of this class. I'm not sure if this is ever used since it is not one of the standard proof methods I've learned about (direct proof, proof by contradiction, proof by induction, etc.) but maybe this shift in perspective could result in some problems being simplified?

Actually this is one of the main proof techniques used in modern math. It can't by itself solve "difficult open problems" - if it could, they wouldn't be difficult or open! But the axiomatic method vastly streamlines the whole process of doing math, by reducing our need to copy proofs over and over in different contexts.

For example supposed you're doing algebra. If you have some ring and you want to prove things about it, the first thing you'll do is ask whether it obeys the axioms of a field, or an integral domain, or a semisimple ring, or a noetherian ring, or an artinian ring, etcetera etcetera. There are dozens of these axiom systems. As soon as you check your ring obeys some of these axioms, you instantly gain access to a whole world of theorems. Learning ring theory largely consists of learning these various axioms, the theorems they imply, and examples of rings obeying these axioms.

The same is true of every other branch of math. By deploying multiple axiom systems hand in hand, we tackle hard problems without having to redo lots of existing work.

For a really hard problem like Fermat's Last Theorem, people must be using results from hundreds of different axiom systems.

By the way, what you're calling axiom systems are also called "definitions". E.g. we define a Yoneda structure to be a blah-di-blah obeying axioms 1, 2 and 3.

Nathanael Arkor (Apr 18 2024 at 08:32):

fosco said:

I have more than one idea on how and why formal category theory is a syntax... we all do (and I consider myself the dumbest of the crowd :D). Somehow making this precise in a satisfactory way is a holy grail of formal ct.

This doesn't align with my experience. It's not clear to me what kinds of problems would be more easily solved using a formal calculus for FCT. This isn't a problem that is ever mentioned in texts on FCT, as far as I'm aware.

Claudio Pisani (Apr 18 2024 at 12:30):

John Onstead said:

When first learning category theory, we learn about the Yoneda Lemma and how to prove it. There's an entire proof involving clever uses of the identity morphism (these proofs can be found anywhere). It's then said that category theory is "the set of consequences of the Yoneda Lemma". I'm not sure how hyperbolic that statement is, but clearly the Yoneda lemma is a key first step in many proofs within category theory, thus making its own proof even more important to understand.

Probably, this is not strictly related to your question, but personally I had a better relationship with the Yoneda lemma since I learned to see it in the following way.
Given a category $C$, the category $Cat/C$ has both a reflection and a coreflection in $dof/C$, the category of discrete (op)fibrations over $C$.
In particular, for any object $x\in C$, considered as a functor $x:1 \to C$ in $Cat/C$, its reflection $\overline x$
in discrete opfibrations has the set of arrows $C(x,y)$ as its fiber over $y\in C$ etc.
That is, it corresponds to the representable $C(x,-)$ under the equivalence $dof/C = Set^C$.
Then the adjunction between $dof/C$ and $Cat/C$ gives, as a particular case, the Yoneda lemma:
$Nat(C(x,-),F) = dof/C(\overline x;F) = Cat/C(x,F) = Fx$.
I find this form of Yoneda more visualizable or concrete than the usual one, bringing it in a more ordinary position.
This is how I would introduce it in a course of category theory: the "best" way to turn an object of $C$ in a discrete opfibration over $C$.

John Onstead (Apr 18 2024 at 14:09):

Ah thanks for the insight! I probably need to read more math proofs, maybe I can see some examples of this in action!
Fields, integral domains, semisimple rings, etc. all form categories (subcategories of Ring). This makes me wonder about the connection between categories and the axioms/theorems/statements that apply to the objects inside of them, but there's some things I'm still not clear about in this regard. I'll ask another question making these more concrete.

Jean-Baptiste Vienney (Apr 18 2024 at 17:43):

There is a lot to say about the connection between categories and the axioms/theorems/statements that apply to the objects inside of them! This is basically what categorical logic is about.

John Baez (Apr 18 2024 at 19:00):

In the case of rings, this is also what books like Anderson and Fuller's Rings and Categories of Modules is about. Here the idea is not to study various subcategories of Ring, although that is also great fun. The idea is that every ring $R$ has a category of modules, $R\mathrm{Mod}$, and we can learn a lot about a ring $R$ by studying $R\mathrm{Mod}$ and its properties. In fact there's an important 2-category of

• categories $R\mathrm{Mod}$ (which are [[abelian categories]])
• [[additive functors]] between such categories
• natural transformations between such functors

and studying this plays an important role in ring theory (though Anderson and Fuller never mention 2-categories).

John Onstead (Apr 18 2024 at 19:08):

@Jean-Baptiste Vienney Yes, though in my question here I make a confusion I have about this more precise. Internalizing statements about a mathematical object via categorical logic works for a category you define some object in, not the category of the mathematical object itself- for instance, any statement made about groups (like the group axioms or any theorem about groups) exists internally to Set, not Grp. I wanted to know what statements about groups means in the context of Grp itself, not Set. For instance, you can give a commutative diagram for each group axiom in Set. But where do the group axioms appear in Grp? Where do I look inside of Grp to find them?

John Onstead (Apr 18 2024 at 19:09):

@Claudio Pisani Ah I didn't see this post earlier. This is a really fascinating take on the Yoneda Lemma, I don't believe I've seen it introduced that way before. I'll certainly have to think more about it!

John Baez (Apr 18 2024 at 19:58):

John Onstead said:

But where do the group axioms appear in Grp? Where do I look inside of Grp to find them?

I don't know how to do that, but you can find them systematically if you're also given the forgetful functor Grp $\to$ Set. The same method works for the category of rings, etc.

Julius Hamilton (Apr 18 2024 at 20:06):

What specifically should that functor map each group to, in order for it to capture information about the group axioms?

Julius Hamilton (Apr 18 2024 at 20:07):

Sets representing the values of the law of composition (as a relation)?

Kevin Carlson (Arlin) (Apr 18 2024 at 20:20):

No, the ordinary forgetful functor mapping a group to its underlying set.

Julius Hamilton (Apr 18 2024 at 21:08):

I’m trying to relate this to this idea of a representable functor, but I think there’s a detail I’m not clear on.

For a functor $F: C \to Set$, if for all $X \in Ob(C)$, $Hom(\Omega, X) \cong F(X)$, we call $F$ a representable functor, and I think we call $\Omega$ a classifying object.

My hope is that we interpret $Hom(\Omega, X)$ as $F(X)$. Then if $C$ is $Grp$, $X$ is a group, and $F(X)$ is the base set of $X$, it would seem to be saying that $Hom(\Omega, X)$ is “the base set”. In that case, it would seem like $\Omega$ “adds the group structure” to the set represented by $Hom(\Omega, X)$. Then that would mean that $\Omega$ is some very special group, I think. How inaccurate is this view; and also, I realized I don’t understand what “bijective” would mean in this case, since that term applies to functions.

Kevin Carlson (Arlin) (Apr 18 2024 at 21:53):

$\Omega$ is definitely a very special group, and it’s true in some sense that $X$ gets its group structure from $\Omega.$ You should try to figure out which group has the property that group homomorphisms out of it are naturally “the same as” elements of the codomain.

Kevin Carlson (Arlin) (Apr 18 2024 at 21:53):

I’m not sure which use of “bijective” you’re referring to. You wrote $\cong$ at one point but it’s between two sets so there’s no problem with that being a bijection.

Jean-Baptiste Vienney (Apr 18 2024 at 22:09):

The axiom of a group homomorphisms correspond to the naturality of the multiplication $\nabla:A \times A \rightarrow A$ in the category of groups and all functions between them. The axioms of a group can somehow be expressed as commutative diagrams in this same category using this natural transformations and also the two natural transformations $\eta:\top \rightarrow A$ and $\_^{-1}:A \rightarrow A$ (the naturality of these ones being implied by the naturality of $\nabla$) but all this is not happening in Grp because the multiplication, the unit and the inverse are not group homomorphisms...

Jean-Baptiste Vienney (Apr 18 2024 at 22:15):

In the same way, you can't state the binomial theorem in the category of commutative rings, because it involves maps which are not ring homomorphisms...

Jean-Baptiste Vienney (Apr 18 2024 at 22:19):

If you don't want sets, you can express the axioms of a group, a ring and similar structures in any cartesian category.

Jean-Baptiste Vienney (Apr 18 2024 at 22:23):

Sorry, you must add a forgetful functor somewhere I think for the natural transformations above.

Kevin Carlson (Arlin) (Apr 18 2024 at 23:32):

I don't think the "category of groups and all functions between them" is a good thing to consider--it's just an inconvenient way of talking about the category of groups with its forgetful functor.

Kevin Carlson (Arlin) (Apr 18 2024 at 23:34):

And as you suggested, your $\nabla$ is not actually natural in that category. It's a natural transformation from $U(-)\times U(-)\to U$ where $U$ is the forgetful functor. But that's still not really how I'd try to "find the axioms of a group" in the category of groups (with its forgetful functor).

John Onstead (Apr 18 2024 at 23:57):

Thanks for the help; I do apologize that my question was a little vague since identifying what something "looks like" in a category isn't necessarily a standard category theoretic concept. But it seems to me from what was stated that you can't always tell what statements the objects in a category obey just from the category itself, at least not without the forgetful functor. I guess this makes sense, since the forgetful functor tells you which category the objects in your category are "defined" from. Especially since it is possible that objects in equivalent category can be defined in completely different ways (with different axioms involved) based off of different categories (like how a monoidal poset is a monoid object in Pos and also a "partial order object" in Mon).

Even if this is true, statements have to be doing something to these categories, at least in terms of their structure. For instance, couldn't Lagrange's theorem for groups be seen as some form of restriction on the way subobjects must act within the category Grp? Maybe a better question would then be: in which ways does a statement about a class of objects restrict the possible structures of the category of that class of objects?

fosco (Apr 19 2024 at 07:32):

Nathanael Arkor said:

fosco said:

I have more than one idea on how and why formal category theory is a syntax... we all do (and I consider myself the dumbest of the crowd :grinning:). Somehow making this precise in a satisfactory way is a holy grail of formal ct.

This doesn't align with my experience. It's not clear to me what kinds of problems would be more easily solved using a formal calculus for FCT. This isn't a problem that is ever mentioned in texts on FCT, as far as I'm aware.

I never said that the problem is using the language, as much as it is to find it. There are proposals, as you know better than me. The agreement on how well they work and what's their domain of applicability is still under construction

(BTW: texts on FCT? Where have you seen one :grinning: )

Nathanael Arkor (Apr 19 2024 at 08:01):

fosco said:

Nathanael Arkor said:

fosco said:

I have more than one idea on how and why formal category theory is a syntax... we all do (and I consider myself the dumbest of the crowd :D). Somehow making this precise in a satisfactory way is a holy grail of formal ct.

This doesn't align with my experience. It's not clear to me what kinds of problems would be more easily solved using a formal calculus for FCT. This isn't a problem that is ever mentioned in texts on FCT, as far as I'm aware.

I never said that the problem is using the language, as much as it is to find it.

But what point is there in finding a language if it doesn't have uses?

Nathanael Arkor (Apr 19 2024 at 08:01):

fosco said:

Nathanael Arkor said:

fosco said:

I have more than one idea on how and why formal category theory is a syntax... we all do (and I consider myself the dumbest of the crowd :D). Somehow making this precise in a satisfactory way is a holy grail of formal ct.

This doesn't align with my experience. It's not clear to me what kinds of problems would be more easily solved using a formal calculus for FCT. This isn't a problem that is ever mentioned in texts on FCT, as far as I'm aware.

(BTW: texts on FCT? Where have you seen one :D )

Well, I just mean papers.

John Onstead (Apr 19 2024 at 13:20):

I finally think I understand it now after giving some more though! I realize the problem of trying to determine the impact of a statement holding for objects inside a category is just a "categorification" of the original axiomatization process we discussed above. In that process, we had some singular structure, proved a theorem about it, and turned this theorem into a definition for "an X", such that we could complete the original proof by proving that our original structure was an X. Now, it's the exact same situation but instead of a singular structure we have a class/category of structures, and the theorem we proved is about the class/category as a whole (applying to all objects within it). We can turn this theorem into a definition for an "X category", a category with extra structure/property such that a version of our original theorem holds "inside" any X category, and we can complete the original proof by proving our original category can have the structure of an X category on it in the right way. I believe this reasoning works for the Yoneda Lemma: we start with the Yoneda Lemma as a theorem about the category Cat that applies to all objects (categories) within it, and then define an axiomatization of this in a Yoneda Structure, so that we can then prove the Yoneda Lemma by proving Cat has a Yoneda Structure on it.

This is a categorification because X categories form a 2-category. It's also a categorification in the 1-theory to 2-theory sense: in our first case, we were examining statements modeled in/internal to, say, Set when axiomatizing our theorem into a definition. Now, we are examining models into Cat since we are determining what extra properties and structure our category should have for an internal version of our statement to hold.

John Onstead (Apr 19 2024 at 13:34):

I've got a decent example to illustrate with Lagrange's Theorem. Lagrange's theorem is not a statement about a specific object but rather a whole class of objects, that being the class of all finite groups (the category FinGrp), so it will work well as an example. Our job now is to axiomatize the properties we'd like a category "like" FinGrp to have such that something like Lagrange's Theorem holds "inside" them as well. To do this, we will define the notion of a "Lagrange category" to be the following: A Lagrange Category is a category C, equipped with a faithful functor F (not necessarily into Set), such that such that if H is a subobject of G in C, then F(G) ~ Coset(G, H) x F(H) in the codomain of the faithful functor. (I'm not sure how to internalize the notion of the set of left cosets of H in G in an arbitrary category so I just called this a "coset" construction). I believe if I did everything right (I probably did not since I kind of got into category theory before group theory, please correct me on anything I got wrong!) then for C = FinGrp and F the forgetful functor from FinGrp to Set, this specializes to Lagrange's theorem. Then, to prove Lagrange's theorem holds for all groups, thus all objects in FinGrp, we can just show that FinGrp has such a Lagrange Category structure on it.

Nathanael Arkor (Apr 19 2024 at 13:41):

You have the implication the opposite way round to how I understand the situation. Say we have some theorem A about a structure X, which is a special kind of Y. Then we might try to define conditions on a Y for which we can state an analogue of A (but not prove it in general), which we might call B. We might then call a Y for which B holds a "B-Y". Now, the fact that X is itself a B-Y is exactly the statement that theorem A holds.

Nathanael Arkor (Apr 19 2024 at 13:42):

However, it seems misleading to say that we can prove that theorem A holds by showing that X is a B-Y (even if that is technically true, because theorem A iff X is a B-Y). Rather, we use theorem A to show that X is a B-Y.

Nathanael Arkor (Apr 19 2024 at 13:42):

In the concrete example, we use the Yoneda lemma to show that Cat has a Yoneda structure. We don't use the fact that Cat has a Yoneda structure to prove the Yoneda lemma.

Nathanael Arkor (Apr 19 2024 at 13:43):

Because the entire point was that we already knew the Yoneda lemma held, and we were trying to axiomatise this situation.

Nathanael Arkor (Apr 19 2024 at 13:45):

Then, each time we want to find a new example of a Yoneda structure, the proof that a particular 2-category has a Yoneda structure is analogous to proving a Yoneda lemma for that 2-category.