Monad algebra forgetful functor creates limits

ID: monad-algebra-forgetful-functor-creates-limits

Given a diagram of algebras for a monad, take any chosen limit of its underlying diagram. The displayed equations uniquely determine , because their right-hand sides form a cone. Joint monicity of the limit projections proves and . The same projection argument proves that every induced mediating map preserves the algebra action. Thus the forgetful functor strictly creates this limit with the prescribed underlying cone, without assuming the monad preserves limits.

New to topics? Read the docs here!