@TimCampion yeah that's a fair point. perhaps not. I was thinking that this sort of behavior was restricted to things living under <HF_p> but now I'm not sure.
I read that there is a sort of transitivity similar to the one of ordinary kan extensions; e.g. if X \subset Y \subset Z and F:^: Z \to C is such that F is an operadic kan extension of F| Y, F|Y is an o.k.e of F| X, then F is an o.k.e of F|Z
Lurie Proof is quite complicated, and also does not shed light on the converse (as there is in Kan Extensions: if one of the two intermediate - I think the second - is Kan, then the global is Kan iff the other intermediate is Kan)
Thank you!!
I am trying to formulate the factorization algebra property in terms of operadic Kan extensions, and then show that the prefactorization algebra that factorization homology gives (defined as: on each U I assign \int_U A, for some fixed A E_n algebra) a factorization algebra
There is a passage in which I got stuck.. :(
If you think you could help better with the concrete situation I can write it down
So, the universal property I was thinking of is HA.3.1.3.2, which is formulated in a slightly different manner since there Lurie talks about "q-free algebras" but they are basically the same thing (and what most people think of when they talk about operadic Kan extensions)
I really dislike how that chapter of HA is set up
In general the whole approach Lurie takes to Kan extensions (both ordinary and operadic) can be greatly improved upon, so I wouldn't waste too much time trying to understand the details of the proofs
But what are practical theorems one can use to show that something is a Kan extension, rather than proving by hand that some stuff form an operadic colimit?
In my case is really likely to come from some abstract manipulations
In practice I've found that what people use of that theory is: (1) The existence theorems for OKEs and (2) The formulas for the underlying objects of the OKEs
In particular, the universal property I cited above often allows you to construct a map between the OKE and the object you are interested in, and then you just check if it is an equivalence on underlying objects