Naturality of linear Hom-complex cohomology classes

Three degreewise R-linear maps commuting with the two adjacent Hom-complex differentials induce maps on the concrete kernel/range quotient and on Mathlib's CohomologyClass. The linear equivalence between those presentations commutes with the induced maps. The source and target complexes may live in different R-linear preadditive categories.

This is a generic cochain-complex statement; no localization or derived-Hom comparison is asserted here.

def CochainComplex.HomComplex.cohomologyClassMapLinear {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 : ℤ) {C' : Type v'} [CategoryTheory.Category.{w', v'} C'] [CategoryTheory.Preadditive C'] [CategoryTheory.Linear R C'] (P' Q' : CochainComplex C' ℤ) (fprev : Cochain P Q (n - 1) →ₗ[R] Cochain P' Q' (n - 1)) (fcur : Cochain P Q n →ₗ[R] Cochain P' Q' n) (fnext : Cochain P Q (n + 1) →ₗ[R] Cochain P' Q' (n + 1)) (hprev : δ_hom R P' Q' (n - 1) n ∘ₗ fprev = fcur ∘ₗ δ_hom R P Q (n - 1) n) (hcur : δ_hom R P' Q' n (n + 1) ∘ₗ fcur = fnext ∘ₗ δ_hom R P Q n (n + 1)) : CohomologyClass P Q n →ₗ[R] CohomologyClass P' Q' n

The map on Mathlib cohomology classes induced by degreewise linear maps commuting with both adjacent Hom-complex differentials.

Equations

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

@[simp]

theorem CochainComplex.HomComplex.cohomologyClassMapLinear_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 : ℤ) {C' : Type v'} [CategoryTheory.Category.{w', v'} C'] [CategoryTheory.Preadditive C'] [CategoryTheory.Linear R C'] (P' Q' : CochainComplex C' ℤ) (fprev : Cochain P Q (n - 1) →ₗ[R] Cochain P' Q' (n - 1)) (fcur : Cochain P Q n →ₗ[R] Cochain P' Q' n) (fnext : Cochain P Q (n + 1) →ₗ[R] Cochain P' Q' (n + 1)) (hprev : δ_hom R P' Q' (n - 1) n ∘ₗ fprev = fcur ∘ₗ δ_hom R P Q (n - 1) n) (hcur : δ_hom R P' Q' n (n + 1) ∘ₗ fcur = fnext ∘ₗ δ_hom R P Q n (n + 1)) (z : Cocycle P Q n) : (cohomologyClassMapLinear P Q n P' Q' fprev fcur fnext hprev hcur) (CohomologyClass.mk z) = CohomologyClass.mk (Cocycle.mk (fcur ↑z) (n + 1) ⋯ ⋯)

On a cocycle class, the induced map applies fcur to its representative.

def CochainComplex.HomComplex.concreteCohomologyMap {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 : ℤ) {C' : Type v'} [CategoryTheory.Category.{w', v'} C'] [CategoryTheory.Preadditive C'] [CategoryTheory.Linear R C'] (P' Q' : CochainComplex C' ℤ) (fprev : Cochain P Q (n - 1) →ₗ[R] Cochain P' Q' (n - 1)) (fcur : Cochain P Q n →ₗ[R] Cochain P' Q' n) (fnext : Cochain P Q (n + 1) →ₗ[R] Cochain P' Q' (n + 1)) (hprev : δ_hom R P' Q' (n - 1) n ∘ₗ fprev = fcur ∘ₗ δ_hom R P Q (n - 1) n) (hcur : δ_hom R P' Q' n (n + 1) ∘ₗ fcur = fnext ∘ₗ δ_hom R P Q n (n + 1)) : ↥(δ_hom R P Q n (n + 1)).ker ⧸ (boundaryToCyclesLinear P Q n).range →ₗ[R] ↥(δ_hom R P' Q' n (n + 1)).ker ⧸ (boundaryToCyclesLinear P' Q' n).range

The induced linear map on the concrete kernel/range presentation of Hom-complex cohomology.

Equations

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

@[simp]

theorem CochainComplex.HomComplex.concreteCohomologyMap_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 : ℤ) {C' : Type v'} [CategoryTheory.Category.{w', v'} C'] [CategoryTheory.Preadditive C'] [CategoryTheory.Linear R C'] (P' Q' : CochainComplex C' ℤ) (fprev : Cochain P Q (n - 1) →ₗ[R] Cochain P' Q' (n - 1)) (fcur : Cochain P Q n →ₗ[R] Cochain P' Q' n) (fnext : Cochain P Q (n + 1) →ₗ[R] Cochain P' Q' (n + 1)) (hprev : δ_hom R P' Q' (n - 1) n ∘ₗ fprev = fcur ∘ₗ δ_hom R P Q (n - 1) n) (hcur : δ_hom R P' Q' n (n + 1) ∘ₗ fcur = fnext ∘ₗ δ_hom R P Q n (n + 1)) (z : ↥(δ_hom R P Q n (n + 1)).ker) : (concreteCohomologyMap P Q n P' Q' fprev fcur fnext hprev hcur) (Submodule.Quotient.mk z) = Submodule.Quotient.mk ⟨fcur ↑z, ⋯⟩

On a concrete quotient class, the induced map applies fcur to its cycle.

theorem CochainComplex.HomComplex.cohomologyClassLinearEquiv_naturality {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 : ℤ) {C' : Type v'} [CategoryTheory.Category.{w', v'} C'] [CategoryTheory.Preadditive C'] [CategoryTheory.Linear R C'] (P' Q' : CochainComplex C' ℤ) (fprev : Cochain P Q (n - 1) →ₗ[R] Cochain P' Q' (n - 1)) (fcur : Cochain P Q n →ₗ[R] Cochain P' Q' n) (fnext : Cochain P Q (n + 1) →ₗ[R] Cochain P' Q' (n + 1)) (hprev : δ_hom R P' Q' (n - 1) n ∘ₗ fprev = fcur ∘ₗ δ_hom R P Q (n - 1) n) (hcur : δ_hom R P' Q' n (n + 1) ∘ₗ fcur = fnext ∘ₗ δ_hom R P Q n (n + 1)) : cohomologyClassMapLinear P Q n P' Q' fprev fcur fnext hprev hcur ∘ₗ ↑(cohomologyClassLinearEquiv P Q n) = ↑(cohomologyClassLinearEquiv P' Q' n) ∘ₗ concreteCohomologyMap P Q n P' Q' fprev fcur fnext hprev hcur

The linear class/quotient adapter is natural for degreewise maps commuting with the Hom-complex differential.

@[simp]

theorem CochainComplex.HomComplex.cohomologyClassIntLinearEquiv_mk (U V : CochainComplex (ModuleCat ℤ) ℤ) (m : ℤ) (z : ↥(δ_hom ℤ U V m (m + 1)).ker) : (cohomologyClassIntLinearEquiv U V m) (Submodule.Quotient.mk z) = CohomologyClass.mk ((cyclesLinearEquiv U V m) z)

The canonical integer equivalence sends a cycle class to its Mathlib cohomology class.

theorem CochainComplex.HomComplex.cohomologyClassIntLinearEquiv_naturality (P Q : CochainComplex (ModuleCat ℤ) ℤ) (n : ℤ) (P' Q' : CochainComplex (ModuleCat ℤ) ℤ) (fprev : Cochain P Q (n - 1) →ₗ[ℤ] Cochain P' Q' (n - 1)) (fcur : Cochain P Q n →ₗ[ℤ] Cochain P' Q' n) (fnext : Cochain P Q (n + 1) →ₗ[ℤ] Cochain P' Q' (n + 1)) (hprev : δ_hom ℤ P' Q' (n - 1) n ∘ₗ fprev = fcur ∘ₗ δ_hom ℤ P Q (n - 1) n) (hcur : δ_hom ℤ P' Q' n (n + 1) ∘ₗ fcur = fnext ∘ₗ δ_hom ℤ P Q n (n + 1)) (x : ↥(δ_hom ℤ P Q n (n + 1)).ker ⧸ (boundaryToCyclesLinear P Q n).range) : (cohomologyClassMapLinear P Q n P' Q' fprev fcur fnext hprev hcur) ((cohomologyClassIntLinearEquiv P Q n) x) = (cohomologyClassIntLinearEquiv P' Q' n) ((concreteCohomologyMap P Q n P' Q' fprev fcur fnext hprev hcur) x)

The generic naturality square also commutes pointwise with canonical integer module structures.