Restriction of module sheaves preserves limits, injectives, and free modules

Restriction along an open immersion has a left adjoint, given by sheafifying the corresponding presheaf pullback along the functor taking an open to its image. It therefore preserves limits, in addition to preserving colimits by Mathlib's restriction--pushforward adjunction. In particular, ambient kernels can be computed after restriction to an open subscheme. Pullback along an open immersion also preserves limits, since it is naturally isomorphic to restriction.

Restriction preserves injective module sheaves because its left adjoint, extension by zero, is exact. Thus injective resolutions may be restricted to an open subscheme without losing injectivity of their terms. Being a left adjoint that preserves the structure sheaf, restriction also sends free module sheaves to free module sheaves on the same generators.

A module sheaf is zero exactly when its restrictions to the members of an open cover are zero (AlgebraicGeometry.Scheme.Modules.isZero_iff_of_iSup_eq_top), by the sheaf condition. Restriction to an open U only sees sections over opens contained in U: a morphism that is an isomorphism on those sections restricts to an isomorphism (AlgebraicGeometry.Scheme.Modules.isIso_restrictFunctor_map_of_isIso_app), and over them the unit of the restriction--pushforward adjunction is an isomorphism on sections (AlgebraicGeometry.Scheme.Modules.isIso_restrictAdjunction_unit_app_app). Restriction along an isomorphism of schemes reflects isomorphisms, a morphism that is an isomorphism over an open is one over every smaller open and, along an open immersion, exactly when it is one over the image, a submodule containing one that is everything over an open is everything over it, and restriction to the slice site over an open preserves epimorphisms.

The adjunction is Mathlib's SheafOfModules.PullbackConstruction.adjunction; the underlying presheaf right adjoint is PresheafOfModules.instIsRightAdjointPushforward.

instance AlgebraicGeometry.Scheme.Modules.restrictFunctorIsRightAdjoint {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : (restrictFunctor f).IsRightAdjoint

Restriction of module sheaves along an open immersion is a right adjoint, so it preserves limits. Its left adjoint is the sheafified presheaf pullback along the open-image functor.

instance AlgebraicGeometry.Scheme.Modules.restrictFunctorAdditive {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : (restrictFunctor f).Additive

Restriction along an open immersion is additive. In particular it preserves the zero morphisms used in kernel diagrams.

noncomputable def AlgebraicGeometry.Scheme.Modules.restrictFunctorInvCompHomIso {X Y : Scheme} (e : X ≅ Y) : (restrictFunctor e.inv).comp (restrictFunctor e.hom) ≅ CategoryTheory.Functor.id X.Modules

Restricting along e.inv and then along e.hom is naturally isomorphic to the identity of X.Modules.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.restrictFunctorInvCompHomIso_hom_app_app {X Y : Scheme} (e : X ≅ Y) (M : X.Modules) (U : X.Opens) : Hom.app ((restrictFunctorInvCompHomIso e).hom.app M) U = M.presheaf.map (CategoryTheory.eqToHom ⋯).op

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.restrictFunctorInvCompHomIso_inv_app_app {X Y : Scheme} (e : X ≅ Y) (M : X.Modules) (U : X.Opens) : Hom.app ((restrictFunctorInvCompHomIso e).inv.app M) U = M.presheaf.map (CategoryTheory.eqToHom ⋯).op

@[instance 100]

instance AlgebraicGeometry.Scheme.Modules.restrictFunctorPreservesInjectiveObjects {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : (restrictFunctor f).PreservesInjectiveObjects

Restriction along any open immersion preserves injective module sheaves.

instance AlgebraicGeometry.Scheme.Hom.preservesLimits_pullback_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : CategoryTheory.Limits.PreservesLimits (Modules.pullback f)

Pullback along an open immersion preserves limits, since it is restriction.

noncomputable def AlgebraicGeometry.Scheme.Modules.restrictFreeIso {X Y : Scheme} (f : Y ⟶ X) [IsOpenImmersion f] (ι : Type u) : restrict (SheafOfModules.free ι) f ≅ SheafOfModules.free ι

Restriction along an open immersion sends the free module on ι to the free module on ι.

theorem AlgebraicGeometry.Scheme.Modules.isZero_iff_of_iSup_eq_top {X : Scheme} {ι : Type u_1} (U : ι → X.Opens) (hU : iSup U = ⊤) (M : X.Modules) : CategoryTheory.Limits.IsZero M ↔ ∀ (i : ι), CategoryTheory.Limits.IsZero (M.restrict (U i).ι)

A sheaf of modules on a scheme is zero exactly when its restrictions to the members of an open cover are zero.

theorem AlgebraicGeometry.Scheme.Modules.isIso_restrictFunctor_map_of_isIso_app {X : Scheme} {M N : X.Modules} (φ : M ⟶ N) (U : X.Opens) (h : ∀ V ≤ U, CategoryTheory.IsIso (Hom.app φ V)) : CategoryTheory.IsIso ((restrictFunctor U.ι).map φ)

A morphism of 𝒪_X-modules restricts to an isomorphism over an open U if it is an isomorphism on sections over every open contained in U.

theorem AlgebraicGeometry.Scheme.Modules.isIso_restrictAdjunction_unit_app_app {X : Scheme} (U : X.Opens) (M : X.Modules) {V : X.Opens} (hV : V ≤ U) : CategoryTheory.IsIso (Hom.app ((restrictAdjunction U.ι).unit.app M) V)

Over an open V contained in U, the unit M ⟶ U.ι_* (M|_U) of the restriction-pushforward adjunction is an isomorphism on sections.

theorem AlgebraicGeometry.Scheme.Modules.isIso_of_isIso_restrictFunctor_map {X Y : Scheme} (j : Y ⟶ X) [CategoryTheory.IsIso j] {M N : X.Modules} (φ : M ⟶ N) [CategoryTheory.IsIso ((restrictFunctor j).map φ)] : CategoryTheory.IsIso φ

Restriction along an isomorphism of schemes reflects isomorphisms of modules.

theorem AlgebraicGeometry.Scheme.Modules.isIso_restrictFunctor_map_of_le {X : Scheme} {M N : X.Modules} (φ : M ⟶ N) {V W : X.Opens} (h : V ≤ W) [CategoryTheory.IsIso ((restrictFunctor W.ι).map φ)] : CategoryTheory.IsIso ((restrictFunctor V.ι).map φ)

A morphism that restricts to an isomorphism over an open W restricts to an isomorphism over every open V ≤ W.

theorem AlgebraicGeometry.Scheme.Modules.isIso_restrictFunctor_map_iff_opensRange {X U : Scheme} (j : U ⟶ X) [IsOpenImmersion j] {M N : X.Modules} (φ : M ⟶ N) : CategoryTheory.IsIso ((restrictFunctor j).map φ) ↔ CategoryTheory.IsIso ((restrictFunctor (Hom.opensRange j).ι).map φ)

A morphism restricts to an isomorphism along an open immersion j if and only if it restricts to an isomorphism over the image of j.

theorem AlgebraicGeometry.Scheme.Modules.isIso_restrictFunctor_map_of_fac {X U : Scheme} (j : U ⟶ X) [IsOpenImmersion j] {N₁ N' N : X.Modules} {i₁ : N₁ ⟶ N} {i : N' ⟶ N} [CategoryTheory.Mono i] (g : N₁ ⟶ N') (hg : CategoryTheory.CategoryStruct.comp g i = i₁) [CategoryTheory.IsIso ((restrictFunctor j).map i₁)] : CategoryTheory.IsIso ((restrictFunctor j).map i)

A submodule i : N' ⟶ N through which a morphism i₁ : N₁ ⟶ N factors restricts to an isomorphism over every open over which i₁ does.

theorem AlgebraicGeometry.Scheme.Modules.epi_overFunctor_map {X : Scheme} {M N : X.Modules} (p : M ⟶ N) [CategoryTheory.Epi p] (U : X.Opens) : CategoryTheory.Epi ((SheafOfModules.overFunctor X.ringCatSheaf U).map p)

Restriction to the slice site over an open preserves epimorphisms: up to the open-subscheme equivalence it is restriction to the open subscheme, a left adjoint.