naturality

Stream: condensed mathematics

[Johan Commelin]

If I'm not mistaken, if 𝓐 is an abelian category, then arrow 𝓐 is also an abelian category. I think this means that if we formulate constructions just for objects, but in a random abelian category, then we might be able to get naturality for free by applying the construction to arrow.mk f. E.g. the naturality of the snake δ, etc...
Not saying this is a useful trick right now for LTE. But it's just a thought that occured to me.

[Peter Scholze]

Ah, this is a neat idea! I wasn't aware of this argument.

[Johan Commelin]

I guess you need to verify that the construction is "functorial" on objects. But that might just be defeq, if we're lucky/careful.

[Adam Topaz]

Yeah I thought about something like this as well (when I was working on naturality of the $$\delta$$s), but I don't think this buys you a free lunch. It probably just means you need to prove that some functors commute with the two projection functors from arrow, and the proofs probably end up being similar to proving naturality anyway.