Linear cohomology classes of the Hom complex

Mathlib defines HomComplex.CohomologyClass as an additive quotient. For an R-linear category, the coboundaries are stable under R, so the concrete kernel/range quotient supplies a compatible R-module structure and an R-linear equivalence. The instance is scoped: callers opt in to this scalar structure rather than changing Mathlib's additive interface globally.

This is an adapter for cohomology classes, not a derived-Hom base-change result.

def CochainComplex.HomComplex.cyclesLinearEquiv {R : Type u} [CommRing R] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (P Q : CochainComplex C ℤ) (n : ℤ) : ↥(δ_hom R P Q n (n + 1)).ker ≃ₗ[R] Cocycle P Q n

Cycles expressed as the kernel of the Hom-complex differential agree linearly with Mathlib's cocycle subtype.

Equations

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

def CochainComplex.HomComplex.boundaryToCyclesLinear {R : Type u} [CommRing R] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (P Q : CochainComplex C ℤ) (n : ℤ) : Cochain P Q (n - 1) →ₗ[R] ↥(δ_hom R P Q n (n + 1)).ker

The preceding Hom-complex differential, restricted to cycles.

Equations

• CochainComplex.HomComplex.boundaryToCyclesLinear P Q n = LinearMap.codRestrict (CochainComplex.HomComplex.δ_hom R P Q n (n + 1)).ker (CochainComplex.HomComplex.δ_hom R P Q (n - 1) n) ⋯

@[implicit_reducible]

def CochainComplex.HomComplex.cohomologyClassModule {R : Type u} [CommRing R] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (P Q : CochainComplex C ℤ) (n : ℤ) : Module R (CohomologyClass P Q n)

The scalar action on Hom-complex cohomology classes, transported from the concrete kernel/range quotient. This instance is scoped to callers that open CochainComplex.HomComplex; it is not a global instance.

Equations

• CochainComplex.HomComplex.cohomologyClassModule P Q n = AddEquiv.module R (CochainComplex.HomComplex.quotientAddEquiv✝ P Q n).symm

def CochainComplex.HomComplex.cohomologyClassLinearEquiv {R : Type u} [CommRing R] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (P Q : CochainComplex C ℤ) (n : ℤ) : (↥(δ_hom R P Q n (n + 1)).ker ⧸ (boundaryToCyclesLinear P Q n).range) ≃ₗ[R] CohomologyClass P Q n

The concrete kernel/range quotient identifies linearly with Mathlib's cohomology classes.

Equations

• CochainComplex.HomComplex.cohomologyClassLinearEquiv P Q n = (AddEquiv.linearEquiv R (CochainComplex.HomComplex.quotientAddEquiv✝ P Q n).symm).symm

@[simp]

theorem CochainComplex.HomComplex.cohomologyClassLinearEquiv_mk {R : Type u} [CommRing R] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (P Q : CochainComplex C ℤ) (n : ℤ) (z : ↥(δ_hom R P Q n (n + 1)).ker) : (cohomologyClassLinearEquiv P Q n) (Submodule.Quotient.mk z) = CohomologyClass.mk ((cyclesLinearEquiv P Q n) z)

@[simp]

theorem CochainComplex.HomComplex.cohomologyClass_mk_smul {R : Type u} [CommRing R] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (P Q : CochainComplex C ℤ) (n : ℤ) (r : R) (z : Cocycle P Q n) : CohomologyClass.mk (r • z) = r • CohomologyClass.mk z

@[simp]

theorem CochainComplex.HomComplex.cohomologyClass_mk_zsmul {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] (P Q : CochainComplex C ℤ) (n r : ℤ) (z : Cocycle P Q n) : CohomologyClass.mk (r • z) = r • CohomologyClass.mk z

Integer scaling of cohomology classes agrees with scaling cocycle representatives, including when Lean uses the canonical integer action.

noncomputable def CochainComplex.HomComplex.cohomologyClassIntLinearEquiv (P Q : CochainComplex (ModuleCat ℤ) ℤ) (n : ℤ) : (↥(δ_hom ℤ P Q n (n + 1)).ker ⧸ (boundaryToCyclesLinear P Q n).range) ≃ₗ[ℤ] CohomologyClass P Q n

For complexes of integer modules, the quotient identifies with cohomology classes using the canonical integer module structures on both additive groups.

Equations

• CochainComplex.HomComplex.cohomologyClassIntLinearEquiv P Q n = (CochainComplex.HomComplex.quotientAddEquiv✝ P Q n).toIntLinearEquiv