As I have been pursuing algebraic geometry over the last two years I have slowly developed some language of category theory to the point where category theory, in some sense, ‘seems natural’, because now it feels motivated by its interaction with algebraic geometry. Recently I have started skimming some books on general category theory, and I have some related questions pertaining to the axioms and definition of a category. I am using the definition given on Wikipedia.
Most of my questions that follow are irrelevant as long as the category is ‘naturally arising’ in some way (e.g. at least locally small) and the morphisms are some familiar way of connecting objects (e.g. functions), so I ask my questions geared towards a completely arbitrary category, C, such that all of the data and axioms in the Wikipedia definition is satisfied.
Each part of the definition requires specifying a class of something (objects or morphisms). Is there a standard formalization of a proper class that is used in category theory? If not, is there some canonical way to think of a proper class that is sufficient for having a firm foundation for category theory?
By specifying my class of morphisms, we have the hom class, hom(a,b) (a subclass?), for any objects a and b. To define a category one must also specify how to compose morphisms. In a usual setting, specifying the morphisms alone usually carries this information without mention. This is the requirement that we have a binary operation hom(a,b) $/times$ hom(b,c) /to hom(a,c). My question here is, is the notion of cartesian product and binary operation formalized for proper classes? Can you just ‘localize’ the proper class to be a set in any specific place as needed? Also, for a long time I interpreted this axiom as essentially saying that anytime I have the morphisms f: A —> B, and g: B —> C, I necessarily have a commutative triangle where the diagonal arrow is $g /circ f$. Is this an acceptable way to think of this? I.e, if I specified some morphisms that had a natural way to be composed associatively (like functions of sets), but I perversely specified my binary composition operation to be something unusual, yet satisfying associativity and identity, it wouldn’t effect the fact that I have a commutative triangle because the composition operation I defined is the one the category would use to determine what diagrams are commutative and which aren’t? I.e the actual composition function in the usual sense $g /circ f$ may be a morphism in my hom class, but I have defined $g /circ f$ to be something different, is the triangle I get still considered commutative? I hope this question is clear, sorry for being confusing.
Lastly, the associativity axiom and the identity axiom both use the symbol “=“ as a connective between elements of the hom class (I don’t know anything about classes, I assume element is still used to mean something “in” the class?). Is this notion of “=“ something that is determined by how I have specified my hom class? For example, if morphisms are usual set theoretic functions, then we have a natural way to check if two functions are the same using the “subset of Cartesian product” definition, since the first axiom of ZFC tells us exactly what it means for two sets to be the equal. Then two such functions would be the “same” / “=“ in the sense that they represent the same element of my hom class, because I determined the truth of “f = g” using the “=“ determined by ZFC axiom 1. However, in this axiom, how the truth value is decided partially only clear since we only allow sets as elements, so when we compare elements of sets we always have the axiom to decide if two elements are equal. In usual Mathematics my elements could be anything. So how should I interpret the meaning of “=“ in the axioms of identity and associativity? Does it depend on the objects I define to be morphisms (depends of the specification of Hom class)? Does it depend on a logic (logical / first order characterizations using properties for what “=“ means)? Or is it actually a category theoretic notion of “=“, in the sense that we could characterize the equality of two morphisms by some universal property?
Edit: Or is category theory avoiding these foundational issues by not making these things precise, and that it is just the case that if C Is some category, then “id $/circ f$ = f” is a true statement in whatever logic or interpretation has been chosen?
Also, I’m really sorry my question is so sloppy. I’m on my phone right now but will be on a computer soon and polish this up a bit.