Exactness and base change of the sheaf associated with a module

The functor M ↦ M~ from R-modules to 𝒪_{Spec R}-modules is exact. It preserves finite colimits as a left adjoint of the global-section functor, and it preserves monomorphisms because a section of M~ over an open subset U is a family of elements of the localizations M_p, p ∈ U, that is locally a fraction, and localization preserves injectivity.

For a ring map φ : R ⟶ S and an R-module M, the pullback of the quasi-coherent sheaf M~ along Spec φ : Spec S ⟶ Spec R is the sheaf associated with the base change S ⊗_R M: (Spec φ)^* M~ ≅ (S ⊗_R M)~, naturally in M.

Both functors M ↦ (Spec φ)^* M~ and M ↦ (S ⊗_R M)~ are left adjoint to taking global sections followed by restriction of scalars along φ, so the isomorphism is the uniqueness of left adjoints. On global sections it sends the pullback of the section m of M~ to the section 1 ⊗ m.

As an application, the sheaf associated with a finitely generated projective R-module is finite locally free. Every prime p of R has a basic open neighbourhood D(r) on which M_r is a finite free R_r-module. Since D(r) ≅ Spec R_r, the restriction of M~ to D(r) is the pullback of M~ to Spec R_r, which is the sheaf associated with R_r ⊗_R M ≅ M_r, hence free of finite rank.

Since M~ is left adjoint to taking global sections, with unit the map M → Γ(M~), a morphism out of M~ is determined by where it sends the global sections coming from M.

Main declarations

• TauCeti.AlgebraicGeometry.tilde_map_app_injective: an injective linear map M ⟶ N induces injective maps M~(U) ⟶ N~(U) on sections;
• TauCeti.AlgebraicGeometry.preservesFiniteLimits_tildeFunctor: the functor M ↦ M~ preserves finite limits, hence (with its preservation of colimits) short exact sequences;
• Scheme.Modules.tildeKernelIso: the affine computation of ambient kernels of morphisms between quasicoherent sheaves, with tildeKernelIso_hom_comp_ι identifying the kernel inclusion;
• TauCeti.AlgebraicGeometry.tildeFunctorCompPullbackIso: the isomorphism (Spec φ)^* M~ ≅ (S ⊗_R M)~, natural in M;
• TauCeti.AlgebraicGeometry.unit_tildeFunctorCompPullbackIso_hom_app: its characterization on global sections;
• TauCeti.AlgebraicGeometry.isFiniteLocallyFree_tilde: M~ is finite locally free when M is finitely generated and projective;
• TauCeti.AlgebraicGeometry.tilde_hom_ext: a morphism out of M~ is determined by its values on the global sections coming from M.

References

• R. Hartshorne, Algebraic Geometry, Proposition II.5.2 (a) (exactness) and (e) (base change)
• The Stacks Project, Tag 00NX

theorem TauCeti.AlgebraicGeometry.tilde_map_app_injective {R : CommRingCat} {M N : ModuleCat ↑R} (f : M ⟶ N) (hf : Function.Injective ⇑(ModuleCat.Hom.hom f)) (U : (AlgebraicGeometry.Spec R).Opensᵒᵖ) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((AlgebraicGeometry.tilde.map f).val.app U))

The map M~(U) ⟶ N~(U) on sections induced by an injective linear map f : M ⟶ N is injective.

instance TauCeti.AlgebraicGeometry.mono_tilde_map {R : CommRingCat} {M N : ModuleCat ↑R} (f : M ⟶ N) [CategoryTheory.Mono f] : CategoryTheory.Mono (AlgebraicGeometry.tilde.map f)

The functor M ↦ M~ sends monomorphisms of R-modules to monomorphisms of 𝒪_{Spec R}-modules.

instance TauCeti.AlgebraicGeometry.preservesFiniteLimits_tildeFunctor {R : CommRingCat} : CategoryTheory.Limits.PreservesFiniteLimits (AlgebraicGeometry.tilde.functor R)

The functor M ↦ M~ is left exact. Being a left adjoint, it is also right exact, so it sends short exact sequences of R-modules to short exact sequences of 𝒪_{Spec R}-modules.

noncomputable def AlgebraicGeometry.Scheme.Modules.tildeKernelIso {R : CommRingCat} {M N : (Spec R).Modules} (f : M ⟶ N) [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] : tilde (CategoryTheory.Limits.kernel (moduleSpecΓFunctor.map f)) ≅ CategoryTheory.Limits.kernel f

The kernel of a morphism of quasicoherent sheaves on a spectrum is the sheaf associated with the kernel of its map on global sections. The comparison uses the counit of tilde.adjunction and the canonical kernel comparison of the exact tilde functor.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.tildeKernelIso_hom_comp_ι {R : CommRingCat} {M N : (Spec R).Modules} (f : M ⟶ N) [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] : CategoryTheory.CategoryStruct.comp (tildeKernelIso f).hom (CategoryTheory.Limits.kernel.ι f) = CategoryTheory.CategoryStruct.comp ((tilde.functor R).map (CategoryTheory.Limits.kernel.ι (moduleSpecΓFunctor.map f))) M.fromTildeΓ

The affine kernel comparison intertwines kernel inclusions through the counit of the tilde/global-sections adjunction.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.tildeKernelIso_hom_comp_ι_assoc {R : CommRingCat} {M N : (Spec R).Modules} (f : M ⟶ N) [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] {Z : (Spec R).Modules} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (tildeKernelIso f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((tilde.functor R).map (CategoryTheory.Limits.kernel.ι (moduleSpecΓFunctor.map f))) M.fromTildeΓ) h

The affine kernel comparison intertwines kernel inclusions through the counit of the tilde/global-sections adjunction.

noncomputable def TauCeti.AlgebraicGeometry.pushforwardCompModuleSpecΓFunctorIso {R S : CommRingCat} (φ : R ⟶ S) : (AlgebraicGeometry.Scheme.Modules.pushforward (AlgebraicGeometry.Spec.map φ)).comp AlgebraicGeometry.moduleSpecΓFunctor ≅ AlgebraicGeometry.moduleSpecΓFunctor.comp (ModuleCat.restrictScalars (CommRingCat.Hom.hom φ))

Global sections of the pushforward along Spec φ are the global sections upstairs, with scalars restricted along φ.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.pushforwardCompModuleSpecΓFunctorIso_hom_app_apply {R S : CommRingCat} (φ : R ⟶ S) (N : (AlgebraicGeometry.Spec S).Modules) (x : ↑(AlgebraicGeometry.moduleSpecΓFunctor.obj ((AlgebraicGeometry.Scheme.Modules.pushforward (AlgebraicGeometry.Spec.map φ)).obj N))) : (ModuleCat.Hom.hom ((pushforwardCompModuleSpecΓFunctorIso φ).hom.app N)) x = x

pushforwardCompModuleSpecΓFunctorIso is the identity on global sections.

@[simp]

theorem TauCeti.AlgebraicGeometry.pushforwardCompModuleSpecΓFunctorIso_inv_app_apply {R S : CommRingCat} (φ : R ⟶ S) (N : (AlgebraicGeometry.Spec S).Modules) (x : ↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom φ)).obj (AlgebraicGeometry.moduleSpecΓFunctor.obj N))) : (ModuleCat.Hom.hom ((pushforwardCompModuleSpecΓFunctorIso φ).inv.app N)) x = x

The inverse of pushforwardCompModuleSpecΓFunctorIso is the identity on global sections.

noncomputable def TauCeti.AlgebraicGeometry.tildeFunctorCompPullbackIso {R S : CommRingCat} (φ : R ⟶ S) : (AlgebraicGeometry.tilde.functor R).comp (AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ)) ≅ (ModuleCat.extendScalars (CommRingCat.Hom.hom φ)).comp (AlgebraicGeometry.tilde.functor S)

The pullback along Spec φ of the sheaf associated with an R-module M is the sheaf associated with the base change S ⊗_R M, naturally in M.

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.unit_tildeFunctorCompPullbackIso_hom_app {R S : CommRingCat} (φ : R ⟶ S) (M : ModuleCat ↑R) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.adjunction.unit.app M) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.moduleSpecΓFunctor.map ((AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction (AlgebraicGeometry.Spec.map φ)).unit.app (AlgebraicGeometry.tilde M))) (CategoryTheory.CategoryStruct.comp ((pushforwardCompModuleSpecΓFunctorIso φ).hom.app ((AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ)).obj (AlgebraicGeometry.tilde M))) ((ModuleCat.restrictScalars (CommRingCat.Hom.hom φ)).map (AlgebraicGeometry.moduleSpecΓFunctor.map ((tildeFunctorCompPullbackIso φ).hom.app M))))) = CategoryTheory.CategoryStruct.comp ((ModuleCat.extendRestrictScalarsAdj (CommRingCat.Hom.hom φ)).unit.app M) ((ModuleCat.restrictScalars (CommRingCat.Hom.hom φ)).map (AlgebraicGeometry.tilde.adjunction.unit.app (ModuleCat.ExtendScalars.obj' (CommRingCat.Hom.hom φ) M)))

The characteristic property of tildeFunctorCompPullbackIso on global sections: it sends the pullback of the section m of M~ to the section 1 ⊗ m of (S ⊗_R M)~.

theorem TauCeti.AlgebraicGeometry.isFiniteLocallyFree_tilde {R : CommRingCat} (M : ModuleCat ↑R) [Module.Finite ↑R ↑M] [Module.Projective ↑R ↑M] : AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree (AlgebraicGeometry.Spec R) (AlgebraicGeometry.tilde M)

The sheaf associated with a finitely generated projective R-module is a finite locally free 𝒪_{Spec R}-module.

theorem TauCeti.AlgebraicGeometry.tilde_hom_ext {R : CommRingCat} {M : ModuleCat ↑R} {N : (AlgebraicGeometry.Spec R).Modules} {f g : (AlgebraicGeometry.tilde.functor R).obj M ⟶ N} (h : ∀ (m : ↑M), (CategoryTheory.ConcreteCategory.hom (f.val.app (Opposite.op ⊤))) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.tilde.toOpen M ⊤)) m) = (CategoryTheory.ConcreteCategory.hom (g.val.app (Opposite.op ⊤))) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.tilde.toOpen M ⊤)) m)) : f = g

Two morphisms out of M~ agree as soon as they agree on the global sections coming from M.