Kernels and localization of modules

This file contains the algebraic kernel maps used to express that localization of modules is left exact. The statements are independent of sites and schemes: the geometric coherent-sheaf argument is a consumer of this root.

Main results

• LinearMap.kerMap is the map on kernels induced by a commutative square;
• IsLocalizedModule.kerMap proves that the induced linear map is a localization map;
• IsLocalizedModule.kernelMap is the corresponding statement for categorical kernels in ModuleCat;
• IsLocalizedModule.kernelNatTrans applies the result to a natural transformation between finite-limit-preserving functors.

def LinearMap.kerMap {A M M' N N' : Type w} [CommSemiring A] [AddCommMonoid M] [Module A M] [AddCommMonoid M'] [Module A M'] [AddCommMonoid N] [Module A N] [AddCommMonoid N'] [Module A N'] (a : M →ₗ[A] M') (b : N →ₗ[A] N') (g : M →ₗ[A] N) (g' : M' →ₗ[A] N') (h : g' ∘ₗ a = b ∘ₗ g) : ↥g.ker →ₗ[A] ↥g'.ker

The map on kernels induced by a commutative square of linear maps.

Equations

• a.kerMap b g g' h = { toFun := fun (x : ↥g.ker) => ⟨a ↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

theorem IsLocalizedModule.kerMap {A M M' N N' : Type w} [CommSemiring A] [AddCommMonoid M] [Module A M] [AddCommMonoid M'] [Module A M'] [AddCommMonoid N] [Module A N] [AddCommMonoid N'] [Module A N'] (S : Submonoid A) (a : M →ₗ[A] M') [ha : IsLocalizedModule S a] (b : N →ₗ[A] N') [hb : IsLocalizedModule S b] (g : M →ₗ[A] N) (g' : M' →ₗ[A] N') (h : g' ∘ₗ a = b ∘ₗ g) : IsLocalizedModule S (a.kerMap b g g' h)

Localization commutes with kernels, for arbitrary choices of localized targets.

theorem IsLocalizedModule.kernelMap {A : Type w} [CommRing A] (S : Submonoid A) {M M' N N' : ModuleCat A} (a : M ⟶ M') [IsLocalizedModule S (ModuleCat.Hom.hom a)] (b : N ⟶ N') [IsLocalizedModule S (ModuleCat.Hom.hom b)] (g : M ⟶ N) (g' : M' ⟶ N') (h : CategoryTheory.CategoryStruct.comp g b = CategoryTheory.CategoryStruct.comp a g') : IsLocalizedModule S (ModuleCat.Hom.hom (CategoryTheory.Limits.kernel.map g g' a b h))

Localization commutes with the map on categorical kernels in ModuleCat.

theorem IsLocalizedModule.kernelNatTrans {A : Type w} [CommRing A] (S : Submonoid A) {C : Type (w + 1)} [CategoryTheory.Category.{w, w + 1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F G : CategoryTheory.Functor C (ModuleCat A)) [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteLimits G] (α : F ⟶ G) {X Y : C} (g : X ⟶ Y) [CategoryTheory.Limits.HasKernel g] [IsLocalizedModule S (ModuleCat.Hom.hom (α.app X))] [IsLocalizedModule S (ModuleCat.Hom.hom (α.app Y))] : IsLocalizedModule S (ModuleCat.Hom.hom (α.app (CategoryTheory.Limits.kernel g)))

A natural transformation whose endpoint components are localization maps remains a localization map on kernels, provided both functors preserve finite limits.