Successor equivalences for the filtered two-term pages

This file proves, from the concrete representative definitions in FilteredTwoTermPages, that the next source page is the kernel of the page differential and that the next target page is its cokernel.

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.sourceSuccInclusion {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] ↥(K.cycles r p)

Include cycles surviving the next page into the current cycle numerator.

Equations

• K.sourceSuccInclusion r p = Submodule.inclusion ⋯

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

The map from the next source page to the current source page.

Equations

• K.sourceSuccMap r p = (Submodule.comap (K.cycles (r + 1) p).subtype (K.G (p + 1))).mapQ (Submodule.comap (K.cycles r p).subtype (K.G (p + 1))) (K.sourceSuccInclusion r p) ⋯

@[simp]

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

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

The canonical map from the next source page into the kernel of d_r.

Equations

• K.sourceSuccKernelMap r p = LinearMap.codRestrict (K.drop r p).ker (K.sourceSuccMap r p) ⋯

noncomputable def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.sourceSuccEquivKerDrop {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) : K.SourcePage (r + 1) p ≃ₗ[k] ↥(K.drop r p).ker

On the source, the next page is the kernel of the current page differential.

Equations

• K.sourceSuccEquivKerDrop r p = LinearEquiv.ofBijective (K.sourceSuccKernelMap r p) ⋯

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

The quotient map from a target page to its successor page.

Equations

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

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

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.ker_targetSuccMap_eq_range_drop {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) : (K.targetSuccMap r (p + ↑r)).ker = (K.drop r p).range

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

The map from the cokernel of d_r to the next target page.

Equations

• K.targetCokernelMap r p = (K.drop r p).range.liftQ (K.targetSuccMap r (p + ↑r)) ⋯

noncomputable def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.targetSuccEquivCokerDrop {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) : K.TargetPage (r + 1) (p + ↑r) ≃ₗ[k] K.TargetPage r (p + ↑r) ⧸ (K.drop r p).range

On the target, the next page is the cokernel of the current page differential.

Equations

• K.targetSuccEquivCokerDrop r p = (LinearEquiv.ofBijective (K.targetCokernelMap r p) ⋯).symm