Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry beauty book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-theory cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 14th 2018

    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 AA, the statement is that if q,pA[[x]]q, p \in A[ [x] ] are power series, with 00 the constant coefficient of pp, then (qp)(x)=q(p(x))p(x)(q \circ p)'(x) = q'(p(x))p'(x) under the usual definitions.

    Let D=A[y]/(y 2)D = A[y]/(y^2) be the representing object for derivations. Let δ:A[[x]]A[[x]] ADA[[x]][y]/(y 2)\delta: A[ [x] ] \to A[ [x] ] \otimes_A D \cong A[ [x] ][y]/(y^2) be the unique topological AA-algebra map (under the (x)(x)-adic topologies) that sends xx to x+yx + y. (If it helps, think δ(q)=q(x+y)\delta(q) = q(x + y).) For pA[[x]]p \in A[ [x] ], define pp' via the equation δ(p)=p(x)+p(x)y\delta(p) = p(x) + p'(x)y.

    Let π:A[[x]] ADA[[x]] AD\pi: A[ [x] ] \otimes_A D \to A[ [x] ] \otimes_A D be the unique topological algebra map taking xx to p(x)p(x) and yy to p(x)yp'(x)y. Let p:A[[x]]A[[x]]- \circ p: A[ [x] ] \to A[ [x] ] denote the unique topological algebra map that takes xx to pp. Then the diagram

    A[[x]] δ A[[x]] AD p π A[[x]] δ A[[x]] AD\array{ A[ [x] ] & \stackrel{\delta}{\to} & A[ [x] ] \otimes_A D \\ \mathllap{- \circ p} \downarrow & & \downarrow \mathrlap{\pi} \\ A[ [x] ] & \underset{\delta}{\to} & A[ [x] ] \otimes_A D }

    commutes in the category of topological algebras, since the two legs agree when evaluated at the generator xx. But then, evaluating each leg at a power series qA[[x]]q \in A [ [x]], we have

    [δ(p)](q)=δ(qp)=(qp)(x)+(qp)(x)y[\delta(- \circ p)](q) = \delta(q \circ p) = (q \circ p)(x) + (q \circ p)'(x)y


    [πδ](q)=π(δ(q))=π(q(x)+q(x)y)=q(p(x))+q(p(x))(p(x)y)[\pi \delta](q) = \pi(\delta(q)) = \pi(q(x) + q'(x)y) = q(p(x)) + q'(p(x))(p'(x)y)

    whence the coefficients of yy agree: (qp)(x)=q(p(x))p(x)(q \circ p)'(x) = q'(p(x))p'(x).

    • CommentRowNumber2.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 14th 2018

    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 yy we have

    (p(x)+p(x)y) n=p(x)+np(x) n1p(x)y\left(p(x) + p'(x)y\right)^n = p(x) + n p(x)^{n-1} p'(x)y

    say by the binomial theorem, or by an inductive argument. This gives the chain rule (qp)(x)=q(p(x))p(x)(q \circ p)'(x) = q'(p(x)) \cdot p'(x) at least for q(x)=x nq(x) = x^n. Then extend to all power series q(x)= n0a nx nq(x) = \sum_{n \geq 0} a_n x^n 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]]A[ [x] ].

  1. 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 pA[[x]]p \in A[ [x] ], define pp' via the equation δ(p)=p(x)+p(x)y\delta(p) = p(x) + p'(x)y.

    …I think one would need the binomial theorem or similar to identify pp' with one of the usual definitions. But perhaps I’m missing something?

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 14th 2018

    Thanks! I just meant that with that definition of pp', 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:RRp: R \to R is a function on the line and DD denotes the walking tangent vector, then under the Kock-Lawvere axiom which asserts an isomorphism R×RR DR \times R \cong R^D we may form a composite

    RΔR×RR Dp DR DR×RR \stackrel{\Delta}{\to} R \times R \cong R^D \stackrel{p^D}{\to} R^D \cong R \times R

    which is just p,p:RR×R\langle p, p' \rangle: R \to R \times 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(-)^D, it still took me some time to massage it into the form above.

  2. Ah, I didn’t realise that this definition of pp' was one of the novel aspects, even if inspired by SDG. Then the observation is nicer still!

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 14th 2018

    Sorry, I might not have made myself clear. I don’t think “my” definition of pp' 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 π\pi. 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.

  3. Ah, I see. Would it be possible to provide some reference for this definition of pp'? 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.

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 15th 2018
    • (edited Oct 15th 2018)

    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 C^\infty functions, rather than power series with coefficients in a commutative ring AA. In other words, replace AA with \mathbb{R} and A[[x]]A[ [x] ] with the ring C=C ()C = C^\infty(\mathbb{R}) of C C^\infty functions on \mathbb{R}. (Doing it with polynomials would probably be equally convincing.)

    So again we have the ring of dual numbers D=[y]/(y 2)D = \mathbb{R}[y]/(y^2). Given a point x 0x_0 \in \mathbb{R}, Hadamard’s lemma allows us to expand any function f(x)Cf(x) \in C in the form f(x 0)+a 1(xx 0)+g(x)(xx 0) 2f(x_0) + a_1(x - x_0) + g(x)(x - x_0)^2 for some unique number a 1a_1 and function g(x)Cg(x) \in C, and f(x 0)f'(x_0) is according to standard definition this value a 1a_1. In other words, there is by this lemma a canonical isomorphism

    C/(xx 0) 2CDC/(x - x_0)^2C \cong D

    which maps the residue class of f(x)f(x) to f(x 0)+f(x 0)yDf(x_0) + f'(x_0)y \in D. In fact any homomorphism ϕ:CD\phi: C \to D, written in the form ϕ(f)=ϕ 0(f)+ϕ 1(f)y\phi(f) = \phi_0(f) + \phi_1(f)y, is given by (1) a homomorphism ϕ 0:C\phi_0: C \to \mathbb{R}, with any such on C=C ()C = C^\infty(\mathbb{R}) being evaluation at a uniquely determined point x 0x_0, and (2) a derivation ϕ 1:C\phi_1: C \to \mathbb{R}, meaning a linear function satisfying ϕ 1(fg)=ϕ 1(f)ϕ 0(g)+ϕ 0(f)ϕ 1(g)=ϕ 1(f)g(x 0)+f(x 0)ϕ 1(g)\phi_1(f g) = \phi_1(f)\phi_0(g) + \phi_0(f)\phi_1(g) = \phi_1(f)g(x_0) + f(x_0)\phi_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)=xf(x) = x to its correct derivative 11 at x 0x_0. Hence we would want the ϕ:CD\phi: C \to D such that ϕ(x)=x 0+1y\phi(x) = x_0 + 1 \cdot y. Since CC is the free C C^\infty ring on a generator xx, this condition uniquely determines ϕ\phi (the book by Moerdijk and Reyes would be a good reference for the theory of C C^\infty rings).

    The set-up I used just packages all these ϕ\phi into the single homomorphism δ:CC DC[y]/(y 2)\delta: C \to C \otimes_\mathbb{R} D \cong C[y]/(y^2) that sends xx to x+yx + y, so that when we compute the composite

    CδC Dev x 01 DDC \stackrel{\delta}{\to} C \otimes_\mathbb{R} D \stackrel{ev_{x_0} \otimes 1}{\to} \mathbb{R} \otimes_\mathbb{R} D \cong D

    we find that it sends f(x)f(x) to f(x 0)+f(x 0)yf(x_0) + f'(x_0)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.

    • CommentRowNumber9.
    • CommentAuthorRichard Williamson
    • CommentTimeOct 15th 2018
    • (edited Oct 15th 2018)

    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.

    • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 15th 2018

    Thanks for the suggestions, Richard – they make sense. I’ll look into it and think about how to do it decorously.

  4. Great! Thanks again for the nice additions!