Creating a new category that is the 'opposite' of an existing category (Ex 3.1 from Aluffi Chapter 0) This is the first exercise in the section that introduces Categories in Aluffi's Algebra text (Ch.1 Sec.3). Since this is my first exposure to categories, I wanted to know if:

*

*I'm properly understanding the basic definition of a category

*My logic is correct

*The language and notation in my proof are idiomatic (e.g. Aluffi seems to use set-theoretic notation like $\in$ in the exposition).

Exercise 3.1:
Let $\mathsf{C}$ be a category. Consider a structure $\mathsf{C}^{op}$ with

*

*$\mathrm{Obj}(\mathsf{C}^{op}) := \mathrm{Obj}(\mathsf{C})$

*for $A,B$ objects of $\mathsf{C}^{op}$ (hence objects of $\mathsf{C}$), $\mathrm{Hom}_{\mathsf{C}^{op}}(A,B) := \mathrm{Hom}_{\mathsf{C}}(B,A)$.

Show how to make this into a category (that is, define composition of morphisms in $\mathsf{C}^{op}$ and verify the properties listed in $\S3.1$).
Intuitively, the 'opposite' category $\mathsf{C}^{op}$ is simply obtained by 'reversing all the arrows' in $\mathsf{C}$.
My Solution (original; see below for updated solution based on feedback):
Remember that by definition, a category must have i) an identity morphism for all objects in the category and ii) a composition morphism for any pairs of morphisms. Additionally, the composition must satisfy two additional properties: a) associativity and b) unital (e.g. for $f: X \to Y, f1_X = 1_Yf = f$).
i) Identity morphism: If $A$ is an object in $\mathsf{C}^{op}$, it also exists in $\mathsf{C}$ (by definition of $\mathrm{Obj}(\mathsf{C}^{op})$). Since $\mathsf{C}$ is a category, it satisfies the property of having an identity morphism for each object. Since we chose $A$ in $\mathsf{C}^{op}$ arbitrarily, it follows that every object in $\mathsf{C}^{op}$ has an identity morphism.
ii) Composition morphism: Let's define composition of morphisms as follows: for $f \in \mathrm{Hom}_{\mathsf{C}^{op}}(A,B)$ and $g \in \mathrm{Hom}_{\mathsf{C}^{op}}(B,C)$, define $fg \in \mathrm{Hom}_{\mathsf{C}^{op}}(A,C)$ such that $fg = gf \in \mathrm{Hom}_{\mathsf{C}}(C,A)$. We know $gf$ exists because $\mathsf{C}$ is a category and thus satisfies the condition of having a composition morphism for all pairs of morphisms.
To prove that the composition morphism is both associative and unital:
a) Associativity: Let $f \in \mathrm{Hom}_{\mathsf{C}^{op}}(A,B), g \in \mathrm{Hom}_{\mathsf{C}^{op}}(B,C),$ and $h \in \mathrm{Hom}_{\mathsf{C}^{op}}(C,D)$. Then $(fg)h = (gf)h = h(gf) = (hg)f = (gh)f = f(gh)$. Where the 1st, 2nd, 4th, and 5th equalities are due to the definition we chose for the composition of morphisms, and the 3rd equality is true because $\mathsf{C}$ is a category and thus is associative.
b) Unital: Let $f \in \mathrm{Hom}_{\mathsf{C}^{op}}(A,B)$, then:

*

*$f1_A = 1_Af = f$

*$1_Bf = f1_B = f$
Where for both statements, the first equality is due to our definition of composition and the second equality is true because $\mathsf{C}$ is a category and thus is unital.
Thank you

Solution (updated):
Remember that by definition, a category must have i) a composition morphism that satisfies associativity for any pairs of morphisms and ii) an identity morphism that is unital for all objects in the category (e.g. for $f: X \to Y, f1_X = 1_Yf = f$).
i) Composition morphism: Let's define composition of morphisms as follows: for $f \in \mathrm{Hom}_{\mathsf{C}^{op}}(A,B)$ and $g \in \mathrm{Hom}_{\mathsf{C}^{op}}(B,C)$, define $f \circ{'} g \in \mathrm{Hom}_{\mathsf{C}^{op}}(A,C)$ such that $f \circ{'} g = g \circ f \in \mathrm{Hom}_{\mathsf{C}}(C,A)$. We know $g \circ f$ exists because $\mathsf{C}$ is a category and thus satisfies the condition of having a composition morphism for all pairs of morphisms.
To show that the composition morphism is associative, let $f \in \mathrm{Hom}_{\mathsf{C}^{op}}(A,B), g \in \mathrm{Hom}_{\mathsf{C}^{op}}(B,C),$ and $h \in \mathrm{Hom}_{\mathsf{C}^{op}}(C,D)$. Then $(f \circ{'} g) \circ{'} h = (g \circ f) \circ{'} h = h \circ (g \circ f) = (h \circ g) \circ f = (g \circ{'} h) \circ f = f \circ{'} (g \circ{'} h)$. Where the 1st, 2nd, 4th, and 5th equalities are due to the definition we chose for the composition of morphisms, and the 3rd equality is true because $\mathsf{C}$ is a category and thus its morphisms are associative.
ii) Identity morphism: If $A$ is an object in $\mathsf{C}^{op}$, it also exists in $\mathsf{C}$ (by definition of $\mathrm{Obj}(\mathsf{C}^{op})$). Since $\mathsf{C}$ is a category, it satisfies the property of having an identity morphism for each object. Let's define $1_A$ for any $A$ in $\mathsf{C}^{op}$ to be the same as $1_A$ for the same $A$ in $\mathsf{C}$.
To show that the identity morphism is unital, let $f \in \mathrm{Hom}_{\mathsf{C}^{op}}(A,B)$, then:

*

*$f \circ{'} 1_A = 1_A \circ f = f$

*$1_B \circ{'} f = f \circ 1_B = f$
Where for both statements, the first equality is due to our definition of composition and the second equality is true because $\mathsf{C}$ is a category and thus its identity morphisms are unital.
 A: Basically yes :) Two comments: The identities and composition are part of the data of a category. So in i) it does not make much sense to give a reason why the opposite has identities. Instead you can just say what they are, and you only have to check their axioms later, which you did. Second, maybe it is helpful in this case to use two different symbols, one for the composition in C and one for the composition in the opposite of C. Everything else is fine.
A: Seems generally correct, but you could be a bit more careful.
i) An 'identity morphism' is just a distinguished element of $Hom_\mathsf{C}(A,A)$. Given a choice of $1_A$ in the category $\mathsf{C}$, it makes sense to define the identity morphism of $A$ in $\mathsf{C}^{op}$ by choosing the same $1_A$, since you know $Hom_{\mathsf{C}^{op}}(A,A) = Hom_\mathsf{C}(A,A)$.
A morphism being the identity is not an intrinsic property of some particular function, it is a structural property of a morphism in a category, so if you are building a new category you need to say what the identities are.
ii)b Take a morphism $f\in Hom_{\mathsf{C}^{op}}(A,B)$ corresponding to $f'\in Hom_{\mathsf{C}}(B,A)$. The morphism $f\circ 1_A \in Hom_{\mathsf{C}^{op}}(A,B)$ is, by your definition of composition, the morphism corresponding to $1_A\circ f'\in Hom_{\mathsf{C}}(B,A)$ which is $f'\in Hom_{\mathsf{C}}(B,A)$. Thus $f\circ 1_A = f$.
You could just use the same letters for $f$ and $f'$, of course, I just wanted to emphasize that they 'go in different directions', i.e. 'live in different categories'.
Logically speaking I would prefer you write ii) and ii)a together and put ii)b and i) together: the composition is a law for combining morphisms, calling something an identity only makes sense after defining composition. You cannot call $0$ an additive identity without knowing what addition is.
