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.

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.

Equations

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

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.

Equations

• CochainComplex.HomComplex.CohomologyClass K L n = (CochainComplex.HomComplex.Cocycle K L n ⧸ CochainComplex.HomComplex.coboundaries K L n)

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)

Equations

• CochainComplex.HomComplex.instAddCommGroupCohomologyClass K L n = inferInstanceAs (AddCommGroup (CochainComplex.HomComplex.Cocycle K L n ⧸ CochainComplex.HomComplex.coboundaries 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.

Equations

• CochainComplex.HomComplex.CohomologyClass.mk x = ⟦x⟧

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.

Equations

• CochainComplex.HomComplex.CohomologyClass.mkAddMonoidHom K L n = { toFun := CochainComplex.HomComplex.CohomologyClass.mk, map_zero' := ⋯, map_add' := ⋯ }

@[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.

Equations

• CochainComplex.HomComplex.CohomologyClass.descAddMonoidHom f hf = QuotientAddGroup.lift (CochainComplex.HomComplex.coboundaries K L n) f hf

@[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.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.

Equations

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

@[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)

@[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'_π {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

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.

Equations

• CochainComplex.HomComplex.leftHomologyData K L n = CochainComplex.HomComplex.leftHomologyData' K L ((ComplexShape.up ℤ).prev n) n ((ComplexShape.up ℤ).next n) ⋯ ⋯

@[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_π_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

@[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

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.

Equations

• CochainComplex.HomComplex.homologyAddEquiv K L n = (CochainComplex.HomComplex.leftHomologyData K L n).homologyIso.addCommGroupIsoToAddEquiv