Two-open gluing of an actual scalar-extended pullback unit

The scalar-extended pullback unit is an isomorphism on a two-open union when it is an isomorphism on both opens and their intersection, provided extension of scalars preserves finite limits. This is an underived gluing step. The open-section isomorphism hypotheses are not established here.

theorem AlgebraicGeometry.Scheme.Modules.fixedBasePullbackOpenAfterExtension_isIso_sup {R A : CommRingCat} {Y Z : Scheme} (φ : R ⟶ Y.presheaf.obj (Opposite.op ⊤)) (f : Z ⟶ Y) (M : Y.Modules) (a : R ⟶ A) (ψ : A ⟶ Z.presheaf.obj (Opposite.op ⊤)) [CategoryTheory.Limits.PreservesFiniteLimits (ModuleCat.extendScalars (CommRingCat.Hom.hom a))] (U V : Y.Opens) (compat : CategoryTheory.CategoryStruct.comp φ (Hom.appTop f) = CategoryTheory.CategoryStruct.comp a ψ) [CategoryTheory.IsIso (fixedBasePullbackOpenAfterExtension φ f M a ψ U compat)] [CategoryTheory.IsIso (fixedBasePullbackOpenAfterExtension φ f M a ψ V compat)] [CategoryTheory.IsIso (fixedBasePullbackOpenAfterExtension φ f M a ψ (U ⊓ V) compat)] : CategoryTheory.IsIso (fixedBasePullbackOpenAfterExtension φ f M a ψ (U ⊔ V) compat)

If the actual extended pullback unit is invertible on two opens and their intersection, it is invertible on their union. The only algebraic hypothesis is finite-limit preservation of scalar extension.