Morphisms from a chain complex into an object

For a chain complex X in a k-linear abelian category C and an object Y : C, Mathlib's ChainComplex.linearYonedaObj is the cochain complex of k-modules which in degree i is the module of morphisms X.X i ⟶ Y, with differential given by precomposition with the differential of X. This file makes the construction a contravariant functor of X, shows that it takes a chain homotopy to a cochain homotopy, and shows that it takes a short exact sequence of chain complexes which is split in each degree to a short exact sequence of cochain complexes. It also records elementwise descriptions of the differential, cocycles, coboundaries and cohomology classes of Hom(X, Y), and of the maps between them induced by chain maps. Postcomposition with coefficient morphisms is provided by ChainComplex.linearYonedaObjMap.

The functor Hom(-, Y) is only left exact, so the splitting hypothesis cannot be dropped. It holds for the singular chains of a pair of spaces, which is how the long exact sequence in singular cohomology is obtained from the one of chain complexes.

Main declarations

• TauCeti.ChainComplex.linearYonedaFunctor: the functor X ↦ Hom(X, Y) from chain complexes to cochain complexes of k-modules.
• TauCeti.ChainComplex.shortExact_map_linearYonedaFunctor: Hom(-, Y) preserves short exactness of degreewise split sequences.
• Homotopy.linearYonedaFunctorMap: Hom(-, Y) takes a chain homotopy to a cochain homotopy.
• TauCeti.HomotopyEquiv.linearYonedaFunctorMap: Hom(-, Y) takes a chain homotopy equivalence to a cochain homotopy equivalence in the opposite direction.

noncomputable def TauCeti.ChainComplex.linearYonedaFunctor {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (Y : C) : CategoryTheory.Functor (ChainComplex C α)ᵒᵖ (CochainComplex (ModuleCat k) α)

The contravariant functor sending a chain complex X to the cochain complex of k-modules Hom(X, Y), which in degree i is the module of morphisms X.X i ⟶ Y.

Equations

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

instance TauCeti.ChainComplex.instAdditiveOppositeChainComplexCochainComplexModuleCatLinearYonedaFunctor {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (Y : C) : (linearYonedaFunctor k Y).Additive

noncomputable def Homotopy.linearYonedaFunctorMap {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (Y : C) {X X' : ChainComplex C α} {φ ψ : X ⟶ X'} (h : Homotopy φ ψ) : Homotopy ((TauCeti.ChainComplex.linearYonedaFunctor k Y).map φ.op) ((TauCeti.ChainComplex.linearYonedaFunctor k Y).map ψ.op)

Hom(-, Y) takes a chain homotopy between two chain maps φ, ψ : X ⟶ X' to a cochain homotopy between the two maps Hom(X', Y) ⟶ Hom(X, Y) obtained by precomposition.

Equations

• Homotopy.linearYonedaFunctorMap k Y h = (((CategoryTheory.linearYoneda k C).obj Y).rightOp.mapHomotopy h).unop

noncomputable def TauCeti.HomotopyEquiv.linearYonedaFunctorMap {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (Y : C) {X X' : ChainComplex C α} (h : HomotopyEquiv X X') : HomotopyEquiv ((ChainComplex.linearYonedaFunctor k Y).obj (Opposite.op X')) ((ChainComplex.linearYonedaFunctor k Y).obj (Opposite.op X))

Hom(-, Y) takes a chain homotopy equivalence to a cochain homotopy equivalence in the opposite direction, with maps given by precomposition.

Equations

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

@[simp]

theorem TauCeti.HomotopyEquiv.linearYonedaFunctorMap_hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (Y : C) {X X' : ChainComplex C α} (h : HomotopyEquiv X X') : (linearYonedaFunctorMap k Y h).hom = (ChainComplex.linearYonedaFunctor k Y).map h.hom.op

The forward map of the induced homotopy equivalence is precomposition with h.hom.

@[simp]

theorem TauCeti.HomotopyEquiv.linearYonedaFunctorMap_inv {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (Y : C) {X X' : ChainComplex C α} (h : HomotopyEquiv X X') : (linearYonedaFunctorMap k Y h).inv = (ChainComplex.linearYonedaFunctor k Y).map h.inv.op

The inverse map of the induced homotopy equivalence is precomposition with h.inv.

@[simp]

theorem TauCeti.ChainComplex.linearYonedaFunctor_obj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (Y : C) (X : (ChainComplex C α)ᵒᵖ) : (linearYonedaFunctor k Y).obj X = (Opposite.unop X).linearYonedaObj k Y

@[simp]

theorem TauCeti.ChainComplex.linearYonedaFunctor_map_f_hom_apply {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (Y : C) {X X' : (ChainComplex C α)ᵒᵖ} (φ : X ⟶ X') (i : α) (g : ↑(((Opposite.unop X).linearYonedaObj k Y).X i)) : (CategoryTheory.ConcreteCategory.hom (((linearYonedaFunctor k Y).map φ).f i)) g = CategoryTheory.CategoryStruct.comp (φ.unop.f i) g

The map Hom(X', Y) ⟶ Hom(X, Y) induced by a chain map X ⟶ X' is precomposition.

@[simp]

theorem Homotopy.linearYonedaFunctorMap_hom_apply {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (Y : C) {X X' : ChainComplex C α} {φ ψ : X ⟶ X'} (h : Homotopy φ ψ) (i j : α) (g : ↑((X'.linearYonedaObj k Y).X i)) : (CategoryTheory.ConcreteCategory.hom ((linearYonedaFunctorMap k Y h).hom i j)) g = CategoryTheory.CategoryStruct.comp (h.hom j i) g

The cochain homotopy induced by a chain homotopy h is precomposition with h.

theorem TauCeti.ChainComplex.shortExact_map_linearYonedaFunctor {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (Y : C) {S : CategoryTheory.ShortComplex (ChainComplex C α)} (hS : S.ShortExact) [∀ (i : α), CategoryTheory.IsSplitMono (S.f.f i)] : (S.op.map (linearYonedaFunctor k Y)).ShortExact

The functor Hom(-, Y) takes a short exact sequence 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 of chain complexes which is split in each degree to a short exact sequence 0 ⟶ Hom(X₃, Y) ⟶ Hom(X₂, Y) ⟶ Hom(X₁, Y) ⟶ 0 of cochain complexes.

noncomputable def ChainComplex.linearYonedaObjMap {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (X : ChainComplex C α) {Y Z : C} (g : Y ⟶ Z) : X.linearYonedaObj k Y ⟶ X.linearYonedaObj k Z

Postcomposition with a coefficient morphism induces a map of cochain complexes Hom(X, Y) ⟶ Hom(X, Z).

Equations

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

@[simp]

theorem ChainComplex.linearYonedaObjMap_f_hom_apply {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (X : ChainComplex C α) {Y Z : C} (g : Y ⟶ Z) (i : α) (a : X.X i ⟶ Y) : (CategoryTheory.ConcreteCategory.hom ((linearYonedaObjMap k X g).f i)) a = CategoryTheory.CategoryStruct.comp a g

The coefficient map on cochains is postcomposition.

@[simp]

theorem ChainComplex.linearYonedaObjMap_id {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (X : ChainComplex C α) (Y : C) : linearYonedaObjMap k X (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.id (X.linearYonedaObj k Y)

Identity coefficient maps induce identity maps of cochain complexes.

@[simp]

theorem ChainComplex.linearYonedaObjMap_comp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (X : ChainComplex C α) {Y Z T : C} (g : Y ⟶ Z) (h : Z ⟶ T) : linearYonedaObjMap k X (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (linearYonedaObjMap k X g) (linearYonedaObjMap k X h)

Coefficient maps on cochain complexes preserve composition.

@[simp]

theorem ChainComplex.homologyMap_linearYonedaObjMap_homologyπ_apply {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (X : ChainComplex C α) {Y Z : C} (g : Y ⟶ Z) (i : α) (a : ↑(HomologicalComplex.cycles (X.linearYonedaObj k Y) i)) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap (linearYonedaObjMap k X g) i)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (X.linearYonedaObj k Y) i)) a) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (X.linearYonedaObj k Z) i)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.cyclesMap (linearYonedaObjMap k X g) i)) a)

The coefficient map sends the class of a cocycle to the class of its image.

@[simp]

theorem ChainComplex.iCycles_cyclesMap_linearYonedaObjMap_apply {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] (X : ChainComplex C α) {Y Z : C} (g : Y ⟶ Z) (i : α) (a : ↑(HomologicalComplex.cycles (X.linearYonedaObj k Y) i)) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (X.linearYonedaObj k Z) i)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.cyclesMap (linearYonedaObjMap k X g) i)) a) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (X.linearYonedaObj k Y) i)) a) g

The coefficient map on cocycles is postcomposition.

theorem TauCeti.ChainComplex.linearYonedaObj_d_apply {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] {Y : C} {X : ChainComplex C α} (i j : α) (g : ↑((X.linearYonedaObj k Y).X i)) : (CategoryTheory.ConcreteCategory.hom ((X.linearYonedaObj k Y).d i j)) g = CategoryTheory.CategoryStruct.comp (X.d j i) g

The differential of Hom(X, Y) is precomposition with the differential of X.

theorem TauCeti.ChainComplex.d_comp_linearYonedaObj_iCycles {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] {Y : C} {X : ChainComplex C α} (i j : α) (a : ↑(HomologicalComplex.cycles (X.linearYonedaObj k Y) i)) : CategoryTheory.CategoryStruct.comp (X.d j i) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (X.linearYonedaObj k Y) i)) a) = 0

A cocycle a of Hom(X, Y) vanishes on boundaries: a ∘ d is the zero of the module (X.linearYonedaObj k Y).X j.

theorem TauCeti.ChainComplex.linearYonedaObj_iCycles_toCycles_apply {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] {Y : C} {X : ChainComplex C α} (i j : α) (g : ↑((X.linearYonedaObj k Y).X i)) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (X.linearYonedaObj k Y) j)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.toCycles (X.linearYonedaObj k Y) i j)) g) = CategoryTheory.CategoryStruct.comp (X.d j i) g

The coboundary of a cochain g of Hom(X, Y) is g ∘ d.

theorem TauCeti.ChainComplex.linearYonedaObj_homologyπ_toCycles_apply {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] {Y : C} {X : ChainComplex C α} (i j : α) (g : ↑((X.linearYonedaObj k Y).X i)) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (X.linearYonedaObj k Y) j)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.toCycles (X.linearYonedaObj k Y) i j)) g) = 0

A coboundary of Hom(X, Y) has zero cohomology class.

theorem TauCeti.ChainComplex.homologyMap_linearYonedaFunctor_map_homologyπ_apply {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] {Y : C} {X X' : ChainComplex C α} (f : X' ⟶ X) (i : α) (a : ↑(HomologicalComplex.cycles (X.linearYonedaObj k Y) i)) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap ((linearYonedaFunctor k Y).map f.op) i)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (X.linearYonedaObj k Y) i)) a) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (X'.linearYonedaObj k Y) i)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.cyclesMap ((linearYonedaFunctor k Y).map f.op) i)) a)

The map on cohomology H(Hom(X, Y)) ⟶ H(Hom(X', Y)) induced by a chain map f : X' ⟶ X sends the class of a cocycle to the class of its image in the cocycles of Hom(X', Y).

theorem TauCeti.ChainComplex.iCycles_cyclesMap_linearYonedaFunctor_map_apply {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] {Y : C} {X X' : ChainComplex C α} (f : X' ⟶ X) (i : α) (a : ↑(HomologicalComplex.cycles (X.linearYonedaObj k Y) i)) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (X'.linearYonedaObj k Y) i)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.cyclesMap ((linearYonedaFunctor k Y).map f.op) i)) a) = CategoryTheory.CategoryStruct.comp (f.f i) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (X.linearYonedaObj k Y) i)) a)

The map on cocycles Z(Hom(X, Y)) ⟶ Z(Hom(X', Y)) induced by a chain map f : X' ⟶ X is precomposition with f.