Pullback of modules and inverse image of the underlying abelian sheaves

Let g : Y ⟶ X be a morphism of schemes and M a sheaf of modules on X. Pushforward of sheaves of modules along g and pushforward of abelian sheaves along g agree on underlying abelian sheaves. Taking mates under the two pullback--pushforward adjunctions gives a comparison g⁻¹ M ⟶ g^* M from the inverse image of the underlying abelian sheaf of M to the underlying abelian sheaf of the module pullback, natural in M.

Main declarations

• AlgebraicGeometry.Scheme.Hom.toSheafPullbackComparison: the comparison g⁻¹ M ⟶ g^* M;
• AlgebraicGeometry.Scheme.Hom.toSheafPullbackComparison_unit: the unit of the module pullback is the unit of the abelian inverse image followed by the comparison.

noncomputable def AlgebraicGeometry.Scheme.Hom.toSheafPullbackComparison {X Y : Scheme} (g : Y ⟶ X) : (TauCeti.AlgebraicGeometry.Scheme.Modules.toSheaf X).comp ((TopologicalSpace.Opens.map g.base).sheafPullback AddCommGrpCat (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Y)) ⟶ (Modules.pullback g).comp (TauCeti.AlgebraicGeometry.Scheme.Modules.toSheaf Y)

The comparison g⁻¹ M ⟶ g^* M from the inverse image of the underlying abelian sheaf of M to the underlying abelian sheaf of its pullback as a sheaf of modules: the mate of the equality of the underlying abelian sheaves of g_* N computed in both ways.

theorem AlgebraicGeometry.Scheme.Hom.toSheafPullbackComparison_unit {X Y : Scheme} (g : Y ⟶ X) (M : X.Modules) : (TauCeti.AlgebraicGeometry.Scheme.Modules.toSheaf X).map ((Modules.pullbackPushforwardAdjunction g).unit.app M) = CategoryTheory.CategoryStruct.comp (((TopologicalSpace.Opens.map g.base).sheafAdjunctionContinuous AddCommGrpCat (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Y)).unit.app ((TauCeti.AlgebraicGeometry.Scheme.Modules.toSheaf X).obj M)) (((TopologicalSpace.Opens.map g.base).sheafPushforwardContinuous AddCommGrpCat (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Y)).map ((toSheafPullbackComparison g).app M))

On sections, the unit of the module pullback is the abelian unit followed by the comparison g⁻¹ M ⟶ g^* M.