User:Michiexile/MATH198/Lecture 7
IMPORTANT NOTE: THESE NOTES ARE STILL UNDER DEVELOPMENT. PLEASE WAIT UNTIL AFTER THE LECTURE WITH HANDING ANYTHING IN, OR TREATING THE NOTES AS READY TO READ.
Last week we saw what an adjunction was. Here's one thing we can do with adjunctions.
One piece of notation we didn't cover last week was writing Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle U\turnstile F} for the statement is left adjoint to .
Now, let Failed to parse (unknown function "\turnstile"): {\displaystyle U\turnstile F} . We set . Then we have natural transformations
such that is associative and is the unit of .
These requirements remind us of the definition of a monoid - and this is not that much of a surprise. To see the exact connection, and to garner a wider spread of definitions.
Algebraic objects in categories
$THEORY objects in Categories.
Now, we call something a monad in a category if it is a monoid object in the category of endofunctors of that category.
We thus define a monad in a category to be a monoid in that category.
Thus: a monad with this definition in Haskell is:
- a type of kind
m :: * -> *
. - equipped with functions
return :: a -> m a
join :: m m a -> m a
- examples:
List:
return x = [x]
join (l:lsts) = l ++ join lsts
Maybe:
return x = Just x
join (Just (Just x)) = Just x
join _ = Nothing
Note: not quite what Haskell claims a monad to be. Other related concepts:
- Kleisli category & factorization of monads: if we start with T a
monad, then can we find an adjunction U -| F to _somewhere_ such that T = UF? And the monoidal structure is given by U e_FX and eta_X?
- From the Kleisli Category to monadic bind.
- Monads and sequencing.
Some adjunctions we already know
- initial/terminal are adjunctions.
- (co)-products are adjunctions.
- Actually, all (co)limits are adjunctions.
Some adjunctions we don't know yet
- Existential and universal qualifiers as adjunctions.
- Powersets and im(f) -| f^\inv
Properties of adjoints
RAPL: Right Adjoints Preserve Limits
Recognizing adjoints
Theorem (Freyd: The Adjoint Functor Theorem)