It looks like you're new here. If you want to get involved, click one of these buttons!

- All Categories 2.3K
- Chat 494
- ACT Study Group 5
- Azimuth Math Review 6
- MIT 2020: Programming with Categories 53
- MIT 2020: Lectures 21
- MIT 2020: Exercises 25
- MIT 2019: Applied Category Theory 339
- MIT 2019: Lectures 79
- MIT 2019: Exercises 149
- MIT 2019: Chat 50
- UCR ACT Seminar 4
- General 64
- Azimuth Code Project 110
- Drafts 1
- Math Syntax Demos 15
- Wiki - Latest Changes 1
- Strategy 110
- Azimuth Project 1.1K

Options

From the Wikipedia article on monads:

A *monad* on a category \(C\) consists of an endofunctor \(T: C \rightarrow C\) together with two natural transformations: \(\eta: 1_C \rightarrow T\) (where \(1_C\) denotes the identity functor on \(C\)) and \(\mu: T^2 \rightarrow T\) (where \(T^2\) is the functor \(T \circ T\) from \(C\) to \(C\)). These are required to fulfull the following "coherence" conditions:

\(\mu \circ T\mu = \mu \circ \mu T\) (as natural transformations \(T^3 \rightarrow T\);

\(\mu \circ T\eta = \mu \circ \eta T = 1_T\) (as natural transformations \(T \rightarrow T\); here \(1_T\) denotes the identity transformation from \(T\) to \(T\).

See this section of the wikipedia article on natural transformations for the explanation of the notations \(T \mu\) and \(\mu T\).

Tagged:

## Comments

Example: The power set monad

The

power set monadis monad on the category Set: For a set \(A\) let \(T(A)\) be the power set of \(A\) (which consists of all subsets of \(A\)) and for a function \(f: A \rightarrow B\) let \(T(f)\) be the function between the power sets induced by taking direct images under \(f\). For every set \(A\), we have a map \(\eta_T: A \rightarrow T(A)\), which assigns to every \(a \in A\) the singleton \(\lbrace a \rbrace\). The function:\[\mu_A: T(T(A)) \rightarrow T(A)\]

takes a set of sets to its union. These data describe a monad.

`Example: The power set monad The _power set monad_ is monad on the category Set: For a set \\(A\\) let \\(T(A)\\) be the power set of \\(A\\) (which consists of all subsets of \\(A\\)) and for a function \\(f: A \rightarrow B\\) let \\(T(f)\\) be the function between the power sets induced by taking direct images under \\(f\\). For every set \\(A\\), we have a map \\(\eta_T: A \rightarrow T(A)\\), which assigns to every \\(a \in A\\) the singleton \\(\lbrace a \rbrace\\). The function: \\[\mu_A: T(T(A)) \rightarrow T(A)\\] takes a set of sets to its union. These data describe a monad.`

Exercise: Prove this claim.

`Exercise: Prove this claim.`

We can break the proof up into components.

Proposition 1. T is a functor.

Proposition 2. \(\mu: T^2 \rightarrow T\) is a natural transformation.

Proposition 3. \(\eta: 1_T \rightarrow T\) is a natural transformation.

Proposition 4. \(\mu \circ T\mu = \mu \circ \mu T\) (as natural transformations \(T^3 \rightarrow T\))

Proposition 5. \(\mu \circ T\eta = \mu \circ \eta T = 1_T\) (as natural transformations \(T \rightarrow T\); here \(1_T\) denotes the identity transformation from \(T\) to \(T\))

`We can break the proof up into components. Proposition 1. T is a functor. Proposition 2. \\(\mu: T^2 \rightarrow T\\) is a natural transformation. Proposition 3. \\(\eta: 1_T \rightarrow T\\) is a natural transformation. Proposition 4. \\(\mu \circ T\mu = \mu \circ \mu T\\) (as natural transformations \\(T^3 \rightarrow T\\)) Proposition 5. \\(\mu \circ T\eta = \mu \circ \eta T = 1_T\\) (as natural transformations \\(T \rightarrow T\\); here \\(1_T\\) denotes the identity transformation from \\(T\\) to \\(T\\))`

But before digging into the proofs, I'll take some space to unpack the definitions a bit. First I'll give a more elaborated explanation of the power set monad.

A monad T is a special kind of endofunctor \(T: C \rightarrow C\) on a category \(C)\).

In the case of the power set monad, \(C\) is the category \(Set\). The functor \(T: Set \rightarrow Set\) is that which sends every set \(A\) to its powerset \(2^A\), defined as the set of all subsets of \(A\).

Now to complete the definition of this functor, we need to specify how it acts on morphisms \(f: A \rightarrow B\). Well, in our category \(Set\), such a morphism \(f\) is a function from set \(A\) to set \(B\). We need to define the result of applying functor \(T\) to morphism \(f\). Now, by the definition of a functor, \(T(f)\) is required to be another function, of type \(T(f): T(A) \rightarrow T(B)\). Which is to say, \(T(f): 2^A \rightarrow 2^B\).

Now, given that we have a function \(f\) mapping set \(A\) into set \(B\), what could this function \(T(f)\) be, which must map \(2^A\) into \(2^B\)?

Well a mapping from \(2^A\) into \(2^B\) is just another way of saying a function that maps subsets of \(A\) to subsets of \(B\).

Given that \(f\) maps elements of \(A\) to elements of \(B\), there is a clear candidate for \(T(f)\) mapping subsets of \(A\) to subsets of \(B\). Given a subset of \(A\), the action of \(T(f)\) will be to apply \(f\) to every element of \(A\) and collect the results to form a subset of \(B\).

We say that \(T(f)\) is the

liftingof \(f: A \rightarrow B\) to a function from \(2^A\) to \(2^B\):\[T(f)(A) = \lbrace f(x) | x \in A \rbrace\]

This is referred to as the

direct imageof \(A\) under \(f\).`But before digging into the proofs, I'll take some space to unpack the definitions a bit. First I'll give a more elaborated explanation of the power set monad. A monad T is a special kind of endofunctor \\(T: C \rightarrow C\\) on a category \\(C)\\). In the case of the power set monad, \\(C\\) is the category \\(Set\\). The functor \\(T: Set \rightarrow Set\\) is that which sends every set \\(A\\) to its powerset \\(2^A\\), defined as the set of all subsets of \\(A\\). Now to complete the definition of this functor, we need to specify how it acts on morphisms \\(f: A \rightarrow B\\). Well, in our category \\(Set\\), such a morphism \\(f\\) is a function from set \\(A\\) to set \\(B\\). We need to define the result of applying functor \\(T\\) to morphism \\(f\\). Now, by the definition of a functor, \\(T(f)\\) is required to be another function, of type \\(T(f): T(A) \rightarrow T(B)\\). Which is to say, \\(T(f): 2^A \rightarrow 2^B\\). Now, given that we have a function \\(f\\) mapping set \\(A\\) into set \\(B\\), what could this function \\(T(f)\\) be, which must map \\(2^A\\) into \\(2^B\\)? Well a mapping from \\(2^A\\) into \\(2^B\\) is just another way of saying a function that maps subsets of \\(A\\) to subsets of \\(B\\). Given that \\(f\\) maps elements of \\(A\\) to elements of \\(B\\), there is a clear candidate for \\(T(f)\\) mapping subsets of \\(A\\) to subsets of \\(B\\). Given a subset of \\(A\\), the action of \\(T(f)\\) will be to apply \\(f\\) to every element of \\(A\\) and collect the results to form a subset of \\(B\\). We say that \\(T(f)\\) is the _lifting_ of \\(f: A \rightarrow B\\) to a function from \\(2^A\\) to \\(2^B\\): \\[T(f)(A) = \lbrace f(x) | x \in A \rbrace\\] This is referred to as the _direct image_ of \\(A\\) under \\(f\\).`

Now Proposition 1 asks us to show that this \(T\) is actually a

bona fidefunctor. It's not enough to define any old mapping from the objects and morphisms of one category to the objects and morphisms of another category. In order to qualify as a functor, such a mapping from one category to another must bestructure preserving. Specifically, it needs to preserve two structures: composition, and identities.Preserving composition means that given \(f: A \rightarrow B\) and \(g: B \rightarrow C\), with composition\(f \triangleright g: A \rightarrow C\), it must be the case that:

\[T(f \triangleright g) = T(f) \triangleright T(g)\]

In words, this says that if we lift the composition of two functions, we get the same result as when we lift the functions separately and then compose.

Preserving identities means that given \(Id_A: A \rightarrow A\), it must be the case that:

\[T(Id_A) = Id_{T_A}\]

This says that if we lift the identity function on a set \(A\), then we get the identity function on the power set \(2^A\).

Both of these statements are true. And so we have proven that \(T\) is a functor.

`Now Proposition 1 asks us to show that this \\(T\\) is actually a _bona fide_ functor. It's not enough to define any old mapping from the objects and morphisms of one category to the objects and morphisms of another category. In order to qualify as a functor, such a mapping from one category to another must be _structure preserving_. Specifically, it needs to preserve two structures: composition, and identities. Preserving composition means that given \\(f: A \rightarrow B\\) and \\(g: B \rightarrow C\\), with composition\\(f \triangleright g: A \rightarrow C\\), it must be the case that: \\[T(f \triangleright g) = T(f) \triangleright T(g)\\] In words, this says that if we lift the composition of two functions, we get the same result as when we lift the functions separately and then compose. Preserving identities means that given \\(Id_A: A \rightarrow A\\), it must be the case that: \\[T(Id_A) = Id_{T_A}\\] This says that if we lift the identity function on a set \\(A\\), then we get the identity function on the power set \\(2^A\\). Both of these statements are true. And so we have proven that \\(T\\) is a functor.`

Next, in Proposition 2, we are asked to prove that \(\mu: T^2 \rightarrow T\) is a natural transformation. Let's unpack this now!

Now, before proving that it is a natural transformation, let's review what this \(\mu\) is. From the definition above, we see that it is a family of functions, with one member of the family \(\mu_A\) for every set \(A\).

The type of \(\mu_A\) is given by:

\[\mu_A: T(T(A)) \rightarrow T(A)\]

Now we can rewrite this as:

\[\mu_A: 2^{2^A} \rightarrow 2^A\]

What's \(2^{2^A}\)? That's the powerset of the powerset, which consists of sets of subsets of \(A\).

\(\mu_A\) must therefore map a set of subsets of \(A\) to a single subset of \(A\).

As stated above, \(\mu_A\) maps a set of subsets to their union:

\[\mu_A(S \subseteq 2^A) = \bigcup S\]

`Next, in Proposition 2, we are asked to prove that \\(\mu: T^2 \rightarrow T\\) is a natural transformation. Let's unpack this now! Now, before proving that it is a natural transformation, let's review what this \\(\mu\\) is. From the definition above, we see that it is a family of functions, with one member of the family \\(\mu_A\\) for every set \\(A\\). The type of \\(\mu_A\\) is given by: \\[\mu_A: T(T(A)) \rightarrow T(A)\\] Now we can rewrite this as: \\[\mu_A: 2^{2^A} \rightarrow 2^A\\] What's \\(2^{2^A}\\)? That's the powerset of the powerset, which consists of sets of subsets of \\(A\\). \\(\mu_A\\) must therefore map a set of subsets of \\(A\\) to a single subset of \\(A\\). As stated above, \\(\mu_A\\) maps a set of subsets to their union: \\[\mu_A(S \subseteq 2^A) = \bigcup S\\]`

Now let's look into the claim that this family of functions \(\mu_A\) constitutes a 'natural transformation' from \(T^2\) to \(T\).

`Now let's look into the claim that this family of functions \\(\mu_A\\) constitutes a 'natural transformation' from \\(T^2\\) to \\(T\\).`

Natural transformations are mappings between functors. Here, the source functor is \(T^2\) -- which is the functor obtained by applying \(T\) twice in succession -- and the target functor is \(T\).

Suppose \(F\) and \(G\) are functors from category \(C\) to category \(D\). Then a natural transformation \(\mu\) from \(C\) to \(D\) assigns to each object \(c\) in \(C\) some arrow \(\mu_c\) taking \(F(c)\) to \(G(c)\).

In the case of the working example, \(C\) and \(D\) are the category \(Set\); \(F\) is the functor \(T^2\) and \(G\) is the functor \(T\). So any natural transformation between \(T^2\) and \(T\) must give, for each set \(A\), an arrow \(\mu_A\) taking \(T^2(A) = 2^{2^A}\) to \(T(A) = 2^A\).

That is exactly the form that we observed for \(\mu_A\), above, in comment 6. So we're on the right track for showing that \(\mu_A\) is a natural transformation from \(T^2\) to \(T\).

`Natural transformations are mappings between functors. Here, the source functor is \\(T^2\\) -- which is the functor obtained by applying \\(T\\) twice in succession -- and the target functor is \\(T\\). Suppose \\(F\\) and \\(G\\) are functors from category \\(C\\) to category \\(D\\). Then a natural transformation \\(\mu\\) from \\(C\\) to \\(D\\) assigns to each object \\(c\\) in \\(C\\) some arrow \\(\mu_c\\) taking \\(F(c)\\) to \\(G(c)\\). In the case of the working example, \\(C\\) and \\(D\\) are the category \\(Set\\); \\(F\\) is the functor \\(T^2\\) and \\(G\\) is the functor \\(T\\). So any natural transformation between \\(T^2\\) and \\(T\\) must give, for each set \\(A\\), an arrow \\(\mu_A\\) taking \\(T^2(A) = 2^{2^A}\\) to \\(T(A) = 2^A\\). That is exactly the form that we observed for \\(\mu_A\\), above, in comment 6. So we're on the right track for showing that \\(\mu_A\\) is a natural transformation from \\(T^2\\) to \\(T\\).`

\(\require{begingroup}\begingroup\require{AMScd}\newcommand{\tlap}[1]{\raisebox{0pt}[0pt][0pt]{#1}}\newcommand{\blap}[1]{\vbox to 0pt{\hbox{#1}\vss}}\) But a natural transformation is not just any old family of arrows of the prescribed type \(\mu_A: F(A) \rightarrow G(A)\). There is a 'naturality' constraint, which is motivated by the following considerations.

Suppose we have an arrow \(\alpha: c_1 \rightarrow c_2\) in \(C\). Now consider the application of the functors \(F\) and \(G\) to \(\alpha\). From the arrow \(\alpha\) in \(C\), we can obtain the pair of arrows \(F(\alpha), G(\alpha)\) in \(D\). Each functor gives a different image in \(D\) of the arrow \(\alpha\) in \(C\).

A natural transformation \(\mu_c\) from \(F\) to \(G\) gives a systematic way to 'transition' from the arrow \(F(\alpha): F(c_1) \rightarrow F(c_2)\) to the arrow \(G(\alpha): G(c_1) \rightarrow G(c_2)\). The constraint on the family of morphisms \(\mu_c\) is that for all \(\alpha: c_1 \rightarrow c_2\), the following diagram must commute:

\begin{CD} F(c_1) @>F(\alpha)>> F(c_2) \\@V{\mu_{c_1}}VV {}@VV{\mu_{c_2}}V \\ G(c_1) @>>G(\alpha)> G(c_2) \end{CD}

There are two ways to get from \(F(c_1)\) to \(G(c_2\) We can either first go through \(F(\alpha)\) and then through the natural transformation, or first go through the natural transformation and then through \(G(\alpha)\). These are required to be the same, by the naturality constraint on the arrows \(\mu_c\).

Written as a formula, the naturality constraint states that:

\[F(\alpha) \triangleright \mu_{c_2} = \mu_{c_1} \triangleright G(\alpha)\]

`\\(\require{begingroup}\begingroup\require{AMScd}\newcommand{\tlap}[1]{\raisebox{0pt}[0pt][0pt]{#1}}\newcommand{\blap}[1]{\vbox to 0pt{\hbox{#1}\vss}}\\) But a natural transformation is not just any old family of arrows of the prescribed type \\(\mu_A: F(A) \rightarrow G(A)\\). There is a 'naturality' constraint, which is motivated by the following considerations. Suppose we have an arrow \\(\alpha: c_1 \rightarrow c_2\\) in \\(C\\). Now consider the application of the functors \\(F\\) and \\(G\\) to \\(\alpha\\). From the arrow \\(\alpha\\) in \\(C\\), we can obtain the pair of arrows \\(F(\alpha), G(\alpha)\\) in \\(D\\). Each functor gives a different image in \\(D\\) of the arrow \\(\alpha\\) in \\(C\\). A natural transformation \\(\mu_c\\) from \\(F\\) to \\(G\\) gives a systematic way to 'transition' from the arrow \\(F(\alpha): F(c_1) \rightarrow F(c_2)\\) to the arrow \\(G(\alpha): G(c_1) \rightarrow G(c_2)\\). The constraint on the family of morphisms \\(\mu_c\\) is that for all \\(\alpha: c_1 \rightarrow c_2\\), the following diagram must commute: \begin{CD} F(c_1) @>F(\alpha)>> F(c_2) \\\@V{\mu_{c_1}}VV {}@VV{\mu_{c_2}}V \\\ G(c_1) @>>G(\alpha)> G(c_2) \end{CD} There are two ways to get from \\(F(c_1)\\) to \\(G(c_2\\) We can either first go through \\(F(\alpha)\\) and then through the natural transformation, or first go through the natural transformation and then through \\(G(\alpha)\\). These are required to be the same, by the naturality constraint on the arrows \\(\mu_c\\). Written as a formula, the naturality constraint states that: \\[F(\alpha) \triangleright \mu_{c_2} = \mu_{c_1} \triangleright G(\alpha)\\]`

\(\require{begingroup}\begingroup\require{AMScd}\newcommand{\tlap}[1]{\raisebox{0pt}[0pt][0pt]{#1}}\newcommand{\blap}[1]{\vbox to 0pt{\hbox{#1}\vss}}\) Let's instantiate back to our example, where \(F\) is \(T^2\), and \(G\) is \(T\).

Suppose \(A\) and \(B\) are sets in \(Set\), and that \(\alpha: A \rightarrow B\). Then the naturality diagram instantiates down to the following:

\begin{CD} T^2(A) @>T^2(\alpha)>> T^2(B) \\@V{\mu_{A}}VV {}@VV{\mu_{B}}V \\ T(A) @>>T(\alpha)> T(B) \end{CD}

Written as a formula, the constraint is:

\[T^2(\alpha) \triangleright \mu_B = \mu_A \triangleright T(\alpha)\]

Both of these compositions give a function going from the top-left to the bottom-right of the diagram, i.e., from \(T^2(A)\) to \(T(B)\), i.e., from \(2^{2^A}\) to \(2^B\).

So let's choose an \(x\) in \(2^{2^A}\). That means \(x\) is a set of subsets of \(A\).

The first composition applies \(T^2(\alpha)\) to \(x\) and then sends that through \(\mu_B\).

That means mapping \(\alpha\) to all the elements of \(A\) in \(x\), which yields a set of subsets of \(B\), and then taking the union of these subsets, to obtain a single subset of \(B\).

The second composition takes the union of all the elements in \(x\) to obtain a single subset of \(A\), and then maps \(\alpha\) over all the elements in this subset, to obtain a single subset of \(B\).

These two processes both convert \(x\) to the same subset of \(B\).

So the diagram commutes.

That means that the naturality condition is satisfied.

So we have shown that the family of functions \(\mu_A\) is a natural transformation from \(T^2\) to \(T\).

That completes the proof of Proposition 2.

`\\(\require{begingroup}\begingroup\require{AMScd}\newcommand{\tlap}[1]{\raisebox{0pt}[0pt][0pt]{#1}}\newcommand{\blap}[1]{\vbox to 0pt{\hbox{#1}\vss}}\\) Let's instantiate back to our example, where \\(F\\) is \\(T^2\\), and \\(G\\) is \\(T\\). Suppose \\(A\\) and \\(B\\) are sets in \\(Set\\), and that \\(\alpha: A \rightarrow B\\). Then the naturality diagram instantiates down to the following: \begin{CD} T^2(A) @>T^2(\alpha)>> T^2(B) \\\@V{\mu_{A}}VV {}@VV{\mu_{B}}V \\\ T(A) @>>T(\alpha)> T(B) \end{CD} Written as a formula, the constraint is: \\[T^2(\alpha) \triangleright \mu_B = \mu_A \triangleright T(\alpha)\\] Both of these compositions give a function going from the top-left to the bottom-right of the diagram, i.e., from \\(T^2(A)\\) to \\(T(B)\\), i.e., from \\(2^{2^A}\\) to \\(2^B\\). So let's choose an \\(x\\) in \\(2^{2^A}\\). That means \\(x\\) is a set of subsets of \\(A\\). The first composition applies \\(T^2(\alpha)\\) to \\(x\\) and then sends that through \\(\mu_B\\). That means mapping \\(\alpha\\) to all the elements of \\(A\\) in \\(x\\), which yields a set of subsets of \\(B\\), and then taking the union of these subsets, to obtain a single subset of \\(B\\). The second composition takes the union of all the elements in \\(x\\) to obtain a single subset of \\(A\\), and then maps \\(\alpha\\) over all the elements in this subset, to obtain a single subset of \\(B\\). These two processes both convert \\(x\\) to the same subset of \\(B\\). So the diagram commutes. That means that the naturality condition is satisfied. So we have shown that the family of functions \\(\mu_A\\) is a natural transformation from \\(T^2\\) to \\(T\\). That completes the proof of Proposition 2.`

Notice that when we finally got to the crux of the proof -- which was to show that the two compositions are equal -- the naturality condition turned out to be a very evident fact. Namely, that we get the same result when we take unions and then map a function, as when we map the function and then take unions. If we made a sketch of this on the whiteboard for any reasonable programmer, they would say, of course, that's obvious!

This is reminiscent of Michael Spivak's comment, which I quoted in Talk 2:

We have to do a lot of detailed accounting, to keep track of what the definitions are saying and how they are to be applied to the situation at hand. But if we can stay organized and on-point, then the actual core of the proof may turn out to be not so hard actually. Fingers crossed...

`Notice that when we finally got to the crux of the proof -- which was to show that the two compositions are equal -- the naturality condition turned out to be a very evident fact. Namely, that we get the same result when we take unions and then map a function, as when we map the function and then take unions. If we made a sketch of this on the whiteboard for any reasonable programmer, they would say, of course, that's obvious! This is reminiscent of Michael Spivak's comment, which I quoted in [Talk 2](https://forum.azimuthproject.org/discussion/2438/talk-2-complex-definitions-simple-proof): > Yet the proof of this theorem is, in the mathematician's sense, an utter triviality -- a straightforward computation. On the other hand, even the statement of this triviality cannot be understood without a hoarde of difficult definitions We have to do a lot of detailed accounting, to keep track of what the definitions are saying and how they are to be applied to the situation at hand. But if we can stay organized and on-point, then the actual core of the proof may turn out to be not so hard actually. Fingers crossed...`