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.
This is more for the sake of amusement than anything else: perhaps the softest imaginable proof of the chain rule for formal power series.
Working over a commutative ring , the statement is that if are power series, with the constant coefficient of , then under the usual definitions.
Let be the representing object for derivations. Let be the unique topological -algebra map (under the -adic topologies) that sends to . (If it helps, think .) For , define via the equation .
Let be the unique topological algebra map taking to and to . Let denote the unique topological algebra map that takes to . Then the diagram
commutes in the category of topological algebras, since the two legs agree when evaluated at the generator . But then, evaluating each leg at a power series , we have
and
whence the coefficients of agree: .
Well, I’ll admit it’s a little silly, almost parodic in the manner of Mathematics Made Difficult. A halfway normal proof might start the same way but then observe that in the ring with square-nilpotent we have
say by the binomial theorem, or by an inductive argument. This gives the chain rule at least for . Then extend to all power series by linearity, continuity, etc. Of course that’s just one approach; there are others (such as ’meta’ approaches that observe that the usual analysis proof implies the result in formal algebra).
Any of those could be easier to follow than what I produced above. So what’s the point? Nothing, really, except that it amused me that one could prove the statement with virtually zero calculation (like the binomial theorem) anywhere – just by sticking to pure concepts and using the universal property of .
Nice, and good fun! I think that your argument is perfectly easy to follow, indeed a very nice to proceed! However, regarding avoiding use of calculation, I’m not sure this is really the case, for in the following line…
For , define via the equation .
…I think one would need the binomial theorem or similar to identify with one of the usual definitions. But perhaps I’m missing something?
Thanks! I just meant that with that definition of , we prove the chain rule with a minimum of calculation. Other properties might require more calculation.
Of course, the definition is just the algebraic analogue of something familiar from SDG: if is a function on the line and denotes the walking tangent vector, then under the Kock-Lawvere axiom which asserts an isomorphism we may form a composite
which is just . (It’s a little easy here to get turned around with algebro-geometric duality, but I believe it works as advertised.) Even with all these hints, though, plus the fact that the chain rule is trying to express the functoriality of the tangent bundle vector , it still took me some time to massage it into the form above.
Ah, I didn’t realise that this definition of was one of the novel aspects, even if inspired by SDG. Then the observation is nicer still!
Sorry, I might not have made myself clear. I don’t think “my” definition of is novel. The part that took massaging was the proof of the chain rule I came up with; specifically, the end run (American slang) around the diagram where I sneak in this map I called . That technique might not be novel either, but I can at least say it’s not something I’d seen before.
I’ve now added this demonstration to chain rule.
Ah, I see. Would it be possible to provide some reference for this definition of ? I suppose in a way it is tied up with the identification of the representing object for derivations, but it would be good to make that more explicit.
Giving a reference is a slight embarrassment of riches problem. (If Urs is reading this, he might know a canonical reference right away.) Let me show the definition gives the correct answer in the mother of all contexts which is that of real-valued functions, rather than power series with coefficients in a commutative ring . In other words, replace with and with the ring of functions on . (Doing it with polynomials would probably be equally convincing.)
So again we have the ring of dual numbers . Given a point , Hadamard’s lemma allows us to expand any function in the form for some unique number and function , and is according to standard definition this value . In other words, there is by this lemma a canonical isomorphism
which maps the residue class of to . In fact any homomorphism , written in the form , is given by (1) a homomorphism , with any such on being evaluation at a uniquely determined point , and (2) a derivation , meaning a linear function satisfying . There is a whole tangent line’s worth of possible derivations, but the particular one we want will take the function to its correct derivative at . Hence we would want the such that . Since is the free ring on a generator , this condition uniquely determines (the book by Moerdijk and Reyes would be a good reference for the theory of rings).
The set-up I used just packages all these into the single homomorphism that sends to , so that when we compute the composite
we find that it sends to , as promised.
I haven’t checked the nLab to see to what extent we’ve already attested to these facts, but it’s pretty standard material in SDG and algebraic geometry.
It would be very nice to include this somewhere if we do not already have it, perhaps at differentiation, and then link to it from your argument chain rule. It looks like we may have something at differentiation which is similar to what you wrote in #8, but probably you could incorporate some more of #8 there.
With regard to actual formal power series, it follows very easily, as far as I see, from the binomial theorem/induction that we have the right thing (i.e. the usual formal derivative of power series). But again it would be good to put this observation in somewhere, if we do not already have it, and link to it from your argument at chain rule.
Thanks for the suggestions, Richard – they make sense. I’ll look into it and think about how to do it decorously.
Great! Thanks again for the nice additions!
1 to 11 of 11