K(n)-local semiadditivity

As an application of the theory developed so far, we reprove the seminal result of Hopkins–Lurie that the category of K(n)-local spectra is \infty-semiadditive. Their proof relied on classical computations of K(n)-cohomology of Eilenberg-MacLane anima by Ravenel–Wilson; we instead will present a more compact proof due to Ben-Moshe that uses more modern developments. It starts by bootstrapping off of classical Tate vanishing results in chromatically localized spectra (both T(n)- and K(n)-local spectra) due to Greenlees-Sadofsky, Hovey-Sadofsky, and Kuhn. We then induct on chromatic height using recent higher descent results surrounding how algebraic K-theory interacts with higher semiadditivity (Ben-Moshe–Carmeli–Schlank–Yanovski), along with redshift phenomena of Lubin–Tate spectra (Yuan) and the Chromatic Nullstellensatz (Burklund–Schlank–Yuan). Along the way, we also show that the height n monochromatic categories are also \infty-semiadditive.