Finite limits in the category of opens

The opens of a topological space form a complete lattice, so as a category they have finite limits — the product of U and V is U ⊓ V, the terminal object is the whole space. Mathlib proves exactly this for any SemilatticeInf with an OrderTop, in CategoryTheory.Limits.CompleteLattice. Neither instance fires on TopologicalSpace.Opens X. This file supplies both, once.

Why the general instances do not fire

Opens X reaches its order twice over: through the bespoke TopologicalSpace.Opens.instPartialOrder, derived from SetLike, and through the one inside TopologicalSpace.Opens.instCompleteLattice, which is a CompleteLattice.copy built to be definitionally equal to it. Instance search unifies at reducible transparency, where the copy does not unfold, so OrderTop (Opens X) and BoundedOrder (Opens X) are not found — even though CompleteLattice, Order.Frame, SemilatticeInf, Lattice and Top all are.

Everything in CategoryTheory.Limits.CompleteLattice sits above OrderTop, so every limit instance on the site X.Opens is unreachable by default.

Naming the projections explicitly typechecks at default transparency, which is what orderTop and semilatticeInf below do. They are private: OrderTop extends Top, and Opens already has a Top, so a global OrderTop instance would create a data-carrying diamond that could silently break existing simp lemmas about ⊤. The bridge belongs inside the proofs, not in the instance graph.

What is exported — HasBinaryProducts and HasFiniteLimits — is Prop-valued, so no diamond is created by supplying it, and a later Mathlib instance of the same shape would be a harmless duplicate.

Why this matters here

SheafOfModules.Presentation.quasicoherentData — and therefore SheafOfModules.IsFinitePresentation.of_presentation — assumes [HasBinaryProducts C] for the site C. For a scheme X the site is X.Opens, so without these a global presentation cannot be turned into finite presentation on a scheme at all. Mathlib never instantiates quasicoherentData at a scheme site, which is why the gap has not surfaced upstream.

This file replaces two independent workarounds for the same gap — an earlier global hasBinaryProducts module and local instances in the generic Algebra/Category/ModuleCat/Sheaf/Presentation/Locality.lean argument — so that the topological specialization is supplied once rather than reconstructed by each geometric consumer.

This is DerivedAlgGeo-owned infrastructure. If Mathlib later exposes equivalent reachable lattice instances, this module can be simplified or deleted; contributing that fix upstream is useful but is not a prerequisite or maintenance obligation for this project.

instance TopologicalSpace.Opens.hasBinaryProducts (X : Type u) [TopologicalSpace X] : CategoryTheory.Limits.HasBinaryProducts (Opens X)

The opens of a topological space have binary products, given by intersection.

instance TopologicalSpace.Opens.hasFiniteLimits (X : Type u) [TopologicalSpace X] : CategoryTheory.Limits.HasFiniteLimits (Opens X)

The opens of a topological space have all finite limits.