Skip to main content
MathOverflow

Return to Answer

added 16 characters in body
Source Link
Simon Henry
Simon Henry
  • 42.4k
  • 5
  • 107
  • 205

Proposition: It is inconsistent with ZF (even with IZF) that every endofunctor of the category of sets admit a free monads.

Proposition: It is inconsistent with ZF that every endofunctor of the category of sets admit a free monads.

Proposition: It is inconsistent with ZF (even with IZF) that every endofunctor of the category of sets admit a free monads.

added 9 characters in body
Source Link
Simon Henry
Simon Henry
  • 42.4k
  • 5
  • 107
  • 205

proof: Consider the power-set endofunctor $X \mapsto \mathcal{P}(X)$, if the free monad on $\mathcal{P}$ existed, then as endomorphism monad exists in Set, the category of algebras for this monad would be the algebras for the endofunctor $\mathcal{P}$. In partiular the category of $\mathcal{P}-algebra$ would have an initial object, but by a well known theorem of Lambek, an initial algebra for an endofunctor $\mathcal{P}$ is always have the propertysuch that $\mathcal{P}(X) \simeq X$, but this is impossible by the diagonal argument. $\square$

proof: Consider the power-set endofunctor $X \mapsto \mathcal{P}(X)$, if the free monad on $\mathcal{P}$ existed, then as endomorphism monad exists in Set, the category of algebras for this monad would be the algebras for the endofunctor $\mathcal{P}$. In partiular the category of $\mathcal{P}-algebra$ would have an initial object, but by a well known theorem of Lambek, an initial algebra for an endofunctor always have the property $\mathcal{P}(X) \simeq X$, but this is impossible by the diagonal argument. $\square$

proof: Consider the power-set endofunctor $X \mapsto \mathcal{P}(X)$, if the free monad on $\mathcal{P}$ existed, then as endomorphism monad exists in Set, the category of algebras for this monad would be the algebras for the endofunctor $\mathcal{P}$. In partiular the category of $\mathcal{P}-algebra$ would have an initial object, but by a well known theorem of Lambek, an initial algebra for an endofunctor $\mathcal{P}$ is always such that $\mathcal{P}(X) \simeq X$, but this is impossible by the diagonal argument. $\square$

Source Link
Simon Henry
Simon Henry
  • 42.4k
  • 5
  • 107
  • 205

These question of existence of free monad are not "derailling" the discusion. They are the whole point of the discusion. Let me clarify :

If I'm not mistaken, we have the following:

Theorem: Let $V$ be a monoidal category. Let $A$ be the category of monoids in $V$, then the forgetfull functor $U: A \to V$ is monadic if and only if it admits a left adjoint.

Sketch of the Proof: Just check the other two conditions of Beck criterion. The forgetfull functor is conservative. So we need to check that it create U-split coequalizer. Given a U-split coequalizer diagram $ X \rightrightarrows Y$ in $A$, and let $Z$ be its colimit in $V$ ( which exists by assumption). Then $Z$ comes with a monoid structure because the colimit defining it is split, so preserved by any functor, in particular the tensor product, so that $Z \otimes Z $ is the coequalizer of $X \otimes X$ and $ Y \otimes Y$ which you can use to construct an operaion $ Z \otimes Z \to Z$ making the relevant maps morphism of monoids.

With a little bit of additional work, you can conclude that this makes $Z$ a colimit in the category of monoids. $\square$

It follows that :

Corollary: Given $C$ any category, and $S \subset End(C)$ a full subcategory of endofunctors such that, $S$ contains the identity, is closed under composition, and every element of $S$ generates a free monads which is also in $S$, then the category of monads that are in $S$ is monadic over $S$.

Proof: Apply the previous result to the monoidal category $S$ (for the composition of endofunctors). $\square$

So the all point of the question is to find nice class of endofunctor for which free monads construction are available. For example :

Proposition : If $C$ is a locally presentable then the category of accessible monads on $C$ is monadic over the category of accessible endofunctor on $C$.

Though I have to insist that I do not know any exemple of category for which free monad construction on $C$ exists unconditionally. In fact, I'm relatively convinced this is impossible. To give an example :

Proposition: It is inconsistent with ZF that every endofunctor of the category of sets admit a free monads.

proof: Consider the power-set endofunctor $X \mapsto \mathcal{P}(X)$, if the free monad on $\mathcal{P}$ existed, then as endomorphism monad exists in Set, the category of algebras for this monad would be the algebras for the endofunctor $\mathcal{P}$. In partiular the category of $\mathcal{P}-algebra$ would have an initial object, but by a well known theorem of Lambek, an initial algebra for an endofunctor always have the property $\mathcal{P}(X) \simeq X$, but this is impossible by the diagonal argument. $\square$

So, unless the type theory you are using is inconsistent with ZFC, or you are using a notion of "endofunctor of sets" that does not corresponds to the usual notion, you won't be able to show that any endofunctor of the category of sets admit a free monad.

I don't quite understand what you are trying to explain with universes, but I think the problem you'll run into is that if you start form an endomorphism of the category of U-sets, then you might be able to construct something that look like a free monad on the category of V-sets for V a larger universe, but that's no longer a monad on U-set, so the forgetfull functor don't take you back to an endofunctor on U-set, but on V-set, but if you start with an endofunctor on $V$-set, then you need to go to an even larger universe W to get your free monad, but for endofunctors on W you'll need to get to a larger one and so one... And if your theory is consistent with ZFC, you can never find this way a setting where both the free monad and the forgetfull functor are simultenously defined, so that you can have a well defined "free monad monad" that acts on a category.

What will work (and maybe this is essentially what you are doing) is that if $\kappa$ is an innaccesible cardinal ( any regular cardinal actually), then any endofunctor of the category of $\kappa$-small sets can be extended into a $\kappa$-accessible endofunctor of the category of all sets, and then amongst $\kappa$-accessible endofunctors free monad constructions are available, and you can get a monadicity result by working with $\kappa$-accessible endofunctor.