Skip to content

Ringed spaces

Full ringed-space restriction, open-cover gluing and inverse-image factorization; scalar extension of module presheaves and sheaves; a concrete inverse-image module-presheaf Hom adjunction for arbitrary continuous maps; and root-exported continuous module-sheaf inverse image with a bundled linear Hom adjunction; and root-exported full-morphism module pushforward and explicit sheafified right-tensor pullback with their adjunction and native comparison; and identity/composition coherence, commutative-square push-pull mates, and horizontal and vertical pasting laws for those actual module functors; and constant-closed full ringed morphisms to local affine spectra from ring maps to global sections, with an all-affine-induced-map exclusion when such a map sends a maximal-ideal element to a unit of a nontrivial commutative target ring; and continuous-function sheaves, evaluation, functorial maps and open immersions of ringed spaces over topological commutative rings, with local stalks and corresponding locally ringed-space maps and open immersions over T1 topological fields; and finite-order chart-dependent scalar-function sheaves over nontrivially normed fields, with local stalks, smooth-to-finite comparison and a natural order-zero isomorphism to the existing continuous-function sheaf; and pullbacks along finite-regularity maps with locally ringed-space identity and composition laws and smooth/continuous endpoint naturality.

Quoted from the project description in formalization.yaml of FormalFrontier/ringed-spaces at commit 052015f0, Apache-2.0.

2 articles: 2 for headline results in its README whose declaration link names a declaration the scan finds in the linked file. Its other headline results are quoted where they stand.

Facts

From the repository and its formalization.yaml; the review and automation statements are quoted as written.

  • Repository: FormalFrontier/ringed-spaces, read at commit 052015f0 (2026-10-29).
  • Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
  • License: Apache-2.0.
  • Authors: Formal Frontier Agents.
  • Review status: “self-assessed”.
  • Review notes: “This metadata describes the library and does not self-certify independent acceptance of any new release, rights clearance, proof integrity or source coverage. Revision-specific review and release evidence is recorded separately.”
  • Automation: agent; framework “Agent-assisted Lean development”; tool setup “Agent-assisted Lean development with the repository-pinned Lean and mathlib revisions and kernel checking. Mathematical statements, attribution and release acceptance require independent review.”

Literature

The sources its formalization.yaml names, with their relationship to it.

Builds on

Headline results

Quoted from the headline results in README.md of FormalFrontier/ringed-spaces at commit 052015f0, Apache-2.0.

Restriction and indexed gluing. For X Y : RingedSpace.{u, u}, RingedSpace.isPullback_restrictInf identifies the literal intersection of two opens with the pullback of their full restrictions. Compatible morphisms on any J : Type u-indexed open cover glue uniquely to a full morphism X ⟶ Y, also when J and X are empty; OpenCover.existsUnique_gluing_of_intersection accepts literal-intersection compatibility. To compare morphisms glued on different covers, the cross-cover guide applies the existing restriction, gluing and full-morphism extensionality equations.

Inverse-image factorization. For Y : RingedSpace.{u, u} and a continuous map g : T ⟶ Y.carrier, T : TopCat.{u}, RingedSpace.inverseImage has literal carrier T and mathlib's inverse-image ring sheaf. Every full f : X ⟶ Y factors through it by toInverseImage_ofInverseImage; this is not a categorical ringed-space fiber product.

DefinitionContinuous-function spaces#

A topological commutative ring R gives a ContinuousFunctions.ringedSpace with stalk evaluation and full maps induced by continuous maps; open embeddings give ringed-space open immersions. For a T1 topological field K with a topological division-ring structure, its stalks are local and the maps and open immersions are locally ringed. See the continuous-functions guide.

Quoted from the headline results in README.md of FormalFrontier/ringed-spaces at commit 052015f0, Apache-2.0.

Lean

Read from the source at commit 052015f0, without running Lean.

Sources
LeanContinuousFunctions.ringedSpace

DefinitionFinite-regularity scalar functions#

For a charted space over a nontrivially normed field, FiniteRegularityFunctions.sheaf gives chosen-chart C^r scalar sections for r : ℕ and local stalks without an IsManifold or nonempty-carrier assumption. Smooth sections weaken to finite order; order zero is naturally isomorphic to the existing continuous scalar sheaf, including compatible stalk evaluation. Finite-C^r maps pull sections back and induce locally ringed-space morphisms compatible with identity, composition and both endpoint sheaf comparisons. For an open subtype with its induced charts, inclusion is an open immersion of locally ringed spaces; the restriction comparison satisfies both whole-arrow factorization equations. On a finite-order manifold with the self model 𝓘(𝕜, E), localBall restricts the chosen chart near any point to a diffeomorphism onto an entire positive-radius ball in the normed model space. Its locally ringed-space isomorphism identifies the restricted ambient scalar-function space with the ball's scalar-function space. See the finite-regularity guide.

Quoted from the headline results in README.md of FormalFrontier/ringed-spaces at commit 052015f0, Apache-2.0.

Lean

Read from the source at commit 052015f0, without running Lean.

Sources
LeanFiniteRegularityFunctions.sheaf

Indexed chart balls and smooth scalar functions. For any regularity n : ℕ∞ω, a self-model manifold has chart coordinates on a neighborhood diffeomorphic to an entire positive-radius model ball, with no dimension or completeness assumption. At smooth regularity ∞, the restricted ambient canonical smooth scalar locally ringed space is isomorphic to the canonical one on that ball; its whole arrows and full-composite germ and section evaluations are explicit. See the chart-ball guide.

Recovering smooth maps from scalar-preserving morphisms. For canonical smooth scalar presheaves on charted spaces over a nontrivially normed field, preservation of global field constants is equivalent to preservation on every open. The evaluation law identifies pullbacks of arbitrary sections with precomposition, without dimensionality or completeness requirements. For arbitrary canonical charted targets, scalar-preserving full morphisms with the same base map coincide; a separately supplied smoothness proof identifies the full induced morphism. If the target is an open subset of a finite-dimensional normed space over a complete field, smoothness of the base map follows; no dimensionality or manifold-regularity assumption is imposed on the source. For real scalars, preservation of constants follows from uniqueness of real ring endomorphisms; for complex scalars it is an explicit hypothesis. The scalar field and space carriers share a universe; source model universes are independent. See SmoothScalarReconstruction.

Holomorphic scalar sections. On open and nested-open subtypes of the finite-dimensional complex normed spaces, complex differentiability into complete complex normed spaces is equivalent to complex smoothness. For scalar-valued functions, the canonical smooth scalar sheaf accepts them directly as sections, with pointwise evaluation, restriction, and sheaf and locally ringed-space maps that precompose representatives on inverse-image opens. The chartwise version assumes a smooth manifold structure; it does not upgrade a merely holomorphic atlas or identify arbitrary structure sheaves. The scalar-sheaf API retains Mathlib's common-universe restriction.

Finite-dimensional complex atlas regularity. On a given charted space over a boundaryless complex model with finite-dimensional coordinates, differentiability of every ordered chart transition in model coordinates on its exact transition domain implies analytic manifold regularity at ω, hence complex smoothness at ∞. An order-one manifold structure also gives analytic regularity; neither construction replaces the original atlas. The hypotheses concern transitions, not an arbitrary structure sheaf. Apply isManifold_omega_of_differentiableOn_chartTransitions explicitly to the existing charts; importing the module does not install a global upgrade instance. See complex atlas regularity.

Mixed-compatible atlases. For two specified atlases on one topological space, membership of every ordered mixed chart transition in a structure groupoid gives both atlases' own regularity and equality of their maximal atlases, without assuming either is already regular. For mixed C^n transitions, the point-preserving comparison is a C^n diffeomorphism to a typed ULift copy retaining the entire second atlas. See CompatibleAtlases.

Compatible-atlas smooth scalar sheaves. Two specified smooth-compatible atlases on the same topology give an identity-base isomorphism between their canonical smooth scalar locally ringed spaces. The complete forward and inverse maps are smooth precomposition; their section-ring equivalences preserve values and scalar constants on every open, commute with restriction, and preserve germ evaluation. No dimension, completeness or separation hypothesis is needed. This compares canonical sheaves, not an arbitrary structure sheaf. See CompatibleAtlasSheaf.

Change of coefficient sheaves. A full natural map of commutative-ring presheaves induces a tensor-presheaf/restriction-of-scalars adjunction; with the required site sheafification witnesses, a full map of ring sheaves gives the sheafified adjunction. Right-factor tensor extension is naturally isomorphic to left-factor extension. See scalar extension and right-factor symmetry.

Continuous inverse images of modules. Neighborhood-colimit module presheaf inverse image and its genuine sheafification have bundled linear Hom adjunctions to the corresponding native pushforwards, with whole additive-sheaf comparisons; the additive comparison alone does not provide coefficient transport. See the presheaf and sheaf guides.

Full-morphism module functors. For any full f : X ⟶ Y, the original ring-sheaf structure map defines module pushforward; explicit sheafified right-tensor pullback is its left adjoint, with a comparison to native pullback. Composition and identity comparisons and the push–pull mate of any commutative square satisfy horizontal and vertical pasting laws; no general invertibility of that mate is claimed. See the pushforward, pullback, coherence and pasting guides.

Constant closed-point morphisms. For a commutative local ring R, any ring map from R to global sections of a ringed space constructs a full morphism with constant closed-point base. For same-universe commutative R, S, [Nontrivial S], and a map alpha : R →+* S sending an element of IsLocalRing.maximalIdeal R to a unit, this morphism Spec S ⟶ Spec R differs from every affine-induced full morphism. Neither construction asserts a scheme morphism. See the constructor and non-affineness guides.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.