Complex shapes for pages of spectral sequences

In this file, we define complex shapes which correspond to pages of spectral sequences:

• ComplexShape.spectralSequenceNat: for any u : ℤ × ℤ, this is the complex shape on ℕ × ℕ corresponding to differentials of ComplexShape.up' u : ComplexShape (ℤ × ℤ) with source and target in ℕ × ℕ. (With u := (r, 1 - r), this will apply to the rth-page of first quadrant E₂ cohomological spectral sequence).
• ComplexShape.spectralSequenceFin: for any u : ℤ × ℤ and l : ℕ, this is a similar definition as ComplexShape.spectralSequenceNat but for ℤ × Fin l (identified as a subset of ℤ × ℤ). (This could be used for spectral sequences associated to a finite filtration.)

def ComplexShape.spectralSequenceNat (u : ℤ × ℤ) : ComplexShape (ℕ × ℕ)

For u : ℤ × ℤ, this is the complex shape on ℕ × ℕ, which connects a to b when the equality a + u = b holds in ℤ × ℤ.

Equations

• ComplexShape.spectralSequenceNat u = { Rel := fun (a b : ℕ × ℕ) => ↑a.fst + u.fst = ↑b.fst ∧ ↑a.snd + u.snd = ↑b.snd, next_eq := ⋯, prev_eq := ⋯ }

@[simp]

theorem ComplexShape.spectralSequenceNat_rel_iff (u : ℤ × ℤ) (a b : ℕ × ℕ) : (spectralSequenceNat u).Rel a b ↔ ↑a.fst + u.fst = ↑b.fst ∧ ↑a.snd + u.snd = ↑b.snd

def ComplexShape.spectralSequenceFin (l : ℕ) (u : ℤ × ℤ) : ComplexShape (ℤ × Fin l)

For l : ℕ and u : ℤ × ℤ, this is the complex shape on ℤ × Fin l, which connects a to b when the equality a + u = b holds in ℤ × ℤ.

Equations

• ComplexShape.spectralSequenceFin l u = { Rel := fun (a b : ℤ × Fin l) => a.fst + u.fst = b.fst ∧ ↑↑a.snd + u.snd = ↑↑b.snd, next_eq := ⋯, prev_eq := ⋯ }

@[simp]

theorem ComplexShape.spectralSequenceFin_rel_iff {l : ℕ} (u : ℤ × ℤ) (a b : ℤ × Fin l) : (spectralSequenceFin l u).Rel a b ↔ a.fst + u.fst = b.fst ∧ ↑↑a.snd + u.snd = ↑↑b.snd