- 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)
When \(d_r^{\delta _n}(x) = \lambda ^{r-n-1}y\) has no crossing, then \(d_r^{\delta _n}(\lambda ^a x) = \lambda ^{a+r-n-1}y\) also has no crossing.
For the convenience of readers to check gradings, whenever we write
for \(f: \Sigma ^{m,w} \nu X\to \nu Y\), \(x\in E_\infty ^{s_1,t_1,w_1}(\nu X)\) and \(y\in E_\infty ^{s_2,t_2,w_2}(\nu Y)\), the following conditions must hold:
The crossing defined here is opposite to crossings in Moss’s theorem.
For \(x,y,\delta \) in Proposition 4.5 we always have
if \(0\le a\le n\) and \(0\le a+r-n-1{\lt}m-n\) (the differential is trivial if \(a\) exceeds this range).
Suppose \(r\ge n+1\) and \(d_r(x)=y\), where
A crossing of \(d_r(x)=y\) on the \(E_{n+1}\)-page refers to an essential Adams differential
where
with \(0{\lt}a\le n-1\) and \(0\le b\le r-n-1\). See Figure 1.
From Definition 4.9, it immediately follows that there are no crossings of any differential on the \(E_2\)-page, as this would require \(0{\lt} a \le n-1 = 0\). According to Proposition 4.11, this reflects the fact that \(\delta _1\)-extensions have no crossings for degree reasons.
There are certain special maps between synthetic spectra that we want to consider. For any \(n{\lt}m\le \infty \) and a spectrum \(X\), we have the following distinguished triangles of \(\mathrm{H}{\mathbb F}_2\)-synthetic spectra
We simply write \(\rho =\rho _{n,m}\), \(\delta =\delta _{n,m}\) by abuse of notation if \(n,m\) is understood in the context. When \(m=\infty \), this sequence is interpreted as
Let \(X \in \mathcal{S}^{\mathrm{fin}}\) be a finite spectrum. The synthetic Adams spectral sequence for \(\nu X\) is isomorphic to the \(\lambda \)-Bockstein spectral sequence:
\(E_2^{s,t}(X) \cong \pi _{t-s,t}(\nu X / \lambda )\).
If there is a classical Adams differential \(d_r x = y\) for \(x \in E_2^{s,t}(X) \cong \pi _{t-s,t}(\nu X / \lambda )\), then \(x\) admits a lift to \(\pi _{t-s,t}(\nu X / \lambda ^{r-1})\) whose image under the Bockstein \(\nu X / \lambda ^{r-1} \to \Sigma ^{1,-r+1} \nu X / \lambda \) equals \(d_r(x)\).
axiom lambda_bockstein_iso (X : 𝒮) :
(SynAdamsSS Syn ((nu 𝒮 Syn).obj X)).r₀ = 2
Consider a homotopy commutative diagram of converging spectral sequences \(V_1 \xrightarrow {p} V_3 \xrightarrow {g} V_4\) with \(q = g \circ p\). If \(d_m^p(x) = z\) and \(d_l^g(z) = w\) has no crossing, then \(d_{m+l}^q(x) = w\).
axiom ess_composition {ω : Type w} [AddCommGroup ω] [DecidableEq ω]
{E₁ E₂ E₃ : SpectralSequence C ω} {ω' : Type w}
{A₁ A₂ A₃ : ω' → C}
{F₁ : Filtration A₁} {F₂ : Filtration A₂} {F₃ : Filtration A₃}
{conv₁ : Convergence E₁ A₁ F₁}
{conv₂ : Convergence E₂ A₂ F₂}
{conv₃ : Convergence E₃ A₃ F₃}
(cm₁₂ : ConvergenceMorphism conv₁ conv₂)
(cm₂₃ : ConvergenceMorphism conv₂ conv₃)
(ess₁₂ : ExtensionSS cm₁₂) (ess₂₃ : ExtensionSS cm₂₃) :
True
If \(g \circ f = 0\) (as morphisms of converging spectral sequences) and \(d_n^f(x) = y\), then \(y\) is a permanent cycle in the \(g\)-ESS: \(d_m^g(y) = 0\) for all \(m \ge 0\).
axiom ess_composition_zero {ω : Type w} [AddCommGroup ω] [DecidableEq ω]
{E₁ E₂ E₃ : SpectralSequence C ω} {ω' : Type w}
{A₁ A₂ A₃ : ω' → C}
{F₁ : Filtration A₁} {F₂ : Filtration A₂} {F₃ : Filtration A₃}
{conv₁ : Convergence E₁ A₁ F₁}
{conv₂ : Convergence E₂ A₂ F₂}
{conv₃ : Convergence E₃ A₃ F₃}
(cm₁₂ : ConvergenceMorphism conv₁ conv₂)
(cm₂₃ : ConvergenceMorphism conv₂ conv₃)
(hzero : ∀ k', cm₁₂.aMap k' ≫ cm₂₃.aMap k' = 0) :
True
Consider a homotopy commutative diagram of converging spectral sequences \(V_1 \xrightarrow {f} V_2 \xrightarrow {q} V_3\) with \(p = q \circ f\). If \(d_n^f(x) = y\), \(d_m^p(x) = z\), and one of the two extensions has no crossing, then \(d_{m-n}^q(y) = z\).
axiom essCommutativity_triangle {ω : Type w} [AddCommGroup ω] [DecidableEq ω]
{E₁ E₂ E₃ : SpectralSequence C ω} {ω' : Type w}
{A₁ A₂ A₃ : ω' → C}
{F₁ : Filtration A₁} {F₂ : Filtration A₂} {F₃ : Filtration A₃}
{conv₁ : Convergence E₁ A₁ F₁} {conv₂ : Convergence E₂ A₂ F₂}
{conv₃ : Convergence E₃ A₃ F₃}
(cmf : ConvergenceMorphism conv₁ conv₂)
(cmp : ConvergenceMorphism conv₁ conv₃)
(cmq : ConvergenceMorphism conv₂ conv₃)
(essf : ExtensionSS cmf) (essp : ExtensionSS cmp) (essq : ExtensionSS cmq)
(_abutment_comm : ∀ (k' : ω'), cmf.aMap k' ≫ cmq.aMap k' = cmp.aMap k')
(_eInfty_comm : ∀ (k : ω), cmf.eMap k ≫ cmq.eMap k = cmp.eMap k)
(n m : ℤ) (kx ky kz : ω)
(_hn : 0 ≤ n) (_hm : 0 ≤ m) (_hmn : n ≤ m)
(_hf_rel : ESSRelation essf n kx ky)
(_hp_rel : ESSRelation essp m kx kz)
(ddf : DifferentialDatum C ω)
(_hddf : ddf.E = E₁ ∧ ddf.r = n ∧ ddf.k = kx)
(ddp : DifferentialDatum C ω)
(_hddp : ddp.E = E₁ ∧ ddp.r = m ∧ ddp.k = kx)
(_hf_or_p_nc : NoCrossing ddf ∨ NoCrossing ddp) :
ESSRelation essq (m - n) ky kz
The \(f\)-extension spectral sequence (\(f\)-ESS) is the spectral sequence
obtained by applying the filtered complex construction (Theorem 0.25) to the underlying filtered chain complex of Definition 0.34. By Theorem 0.26, if the filtrations on \(A_1\) and \(A_2\) are exhaustive and Hausdorff (which holds when they are bounded), then the \(f\)-ESS converges to the homology of the underlying complex, i.e., to \(\ker (f_A) \oplus \mathrm{coker}(f_A)\).
structure ExtensionSS {ω : Type w} [AddCommGroup ω] [DecidableEq ω]
{E₁ E₂ : SpectralSequence C ω} {ω' : Type w}
{A₁ A₂ : ω' → C} {F₁ : Filtration A₁} {F₂ : Filtration A₂}
{conv₁ : Convergence E₁ A₁ F₁} {conv₂ : Convergence E₂ A₂ F₂}
(cm : ConvergenceMorphism conv₁ conv₂) where
/-- The ESS differential at page n from bidegree k₁ to k₂ -/
essDiff : ℤ → ω → ω → C
/-- The ESS boundary group at page n, bidegree k -/
essBoundary : ℤ → ω → C
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
axiom einfty_nuX_mod_lambda (X : 𝒮) (r : ℕ) (hr : 0 < r)
(s t w : ℤ) (h : t - w < 0 ∨ (r : ℤ) ≤ t - w) :
IsZero ((SynAdamsSS Syn (XModLambdaN ((nu 𝒮 Syn).obj X) r)).Page 2
(s, t, w))
Let \(X \in \mathcal{S}^{\mathrm{fin}}\) be a finite spectrum. The \(E_\infty \)-page of the synthetic Adams spectral sequence for \(\nu X\) is
theorem einfty_nuX (X : 𝒮) (s t w : ℤ) (htw : t < w) :
IsZero ((SynAdamsEInfty 𝒮 Syn X).EInfty (s, t, w)) := by
...
The Adams differential \(d_r(x)=y\) has a crossing on the \(E_{n+1}\)-page if and only if the corresponding \(\delta _n\)-extension
for
has a crossing.
Suppose in the classical Adams spectral sequence of \(X\) we have \(d_r(x)=y\), where \(x\in Z_{r-1}^{s,t}(X)\) and \(y\in Z_\infty ^{s+r,t+r-1}(X)\). Consider the map
If \(r\ge n+1\), then we view \(x\) as an element of
\[ E_\infty ^{s,t,t}(\nu X/\lambda ^n)\cong Z_n^{s,t}(X), \]and \(\lambda ^{r-n-1} y\) as an element of
\[ E_\infty ^{s+r,t+r-1, t+n}(\nu X/\lambda ^{m-n})\cong Z_{m-r+1}^{s+r,t+r-1}(X)/B_{r-n}^{s+r,t+r-1}(X). \]We then have
\[ d^{\delta }_r(x)=\lambda ^{r-n-1}y, \]which is trivial if \(r{\gt}m\).
If \(r{\lt}n+1\), then we view \(\lambda ^{n+1-r}x\) as an element of
\[ E_\infty ^{s,t,t-n-1+r}(\nu X/\lambda ^n)\cong Z^{s,t}_{r-1}(X)/B^{s,t}_{n+2-r}(X), \]and \(y\) as an element of
\[ E_\infty ^{s+r,t+r-1, t+r-1}(\nu X)\cong Z_\infty ^{s+r,t+r-1}(X). \]In this case, we have
\[ d^{\delta }_r(\lambda ^{n+1-r}x)=y. \]
The only nonzero differentials in the extension spectral sequences for the maps \(\lambda ^n\) and \(\rho \) from Notation 4.1 are the \(d_0\)’s:
As a result, these \(d_0\)’s have no crossings.
As indicated in the proof, the right-hand side of equation (4.4) (considered as a subset of \(Z_\infty ^{s+r,t+r-1}(X)\)) is a coset of
which is the same as the value of the classical Adams differential \(d_r(x)=y\). This implies that the equation (4.4) holds and is essential if and only if \(d_r(x)=y\) holds and is essential. Therefore the \(\delta \)-ESS encodes the same information as the classical Adams spectral sequence.