Single complexes, arbitrary embeddings, and bicomplex symmetry #

For any source and target complex shapes, source degree, embedding, and image degree j, extending a single and mapping it degreewise along an independent complex shape gives a bicomplex naturally isomorphic to the flipped single at j. The comparison requires only zero morphisms and a zero object, and factors through the arbitrary-shape mapped-single/flip isomorphism rather than a definitional equality.

Main results #

HomologicalComplex₂.singleMapHomologicalComplexFlipIso identifies the mapped-single and flipped-bicomplex functors for arbitrary complex shapes.
HomologicalComplex₂.singleExtendMapFlipIso identifies an extended single at an arbitrary source degree with the flipped bicomplex at its image degree, for arbitrary source, target, and mapped complex shapes.

Implementation notes #

At each outer degree, the component is the inverse of Mathlib's HomologicalComplex.singleMapHomologicalComplex for the evaluation functor. Differential compatibility splits the supported inner degree from the zero ones. Naturality follows from that existing comparison. The arbitrary-image embedding theorem composes the natural single-extension and flip isomorphisms.

References #

The proof uses Mathlib's HomologicalComplex.singleMapHomologicalComplex, HomologicalComplex.Hom.isoOfComponents, HomologicalComplex₂.flipFunctor, and the repository's HomologicalComplex.singleCompExtendIso.

source

noncomputable def HomologicalComplex₂.singleMapHomologicalComplexFlipIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {I : Type u_1} {J : Type u_2} (c₁ : ComplexShape I) (c₂ : ComplexShape J) [DecidableEq J] (j₀ : J) :

(HomologicalComplex.single C c₂ j₀).mapHomologicalComplex c₁ ≅ (HomologicalComplex.single (HomologicalComplex C c₁) c₂ j₀).comp (flipFunctor C c₂ c₁)

The two functors package the complex indices differently, so this comparison is not definitional. Its components use the inverse of HomologicalComplex.singleMapHomologicalComplex; differential compatibility reduces to the supported inner degree and its zero complement.

Equations

HomologicalComplex₂.singleMapHomologicalComplexFlipIso c₁ c₂ j₀ = CategoryTheory.NatIso.ofComponents (HomologicalComplex₂.singleMapHomologicalComplexFlipObjIso✝ c₁ c₂ j₀) ⋯

Instances For

source

noncomputable def HomologicalComplex₂.singleExtendMapFlipIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] {ι : Type u_3} {ι' : Type u_4} {κ : Type u_5} [DecidableEq ι] [DecidableEq ι'] {c : ComplexShape ι} {c' : ComplexShape ι'} (d : ComplexShape κ) (e : c.Embedding c') (i : ι) (j : ι') (h : e.f i = j) :

((HomologicalComplex.single C c i).comp (e.extendFunctor C)).mapHomologicalComplex d ≅ (HomologicalComplex.single (HomologicalComplex C d) c' j).comp (flipFunctor C c' d)

Extending a single at source index i along e with e.f i = j, then mapping along any independent complex shape d, is the flipped single at the image index j. This composes the existing single-extension and flip comparisons, without an additive or total-complex assumption.