Naturality of extension for a single complex #

Mathlib's HomologicalComplex.extendSingleIso identifies the extension of a complex supported at one degree with a single complex at the embedded degree. This module packages those objectwise isomorphisms naturally in the supported object.

Main results #

HomologicalComplex.singleCompExtendIso is natural for an arbitrary embedding of complex shapes and compatible source and target degrees.
HomologicalComplex.singleCompExtendAtImageIso uses the canonical target degree supplied by the embedding.

Implementation notes #

Naturality is checked at the supported degree, where both maps reduce to the original morphism. The source and target use the same ambient zero-morphism and decidable-index instances, so the comparison specializes directly to existing single-complex functors.

References #

The components are Mathlib's HomologicalComplex.extendSingleIso and its supported-degree formula HomologicalComplex.extendSingleIso_hom_f.

source

noncomputable def HomologicalComplex.singleCompExtendIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_1} {ι' : Type u_2} [DecidableEq ι] [DecidableEq ι'] {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (i : ι) (i' : ι') (h : e.f i = i') :

(single C c i).comp (e.extendFunctor C) ≅ single C c' i'

The components are Mathlib's HomologicalComplex.extendSingleIso. Naturality is determined at the supported degree because every other target component is a zero object.

Equations

HomologicalComplex.singleCompExtendIso e i i' h = CategoryTheory.NatIso.ofComponents (fun (X : C) => HomologicalComplex.extendSingleIso e X i i' h) ⋯

Instances For

source

noncomputable def HomologicalComplex.singleCompExtendAtImageIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_1} {ι' : Type u_2} [DecidableEq ι] [DecidableEq ι'] {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (i : ι) :

(single C c i).comp (e.extendFunctor C) ≅ single C c' (e.f i)

For a nonzero source object, only the image degree can be nonzero after extension. This canonical form avoids transporting a separately chosen target index through later natural comparisons.