The action on top sections of a module-sheaf pushforward

For an arbitrary scheme morphism f : Z ⟶ Y, the action of Γ(Y, ⊤) on top sections of f_* M is restriction of the native Γ(Z, ⊤)-action along f.appTop. The carrier identification explicitly uses f ⁻¹ᵁ ⊤ = ⊤. This is an underived identity; no affineness or quasi-coherence is needed.

theorem AlgebraicGeometry.Scheme.Modules.pushforward_obj_obj_top {Z Y : Scheme} (f : Z ⟶ Y) (M : Z.Modules) : ((pushforward f).obj M).presheaf.obj (Opposite.op ⊤) = M.presheaf.obj (Opposite.op ⊤)

Top sections of a pushforward are top sections of the original sheaf, as abelian groups. This records the preimage-of-top transport; the two module actions are compared separately in pushforward_smul_appTop.

theorem AlgebraicGeometry.Scheme.Modules.pushforward_smul_appTop {Z Y : Scheme} (f : Z ⟶ Y) (M : Z.Modules) (a : ↑(Y.presheaf.obj (Opposite.op ⊤))) (m : ↑(((pushforward f).obj M).presheaf.obj (Opposite.op ⊤))) : a • m = (CommRingCat.Hom.hom (Hom.appTop f)) a • have this := m; this

The Γ(Y, ⊤)-action on Γ(f_* M, ⊤) is the native action on Γ(M, ⊤) after applying f.appTop. The show identifies the underlying section carriers; pushforward_obj_obj_top records the top-open equality.