Pages of a filtered two-term complex

This file constructs the Z_r and B_r subquotients for a two-term filtered complex. The page differential is induced by the original differential on representatives; no successor-page equivalence is part of the input.

We use a decreasing, integer-indexed filtration G, as obtained from an increasing filtration F by G p = F (-p).

structure AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm (k : Type u) (M : Type v) [Ring k] [AddCommGroup M] [Module k M] : Type v

A filtration-preserving two-term complex M --f--> M.

• G : ℤ → Submodule k M

  The decreasing filtration on the underlying module.

• antitone : Antitone self.G
• f : M →ₗ[k] M

  The differential of the two-term complex.

• map_le (p : ℤ) : Submodule.map self.f (self.G p) ≤ self.G p

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.cycles {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) : Submodule k M

The numerator of Z_r in the source.

Equations

• K.cycles r p = K.G p ⊓ Submodule.comap K.f (K.G (p + ↑r))

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.boundaries {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) : Submodule k M

The numerator of B_r in the target.

Equations

• K.boundaries r p = K.G p ⊓ Submodule.map K.f (K.G (p - ↑r + 1)) ⊔ K.G (p + 1)

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.next_le {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (p : ℤ) : K.G (p + 1) ≤ K.G p

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.boundaries_le {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) : K.boundaries r p ≤ K.G p

@[reducible, inline]

abbrev AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.SourcePage {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) : Type v

The actual source page. Using the intersection numerator gives the canonical model (G^p ∩ f⁻¹G^{p+r}) / (G^{p+1} ∩ f⁻¹G^{p+r}), equivalent to the displayed (intersection + G^{p+1})/G^{p+1} formula.

Equations

• K.SourcePage r p = (↥(K.cycles r p) ⧸ Submodule.comap (K.cycles r p).subtype (K.G (p + 1)))

@[reducible, inline]

abbrev AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.TargetPage {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) : Type v

The actual target page G^p/B_r.

Equations

• K.TargetPage r p = (↥(K.G p) ⧸ Submodule.comap (K.G p).subtype (K.boundaries r p))

@[instance_reducible]

instance AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.sourcePageAddCommGroup {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) : AddCommGroup (K.SourcePage r p)

Equations

• K.sourcePageAddCommGroup r p = { toAddGroup := (Submodule.Quotient.addCommGroup (Submodule.comap (K.cycles r p).subtype (K.G (p + 1)))).toAddGroup, add_comm := ⋯ }

@[instance_reducible]

instance AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.targetPageAddCommGroup {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) : AddCommGroup (K.TargetPage r p)

Equations

• K.targetPageAddCommGroup r p = { toAddGroup := (Submodule.Quotient.addCommGroup (Submodule.comap (K.G p).subtype (K.boundaries r p))).toAddGroup, add_comm := ⋯ }

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.restrictedDrop {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) : ↥(K.cycles r p) →ₗ[k] ↥(K.G (p + ↑r))

Apply the filtered differential to a cycle representative.

Equations

• K.restrictedDrop r p = LinearMap.codRestrict (K.G (p + ↑r)) (K.f ∘ₗ (K.cycles r p).subtype) ⋯

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.drop {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) : K.SourcePage r p →ₗ[k] K.TargetPage r (p + ↑r)

The page differential, formed by applying f to a representative.

Equations

• K.drop r p = (Submodule.comap (K.cycles r p).subtype (K.G (p + 1))).mapQ (Submodule.comap (K.G (p + ↑r)).subtype (K.boundaries r (p + ↑r))) (K.restrictedDrop r p) ⋯

@[simp]

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.drop_mk {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) (x : ↥(K.cycles r p)) : (K.drop r p) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((K.restrictedDrop r p) x)

Representative formula for the page differential.

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.cycles_succ_le {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) : K.cycles (r + 1) p ≤ K.cycles r p

Cycle numerators decrease from page r to page r+1.

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.boundaries_le_succ {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) : K.boundaries r p ≤ K.boundaries (r + 1) p

Boundary numerators increase from page r to page r+1.

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.drop_mk_eq_zero_of_mem_cycles_succ {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) (x : ↥(K.cycles r p)) (hx : ↑x ∈ K.cycles (r + 1) p) : (K.drop r p) (Submodule.Quotient.mk x) = 0

A representative in Z_{r+1} is killed by the r-page differential.

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.exists_cycles_succ_rep_of_drop_mk_eq_zero {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) (x : ↥(K.cycles r p)) (hx : (K.drop r p) (Submodule.Quotient.mk x) = 0) : ∃ z ∈ K.G (p + 1), ↑x - z ∈ K.cycles (r + 1) p

Conversely, a representative killed by d_r can be changed by an element of G^{p+1} to a representative in Z_{r+1}.

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.mem_boundaries_succ_rep {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) {y : M} (hy : y ∈ K.boundaries (r + 1) p) : ∃ z ∈ K.G (p - ↑r), ∃ e ∈ K.G (p + 1), y = K.f z + e

Every new boundary representative is a drop plus a lower-filtration term.

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.exists_mem_boundaries_of_surjective {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (hG : ∀ (z : M), ∃ (s : ℤ), z ∈ K.G s) (hf : Function.Surjective ⇑K.f) {p : ℤ} {y : M} (hy : y ∈ K.G p) : ∃ (r : ℕ), y ∈ K.boundaries r p

Surjectivity exhausts the target boundary numerators.