Naturality of the target boundary maps

The quotient maps from page one to later target pages commute with every filtered operator.

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

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.totalBoundaryMap_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.totalBoundaryMap r ∘ₗ P.targetTotalMap 1 = P.targetTotalMap (r + 1) ∘ₗ K.totalBoundaryMap r