Naturality of the universal coefficient sequence

The inclusion of Ext¹(Hⱼ(X), Y) into the cohomology of Hom(X, Y) commutes with pullback along chain maps and pushforward along coefficient morphisms. Together with naturality of the Kronecker map, this makes both arrows of the universal coefficient sequence natural in both variables. No compatibility of chosen cycle retractions is needed.

Reference: Hatcher, Algebraic Topology, Section 3.1, Theorem 3.2.

theorem TauCeti.ChainComplex.extToHomology_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {X X' : ChainComplex C α} {Y : C} (f : X' ⟶ X) (i j : α) [CategoryTheory.Projective (HomologicalComplex.cycles X j)] [CategoryTheory.IsSplitMono (HomologicalComplex.iCycles X j)] [CategoryTheory.Projective (HomologicalComplex.cycles X' j)] [CategoryTheory.IsSplitMono (HomologicalComplex.iCycles X' j)] (e : CategoryTheory.Abelian.Ext (HomologicalComplex.homology X j) Y 1) : (extToHomology k X' Y i j) ((CategoryTheory.Abelian.Ext.mk₀ (HomologicalComplex.homologyMap f j)).comp e ⋯) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap ((linearYonedaFunctor k Y).map f.op) i)) ((extToHomology k X Y i j) e)

Pulling back an extension of homology and then including it in cohomology is including it first and pulling back the resulting cohomology class. This holds in particular in the universal coefficient degree i = j + 1.

theorem TauCeti.ChainComplex.extToHomology_coefficient_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {X : ChainComplex C α} {Y Z : C} (g : Y ⟶ Z) (i j : α) [CategoryTheory.Projective (HomologicalComplex.cycles X j)] [CategoryTheory.IsSplitMono (HomologicalComplex.iCycles X j)] (e : CategoryTheory.Abelian.Ext (HomologicalComplex.homology X j) Y 1) : (extToHomology k X Z i j) (e.comp (CategoryTheory.Abelian.Ext.mk₀ g) ⋯) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k X g) i)) ((extToHomology k X Y i j) e)

Pushing an extension forward along a coefficient morphism and then including it in cohomology agrees with applying the induced coefficient map to its cohomology class.