Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Sharpened up some of the discussion at finitary monad (emphasizing equivalence with Lawvere theories), and added some technical applications to reflexive coequalizer. Both were used to support a detailed proof embedded at smooth algebra.
Wow, thanks.
I believe we managed to fix my argument via the adjoint functor theorem by – instead of trying to show cototality– solving the solution set condition. But what you have here is of course uncomparably more powerful. In particular in that you explicitly give the left adjoint. I need to think about what it actually does for the case of smooth algebras…
Yes, I always prefer to give explicit constructions when I can, since that is usually an advantage when doing actual calculations.
As I try to indicate in the proof, “smoothification” of an R-algebra can be thought of as exactly analogous to complexification of an R-vector space: it’s just the canonical way of beefing up the action to one of a larger theory. I think probably the general construction is in Lawvere’s thesis somewhere.
Edit: the tensor product construction can be thought of as “the” natural way of augmenting the two-sided bar construction.
1 to 3 of 3