Pushforward and restriction across an open square #

For any scheme morphism f : X ⟶ Y and open U of Y, compare the two ways to push forward a module sheaf and restrict it across the square

  f ⁻¹ᵁ U  ──(f ⁻¹ᵁ U).ι──>  X
     │                        │
  f ∣_ U                      f
     │                        │
     U   ─────U.ι─────────>   Y

The comparison is independent of finiteness, affineness, and coherence.

Why this is the whole geometric content #

Both composites send an open V of U to the preimage of V under f, viewed in X — image_morphismRestrict_preimage is exactly that equality, and it is at the pin. Opens is a poset, so a natural transformation between functors into it is determined by nothing at all: agreement on objects is the isomorphism, and NatIso.ofComponents discharges naturality because the naturality squares live in a subsingleton.

The comparison of module sheaves, object by object #

pushforwardRestrictIso compares the resulting module sheaves for one M. pushforwardRestrictNatIso assembles these isomorphisms into a functor comparison; its naturality is the naturality of a sheaf morphism on the same transported sections. The coherent pushforward chart argument consumes the object component.

What the comparison rests on #

Both sides have the same sections: Γ(M, f ⁻¹ᵁ (U.ι ''ᵁ V)) and Γ(M, (f ⁻¹ᵁ U).ι ''ᵁ ((f ∣_ U) ⁻¹ᵁ V)) are rfl-equal to the two composites, and the opens are equal by image_morphismRestrict_preimage — the equality this file's first half packages. So the comparison map is that transport, restrictSquareSections.

What has to be proved is that the transport is linear, and this is the "equality of sheaf-of-rings data" the earlier version of this file left open. It decomposes into four steps, three of which are definitional:

each side's scalar action unfolds to an action through Scheme.Hom.app, by rfl;
the open immersion's Scheme.Hom.appIso is the identity — Scheme.Opens.ι_appIso, and this one is not definitional, it needs the rewrite;
the transport is semilinear over X's structure sheaf — Scheme.Modules.map_smul;
the two structure-sheaf maps differ by exactly that transport — morphismRestrict_app, whose eqToHom is the same one, direction included.

Why the naturality square is written with explicit morphisms #

presheaf_map_square_eq is applied at its four opens morphisms spelled out, and that is the whole reason this file needs no maxHeartbeats raise. Left as _, they are metavariables Lean has to solve by unifying against a goal that also carries the instances-transparency defect — which costs more than twenty times the default budget and buys nothing, since the morphisms are determined and can simply be written down. Supplied explicitly, the square closes in one exact, in seconds.

The lesson generalises, and it is the opposite of the reflex: a large heartbeat bump here meant the statement was underspecified, not that the proof was hard.

presheaf_map_square_eq is stated separately because in a clean context its rewrites fire, while at the use site only exact is available — exact unifies up to defeq and never has to match syntactically, which is what the defective goal rules out.

The functor comparison is built from these explicit objectwise components. The mate of the independent pushforward/restriction comparison in the open-immersion direction is the direct pushforward-composite comparison. Pasting the five factors of the independent pullback iso gives the same pushforward-composite comparison under conjugation; the iterated-mate identity then identifies its horizontal mate with the independent comparison. The actual pullback/pushforward units obey the resulting natural open-square unit equation. Its ordinary-section form evaluates the pushforward comparison as restrictSquareSections; this is distinct from slice-site pullbackOverIso transport and does not assert relative base-change invertibility.