Filtered operators on two-term pages

A filtered operator of degree d shifts G p into G (p - d) and commutes with the two-term differential. This file constructs its maps on the concrete source and target pages, proves compatibility with drop, and proves that an operator is unchanged on pages after adding one that shifts an additional filtration level.

structure AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] (K : FilteredTwoTerm k M) (d : ℤ) : Type v

A k-linear operator of filtration degree d commuting with the two-term differential.

• g : M →ₗ[k] M

  The underlying endomorphism of the filtered module.

• commute : K.f ∘ₗ self.g = self.g ∘ₗ K.f
• shift (p : ℤ) (x : M) : x ∈ K.G p → self.g x ∈ K.G (p - d)

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.comp {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) : K.PageOperator (d + e)

Composition of filtered operators.

Equations

• P.comp Q = { g := P.g ∘ₗ Q.g, commute := ⋯, shift := ⋯ }

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.reverseComp {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) : K.PageOperator (d + e)

The reverse-order composition, given the same canonical sum degree.

Equations

• P.reverseComp Q = { g := Q.g ∘ₗ P.g, commute := ⋯, shift := ⋯ }

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.commute_apply {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} {d : ℤ} (P : K.PageOperator d) (x : M) : K.f (P.g x) = P.g (K.f x)

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.sourceRestricted {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.cycles r p) →ₗ[k] ↥(K.cycles r (p - d))

The restriction of the operator to a source-page cycle numerator.

Equations

• P.sourceRestricted r p = LinearMap.codRestrict (K.cycles r (p - d)) (P.g ∘ₗ (K.cycles r p).subtype) ⋯

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.sourceMap {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.SourcePage r p →ₗ[k] K.SourcePage r (p - d)

The operator induced on a source page.

Equations

• P.sourceMap r p = (Submodule.comap (K.cycles r p).subtype (K.G (p + 1))).mapQ (Submodule.comap (K.cycles r (p - d)).subtype (K.G (p - d + 1))) (P.sourceRestricted r p) ⋯

@[simp]

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.sourceMap_mk {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.cycles r p)) : (P.sourceMap r p) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((P.sourceRestricted r p) x)

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.sourcePageCast {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} (r : ℕ) {p q : ℤ} (h : p = q) : K.SourcePage r p ≃ₗ[k] K.SourcePage r q

Transport between equal source-page indices.

Equations

• AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.sourcePageCast r h = h ▸ LinearEquiv.refl k (K.SourcePage r p)

@[simp]

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.sourcePageCast_mk {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} (r : ℕ) {p q : ℤ} (h : p = q) (x : ↥(K.cycles r p)) : (sourcePageCast r h) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (h ▸ x)

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.targetRestricted {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} {d : ℤ} (P : K.PageOperator d) (p : ℤ) : ↥(K.G p) →ₗ[k] ↥(K.G (p - d))

The restriction of the operator to a target-page filtration piece.

Equations

• P.targetRestricted p = LinearMap.codRestrict (K.G (p - d)) (P.g ∘ₗ (K.G p).subtype) ⋯

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.targetMap {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.TargetPage r p →ₗ[k] K.TargetPage r (p - d)

The operator induced on a target page.

Equations

• P.targetMap r p = (Submodule.comap (K.G p).subtype (K.boundaries r p)).mapQ (Submodule.comap (K.G (p - d)).subtype (K.boundaries r (p - d))) (P.targetRestricted p) ⋯

@[simp]

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.targetMap_mk {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.G p)) : (P.targetMap r p) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((P.targetRestricted p) x)

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.targetPageCast {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} (r : ℕ) {p q : ℤ} (h : p = q) : K.TargetPage r p ≃ₗ[k] K.TargetPage r q

Transport between target-page indices known to be equal.

Equations

• AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.targetPageCast r h = h ▸ LinearEquiv.refl k (K.TargetPage r p)

@[simp]

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.targetPageCast_mk {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} (r : ℕ) {p q : ℤ} (h : p = q) (x : ↥(K.G p)) : (targetPageCast r h) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (h ▸ x)

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.targetRestrictedAtDrop {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.G (p + ↑r)) →ₗ[k] ↥(K.G (p - d + ↑r))

Restrict the operator to the target filtration at a page differential.

Equations

• P.targetRestrictedAtDrop r p = LinearMap.codRestrict (K.G (p - d + ↑r)) (P.g ∘ₗ (K.G (p + ↑r)).subtype) ⋯

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.targetMapAtDrop {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.TargetPage r (p + ↑r) →ₗ[k] K.TargetPage r (p - d + ↑r)

The target-page operator at the codomain index of drop, reindexed by the identity (p+r)-d = (p-d)+r.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.targetMapAtDrop_mk {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.G (p + ↑r))) : (P.targetMapAtDrop r p) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((P.targetRestrictedAtDrop r p) x)

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.targetMapAtDrop_eq_cast_targetMap {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} {d : ℤ} (P : K.PageOperator d) (r : ℕ) (p : ℤ) : P.targetMapAtDrop r p = ↑(targetPageCast r ⋯) ∘ₗ P.targetMap r (p + ↑r)

targetMapAtDrop is the general target-page map followed by the canonical reindexing isomorphism.

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.targetMapAtDrop_drop {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.targetMapAtDrop r p) ((K.drop r p) x) = (K.drop r (p - d)) ((P.sourceMap r p) x)

The source and reindexed target operator maps commute with the page differential.

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.targetMap_drop {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) : (targetPageCast r ⋯) ((P.targetMap r (p + ↑r)) ((K.drop r p) x)) = (K.drop r (p - d)) ((P.sourceMap r p) x)

Compatibility of the general source and target page maps with drop, with the unavoidable target-index transport made explicit.

def AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.SameSymbol {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} {d : ℤ} (P Q : K.PageOperator d) : Prop

Two degree-d operators have the same symbol when their difference shifts one additional filtration level.

Equations

• P.SameSymbol Q = ∀ (p : ℤ), ∀ x ∈ K.G p, (P.g - Q.g) x ∈ K.G (p - d + 1)

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.sourceMap_eq_of_sameSymbol {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} {d : ℤ} (P : K.PageOperator d) {Q : K.PageOperator d} (hPQ : P.SameSymbol Q) (r : ℕ) (p : ℤ) : P.sourceMap r p = Q.sourceMap r p

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.targetMap_eq_of_sameSymbol {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} {d : ℤ} (P : K.PageOperator d) {Q : K.PageOperator d} (hPQ : P.SameSymbol Q) (r : ℕ) (p : ℤ) : P.targetMap r p = Q.targetMap r p

theorem AlgebraicAnalysis.FilteredTwoTermPages.FilteredTwoTerm.PageOperator.targetMapAtDrop_eq_of_sameSymbol {k : Type u} [Ring k] {M : Type v} [AddCommGroup M] [Module k M] {K : FilteredTwoTerm k M} {d : ℤ} (P : K.PageOperator d) {Q : K.PageOperator d} (hPQ : P.SameSymbol Q) (r : ℕ) (p : ℤ) : P.targetMapAtDrop r p = Q.targetMapAtDrop r p