Post-composition on Hom complexes and their cohomology classes

Mathlib builds HomComplex A L but leaves it un-functorial in L. This file supplies post-composition with a morphism of complexes as a morphism of Hom complexes, its action on cocycles and cohomology classes, its compatibility with toSmallShiftedHom, and the naturality of the cycles and homology identifications. The injective-resolution presentation of Ext consumes it in Algebra/Homology/DerivedCategory/Ext/InjectiveResolutionNaturality.lean.

noncomputable def CochainComplex.HomComplex.postcompMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (A : CochainComplex C ℤ) {L L' : CochainComplex C ℤ} (g : L ⟶ L') : A.HomComplex L ⟶ A.HomComplex L'

Post-composition with a morphism of complexes, as a morphism of Hom complexes.

Mathlib builds HomComplex A L but leaves it un-functorial in L; this is the map a comparison argument needs when the target complex varies.

Equations

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

def CochainComplex.HomComplex.Cocycle.postcompAddMonoidHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (A : CochainComplex C ℤ) {L L' : CochainComplex C ℤ} (g : L ⟶ L') (n : ℤ) : Cocycle A L n →+ Cocycle A L' n

Post-composition of cocycles with a morphism of complexes, as an additive map.

Cocycles rather than cochains because this is what the left-homology data of the Hom complex names as its cycles object, and the naturality square below has to be typed against that.

Equations

• CochainComplex.HomComplex.Cocycle.postcompAddMonoidHom A g n = { toFun := fun (z : CochainComplex.HomComplex.Cocycle A L n) => z.postcomp g, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem CochainComplex.HomComplex.Cocycle.postcompAddMonoidHom_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (A : CochainComplex C ℤ) {L L' : CochainComplex C ℤ} (g : L ⟶ L') (n : ℤ) (z : Cocycle A L n) : (postcompAddMonoidHom A g n) z = z.postcomp g

@[simp]

theorem CochainComplex.HomComplex.postcompMap_f_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (A : CochainComplex C ℤ) {L L' : CochainComplex C ℤ} (g : L ⟶ L') (n : ℤ) (z : Cochain A L n) : (AddCommGrpCat.Hom.hom ((postcompMap A g).f n)) z = z.comp (Cochain.ofHom g) ⋯

Post-composition acts on a cochain by composing with the morphism, which is what makes the differential square commute.

def CochainComplex.HomComplex.CohomologyClass.postcompCocycleAddMonoidHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {K L L' : CochainComplex C ℤ} {n : ℤ} (g : L ⟶ L') : Cocycle K L n →+ CohomologyClass K L' n

Post-composition of cocycles with a morphism of complexes, as an additive map to cohomology classes.

Equations

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

@[simp]

theorem CochainComplex.HomComplex.CohomologyClass.postcompCocycleAddMonoidHom_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {K L L' : CochainComplex C ℤ} {n : ℤ} (g : L ⟶ L') (z : Cocycle K L n) : (postcompCocycleAddMonoidHom g) z = mk (z.postcomp g)

def CochainComplex.HomComplex.CohomologyClass.postcomp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {K L L' : CochainComplex C ℤ} {n : ℤ} (g : L ⟶ L') : CohomologyClass K L n →+ CohomologyClass K L' n

Post-composition of cohomology classes with a morphism of complexes.

Equations

• CochainComplex.HomComplex.CohomologyClass.postcomp g = CochainComplex.HomComplex.CohomologyClass.descAddMonoidHom (CochainComplex.HomComplex.CohomologyClass.postcompCocycleAddMonoidHom g) ⋯

@[simp]

theorem CochainComplex.HomComplex.CohomologyClass.postcomp_mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {K L L' : CochainComplex C ℤ} {n : ℤ} (g : L ⟶ L') (z : Cocycle K L n) : (postcomp g) (mk z) = mk (z.postcomp g)

Post-composition is computed on a representing cocycle, which is how every statement about it is proved: mk is surjective.

theorem CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHom_postcomp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {K L L' : CochainComplex C ℤ} {n : ℤ} [CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L'] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ L L'] [CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ L' L'] (x : CohomologyClass K L n) (g : L ⟶ L') : ((postcomp g) x).toSmallShiftedHom = x.toSmallShiftedHom.comp (CategoryTheory.Localization.SmallShiftedHom.mk₀ (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) 0 ⋯ g) ⋯

Post-composition of cohomology classes matches composition of shifted morphisms.

@[reducible, inline]

noncomputable abbrev CochainComplex.HomComplex.CohomologyClass.postcompSc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L L' : CochainComplex C ℤ} (A : CochainComplex C ℤ) (g : L ⟶ L') (n : ℤ) : HomologicalComplex.sc (A.HomComplex L) n ⟶ HomologicalComplex.sc (A.HomComplex L') n

The short-complex morphism induced by post-composition, in a fixed degree.

Equations

• CochainComplex.HomComplex.CohomologyClass.postcompSc A g n = (HomologicalComplex.shortComplexFunctor AddCommGrpCat (ComplexShape.up ℤ) n).map (CochainComplex.HomComplex.postcompMap A g)

noncomputable def CochainComplex.HomComplex.CohomologyClass.cocyclePostcomp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L L' : CochainComplex C ℤ} (A : CochainComplex C ℤ) (g : L ⟶ L') (n : ℤ) : (leftHomologyData A L n).K ⟶ (leftHomologyData A L' n).K

Post-composition on cocycles, typed against the left-homology data of the Hom complex.

Equations

• CochainComplex.HomComplex.CohomologyClass.cocyclePostcomp A g n = AddCommGrpCat.ofHom (CochainComplex.HomComplex.Cocycle.postcompAddMonoidHom A g n)

noncomputable def CochainComplex.HomComplex.CohomologyClass.classPostcomp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L L' : CochainComplex C ℤ} (A : CochainComplex C ℤ) (g : L ⟶ L') (n : ℤ) : (leftHomologyData A L n).H ⟶ (leftHomologyData A L' n).H

Post-composition on cohomology classes, typed against the left-homology data.

Equations

• CochainComplex.HomComplex.CohomologyClass.classPostcomp A g n = AddCommGrpCat.ofHom (CochainComplex.HomComplex.CohomologyClass.postcomp g)

theorem CochainComplex.HomComplex.CohomologyClass.postcompAddMonoidHom_comp_i {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L L' : CochainComplex C ℤ} (A : CochainComplex C ℤ) (g : L ⟶ L') (n : ℤ) : CategoryTheory.CategoryStruct.comp (cocyclePostcomp A g n) (leftHomologyData A L' n).i = CategoryTheory.CategoryStruct.comp (leftHomologyData A L n).i (postcompSc A g n).τ₂

The cocycle and cochain forms of post-composition agree under the inclusion of cycles.

This is the whole content of the cycles-level naturality: both sides become the same cochain composition once the mono i is cancelled.

theorem CochainComplex.HomComplex.CohomologyClass.cocyclePostcomp_comp_π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L L' : CochainComplex C ℤ} (A : CochainComplex C ℤ) (g : L ⟶ L') (n : ℤ) : CategoryTheory.CategoryStruct.comp (cocyclePostcomp A g n) (leftHomologyData A L' n).π = CategoryTheory.CategoryStruct.comp (leftHomologyData A L n).π (classPostcomp A g n)

Post-composition descends to classes, which is what lets the epi homologyπ be cancelled in the homology-level statement.

theorem CochainComplex.HomComplex.CohomologyClass.cyclesIso_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L L' : CochainComplex C ℤ} (A : CochainComplex C ℤ) (g : L ⟶ L') (n : ℤ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap (postcompSc A g n)) (leftHomologyData A L' n).cyclesIso.hom = CategoryTheory.CategoryStruct.comp (leftHomologyData A L n).cyclesIso.hom (cocyclePostcomp A g n)

The cycles of the Hom complex are the cocycles, compatibly with post-composition.

Proved by cancelling the mono i and reducing to the cochain level.

theorem CochainComplex.HomComplex.CohomologyClass.homologyIso_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L L' : CochainComplex C ℤ} (A : CochainComplex C ℤ) (g : L ⟶ L') (n : ℤ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (postcompSc A g n)) (leftHomologyData A L' n).homologyIso.hom = CategoryTheory.CategoryStruct.comp (leftHomologyData A L n).homologyIso.hom (classPostcomp A g n)

The homology of the Hom complex is the group of cohomology classes, compatibly with post-composition.

Both sides are determined by their restriction along the epi homologyπ, on which the statement becomes the cycles-level one.

theorem CochainComplex.HomComplex.CohomologyClass.homologyAddEquiv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L L' : CochainComplex C ℤ} (A : CochainComplex C ℤ) (g : L ⟶ L') (n : ℤ) (x : ↑(HomologicalComplex.homology (A.HomComplex L) n)) : (homologyAddEquiv A L' n) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap (postcompMap A g) n)) x) = (postcomp g) ((homologyAddEquiv A L n) x)

Elementwise form: the identification of the homology of a Hom complex with cohomology classes carries the map induced by post-composition to post-composition of classes.