Cohomology of a localized three-term complex

Three degreewise module localizations that commute with consecutive differentials induce a localization of the kernel modulo the preceding image. This is a module-level cohomology statement; it does not identify a particular derived category Hom or assert geometric base change.

def IsLocalizedModule.boundaryToCycles {R : Type u_1} [CommRing R] {M₀ : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [AddCommGroup M₀] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₀] [Module R M₁] [Module R M₂] (d₀ : M₀ →ₗ[R] M₁) (d₁ : M₁ →ₗ[R] M₂) (hd : d₁ ∘ₗ d₀ = 0) : M₀ →ₗ[R] ↥d₁.ker

The first differential, with codomain restricted to cycles of the second.

Equations

• IsLocalizedModule.boundaryToCycles d₀ d₁ hd = LinearMap.codRestrict d₁.ker d₀ ⋯

noncomputable def IsLocalizedModule.localizedDifferential {R : Type u_1} [CommRing R] (S : Submonoid R) {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N₁] [AddCommGroup N₂] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] (f₁ : M₁ →ₗ[R] N₁) (f₂ : M₂ →ₗ[R] N₂) [IsLocalizedModule S f₁] [IsLocalizedModule S f₂] (d₁ : M₁ →ₗ[R] M₂) : N₁ →ₗ[R] N₂

The localized second differential.

Equations

• IsLocalizedModule.localizedDifferential S f₁ f₂ d₁ = (IsLocalizedModule.map S f₁ f₂) d₁

noncomputable def IsLocalizedModule.localizedCyclesMap {R : Type u_1} [CommRing R] (S : Submonoid R) {M₁ : Type u_3} {M₂ : Type u_4} {N₁ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N₁] [AddCommGroup N₂] [Module R M₁] [Module R M₂] [Module R N₁] [Module R N₂] (f₁ : M₁ →ₗ[R] N₁) (f₂ : M₂ →ₗ[R] N₂) [IsLocalizedModule S f₁] [IsLocalizedModule S f₂] (d₁ : M₁ →ₗ[R] M₂) : ↥d₁.ker →ₗ[R] ↥(localizedDifferential S f₁ f₂ d₁).ker

The canonical localization map on cycles.

Equations

• IsLocalizedModule.localizedCyclesMap S f₁ f₂ d₁ = LinearMap.toKerIsLocalized S f₁ f₂ d₁

noncomputable def IsLocalizedModule.localizedBoundaryToCycles {R : Type u_1} [CommRing R] (S : Submonoid R) {M₀ : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₀ : Type u_5} {N₁ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₀] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N₀] [AddCommGroup N₁] [AddCommGroup N₂] [Module R M₀] [Module R M₁] [Module R M₂] [Module R N₀] [Module R N₁] [Module R N₂] (f₀ : M₀ →ₗ[R] N₀) (f₁ : M₁ →ₗ[R] N₁) (f₂ : M₂ →ₗ[R] N₂) [IsLocalizedModule S f₀] [IsLocalizedModule S f₁] [IsLocalizedModule S f₂] (d₀ : M₀ →ₗ[R] M₁) (d₁ : M₁ →ₗ[R] M₂) (hd : d₁ ∘ₗ d₀ = 0) : N₀ →ₗ[R] ↥(localizedDifferential S f₁ f₂ d₁).ker

The localized first differential, with codomain restricted to cycles of the localized second differential.

Equations

• IsLocalizedModule.localizedBoundaryToCycles S f₀ f₁ f₂ d₀ d₁ hd = LinearMap.codRestrict (IsLocalizedModule.localizedDifferential S f₁ f₂ d₁).ker ((IsLocalizedModule.map S f₀ f₁) d₀) ⋯

noncomputable def IsLocalizedModule.cohomologyMap {R : Type u_1} [CommRing R] (S : Submonoid R) {M₀ : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₀ : Type u_5} {N₁ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₀] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N₀] [AddCommGroup N₁] [AddCommGroup N₂] [Module R M₀] [Module R M₁] [Module R M₂] [Module R N₀] [Module R N₁] [Module R N₂] (f₀ : M₀ →ₗ[R] N₀) (f₁ : M₁ →ₗ[R] N₁) (f₂ : M₂ →ₗ[R] N₂) [IsLocalizedModule S f₀] [IsLocalizedModule S f₁] [IsLocalizedModule S f₂] (d₀ : M₀ →ₗ[R] M₁) (d₁ : M₁ →ₗ[R] M₂) (hd : d₁ ∘ₗ d₀ = 0) : ↥d₁.ker ⧸ (boundaryToCycles d₀ d₁ hd).range →ₗ[R] ↥(localizedDifferential S f₁ f₂ d₁).ker ⧸ (localizedBoundaryToCycles S f₀ f₁ f₂ d₀ d₁ hd).range

The map on kernel modulo image induced by three degreewise localizations.

Equations

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

theorem IsLocalizedModule.cohomologyMap_isLocalized {R : Type u_1} [CommRing R] (S : Submonoid R) {M₀ : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {N₀ : Type u_5} {N₁ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₀] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup N₀] [AddCommGroup N₁] [AddCommGroup N₂] [Module R M₀] [Module R M₁] [Module R M₂] [Module R N₀] [Module R N₁] [Module R N₂] (f₀ : M₀ →ₗ[R] N₀) (f₁ : M₁ →ₗ[R] N₁) (f₂ : M₂ →ₗ[R] N₂) [IsLocalizedModule S f₀] [IsLocalizedModule S f₁] [IsLocalizedModule S f₂] (d₀ : M₀ →ₗ[R] M₁) (d₁ : M₁ →ₗ[R] M₂) (hd : d₁ ∘ₗ d₀ = 0) : IsLocalizedModule S (cohomologyMap S f₀ f₁ f₂ d₀ d₁ hd)

Localization is exact on the cohomology quotient of a three-term complex.