Total direct sums of the filtered two-term pages

The page differential has target component indexed by p + r. This file packages the component maps into one direct-sum map; no successor-page interface is assumed here.

@[reducible, inline]

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

The direct sum of the source pages at page r.

Equations

• K.SourceTotal r = DirectSum ℤ fun (p : ℤ) => K.SourcePage r p

@[reducible, inline]

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

The direct sum of the target pages at page r.

Equations

• K.TargetTotal r = DirectSum ℤ fun (p : ℤ) => K.TargetPage r p

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

The total page differential, with the component at p landing at p+r.

The reindexing is expressed by the corresponding direct-sum inclusion, so the formula keeps the target shift visible at the definition site.

Equations

• K.totalDrop r = DirectSum.toModule k ℤ (K.TargetTotal r) fun (p : ℤ) => DirectSum.lof k ℤ (fun (q : ℤ) => K.TargetPage r q) (p + ↑r) ∘ₗ K.drop r p

@[simp]

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.totalDrop_lof {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) (p : ℤ) (x : K.SourcePage r p) : (K.totalDrop r) ((DirectSum.lof k ℤ (fun (q : ℤ) => K.SourcePage r q) p) x) = (DirectSum.lof k ℤ (fun (q : ℤ) => K.TargetPage r q) (p + ↑r)) ((K.drop r p) x)

Component formula for the total differential.

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.totalDrop_lof_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.totalDrop r) ((DirectSum.lof k ℤ (fun (q : ℤ) => K.SourcePage r q) p) (Submodule.Quotient.mk x)) = (DirectSum.lof k ℤ (fun (q : ℤ) => K.TargetPage r q) (p + ↑r)) ((K.drop r p) (Submodule.Quotient.mk x))

Representative formula for a source-page quotient representative.

This compatibility lemma intentionally retains the quotient representative on the right-hand side, although the simplifier can reduce it further.

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

The componentwise successor map on the total source page.

Equations

• K.sourceTotalSuccMap r = DirectSum.lmap fun (p : ℤ) => (K.drop r p).ker.subtype ∘ₗ ↑(K.sourceSuccEquivKerDrop r p)

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

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.range_totalSourceSuccMap {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) : (K.sourceTotalSuccMap r).range = (K.totalDrop r).ker

noncomputable def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.sourceTotalSuccEquivKerDrop {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) : K.SourceTotal (r + 1) ≃ₗ[k] ↥(K.totalDrop r).ker

The total successor source is the actual kernel of the total differential.

Equations

• K.sourceTotalSuccEquivKerDrop r = (LinearEquiv.ofInjective (K.sourceTotalSuccMap r) ⋯).trans (LinearEquiv.ofEq (K.sourceTotalSuccMap r).range (K.totalDrop r).ker ⋯)

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

The componentwise quotient map on the total target page.

Equations

• K.targetTotalSuccMap r = DirectSum.lmap (K.targetSuccMap r)

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.ker_totalTargetSuccMap {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) : (K.targetTotalSuccMap r).ker = (K.totalDrop r).range

noncomputable def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.targetTotalSuccEquivCokerDrop {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (r : ℕ) : K.TargetTotal (r + 1) ≃ₗ[k] K.TargetTotal r ⧸ (K.totalDrop r).range

The total successor target is the actual cokernel of the total differential.

Equations

• K.targetTotalSuccEquivCokerDrop r = (((K.totalDrop r).range.quotEquivOfEq (K.targetTotalSuccMap r).ker ⋯).trans ((K.targetTotalSuccMap r).quotKerEquivOfSurjective ⋯)).symm