Degree-zero Hom-complex cohomology classes under localization

The class map induced by degreewise localization agrees, through the linear class/quotient equivalences, with the localized map on the concrete degree-zero kernel/range quotient. Exactness of module localization then makes this class map a localization map. A half-bounded specialization needs finite presentation only for source terms in Finset.Icc (c - 1) b.

This does not identify derived-category Homs or establish geometric base change.

noncomputable def CochainComplex.HomComplex.cohomologyClassLocalizedMap {R : Type u} [CommRing R] (P Q : CochainComplex (ModuleCat R) ℤ) (S : Submonoid R) : CohomologyClass P Q 0 →ₗ[R] CohomologyClass (CochainComplex.HomComplex.localized✝ S P) (CochainComplex.HomComplex.localized✝ S Q) 0

The degree-zero map on Hom-complex cohomology classes induced by degreewise localization of both complexes.

Equations

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

theorem CochainComplex.HomComplex.concreteCohomologyMap_eq_localized {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)) : concreteCohomologyMap P Q 0 (CochainComplex.HomComplex.localized✝ S P) (CochainComplex.HomComplex.localized✝ S Q) (cochainLocalizedMap P Q (0 - 1) S) (cochainLocalizedMap P Q 0 S) (cochainLocalizedMap P Q (0 + 1) S) ⋯ ⋯ = concreteCohomologyLocalizedMap P Q S hprev hcur hnext

The generic concrete quotient map is the degree-zero map constructed using exact localization. Both maps send a cycle class to its localized cycle.

theorem CochainComplex.HomComplex.cohomologyClassLocalizedMap_naturality {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)) : cohomologyClassLocalizedMap P Q S ∘ₗ ↑(cohomologyClassLinearEquiv P Q 0) = ↑(cohomologyClassLinearEquiv (CochainComplex.HomComplex.localized✝ S P) (CochainComplex.HomComplex.localized✝ S Q) 0) ∘ₗ concreteCohomologyLocalizedMap P Q S hprev hcur hnext

The degree-zero class map commutes with the concrete localization map through the source and target linear class/quotient equivalences.

theorem CochainComplex.HomComplex.cohomologyClassLocalizedMap_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 (cohomologyClassLocalizedMap P Q S)

Localization of the three contributing cochain degrees makes the induced degree-zero map on CohomologyClass a module localization.

theorem CochainComplex.HomComplex.cohomologyClassLocalizedMap_isLocalized_of_bounded_above_below {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 (cohomologyClassLocalizedMap P Q S)

If the source is strictly bounded above by b, the target is strictly bounded below by c, and the source terms in Icc (c - 1) b are finitely presented, the degree-zero class map is a localization.