symmetric monoidal (∞,1)-category of spectra
is a natural isomorphism.
All components of are monomorphisms.
The maps are equal.
Compositions and are always the identity (unit axioms for the monad), and in particular agree; if has all components monic, this implies .
Compatibility of action and unit is , hence also . If then this implies , where the naturality of is used in the second equality. Therefore we exhibited both as a left and a right inverse of .
If every action is iso, then the components of multiplication are isos as a special case, namely of the free action on .
For any monad , the forgetful functor from Eilenberg-Moore category to is faithful: a morphism of -algebras is always a morphism of underlying objects in . To show that it is also full, we consider any pair , in and must show that any is actually a map ; i.e. . But we know that are inverses of respectively and the naturality for says . Compose that equation with on the right and on the left with the result (notice that we used just the invertibility of ).
Trivial, because the Eilenberg-Moore construction induces the original monad by the standard recipe.
By the counit is iso, hence has a unique 2-sided inverse; by triangle identities, and are both right inverses of , hence 2-sided inverses, hence they are equal.
If is an adjunction with fully faithful, then the counit is iso. since where the last equivalence is since is full and faithful; hence by essential unicity of the representing object there is an iso .; let then the adjoint of this identity is the counit of the adjunction; since the hom objects correspond bijectively, the counit is an isomorphism. Hence the multiplication of the induced monad is also an iso.
Part 5 means that in such a case is, up to equivalence a full reflective subcategory of . Conversely, the monad induced by any reflective subcategory is idempotent, so giving an idempotent monad on is equivalent to giving a reflective subcategory of .
In the language of stuff, structure, property, an idempotent monad may be said to equip its algebras with properties only (since is fully faithful), unlike an arbitrary monad, which equips its algebras with at most structure (since is, in general, faithful but not full).
If is idempotent, then it follows in particular that an object of admits at most one structure of -algebra, that this happens precisely when the unit is an isomorphism, and in this case the -algebra structure map is . However, it is possible to have a non-idempotent monad for which any object of admits at most one structure of -algebra, in which case can be said to equip objects of with property-like structure; an easy example is the monad on semigroups whose algebras are monoids.
Let us be in a -category . Part of the structure of an idempotent monad in is of course an idempotent morphism . More precisely (Definition 1.1.9) considers as part of the structure such that an idempotent 1-cell has a 2-isomorphism such that . Equivalently an idempotent morphism is a normalized pseudofunctor from the two object monoid with to .
Recall that a splitting of an idempotent consists of a pair of 1-cells and and a pair of 2-isomorphisms and such that where denotes horizontal composition of 2-cells. Equivalently an splitting of an idempotent is a limit or a colimit of the defining pseudofunctor. If has equalizers or coequalizers, then all its idempotents split.
Now if is a splitting of an idempotemt monad, then are adjoint. And in this case the splitting of an idempotent is equivalently an Eilenberg-Moore object for the monad . In this case is called an adjoint retract of .
Equivalences (resp. cores) in an allegory are precisely those symmetric idempotents which are idempotent monads (resp. comonads). In an allegory the following statements are equivalent: all symmetric idempotents split, idempotent monads split, idempotent comonads split. A similar statement holds at least for some 2-categories.
Let be an idempotent monad on a category . The following conditions on an object of are equivalent:
The object carries an -algebra structure.
(It follows from 3. that there is at most one algebra structure on , given by .)
The implication 1. 2. is immediate. Next, if is any retraction of , we have both and
so 2. implies 3. Finally, if is an isomorphism, put . Then (unit condition), and the associativity condition for ,
follows by inverting the naturality equation . Thus 3. implies 1.
This means that the Eilenberg-Moore category of an idempotent monad is equivalently the reflective subcategory (a “localization” of the ambient category) whose embedding-reflection adjunction gives the idempotent monad.
See also (Borceux, volume 2, corollary 4.2.4).
In modal type theory one thinks of a (idempotent) (co-)monad as a (co-)modal operator and of its algebras as (co-)modal types. In this terminology the above says that categories of (co-)modal types are precisely the (co-)reflective localizations of the ambient type system.
Given a monad , define a functor as the equalizer of and :
This acquires a monad structure. It might not be an idempotent monad (although it will be if is left exact). However we can apply the process again, and continue transfinitely. Define , and if has been defined, put ; at limit ordinals , define to be the inverse limit of the chain
where ranges over ordinals less than . This defines the monad inductively; below, we let denote the unit of this monad.
Since is well-powered (i.e., since each object has only a small number of subobjects), the large limit
exists for each . Hence the large limit exists as an endofunctor. The underlying functor
reflects limits (irrespective of size), so acquires a monad structure defined by the limit. Let be the unit and the multiplication of . For each , there is a monad map defined by the limit projection.
For this it suffices to check that . This may be checked objectwise. So fix an object , and for that particular , choose so large that and are isomorphisms. In particular, is invertible.
Now , since factors through the equalizer . Because is a monad morphism, we have
Finally we must check that satisfies the appropriate universal property. Suppose is an idempotent monad with unit , and let be a monad map. We define by induction: given , we have
so that factors uniquely through the inclusion . This defines ; this is a monad map. The definition of at limit ordinals, where is a limit monad, is clear. Hence factors (uniquely) through the inclusion , as was to be shown.
Let be a commutative ring, and let be a flat (commutative) -algebra. Then the forgetful functor
from -modules to -modules has a left exact left adjoint . The induced monad on the category of -modules preserves equalizers, and so its associated idempotent monad may be formed by taking the equalizer
(To be continued. This example is based on how Joyal and Tierney introduce effective descent for commutative ring homomorphisms, in An Extension of the Galois Theory of Grothendieck. I would like to consult that before going further – Todd.)
Mike Shulman: How about some examples of monads and their associated idempotent monads?
Do 2-monads have associated lax-, colax-, or pseudo-idempotent 2-monads?