Session 3: Composing maps and counting maps
Category having been defined at the end of Article I, we now generally implement maps in the book as Lean morphisms.
A, B, and C are three different sets (or even three different objects in any category); f, g, h, and k are maps with domains and codomains as follows:
A \xrightarrow{f} B, \quad B \xrightarrow{g} A, \quad A \xrightarrow{h} C, \quad C \xrightarrow{k} B.
Two of the expressions below make sense. Find each of the two, and say what its domain and codomain are:
\text{(a)}\; k \circ h \circ g \circ f, \quad\text{(b)}\; k \circ f \circ g, \quad\text{(c)}\; g \circ f \circ g \circ k \circ h.
Solution: Exercise 1
variable {𝒞 : Type u} [Category.{v, u} 𝒞] {A B C : 𝒞}
(f : A ⟶ B) (g : B ⟶ A) (h : A ⟶ C) (k : C ⟶ B)
(a) makes sense, with domain A and codomain B.
#check k ⊚ h ⊚ g ⊚ f
(b) does not make sense, since the codomain of {f \circ g} is B, but the domain of k is C.
#check f ⊚ g
(c) makes sense, with domain A and codomain A.
#check g ⊚ f ⊚ g ⊚ k ⊚ h