Naturality of the spectral object of a filtered complex on graded pieces

A natural transformation α : F ⟶ G of functors ι ⥤ CochainComplex C ℤ induces a morphism of spectral objects CochainComplex.spectralObjectMap α (in TauCeti.Algebra.Homology.SpectralSequence.Filtered.SpectralObject), which on H^n(f) is the map in cohomology of the induced morphism of mapping cones. When F.map f and G.map f are monomorphisms, for instance for a morphism of filtrations, it is the map in cohomology of the induced morphism of cokernels, that is, of graded pieces (CochainComplex.spectralObjectMap_hom_app_spectralObjectHIsoCokernel_hom).

A morphism of complexes f : K ⟶ L sending each piece F n of an increasing filtration of K into the piece G n of an increasing filtration of L induces a morphism of their functors CochainComplex.filtrationFunctorMap f hf : filtrationFunctor F hF ⟶ filtrationFunctor G hG, compatibly with identities and composition, and hence, through spectralObjectMap, a morphism of their spectral sequences.

Main definitions

• CochainComplex.filtrationFunctorMap: the morphism of filtration functors induced by a morphism of filtered complexes.

Main results

• CochainComplex.spectralObjectMap_hom_app_spectralObjectHIsoCokernel_hom: on graded pieces, the morphism of spectral objects is the map in cohomology of the morphism of cokernels.
• CochainComplex.filtrationFunctorMap_id, CochainComplex.filtrationFunctorMap_comp: functoriality of filtrationFunctorMap.

theorem CochainComplex.spectralObjectMap_hom_app_spectralObjectHIsoCokernel_hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {ι : Type u_2} [CategoryTheory.Category.{v_2, u_2} ι] {F G : CategoryTheory.Functor ι (CochainComplex C ℤ)} (α : F ⟶ G) {i j : ι} (f : i ⟶ j) [CategoryTheory.Mono (F.map f)] [CategoryTheory.Mono (G.map f)] (n : ℤ) : CategoryTheory.CategoryStruct.comp (((spectralObjectMap α).hom n).app (CategoryTheory.ComposableArrows.mk₁ f)) (spectralObjectHIsoCokernel G f n).hom = CategoryTheory.CategoryStruct.comp (spectralObjectHIsoCokernel F f n).hom (HomologicalComplex.homologyMap (CategoryTheory.Limits.cokernel.map (F.map f) (G.map f) (α.app i) (α.app j) ⋯) n)

On H^n(f), for monomorphisms F.map f and G.map f, the morphism of spectral objects induced by α is the map in cohomology of the induced morphism of cokernels.

noncomputable def CochainComplex.filtrationFunctorMap {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} {F : ℤ → CategoryTheory.Subobject K} (hF : Monotone F) {G : ℤ → CategoryTheory.Subobject L} (hG : Monotone G) (f : K ⟶ L) (hf : ∀ (n : ℤ), (G n).Factors (CategoryTheory.CategoryStruct.comp (F n).arrow f)) : filtrationFunctor F hF ⟶ filtrationFunctor G hG

The morphism of filtration functors induced by a morphism of filtered complexes: a morphism f : K ⟶ L sending each piece F n into G n restricts to morphisms F n ⟶ G n, natural in n.

@[simp]

theorem CochainComplex.filtrationFunctorMap_app_comp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} {F : ℤ → CategoryTheory.Subobject K} {hF : Monotone F} {G : ℤ → CategoryTheory.Subobject L} {hG : Monotone G} (f : K ⟶ L) (hf : ∀ (n : ℤ), (G n).Factors (CategoryTheory.CategoryStruct.comp (F n).arrow f)) (a : EInt) : CategoryTheory.CategoryStruct.comp ((filtrationFunctorMap hF hG f hf).app a) (CategoryTheory.CategoryStruct.comp (filtrationFunctorObjIso G hG a).hom (filtrationEInt G a).arrow) = CategoryTheory.CategoryStruct.comp (filtrationFunctorObjIso F hF a).hom (CategoryTheory.CategoryStruct.comp (filtrationEInt F a).arrow f)

The components of filtrationFunctorMap f hf are the restrictions of f.

@[simp]

theorem CochainComplex.filtrationFunctorMap_app_comp_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} {F : ℤ → CategoryTheory.Subobject K} {hF : Monotone F} {G : ℤ → CategoryTheory.Subobject L} {hG : Monotone G} (f : K ⟶ L) (hf : ∀ (n : ℤ), (G n).Factors (CategoryTheory.CategoryStruct.comp (F n).arrow f)) (a : EInt) {Z : CochainComplex C ℤ} (h : L ⟶ Z) : CategoryTheory.CategoryStruct.comp ((filtrationFunctorMap hF hG f hf).app a) (CategoryTheory.CategoryStruct.comp (filtrationFunctorObjIso G hG a).hom (CategoryTheory.CategoryStruct.comp (filtrationEInt G a).arrow h)) = CategoryTheory.CategoryStruct.comp (filtrationFunctorObjIso F hF a).hom (CategoryTheory.CategoryStruct.comp (filtrationEInt F a).arrow (CategoryTheory.CategoryStruct.comp f h))

The components of filtrationFunctorMap f hf are the restrictions of f.

theorem CochainComplex.filtrationFunctorMap_congr {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} {F : ℤ → CategoryTheory.Subobject K} {hF : Monotone F} {G : ℤ → CategoryTheory.Subobject L} {hG : Monotone G} {f f' : K ⟶ L} (e : f = f') (hf : ∀ (n : ℤ), (G n).Factors (CategoryTheory.CategoryStruct.comp (F n).arrow f)) : filtrationFunctorMap hF hG f hf = filtrationFunctorMap hF hG f' ⋯

filtrationFunctorMap only depends on the morphism of complexes.

@[simp]

theorem CochainComplex.filtrationFunctorMap_id {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K : CochainComplex C ℤ} {F : ℤ → CategoryTheory.Subobject K} {hF : Monotone F} (hf : ∀ (n : ℤ), (F n).Factors (CategoryTheory.CategoryStruct.comp (F n).arrow (CategoryTheory.CategoryStruct.id K))) : filtrationFunctorMap hF hF (CategoryTheory.CategoryStruct.id K) hf = CategoryTheory.CategoryStruct.id (filtrationFunctor F hF)

The identity of a filtered complex induces the identity of its filtration functor.

theorem CochainComplex.filtrationFunctorMap_comp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {K L N : CochainComplex C ℤ} {F : ℤ → CategoryTheory.Subobject K} {hF : Monotone F} {G : ℤ → CategoryTheory.Subobject L} {hG : Monotone G} {H : ℤ → CategoryTheory.Subobject N} {hH : Monotone H} (f : K ⟶ L) (g : L ⟶ N) (hf : ∀ (n : ℤ), (G n).Factors (CategoryTheory.CategoryStruct.comp (F n).arrow f)) (hg : ∀ (n : ℤ), (H n).Factors (CategoryTheory.CategoryStruct.comp (G n).arrow g)) (hfg : ∀ (n : ℤ), (H n).Factors (CategoryTheory.CategoryStruct.comp (F n).arrow (CategoryTheory.CategoryStruct.comp f g))) : filtrationFunctorMap hF hH (CategoryTheory.CategoryStruct.comp f g) hfg = CategoryTheory.CategoryStruct.comp (filtrationFunctorMap hF hG f hf) (filtrationFunctorMap hG hH g hg)

A composite of morphisms of filtered complexes induces the composite of the morphisms of filtration functors. Not @[simp]: the intermediate filtration cannot be inferred from the left-hand side.