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.
John Onstead (Apr 18 2024 at 14:23):Following from my post yesterday, I have a question that deals in general with what a statement (theorem or axiom) "looks like" in category theory and how it relates to the internal logic/language of a category. So in many cases, categories with extra properties or structure have some "internal language" that you can reason within, with the kind and expressiveness of that reasoning dependent on the properties and structure. For instance, one can think of Lawvere theory categories as having an internal (finitary) algebraic theory, and a product-preserving functor from it represents a model of this theory internalized into the codomain category (by functorial semantics). In this way statements in general can be internalized through models. This is how group objects are internalized from the Lawvere theory of groups: the group axioms are statements written in a finitary algebraic language, and a product preserving functor from the Lawvere theory of groups acts to internalize these statements into some category (for instance, Set). Theorems, as another kind of statement, should be internalizable as well.
But here's where my confusion starts. If I prove a theorem about groups (group objects internal to Set), my work is done within the context of Set and so the theorem is a statement internal to the category Set, not Grp. But if theorems about some object are internalized into the category where such an object can be defined, then what is the theorem doing in the resulting category of those objects? That is, say I prove a theorem about groups- how does this theorem manifest in the category Grp itself? Can it be expressed in the internal language of Grp, or does it manifest in a different way?
Secondly, as mentioned in the previous post, one can axiomatize a theorem and get a class of mathematical objects satisfying the axioms/definition, one of which will include the original setting/structure the theorem was proven for. Of course, classes of mathematical objects, along with their structure-preserving mappings, can be expressed as categories. So my question here is then: how can we tell if a given category has a certain statement as one of its "laws"? Is there a way to define the concept of a "domain of applicability" of a statement which manifests itself as a category property or structure, such that if I prove a category satisfies this property or has this structure, it tells me the objects in the category obey this statement? For instance, some theorems may apply to both groups and monoids, and some may only apply to groups. This means that both Grp and Mon would possess the "domain of applicability" property/structure of the former theorems, but only Grp would of the latter theorems. If this is possible, how would this connect to my previous points on categorical logic and model theory discussed above?
El Mehdi Cherradi (Apr 18 2024 at 14:48):It is important not to confuse the "internal logic" of a category with the "internal language" of a (class of) categories. The latter is the syntax which is used to make some reasoning while the former has to do with semantics, it is a model/instance of the syntax.
I feel like the rest of your question is very much independent of category theory and could be phrased for model theory/type theory. Unless I am misunderstanding your question, if you can express some property in a given language and that you can deduce from the syntactic rules some theorems, then certainly the corresponding statement holds in any model of your syntax.