Pullback comparisons are invertible if they are invertible on affine charts

Let W X : X.Modules ⥤ X.Modules be an endofunctor of module sheaves for every scheme X, such as a symmetric or exterior power, and let c f : W Y ⋙ f^* ⟶ f^* ⋙ W X be comparison maps for every morphism of schemes f : X ⟶ Y. Suppose that the comparisons are compatible with the composition isomorphisms Scheme.Modules.pullbackComp, that they are invertible on quasicoherent modules along open immersions, and that they are invertible on quasicoherent modules along morphisms Spec S ⟶ Spec R of affine spectra. Then c f is invertible on every quasicoherent module, for every morphism f.

The proof reduces first to morphisms with affine target, by restricting to the preimages of the affine opens of Y, then to morphisms between affine schemes, by restricting to the affine opens of X, and finally to morphisms of spectra, along Scheme.isoSpec. Each step uses the composition compatibility and Scheme.Modules.isIso_iff_of_isOpenCover. It is the reduction used for tensor products in Scheme.Modules.isIso_pullback_δ_of_isQuasicoherent, stated for an arbitrary family of comparison maps.

Invertibility along open immersions is itself formal. Along an open immersion j, a comparison whose transpose under the pullback--pushforward adjunction factors through a pushforward comparison q, as does the unit of the restriction--pushforward adjunction together with a restriction isomorphism r, is the inverse of r read through Scheme.Modules.restrictFunctorIsoPullback.

Main declarations

• TauCeti.AlgebraicGeometry.pullbackComparison_app_of_isOpenImmersion: along an open immersion, such a comparison is the inverse of the restriction isomorphism; TauCeti.AlgebraicGeometry.isIso_pullbackComparison_app_of_isOpenImmersion deduces that it is invertible.
• TauCeti.AlgebraicGeometry.isIso_pullbackComparison_app_of_isQuasicoherent: comparison maps compatible with composition, invertible along open immersions and along morphisms of affine spectra, are invertible on quasicoherent modules along every morphism.

References

• R. Hartshorne, Algebraic Geometry, Proposition II.5.2 and Exercise II.5.16.

theorem TauCeti.AlgebraicGeometry.pullbackComparison_app_of_isOpenImmersion {U Y : AlgebraicGeometry.Scheme} (j : U ⟶ Y) [AlgebraicGeometry.IsOpenImmersion j] (W₁ : CategoryTheory.Functor Y.Modules Y.Modules) (W₂ : CategoryTheory.Functor U.Modules U.Modules) (c : W₁.comp (AlgebraicGeometry.Scheme.Modules.pullback j) ⟶ (AlgebraicGeometry.Scheme.Modules.pullback j).comp W₂) (q : (AlgebraicGeometry.Scheme.Modules.pushforward j).comp W₁ ⟶ W₂.comp (AlgebraicGeometry.Scheme.Modules.pushforward j)) (r : (AlgebraicGeometry.Scheme.Modules.restrictFunctor j).comp W₂ ≅ W₁.comp (AlgebraicGeometry.Scheme.Modules.restrictFunctor j)) (M : Y.Modules) (h₁ : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction j).unit.app (W₁.obj M)) ((AlgebraicGeometry.Scheme.Modules.pushforward j).map (c.app M)) = CategoryTheory.CategoryStruct.comp (W₁.map ((AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction j).unit.app M)) (q.app ((AlgebraicGeometry.Scheme.Modules.pullback j).obj M))) (h₂ : (AlgebraicGeometry.Scheme.Modules.restrictAdjunction j).unit.app (W₁.obj M) = CategoryTheory.CategoryStruct.comp (W₁.map ((AlgebraicGeometry.Scheme.Modules.restrictAdjunction j).unit.app M)) (CategoryTheory.CategoryStruct.comp (q.app ((AlgebraicGeometry.Scheme.Modules.restrictFunctor j).obj M)) ((AlgebraicGeometry.Scheme.Modules.pushforward j).map (r.hom.app M)))) : c.app M = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.restrictFunctorIsoPullback j).inv.app (W₁.obj M)) (CategoryTheory.CategoryStruct.comp (r.inv.app M) (W₂.map ((AlgebraicGeometry.Scheme.Modules.restrictFunctorIsoPullback j).hom.app M)))

Along an open immersion j, let c : W₁ ⋙ j^* ⟶ j^* ⋙ W₂ be a comparison whose transpose under the pullback--pushforward adjunction is W₁ of the unit followed by a pushforward comparison q, and suppose that the unit of the restriction--pushforward adjunction factors through q and a restriction isomorphism r : W₂ (M|_U) ≅ (W₁ M)|_U. Then c is the inverse of r, read through the identification Scheme.Modules.restrictFunctorIsoPullback of restriction with pullback.

theorem TauCeti.AlgebraicGeometry.isIso_pullbackComparison_app_of_isOpenImmersion {U Y : AlgebraicGeometry.Scheme} (j : U ⟶ Y) [AlgebraicGeometry.IsOpenImmersion j] (W₁ : CategoryTheory.Functor Y.Modules Y.Modules) (W₂ : CategoryTheory.Functor U.Modules U.Modules) (c : W₁.comp (AlgebraicGeometry.Scheme.Modules.pullback j) ⟶ (AlgebraicGeometry.Scheme.Modules.pullback j).comp W₂) (q : (AlgebraicGeometry.Scheme.Modules.pushforward j).comp W₁ ⟶ W₂.comp (AlgebraicGeometry.Scheme.Modules.pushforward j)) (r : (AlgebraicGeometry.Scheme.Modules.restrictFunctor j).comp W₂ ≅ W₁.comp (AlgebraicGeometry.Scheme.Modules.restrictFunctor j)) (M : Y.Modules) (h₁ : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction j).unit.app (W₁.obj M)) ((AlgebraicGeometry.Scheme.Modules.pushforward j).map (c.app M)) = CategoryTheory.CategoryStruct.comp (W₁.map ((AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction j).unit.app M)) (q.app ((AlgebraicGeometry.Scheme.Modules.pullback j).obj M))) (h₂ : (AlgebraicGeometry.Scheme.Modules.restrictAdjunction j).unit.app (W₁.obj M) = CategoryTheory.CategoryStruct.comp (W₁.map ((AlgebraicGeometry.Scheme.Modules.restrictAdjunction j).unit.app M)) (CategoryTheory.CategoryStruct.comp (q.app ((AlgebraicGeometry.Scheme.Modules.restrictFunctor j).obj M)) ((AlgebraicGeometry.Scheme.Modules.pushforward j).map (r.hom.app M)))) : CategoryTheory.IsIso (c.app M)

Under the hypotheses of pullbackComparison_app_of_isOpenImmersion, the comparison along the open immersion j is invertible.

theorem TauCeti.AlgebraicGeometry.isIso_pullbackComparison_app_of_isQuasicoherent (W : (X : AlgebraicGeometry.Scheme) → CategoryTheory.Functor X.Modules X.Modules) (c : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → (W Y).comp (AlgebraicGeometry.Scheme.Modules.pullback f) ⟶ (AlgebraicGeometry.Scheme.Modules.pullback f).comp (W X)) (hcomp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (M : Z.Modules), CategoryTheory.CategoryStruct.comp ((c (CategoryTheory.CategoryStruct.comp f g)).app M) ((W X).map ((AlgebraicGeometry.Scheme.Modules.pullbackComp f g).inv.app M)) = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackComp f g).inv.app ((W Z).obj M)) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback f).map ((c g).app M)) ((c f).app ((AlgebraicGeometry.Scheme.Modules.pullback g).obj M)))) (hopen : ∀ {U Y : AlgebraicGeometry.Scheme} (j : U ⟶ Y) [AlgebraicGeometry.IsOpenImmersion j] (M : Y.Modules) [SheafOfModules.IsQuasicoherent M], CategoryTheory.IsIso ((c j).app M)) (hspec : ∀ {R S : CommRingCat} (φ : R ⟶ S) (M : (AlgebraicGeometry.Spec R).Modules) [SheafOfModules.IsQuasicoherent M], CategoryTheory.IsIso ((c (AlgebraicGeometry.Spec.map φ)).app M)) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (M : Y.Modules) [SheafOfModules.IsQuasicoherent M] : CategoryTheory.IsIso ((c f).app M)

Pullback comparisons are invertible if they are invertible on affine charts. Comparison maps W Y ⋙ f^* ⟶ f^* ⋙ W X that are compatible with the composition isomorphisms of pullback, and are invertible on quasicoherent modules along open immersions and along morphisms of affine spectra, are invertible on every quasicoherent module along every morphism of schemes.