Boundary exhaustion on the total target pages

The concrete boundary inclusions give maps from the first target page to every later target page. Surjectivity of the underlying differential and exhaustive filtration imply pointwise eventual vanishing; finite support then gives the same statement on the external direct sum.

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

The quotient map induced by B₁ ⊆ B_{r+1} at one target component.

Equations

• K.targetBoundaryMap r p = (Submodule.comap (K.G p).subtype (K.boundaries 1 p)).mapQ (Submodule.comap (K.G p).subtype (K.boundaries (r + 1) p)) LinearMap.id ⋯

@[simp]

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

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.targetBoundaryMap_surjective {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) : Function.Surjective ⇑(K.targetBoundaryMap r p)

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.targetBoundaryMap_ker_mono {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r s : ℕ) (hrs : r ≤ s) (p : ℤ) : (K.targetBoundaryMap r p).ker ≤ (K.targetBoundaryMap s p).ker

The component kernels grow with the page index.

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.totalBoundaryMap {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) : K.TargetTotal 1 →ₗ[k] K.TargetTotal (r + 1)

The total target map into page r+1.

Equations

• K.totalBoundaryMap r = DirectSum.lmap (K.targetBoundaryMap r)

@[simp]

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.totalBoundaryMap_lof {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) (x : K.TargetPage 1 p) : (K.totalBoundaryMap r) ((DirectSum.lof k ℤ (fun (q : ℤ) => K.TargetPage 1 q) p) x) = (DirectSum.lof k ℤ (fun (q : ℤ) => K.TargetPage (r + 1) q) p) ((K.targetBoundaryMap r p) x)

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.totalBoundaryMap_surjective {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) : Function.Surjective ⇑(K.totalBoundaryMap r)

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.totalBoundaryMap_ker_mono {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r s : ℕ) (hrs : r ≤ s) : (K.totalBoundaryMap r).ker ≤ (K.totalBoundaryMap s).ker

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.totalBoundaryMap_eventually_zero {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) (x : K.TargetTotal 1) : ∃ (r : ℕ), (K.totalBoundaryMap r) x = 0

Every finitely supported total target vector is killed at some page.