Total direct-sum actions on filtered two-term pages

This file packages the source and target page actions of a filtered operator into maps on the total direct sums. The index shift is part of the map: an operator of degree d sends the summand at p to the summand at p - d.

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.sourceTotalMap {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} {d : ℤ} (P : K.PageOperator d) (r : ℕ) : K.SourceTotal r →ₗ[k] K.SourceTotal r

The source-page action on the total direct sum.

Equations

• P.sourceTotalMap r = DirectSum.toModule k ℤ (K.SourceTotal r) fun (p : ℤ) => DirectSum.lof k ℤ (fun (q : ℤ) => K.SourcePage r q) (p - d) ∘ₗ P.sourceMap r p

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.targetTotalMap {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} {d : ℤ} (P : K.PageOperator d) (r : ℕ) : K.TargetTotal r →ₗ[k] K.TargetTotal r

The target-page action on the total direct sum.

Equations

• P.targetTotalMap r = DirectSum.toModule k ℤ (K.TargetTotal r) fun (p : ℤ) => DirectSum.lof k ℤ (fun (q : ℤ) => K.TargetPage r q) (p - d) ∘ₗ P.targetMap r p

@[simp]

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.sourceTotalMap_lof {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} {d : ℤ} (P : K.PageOperator d) (r : ℕ) (p : ℤ) (x : K.SourcePage r p) : (P.sourceTotalMap r) ((DirectSum.lof k ℤ (fun (q : ℤ) => K.SourcePage r q) p) x) = (DirectSum.lof k ℤ (fun (q : ℤ) => K.SourcePage r q) (p - d)) ((P.sourceMap r p) x)

@[simp]

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.targetTotalMap_lof {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} {d : ℤ} (P : K.PageOperator d) (r : ℕ) (p : ℤ) (x : K.TargetPage r p) : (P.targetTotalMap r) ((DirectSum.lof k ℤ (fun (q : ℤ) => K.TargetPage r q) p) x) = (DirectSum.lof k ℤ (fun (q : ℤ) => K.TargetPage r q) (p - d)) ((P.targetMap r p) x)

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

The total action intertwines the total page differential.

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.sourceTotalMap_commute_of_commutator_lowers {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} {d : ℤ} (P : K.PageOperator d) {e : ℤ} (Q : K.PageOperator e) (hlower : ∀ (p : ℤ), ∀ z ∈ K.G p, P.g (Q.g z) - Q.g (P.g z) ∈ K.G (p - d - e + 1)) (r : ℕ) : Commute (P.sourceTotalMap r) (Q.sourceTotalMap r)

Lower-order commutators vanish in the total source symbol action.

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.targetTotalMap_commute_of_commutator_lowers {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} {d : ℤ} (P : K.PageOperator d) {e : ℤ} (Q : K.PageOperator e) (hlower : ∀ (p : ℤ), ∀ z ∈ K.G p, P.g (Q.g z) - Q.g (P.g z) ∈ K.G (p - d - e + 1)) (r : ℕ) : Commute (P.targetTotalMap r) (Q.targetTotalMap r)

Lower-order commutators vanish in the total target symbol action.