@AaronMazel-Gee I'm going to take the slightly extreme position that no one should learn category theory by studying the 1-category of strict categories (I assume some worthwhile math research can be done on that 1-category, but pretending it is the object you end up using in practice is doing the students a disservice)

@DenisNardin How are you going to teach students what categories even are, then?

@TomBachmann My idea was more to teach what an equivalence of categories is, and not what an isomorphism of categories is

(I never found the notion of isomorphism of categories useful). But I'll admit that my thoughts on this are a bit half baked

And similarly, I would try to define only invariant notions, even in a first class on category theory, and push the emphasis away from "strict notions"

From trying to formulate an answer I realize that my ideas are even more half-baked ^^.

I guess here is an analogy. We could teach group theory in terms of presentations. But we don't have to: we can write down the correct notion ("a group") directly. How does one write down the correct notion corresponding to the presentation "1-category of strict categories" directly? I suppose "the oo-category of complete segal spaces" is some kind of answer, but I'm not sure how helpful it is for a first course.

Nah, I was thinking a lot more low tech

I'm fine with giving students the definition of category via objects and arrows, and the "strict" notion of functor

I just think we should also give the notion of natural transformation shortly thereafter, natural isomorphism and equivalence of categories, and emphasize that we only care for the notions that are invariant up to equivalence

Of course if we had, say, an axiomatic presentation of the ∞-category of spaces that would allow us to work from it from first principles (similarly to how you can develop analysis just by working in a complete ordered field without ever mentioning Dedekind cuts) it would be amazing. But we're not there yet

Cisinski gave a talk at one of our seminars, where he said that as human beings we have direct access to strict notions in mathematical language and only indirect access to the weak correct notions.

I think that's the main difficulty with trying to introduce ∞-categories before categories, but maybe you mean something more subtle.

Here's an example of a non-replete subcategory that I think is nice to have even if it's not an invariant notion: The inclusion of Δ into FinSet.

@HarryGindi Nice quote!

It's paraphrasing him

I don't want to say it's a quote!!

An ordinary category $\mathcal{C}$ is secretly flagged in the sense of Ayala-Francis: If we denote by $\tilde{\mathcal{C}}$ the complete Segal space associated to $\mathcal{C}$, then $\mathcal{C}_0 \to \tilde{\mathcal{C}}$ is the corresponding flagged $\infty$-category. A strict functor of categories is thus simply a flagged functor. Often this flagging is redundant, and the classical way of getting rid of this redundancy is to speak of equivalences of categories.

I know of one situation where the notion of strict equivalence of categories is meaningful. For any $n \in \mathbf{N} \cup \{\infty\} \cup \{\omega\}$, denote by $\mathbf{LieGrp}_n$ the category of $C^n$-Lie groups. Several classical and deep theorems about Lie groups are subsumed by the observation that for any $m \geq n$ the forgetful functor $\mathbf{LieGrp}_m \to \mathbf{LieGrp}_n$ is a strict equivalence of categories.

@DenisNardin just to clarify what i think you're saying, i think it is valuable to see strict categories on the way to learning about ($\infty$-)categories, just as it is valuable to see topological spaces on the way to learning about $\infty$-groupoids (e.g. to appreciate homotopy pullbacks). i agree that the notion of isomorphism between categories should not be emphasized. i just mean to say that the first definition one sees should involve a set of objects.

@AaronMazel-Gee Well, sure. I don't really know a different one, so we're kind of stuck with it :)

@AdrianClough This is rather interesting... can you elaborate why the statement that those functors are equivalences is weaker (from a practical, diffgeom point of view)?

well, the invariant notion of 1-category should only have a homotopy 1-type as its object of objects; i would say that the (well, "a") correct definition is a complete Segal space (i.e. an $\infty$-functor $\Delta^{op} \to Spaces$) satisfying the condition that its hom-spaces are discrete. but obviously that is inappropriate (not to mention circular) as a first definition!

The circularity is what worries me most :)

But I agree that it ought to be possible to make it into a real definition, and that then it would become the "correct" one

i'm ignorant of homotopy type theory, but at least for now i believe that it is necessary to first make strict definitions

Yeah, I haven't kept up with HoTT, but iirc they're still not able to define ∞-categories completely internally

If they were able it would be a great progress in my perspective

@AdrianClough another good example of a (non-terminally) flagged $(\infty,n)$-category is the fully extended cobordism $n$-category, for $n \geq 5$ or so -- if i recall correctly, this results from nontrivial h-cobordisms

@DenisNardin I heard from someone who does HoTT that Finster found a problem with his definition, so it looks like they're still having trouble

@AaronMazel-Gee MSRI is starting up in 3 hours, 2 hours, or now?

@DenisNardin For concreteness, let us say that $n = 0$ and $m > 0$. Then the fact that $\mathbf{LieGrp}_m \to \mathbf{LieGrp}_0$ is an equivalence of categories tells us that every topological group admits a differentiable structure, and that any topological Lie group homomorphism is automatically differentiable. The fact that we obtain a strict equivalence tells us that every topological Lie group admits a unique differentiable structure.

We can obtain the strict equivalence of categories from the ordinary equivalence of categories by simply noting that for a topological Lie group with two a priori different differentiable structures, the identify morphism must be a diffeomorphism. But the uniqueness already follows from the method by which we obtain the smooth structure in the first place:

@AdrianClough Ah that was what I was about to say...

Given a topological Lie group (or really a locally compact Hausdorff group satisfying the "no small neighbourhood" condition) it is possible to show the set of $1$-parameter subgroups may be equipped with a unique structure of a vector space giving us as an exponential map. The exponential map together with translations then gives us a canonical atlas for our Lie group.

@HarryGindi 2.5 hours from now (it's currently ~8:30am in california)

@AdrianClough what do you mean by a "strict equivalence of categories"? (an equivalence of categories in the usual sense, with the emphasis that the categories are strict? or an isomorphism of strict categories?)

@AaronMazel-Gee An isomorphism of categories.

aye aye

@AaronMazel-Gee This is already visible on the level of $(\infty,1)$-categories: The Segal space of bordisms $\mathbf{Bord}_d$ can be viewed as the flagged $(\infty,1)$-category, where the flagging comes from sending any path in $(\mathbf{Bord}_d)_0$, the space closed $(d-1)$-submanifolds in $\mathbf{R}^\infty$ to its "graph". Such graphs are precisely the invertible bordisms coming from attaching a closed $(d-1)$-dimensional manifold to its cylinder via a diffeomorphism on one side. cont.

In dimensions $\geq 5$ the invertible bordisms are precisely the h-bordisms, and the h-cobordism theorem tells us precisely that not all such invertible bordisms are obtained from diffeomorphisms.

This flagged notion gets used somewhere else, right? You need it to construct the classifier for those flat fibration things iirc

@HarryGindi Yes, the universal exponential fibration is an exponential fibration of flagged $\infty$-categories.

I forget what they are, but iirc it's sort of a weaker version of a correspondence

yeah

This is provided with actual proofs now in the new version of Ayala-Francis?

I remember being disappointed by the dearth of proofs in the version I read several years ago

I don't know; I haven't ready that paper very carefully.

well, they added 12 pages, so they probably added in a bit more detail

@AaronMazel-Gee so wait did it just start

For HF_p[C_p]-modules the C_p fixed point functor is easily seen to be conservative (we can glue the free module from trivials). Is it known if it is true for p-complete spectra?