Localization of Hom-complex cochains under finite effective support

When the source complex is supported in a finite interval and its terms are finitely presented, localization of modules commutes with each degree of its Hom complex. The comparison also commutes with the Hom-complex differential. Finite projective terms provide a useful specialization.

In each fixed degree, a termwise strictly bounded-above source and a termwise strictly bounded-below target also have finite effective support. Finite presentation of the source terms on that degree-dependent interval gives the same localization comparison.

This is a cochain-level statement. It does not yet identify cohomology of Hom complexes, derived-category Homs, or bounded-coherent geometric base change.

noncomputable def CochainComplex.HomComplex.cochainLocalizedMap {R : Type u} [CommRing R] (P Q : CochainComplex (ModuleCat R) ℤ) (n : ℤ) (S : Submonoid R) : Cochain P Q n →ₗ[R] Cochain (((ModuleCat.localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)).obj P) (((ModuleCat.localizedModuleFunctor S).mapHomologicalComplex (ComplexShape.up ℤ)).obj Q) n

The cochain map induced by localizing both complexes degreewise.

Equations

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

theorem CochainComplex.HomComplex.cochainLocalizedMap_delta {R : Type u} [CommRing R] (P Q : CochainComplex (ModuleCat R) ℤ) (n : ℤ) (S : Submonoid R) (m : ℤ) (γ : Cochain P Q n) : (cochainLocalizedMap P Q m S) (δ n m γ) = δ n m ((cochainLocalizedMap P Q n S) γ)

Degreewise localization respects the Hom-complex differential.

theorem CochainComplex.HomComplex.cochainLocalizedMap_isLocalized {R : Type u} [CommRing R] (P Q : CochainComplex (ModuleCat R) ℤ) (n : ℤ) (S : Submonoid R) (a b : ℤ) [P.IsStrictlyGE a] [P.IsStrictlyLE b] [∀ (i : ↥(Finset.Icc a b)), Module.FinitePresentation R ↑(P.X ↑i)] : IsLocalizedModule S (cochainLocalizedMap P Q n S)

A strictly bounded source with finitely presented terms makes every degree of the Hom complex commute with localization.

theorem CochainComplex.HomComplex.cochainLocalizedMap_isLocalized_of_finite_projective {R : Type u} [CommRing R] (P Q : CochainComplex (ModuleCat R) ℤ) (n : ℤ) (S : Submonoid R) (a b : ℤ) [P.IsStrictlyGE a] [P.IsStrictlyLE b] [∀ (i : ↥(Finset.Icc a b)), Module.Finite R ↑(P.X ↑i)] [∀ (i : ↥(Finset.Icc a b)), Module.Projective R ↑(P.X ↑i)] : IsLocalizedModule S (cochainLocalizedMap P Q n S)

Finite projective source terms satisfy the finite-presentation hypothesis of degreewise Hom-complex localization.

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

If the source is termwise strictly bounded above and the target termwise strictly bounded below, each fixed degree of their Hom complex commutes with localization, provided the finitely many source terms that contribute in that degree are finitely presented. The support interval depends on the degree; this is not yet derived-Hom base change.