What is the symmetric monoidal structure on the $(\infty,1)$-category of spectra?
Lurie characterizes the symmetric monoidal structure on $\mathsf{Sp}$ by a universal property (HA.4.8.2.19): it is uniquely determined up to a contractible space of choices by the property that $S^0$ is the unit and $\wedge$ commutes with homotopy colimits in both variables.
I think on first glance this sounds like one of those formal things that doesn't help you 'compute' anything, but I claim that (i) you can get all the computational mileage out of this that you usually get from model categories of spectra and (ii) if you like, you can easily show that your favorite symmetric monoidal model category of spectra models this symmetric monoidal structure.
We'll start with (ii) since that's what you asked about, and it's easier. Suppose you have a model category $\mathbf{M}$ which models spectra (which is something else that can be checked easily from universal properties by its relationship to some model for $\mathsf{Spaces}$, for example). Suppose further that it's a symmetric monoidal model category. Then the underlying $\infty$-category $\mathsf{M}[W^{-1}] \cong \mathsf{Sp}$ inherits a symmetric monoidal structure. To compare it with the 'universal' one, one needs to check that the tensor product commutes with homotopy colimits and that the unit is weakly equivalent to the sphere spectrum. The unit requirement is just always satisfied (otherwise what sort of spectra are you using??) and the homotopy colimit requirement is also always satisfied, because part of the definition of being a symmetric monoidal model category is that $\otimes$ be a left Quillen bifunctor- and that forces the tensor product to commute with homotopy colimits in both variables.
Now let's talk about (i). What does it even mean to 'understand' the smash product of spectra? Well, usually the way a spectrum is handed to us is as a sequence of (say, pointed) spaces $(X_k)$ and maps $\Sigma X_k \to X_{k+1}$. Every model ever includes at least that much data, often with all sorts of extra requirements and structure. But in any case, this data presents a spectrum $X = \mathrm{hocolim}_k \Sigma^{-k}\Sigma^{\infty}X_k$. So, from the universal property we learn that $$ X \wedge Y = \underset{j,k}{\mathrm{hocolim}}\, \Sigma^{-j-k}\left( \Sigma^{\infty}X_j \wedge \Sigma^{\infty}Y_k\right). $$ So now we'd better figure out how to compute $\Sigma^{\infty}A \wedge \Sigma^{\infty} B$ for pointed spaces $A$ and $B$. It's possible to argue very abstractly that $\Sigma^{\infty}$ must be symmetric monoidal, using the methods in HA.4.8.2, but you can also argue as follows: first reduce to the unpointed case, so we want to compute $\Sigma^{\infty}_+A \wedge \Sigma^{\infty}_+B$. But $A$ and $B$ are homotopy colimits of constant diagrams shaped like $A$ and $B$, respectively. And $\Sigma^{\infty}_+$ commutes with homotopy colimits. A little string of equivalences and the fact that $\Sigma^{\infty}_+(*) = S^0$ is the unit gives the result.
Excellent, so just from nonsense we learn that $\Sigma^{\infty}$ is symmetric monoidal. Moving back to our original formula we learn that a 'concrete' computation for the smash product is:
$$X \wedge Y = \underset{j,k}{\mathrm{hocolim}}\, \Sigma^{-j-k}\left( \Sigma^{\infty}X_j \wedge \Sigma^{\infty}Y_k\right) = \underset{j,k}{\mathrm{hocolim}}\, \Sigma^{-j-k}\left( \Sigma^{\infty}(X_j \wedge Y_k)\right).\quad (1)$$
If you like, then at this point you could pick your favorite cofinal copy of $\mathbb{N}$ inside $\mathbb{N} \times \mathbb{N}$ and present this smash product as a sequence of spaces with maps from the suspension of one to the next.
This way of thinking about the smash product is the very original one, going back to Boardman and Adams. Of course they ran into all sorts of technical issues verifying all the properties they wanted out of a symmetric monoidal structure. What happened to those? Well, when dealing with a symmetric monoidal structure one would like (a) properties and (b) the ability to 'compute' what the thing does. The original approach was to begin with (b) and then work hard to verify (a). In the present situation, one begins with (a) using various levels of sophistication and then deduces (b). Of course, lots of technical work went into producing the symmetric monoidal $\infty$-category $\mathsf{Sp}$! But the work pays off: you get a much stronger theorem and a more flexible theory.
Let me go into a bit more detail about comparing with, say, the formula for the smash product one finds for orthogonal spectra. I claim that it is a particular model-categorical presentation of precisely the formula (1). To justify that, I'm going to compare the two formulae directly. So I'll need to review a bit about orthogonal spectra. Recall that an orthogonal spectrum consists of a sequence of pointed spaces $X_n$ equipped with $O(n)$-actions together with compatible, $O(n)\times O(m)$-equivariant, based maps $X_n \wedge S^m \to X_{n+m}$. Given an orthogonal spectrum, one would like to know how to describe the corresponding object in $\mathsf{Sp}$ and how to understand smash products.
We'll take the $\infty$-category $\mathsf{Spaces}$ as 'understood' and the functor $\Sigma^{\infty}$ as also understood. Then an orthogonal spectrum $(X_k)$ presents an object of $\mathsf{Sp}$ by the formula $$X = \underset{\mathbb{N}}{\mathrm{hocolim}}\, \Sigma^{-k}\Sigma^{\infty}X_k$$ Of course, we ignored the orthogonal group action. Luckily, here's a fun fact:
Fun fact. Let $\mathsf{Orth}$ denote the $\infty$-category of real inner product spaces and isometric embeddings. Then the inclusion $\mathbb{N} \to \mathsf{Orth}$ is homotopy final.
It follows that we may compute the homotopy colimit either over $\mathsf{Orth}$ or over $\mathbb{N}$. That's important, because the formula for the smash product of orthogonal spectra is really trying to be a formula for a homotopy colimit over $\mathsf{Orth} \times \mathsf{Orth}$. I won't bother typesetting the formula here (see page 5 of Schwede's book, for example) but unless I'm mistaken one arrives at this formula as follows:
- Take the formula in (1) and replace the homotopy colimit over $\mathbb{N} \times \mathbb{N}$ by a homotopy colimit over $\mathsf{Orth} \times \mathsf{Orth}$.
- To compute that homotopy colimit, we are free to first left Kan extend along $\oplus: \mathsf{Orth} \times \mathsf{Orth} \to \mathsf{Orth}$.
- Stare at the pointwise formula for the left Kan extension evaluated at $\mathbb{R}^n$, and you become interested in a homotopy colimit along all pairs $p+q = n$ together with actions of $O(p) \times O(q)$ etc.
- Now suspend everything n times, erase the $\Sigma^{\infty}$'s, and use one of the standard formulas for computing a homotopy colimit as an ordinary colimit in some model category, and you should get (with cofibrancy conditions if you want the right homotopy type) the previously mentioned formula in the linked book.
The same thing works in symmetric spectra, except that the claim about finality is false. Instead, one uses a cofibrancy condition that allows a lemma of Bökstedt to apply so you can replace $\mathbb{N}$ with the category of finite sets and injections.
Let me add a short observation to Dylan's fantastic answer. There is indeed a more concrete construction of the symmetric monoidal structure on the $\infty$-category of spectra: it is the localized Day convolution.
Let me backtrack one second: we identify spectra as the reduced 1-excisive functor $E:\mathrm{Space}^{fin}_*\to\mathrm{Space}$, that is those functors such that
- $E(*)=*$;
- If $X'\to X\to X''$ is a cofiber sequence, then $E(X')\to E(X)\to E(X'')$ is a fiber sequence.
This is essentially identifying one spectrum $E$ with the functor $X\mapsto \Omega^\infty(E\wedge \Sigma^\infty X)$, in particular $E(S^n)$ is the $n$-th space of the spectrum.
If $C$ is a small symmetric monoidal $\infty$-category and $D$ is a cocomplete symmetric monoidal $\infty$-category where $\otimes$ commutes with colimits in eqch variable, the $\infty$-category $\mathrm{Fun}(C,D)$ comes equipped with a canonical symmetric monoidal structure, called Day convolution with the following properties:
- The tensor product is given by the formula $$ (F\otimes G)(c)={\mathrm{colim}\\ {\scriptsize c'\otimes c''\to c}} F(c')\otimes G(c'')\,;$$
- The unit is the left Kan extension of the inclusion of the unit of $D$ along the inclusion of the unit of $C$. In particular if $D$ is the $\infty$-category of spaces the unit is given by $\mathrm{Map}_C(1_C,-)$;
- The tensor product commutes with colimits separately in each variable;
- $O$-algebras in this symmetric monoidal structure correspond to $O$-monoidal functors from $C$ to $D$, for any ($\infty$-)operad $O$
(see Higher Algebra, 2.2.6 or Glasman's Day convolution for ∞-categories).
Now $\mathrm{Sp}\subseteq\mathrm{Fun}(\mathrm{Space}^{fin}_*,\mathrm{Space})$ is closed under homotopy limits, and so it is a reflective subcategory, that is the inclusion has a left adjoint $\partial_1$. Moreover $\partial_1$ is compatible with the symmetric monoidal structure: for every $F$, the functor $F\otimes-$ sends $\partial_1$-equivalences to $\partial_1$-equivalences (this requires some work to prove but it's not too hard). So by HA.2.2.1.1, this equips $\mathrm{Sp}$ with a symmetric monoidal structure where the unit is the sphere spectrum (which is easily seen to just be $\partial_1$ of the identity) and such that $$E\wedge E' = \partial_1(E\otimes E')\,.$$
How do we know that this coincides with the symmetric monoidal structure that we were able to construct by abstract means as in Dylan's answer? Well, the unit is the sphere spectrum, and $E\wedge-=\partial_1(E\otimes -)$ manifestly commutes with colimits (after all $\partial_1$ is a left adjoint), but there is only one symmetric monoidal structure with these properties!
I thought it might be worth mentioning, as an addendum to the other nice answers, that there is also an $\infty$-categorical approach to the smash product that looks more like the traditional constructions: namely, you can just redo the most classical construction of the smash product on the stable homotopy category (as in Adams's book) using $\infty$-categories. (I suppose this might count as a "folk theorem", and unfortunately I don't think it's been written down in detail anywhere; I learned the idea from Justin Noel.)
Start with the $\infty$-category $\mathrm{PSp}$ of "prespectra", meaning sequences of pointed spaces $X_n$ with maps $\Sigma X_n \to X_{n+1}$. Using the smash product of pointed spaces you can enhance this to an $\infty$-operad: a multimorphism $(X, Y) \to Z$ is given by maps $X_n \wedge Y_m \to Z_{n+m}$ compatible with the structure maps in $X,Y,Z$ (and similarly for multimorphisms with more inputs).
Now consider the subcategory $\mathrm{Sp}$ of "spectra" (or "$\Omega$-spectra"), meaning prespectra $X$ where the adjoint maps $X_n \to \Omega X_{n+1}$ are equivalences. If you restrict the operad structure to this subcategory, I claim you get a symmetric monoidal $\infty$-category: for spectra $X$, $Y$, $Z$, multimorphisms $(X,Y) \to Z$ are represented by maps $X \wedge Y \to Z$ for a spectrum $X \wedge Y$. This spectrum you can define by choosing sequences $i_n$, $j_n$ with $i_n+j_n = n$ (with both unbounded) and setting $(X \wedge Y)_n := X_{i_n} \wedge Y_{j_n}$ - what Adams calls a "handicrafted smash product", if I recall correctly.
Actually working this out precisely would take a fair bit of (probably quite annoying) work, however, and in terms of applications I doubt it would have any advantages over the constructions Dylan and Denis describe.