Exact pullback along open immersions

Mathlib identifies module-sheaf pullback along an open immersion with restriction and proves that restriction commutes with stalks. Combining that comparison with the stalkwise-to-global criterion from Families.FlatPullback proves that pullback along every open immersion is exact. Consequently its ordinary module pullback descends to the concrete derived fibers without an additional exactness hypothesis.

Mathlib also identifies restriction after module-sheaf pushforward with the identity. Applying that counit degreewise gives every complex on the open subscheme an extension to the ambient scheme. After localization this proves that derived pullback along an open immersion is essentially surjective; no exactness of pushforward is needed for this objectwise extension argument.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.openImmersionPullbackStalkForgetIso {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X) : ((Scheme.Modules.pullback f).comp (Scheme.Modules.moduleStalkFunctor X x)).comp (CategoryTheory.forget₂ (ModuleCat ↑(X.presheaf.stalk x)) AddCommGrpCat) ≅ (Scheme.Modules.toPresheaf Y).comp (TopCat.Presheaf.stalkFunctor AddCommGrpCat (f x))

After forgetting the local-ring action, pullback followed by a stalk along an open immersion is the ordinary stalk at the image point.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.openImmersionPullbackStalk_preservesFiniteLimits {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X) : CategoryTheory.Limits.PreservesFiniteLimits ((Scheme.Modules.pullback f).comp (Scheme.Modules.moduleStalkFunctor X x))

Pullback along an open immersion, followed by any module-stalk functor, preserves finite limits.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.openImmersionModulePullback_preservesFiniteLimits {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsOpenImmersion (CategoryTheory.Over.Hom.left f)] : CategoryTheory.Limits.PreservesFiniteLimits (modulePullback f)

Module-sheaf pullback along an open immersion preserves finite limits.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.isExactPullback_of_isOpenImmersion {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsOpenImmersion (CategoryTheory.Over.Hom.left f)] : IsExactPullback f

Pullback along an open immersion of scheme base changes is exact.

@[instance 900]

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.isExactPullbackOfIsOpenImmersion {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsOpenImmersion (CategoryTheory.Over.Hom.left f)] : IsExactPullback f

Exact pullback along open immersions is available to the derived pullback API without a caller-supplied exactness instance.

Essential surjectivity

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.openImmersionModulePullbackPushforwardIso {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsOpenImmersion (CategoryTheory.Over.Hom.left f)] : (modulePushforward f).comp (modulePullback f) ≅ CategoryTheory.Functor.id (CategoryTheory.Over.left T).Modules

Pushforward followed by pullback along an open immersion is naturally isomorphic to the identity on module sheaves. The point is that pullback is restriction in this case, and Mathlib's restriction--pushforward adjunction has invertible counit.

Equations

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

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.openImmersionComplexExtension {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) : CategoryTheory.Functor (CochainComplex (CategoryTheory.Over.left T).Modules ℤ) (CochainComplex (CategoryTheory.Over.left U).Modules ℤ)

Extend a complex on an open subscheme termwise by module-sheaf pushforward. Pushforward need not be exact: this functor is used only to choose an ambient representative whose pullback is the original complex.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.openImmersionComplexPullbackExtensionIso {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsOpenImmersion (CategoryTheory.Over.Hom.left f)] : (openImmersionComplexExtension f).comp (complexPullback f) ≅ CategoryTheory.Functor.id (CochainComplex (CategoryTheory.Over.left T).Modules ℤ)

Pulling back the termwise extension of a complex from an open subscheme recovers that complex.

Equations

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

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullback_essSurj_of_isOpenImmersion {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsOpenImmersion (CategoryTheory.Over.Hom.left f)] : (derivedPullback f).EssSurj

Derived pullback along an open immersion is essentially surjective.

For a derived object on the open subscheme, choose a complex representative, extend it termwise by pushforward, and use the restriction--pushforward counit after applying the derived localization.

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.LeftDerivedPullback.essSurj_of_isOpenImmersion {S : Scheme} {T U : SchemeBaseChange S} {f : T ⟶ U} (P : LeftDerivedPullback f) [IsOpenImmersion (CategoryTheory.Over.Hom.left f)] : P.functor.EssSurj

Every genuine left-derived pullback along an open immersion is essentially surjective. Uniqueness of left-derived functors identifies it with the exact model above.