@PiotrPstrągowski maybe my question is how your first-mentioned isomorphism works at p=2 - I would have thought that triple-tensor product is more naturally H_H as opposed to H_ BP (topologically I don't see how that naturally acquires a Hopf algebroid structure). I concede that the thing you mention is maybe more interesting to ask, but I'm currently interested in the more humble question I asked in my previous post, and would love to know the answer!

From what I can glean you might be suggesting that the answer is "an accident of topology" that the two formal groups for H (real orientation vs complex orientation) differ in grading--but then there is also this thing about the Frobenius which sounds deep! Could you explain more? Is that Frobenius reflected in the topology or do I have to calculate everything in sight and just see that I need to square things at the end to make it all match up?

goodwillie calculus. most descriptions of the chain rule in calculus that I know focus on describing the layers ∂_n (GF) in terms of ∂_p(G) and ∂_q(F). is there a clean description of the terms P_n(GF) in the Taylor tower in terms of P_p(G) and P_q(F)?

in particular i'm mostly interested, say, in a stable setting where the identity functor for range(F) = domain(G) is linear.

@TylerLawson I think Tomer Schlank told me at some point that you can get something like that using Saul Glasman's description of n-excisive functors as Mackey functors. I don't know if this has ever been worked out though, nor if this is any helpful in you setting

Right. I guess what I'm actually getting at is that I want is an "idempotent" version of calculus

So say for the time being we're looking at functors Sp -> Sp. Calculus takes functors F to filtered functors P_n F.

I'd ideally like calculus to take in a filtered functor F_n and produce a filtered functor, and for this to be compatible with, say, a Day convolution for filtered functors.

Is there a name for a map of spaces that induces an injection on all homotopy groups at all basepoints and an injection on π_0 (something like a 'faithful' functor of ∞-groupoids?

nevermind