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 A, the statement is that if q,pβA[[x]] are power series, with 0 the constant coefficient of p, then (qβp)β²(x)=qβ²(p(x))pβ²(x) under the usual definitions.
Let D=A[y]/(y2) be the representing object for derivations. Let Ξ΄:A[[x]]βA[[x]]βADβ A[[x]][y]/(y2) be the unique topological A-algebra map (under the (x)-adic topologies) that sends x to x+y. (If it helps, think Ξ΄(q)=q(x+y).) For pβA[[x]], define pβ² via the equation Ξ΄(p)=p(x)+pβ²(x)y.
Let Ο:A[[x]]βADβA[[x]]βAD be the unique topological algebra map taking x to p(x) and y to pβ²(x)y. Let ββp:A[[x]]βA[[x]] denote the unique topological algebra map that takes x to p. Then the diagram
A[[x]]Ξ΄βA[[x]]βADββpββΟA[[x]]βΞ΄A[[x]]βADcommutes in the category of topological algebras, since the two legs agree when evaluated at the generator x. But then, evaluating each leg at a power series qβA[[x]], we have
[Ξ΄(ββp)](q)=Ξ΄(qβp)=(qβp)(x)+(qβp)β²(x)yand
[ΟΞ΄](q)=Ο(Ξ΄(q))=Ο(q(x)+qβ²(x)y)=q(p(x))+qβ²(p(x))(pβ²(x)y)whence the coefficients of y agree: (qβp)β²(x)=qβ²(p(x))pβ²(x).
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 y we have
(p(x)+pβ²(x)y)n=p(x)+np(x)nβ1pβ²(x)ysay by the binomial theorem, or by an inductive argument. This gives the chain rule (qβp)β²(x)=qβ²(p(x))β pβ²(x) at least for q(x)=xn. Then extend to all power series q(x)=βnβ₯0anxn 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 A[[x]].
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 pβA[[x]], define pβ² via the equation Ξ΄(p)=p(x)+pβ²(x)y.
β¦I think one would need the binomial theorem or similar to identify pβ² with one of the usual definitions. But perhaps Iβm missing something?
Thanks! I just meant that with that definition of pβ², 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 p:RβR is a function on the line and D denotes the walking tangent vector, then under the Kock-Lawvere axiom which asserts an isomorphism RΓRβ RD we may form a composite
RΞβRΓRβ RDpDβRDβ RΓRwhich is just β¨p,pβ²β©:RβRΓR. (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 (β)D, it still took me some time to massage it into the form above.
Ah, I didnβt realise that this definition of pβ² 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 pβ² 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 pβ²? 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 Cβ functions, rather than power series with coefficients in a commutative ring A. In other words, replace A with β and A[[x]] with the ring C=Cβ(β) of Cβ functions on β. (Doing it with polynomials would probably be equally convincing.)
So again we have the ring of dual numbers D=β[y]/(y2). Given a point x0ββ, Hadamardβs lemma allows us to expand any function f(x)βC in the form f(x0)+a1(xβx0)+g(x)(xβx0)2 for some unique number a1 and function g(x)βC, and fβ²(x0) is according to standard definition this value a1. In other words, there is by this lemma a canonical isomorphism
C/(xβx0)2Cβ Dwhich maps the residue class of f(x) to f(x0)+fβ²(x0)yβD. In fact any homomorphism Ο:CβD, written in the form Ο(f)=Ο0(f)+Ο1(f)y, is given by (1) a homomorphism Ο0:Cββ, with any such on C=Cβ(β) being evaluation at a uniquely determined point x0, and (2) a derivation Ο1:Cββ, meaning a linear function satisfying Ο1(fg)=Ο1(f)Ο0(g)+Ο0(f)Ο1(g)=Ο1(f)g(x0)+f(x0)Ο1(g). There is a whole tangent lineβs worth of possible derivations, but the particular one we want will take the function f(x)=x to its correct derivative 1 at x0. Hence we would want the Ο:CβD such that Ο(x)=x0+1β y. Since C is the free Cβ ring on a generator x, this condition uniquely determines Ο (the book by Moerdijk and Reyes would be a good reference for the theory of Cβ rings).
The set-up I used just packages all these Ο into the single homomorphism Ξ΄:CβCββDβ C[y]/(y2) that sends x to x+y, so that when we compute the composite
CΞ΄βCββDevx0β1ββββDβ Dwe find that it sends f(x) to f(x0)+fβ²(x0)y, 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