Cohomology of the hom complex

Given ℤ-indexed cochain complexes K and L, and n : ℤ, we introduce a type HomComplex.CohomologyClass K L n which is the quotient of HomComplex.Cocycle K L n which identifies cohomologous cocycles. We construct this type of cohomology classes instead of using the homology API because Cochain K L can be considered both as a complex of abelian groups or as a complex of R-modules when the category is R-linear. This also complements the API around HomComplex which is centered on terms in types Cochain or Cocycle which are suitable for computations.

We also show that HomComplex.CohomologyClass K L n identifies to the type of morphisms between K and L⟦n⟧ in the homotopy category.

def CochainComplex.HomComplex.coboundaries {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n : ℤ) : AddSubgroup (Cocycle K L n)

The subgroup of Cocycle K L n consisting of coboundaries.

theorem CochainComplex.HomComplex.mem_coboundaries_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (α : Cocycle K L n) (m : ℤ) (hm : m + 1 = n) : α ∈ coboundaries K L n ↔ ∃ (β : Cochain K L m), δ m n β = ↑α

def CochainComplex.HomComplex.CohomologyClass {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n : ℤ) : Type v

The type of cohomology classes of degree n in the complex of morphisms from K to L.

instance CochainComplex.HomComplex.instAddCommGroupCohomologyClass {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n : ℤ) : AddCommGroup (CohomologyClass K L n)

def CochainComplex.HomComplex.CohomologyClass.mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (x : Cocycle K L n) : CohomologyClass K L n

The cohomology class of a cocycle.

theorem CochainComplex.HomComplex.CohomologyClass.mk_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} : Function.Surjective mk

@[simp]

theorem CochainComplex.HomComplex.CohomologyClass.mk_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n : ℤ) : mk 0 = 0

@[simp]

theorem CochainComplex.HomComplex.CohomologyClass.mk_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (x y : Cocycle K L n) : mk (x + y) = mk x + mk y

@[simp]

theorem CochainComplex.HomComplex.CohomologyClass.mk_sub {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (x y : Cocycle K L n) : mk (x - y) = mk x - mk y

@[simp]

theorem CochainComplex.HomComplex.CohomologyClass.mk_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (x : Cocycle K L n) : mk (-x) = -mk x

theorem CochainComplex.HomComplex.CohomologyClass.mk_eq_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (x : Cocycle K L n) : mk x = 0 ↔ x ∈ coboundaries K L n

def CochainComplex.HomComplex.CohomologyClass.mkAddMonoidHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n : ℤ) : Cocycle K L n →+ CohomologyClass K L n

The projection map Cocycle K L n →+ CohomologyClass K L n.

@[simp]

theorem CochainComplex.HomComplex.CohomologyClass.mkAddMonoidHom_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n : ℤ) (x : Cocycle K L n) : (mkAddMonoidHom K L n) x = mk x

def CochainComplex.HomComplex.CohomologyClass.descAddMonoidHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} {G : Type u_2} [AddCommGroup G] (f : Cocycle K L n →+ G) (hf : coboundaries K L n ≤ f.ker) : CohomologyClass K L n →+ G

Constructor for additive morphisms from CohomologyClass K L n.

@[simp]

theorem CochainComplex.HomComplex.CohomologyClass.descAddMonoidHom_cohomologyClass {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} {G : Type u_2} [AddCommGroup G] (f : Cocycle K L n →+ G) (hf : coboundaries K L n ≤ f.ker) (x : Cocycle K L n) : (descAddMonoidHom f hf) (mk x) = f x

def CochainComplex.HomComplex.CohomologyClass.toHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} : CohomologyClass K L n →+ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))

The additive map which sends a cohomology class to the corresponding morphism in the homotopy category.

theorem CochainComplex.HomComplex.CohomologyClass.toHom_mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (x : Cocycle K L n) : toHom (mk x) = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (Cocycle.equivHomShift.symm x)

theorem CochainComplex.HomComplex.CohomologyClass.toHom_mk_eq_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (x : Cocycle K L n) : toHom (mk x) = 0 ↔ x ∈ coboundaries K L n

theorem CochainComplex.HomComplex.CohomologyClass.toHom_bijective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n : ℤ) : Function.Bijective ⇑toHom

noncomputable def CochainComplex.HomComplex.CohomologyClass.homAddEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} : CohomologyClass K L n ≃+ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))

Cohomology classes identify to morphisms in the homotopy category.

@[simp]

theorem CochainComplex.HomComplex.CohomologyClass.homAddEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (a : CohomologyClass K L n) : homAddEquiv a = toHom a

def CochainComplex.HomComplex.leftHomologyData' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n m p : ℤ) (hm : n + 1 = m) (hp : m + 1 = p) : (HomologicalComplex.sc' (K.HomComplex L) n m p).LeftHomologyData

CohomologyClass K L m identifies to the cohomology of the complex HomComplex K L in degree m.

@[simp]

theorem CochainComplex.HomComplex.leftHomologyData'_π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n m p : ℤ) (hm : n + 1 = m) (hp : m + 1 = p) : (leftHomologyData' K L n m p hm hp).π = AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)

@[simp]

theorem CochainComplex.HomComplex.leftHomologyData'_H_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n m p : ℤ) (hm : n + 1 = m) (hp : m + 1 = p) : ↑(leftHomologyData' K L n m p hm hp).H = CohomologyClass K L m

@[simp]

theorem CochainComplex.HomComplex.leftHomologyData'_K_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n m p : ℤ) (hm : n + 1 = m) (hp : m + 1 = p) : ↑(leftHomologyData' K L n m p hm hp).K = Cocycle K L m

@[simp]

theorem CochainComplex.HomComplex.leftHomologyData'_i {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n m p : ℤ) (hm : n + 1 = m) (hp : m + 1 = p) : (leftHomologyData' K L n m p hm hp).i = AddCommGrpCat.ofHom (Cocycle.toCochainAddMonoidHom K L m)

noncomputable def CochainComplex.HomComplex.leftHomologyData {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n : ℤ) : (HomologicalComplex.sc (K.HomComplex L) n).LeftHomologyData

CohomologyClass K L m identifies to the cohomology of the complex HomComplex K L in degree m.

@[simp]

theorem CochainComplex.HomComplex.leftHomologyData_H_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n : ℤ) : ↑(leftHomologyData K L n).H = CohomologyClass K L n

@[simp]

theorem CochainComplex.HomComplex.leftHomologyData_K_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n : ℤ) : ↑(leftHomologyData K L n).K = Cocycle K L n

@[simp]

theorem CochainComplex.HomComplex.leftHomologyData_i_hom_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n : ℤ) (x : Cocycle K L n) : (AddCommGrpCat.Hom.hom (leftHomologyData K L n).i) x = ↑x

@[simp]

theorem CochainComplex.HomComplex.leftHomologyData_π_hom_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n : ℤ) (x : Cocycle K L n) : (AddCommGrpCat.Hom.hom (leftHomologyData K L n).π) x = CohomologyClass.mk x

noncomputable def CochainComplex.HomComplex.homologyAddEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (K L : CochainComplex C ℤ) (n : ℤ) : ↑(HomologicalComplex.homology (K.HomComplex L) n) ≃+ CohomologyClass K L n

The homology of HomComplex K L in degree n identifies to CohomologyClass K L n.