@AdrianClough Why doesn't LieGrp_n → LieGrp_0 being an equivalence imply that every topological Lie group has a unique differential structure? It seems to me like it does.

@MarcHoyois It doesn't imply so on the nose, but only after a modicum of work: The identity map between a topological Lie group equipped with two a priori different differentiable structures must lift to a smooth map, showing that the two structures were in fact the same. Saying that $\mathbf{LieGrp}_n \to \mathbf{LieGrp}_0$ an isomorphism simply encodes as explicit information that one obtains a bijection between topological and differentiable Lie groups.

My point wasn't that it is somehow harder to show that $\mathbf{LieGrp}_n \to \mathbf{LieGrp}_0$ is an isomorphism, rather than an equivalence. My point was that $\mathbf{LieGrp}_n \to \mathbf{LieGrp}_0$ being an isomorphism encodes/reflects something interesting about Lie groups, and thus that the observation that every ordinary category is canoically flagged is not meaningless.

Perhaps the general statement here is that any forgetful functor which is an equivalence is automatically an isomorphism.

As noted further up, uniqueness of differentiable structures is already apparent in their geometric origin, as the differentiable structure on a topological Lie group, comes from the fact that (with a lot of work) it is possible to construct an exponential map, and that together with translations this gives you your atlas.

@AdrianClough I disagree with your point then: I fail to see what relevant information is encoded in the statement that one has a bijection. Note that this statement is dependent on arbitrary definitions: if I choose to think of smooth manifolds as ringed spaces, then I don't have a bijection anymore.

I certainly agree that flagged categories are sometimes relevant, but I don't think that's a good example because we don't actually care about a choice of flag on these categories.