Naturality of the total successor maps

The concrete successor maps on the source and target pages commute with the page action. The proof is by direct-sum induction and quotient representatives; no abstract successor-page interface is used.

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.sourceTotalSuccMap_naturality {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} {d : ℤ} (P : K.PageOperator d) (r : ℕ) : K.sourceTotalSuccMap r ∘ₗ P.sourceTotalMap (r + 1) = P.sourceTotalMap r ∘ₗ K.sourceTotalSuccMap r

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.targetTotalSuccMap_naturality {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} {d : ℤ} (P : K.PageOperator d) (r : ℕ) : K.targetTotalSuccMap r ∘ₗ P.targetTotalMap r = P.targetTotalMap (r + 1) ∘ₗ K.targetTotalSuccMap r