Degree-zero cohomology of a localized Hom complex

The map on the concrete kernel/range quotient of the degree-zero Hom-complex cohomology is a module localization when its three contributing cochain maps are localizations. A bounded-above source, bounded-below target, and finite presentation in the contributing source degrees supply those hypotheses.

This is not a derived-Hom or geometric base-change theorem.

@[reducible, inline]

abbrev CochainComplex.HomComplex.concreteCohomology {R : Type u} [CommRing R] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (E F : CochainComplex C ℤ) : Type w

Degree-zero cohomology of the Hom complex as cycles modulo boundaries.

Equations

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

noncomputable def CochainComplex.HomComplex.concreteCohomologyLocalizedMap {R : Type u} [CommRing R] (P Q : CochainComplex (ModuleCat R) ℤ) (S : Submonoid R) (hprev : IsLocalizedModule S (cochainLocalizedMap P Q (-1) S)) (hcur : IsLocalizedModule S (cochainLocalizedMap P Q 0 S)) (hnext : IsLocalizedModule S (cochainLocalizedMap P Q 1 S)) : concreteCohomology P Q →ₗ[R] concreteCohomology (CochainComplex.HomComplex.localized✝ S P) (CochainComplex.HomComplex.localized✝ S Q)

The canonical map on concrete degree-zero Hom-complex cohomology induced by termwise module localization. Its codomain uses the actual differentials of the localized Hom complex.

Equations

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

@[simp]

theorem CochainComplex.HomComplex.concreteCohomologyLocalizedMap_mk {R : Type u} [CommRing R] (P Q : CochainComplex (ModuleCat R) ℤ) (S : Submonoid R) (hprev : IsLocalizedModule S (cochainLocalizedMap P Q (-1) S)) (hcur : IsLocalizedModule S (cochainLocalizedMap P Q 0 S)) (hnext : IsLocalizedModule S (cochainLocalizedMap P Q 1 S)) (z : ↥(δ_hom R P Q 0 1).ker) : (concreteCohomologyLocalizedMap P Q S hprev hcur hnext) (Submodule.Quotient.mk z) = Submodule.Quotient.mk ⟨(cochainLocalizedMap P Q 0 S) ↑z, ⋯⟩

On a cycle representative, the concrete localization map applies the degree-zero cochain localization map.

theorem CochainComplex.HomComplex.concreteCohomologyLocalizedMap_isLocalized {R : Type u} [CommRing R] (P Q : CochainComplex (ModuleCat R) ℤ) (S : Submonoid R) (hprev : IsLocalizedModule S (cochainLocalizedMap P Q (-1) S)) (hcur : IsLocalizedModule S (cochainLocalizedMap P Q 0 S)) (hnext : IsLocalizedModule S (cochainLocalizedMap P Q 1 S)) : IsLocalizedModule S (concreteCohomologyLocalizedMap P Q S hprev hcur hnext)

Three localized cochain degrees give localization on their degree-zero kernel/range quotient.

noncomputable def CochainComplex.HomComplex.concreteCohomologyLocalizedMapOfBoundedAboveBelow {R : Type u} [CommRing R] (P Q : CochainComplex (ModuleCat R) ℤ) (S : Submonoid R) (c b : ℤ) [P.IsStrictlyLE b] [Q.IsStrictlyGE c] [∀ (i : ↥(Finset.Icc (c - 1) b)), Module.FinitePresentation R ↑(P.X ↑i)] : concreteCohomology P Q →ₗ[R] concreteCohomology (CochainComplex.HomComplex.localized✝ S P) (CochainComplex.HomComplex.localized✝ S Q)

The concrete degree-zero map under half-boundedness and finite presentation in its three contributing degrees.

Equations

• CochainComplex.HomComplex.concreteCohomologyLocalizedMapOfBoundedAboveBelow P Q S c b = CochainComplex.HomComplex.concreteCohomologyLocalizedMap P Q S ⋯ ⋯ ⋯

theorem CochainComplex.HomComplex.concreteCohomologyLocalizedMapOfBoundedAboveBelow_isLocalized {R : Type u} [CommRing R] (P Q : CochainComplex (ModuleCat R) ℤ) (S : Submonoid R) (c b : ℤ) [P.IsStrictlyLE b] [Q.IsStrictlyGE c] [∀ (i : ↥(Finset.Icc (c - 1) b)), Module.FinitePresentation R ↑(P.X ↑i)] : IsLocalizedModule S (concreteCohomologyLocalizedMapOfBoundedAboveBelow P Q S c b)

A strictly bounded-above source and strictly bounded-below target need finite presentation only on Icc (c - 1) b for degree-zero cohomology.