- Boxes (□)
- definitions
- Ellipses (○)
- theorems and lemmas
- Diamonds (◇)
- axioms — unformalized external results
- ■ Draft
- AI-generated, not yet reviewed
- ■ Reviewed
- human confirmed NL content
- ■ Bound
- has
\lean{{}}binding to Lean declaration - Aligned
- human confirmed NL↔Lean semantic match
- Proved
- Lean proof compiled (theorems only)
For a map between classical spectra \(f: X\to Y\), consider the associated synthetic map from Notation 0.126
For any \(2\le r\le \infty \), we denote the following mod \(\lambda ^{r-1}\) reduction maps by \(\hat f_{r-1}\):
Since the synthetic Adams \(E_\infty \)-page contains more information than the classical Adams \(E_\infty \)-page, the \((f,E_\infty )\)-extensions similarly provide more information compared to the classical \(f\)-extensions.
A crossing of the \((f,E_\infty )\)-extension \(d_{n}^{f,E_\infty }(x)=y\) is defined as an essential \((f, E_\infty )\)-extension from some \(x'\in Z_{\infty }^{s+a,t+a}(X)\) to
(where \(\backslash \) denotes the difference of sets, meaning \(y'\) survives to the classical Adams \(E_{\infty }\)-page while it is not hit by any Adams differential) for \(a{\gt}0\) and \(0\le b\le n-a-e(f)\).
A crossing of the \((f,E_r)\)-extension \(d_{n}^{f,E_r}(x)=y\) in (5.3) is defined as an essential \((f, E_{r-a})\)-extension from some \(x'\in Z_{r-1-a}^{s+a,t+a}(X)\) to
(where \(\backslash \) denotes the difference of sets and it means that \(y'\) should survive to the classical Adams \(E_{r-n+b+e(f)}\) page while it should not be hit by an Adams differential of length at most \(1+n-b-e(f)\)) for \(0{\lt}a \le r-2\) and \(0\le b\le n-a-e(f)\). See Figure 3.
Let \(x\in Z^{s,t}_{r-1}(X)\) and \(y\in Z^{s+n,t+n}_{r-1-n+e(f)}(Y)\) for some
We say that there is an \((f,E_r)\)-extension from \(x\) to \(y\), denoted by
if there exists a synthetic \(\hat f_{r-1}\)-extension
where \(x\) is viewed as an element of the subgroup (5.1) with \(k=0\), and \(\lambda ^{n-e(f)} y\) is viewed as an element of the quotient group (5.2) with \(k=0\).
We say that this \((f,E_r)\)-extension in (5.3) is essential if the corresponding synthetic \(\hat f_{r-1}\)-extension in (5.4) is an essential differential in the \(\hat f_{r-1}\)-ESS.
For \(r=\infty \), we similar define an \((f,E_\infty )\)-extension using the corresponding synthetic \(\hat f\)-extension.
A crossing of the \((f,E_r)\)-extension of level \(l\) \(d_{n}^{f,E_r,l}(x)=y\) in (5.5) is defined as an essential \((f, E_{r-a})\)-extension of level \(l\) from some \(x'\in Z_{r-1-a}^{s+a,t+a}(X)\) to
for \(0{\lt}a \le r-2\) and \(0\le b\le n-a-e(f)\).
For \(r=\infty \), we similarly define a crossing of an \((f,E_\infty )\)-extension of level \(l\) as an essential \((f, E_\infty )\)-extension of level \(l\) from some \(x'\in Z_{\infty }^{s+a,t+a}(X)\) to \(y'\in Z_{\infty }^{s+n-b,t+n-b}(Y)\backslash B_{1+n-b-e(f)}^{s+n-b,t+n-b}(Y)\) for \(a{\gt}0\) and \(0\le b\le n-a-e(f)\).
Let \(x\in Z^{s,t}_{r-1}(X)\) and \(y\in Z^{s+n,t+n}_{r-1-n+e(f)}(Y)\) for some
We say that there is an \((f,E_r)\)-extension of level \(l\) from \(x\) to \(y\), denoted by
if there exists a synthetic \(\hat f_{r-1}\)-extension
where \(\lambda ^l x\) is viewed as an element of the subgroup (5.1) with certain \(k\), and \(\lambda ^{n-e(f)+l} y\) is viewed as an element of the quotient group (5.2).
We say that this \((f,E_r)\)-extension of level \(l\) in (5.5) is essential if the corresponding synthetic \(\hat f_{r-1}\)-extension in (5.6) is an essential differential in the \(\hat f_{r-1}\)-ESS.
For \(r=\infty \), we similarly define an \((f,E_\infty )\)-extension of level \(l\) using the corresponding synthetic \(\hat f\)-extension.
Consider an \((f,E_r)\)-extension \(d_{n}^{f,E_r}(x)=y\) in (5.3). The element \(y\) should be interpreted as a coset with indeterminacy given by \(B_{1+n-e(f)}^{s+n,t+n}(Y)\), plus the sum of images of \(d^{\hat f_{r-1}}_{{\lt}n}\) differentials. This \((f,E_r)\)-extension is essential if this coset does not contain 0.
For a map \(f: X \to Y\) which is part of a distinguished triangle \(X \xrightarrow {f} Y \xrightarrow {g} Cf \to \Sigma X\), define
When \(\mathrm{AF}(f) = 0\), we also denote \(\nu f\) by \(\hat{f}\). In both cases, we have \(\hat{f}: \Sigma ^{0,e(f)}\nu X \to \nu Y\) and \(\nu f = \lambda ^{e(f)}\hat{f}\). Furthermore, \(C\hat{f} \simeq \Sigma ^{0,-e(g)}\nu Cf\) (by Axiom 0.124).
Let \(X \in \mathcal{S}^{\mathrm{fin}}\) be a finite spectrum. For \(r \ge 2\), the \(E_\infty \)-page of the synthetic Adams spectral sequence for \(\nu X / \lambda ^r\) is
An \((f,E_\infty )\)-extension \(d_{n}^{f,E_\infty }(x)=y\) has a crossing if and only if the synthetic \(\hat f\)-extension \(d_{n}^{\hat f}(x)=\lambda ^{n-e(f)} y\) has a crossing.
An \((f,E_r)\)-extension of level \(l\) \(d_{n}^{f,E_r,l}(x)=y\) (5.5) has a crossing if and only if the corresponding synthetic \(\hat f_{r-1}\)-extension \(d_{n}^{\hat f_{r-1}}(\lambda ^l x)=\lambda ^{n-e(f)+l} y\) (5.6) has a crossing.
Consider \(f: X\to Y\), \(x\in Z_\infty ^{s,t}(X)\) and \(y\in Z_\infty ^{s+n,t+n}(Y)\). Then
implies that
Consider \(f: X\to Y\), \(x\in Z_\infty ^{s,t}(X)\) and \(y\in Z_\infty ^{s+n,t+n}(Y)\). Then
implies that
Suppose we have an \((f,E_r)\)-extension of level \(l'\),
Then either
there is an essential \((f,E_r)\)-extension of level \(l\), \(d_m^{f,E_r,l}(x) = z\), for some \(m {\lt} n\), or
we have \(d_n^{f,E_r,l}(x) = y + z\) for some \(z\) lying in the indeterminacy of \(d_n^{f,E_r,l'}\).
If an \((f,E_r)\)-extension of level \(l\), \(d_n^{f,E_r,l}(x)=y\), has a crossing, then there is an essential \((f,E_r)\)-extension of level \(0\), \(d_m^{f,E_r,0}(x')=z'\), such that the implied extension at level \(a+l\) satisfies the degree conditions of a crossing.
If an \((f,E_r)\)-extension of level \(l\), \(d_n^{f,E_r,l}(x)=y\), has no crossing, then the induced extension at any level \(l' {\gt} l\) also has no crossing.