Build reusable G-site/G-ringed infrastructure and its rigid instantiation

[dagurtomas]

Goal

Define both:

1. the reusable project-level infrastructure for admissible G-sites and G-ringed spaces, using mathlib's category-theoretic sites API; and
2. its rigid-analytic instantiation: the admissible G-topology and locally G-ringed structure needed for rigid spaces.

This replaces hand-written cover, restriction, gluing, stalk, and germ fields such as those in the closed prototype PR #33. The reusable layer should be shared with the Berkovich analytic-domain instantiation in #38; it must not duplicate abstractions already supplied by mathlib.

Ownership boundary

This issue owns:

• the minimal reusable adapter layer, beyond mathlib's existing APIs, for domain sites equipped with points;
• sheaves of rings or K-algebras on such sites;
• admissible-neighborhood stalks, germs, local-ring conditions, and local morphisms;
• identity, composition, and category packaging for G-ringed and locally G-ringed spaces;
• the rigid admissible-open category, rigid covering families, and their instantiation of that layer.

This issue does not own:

• Berkovich AnalyticDomain or its domain-specific admissible covers: Instantiate the G-site framework for Berkovich analytic domains #38;
• the affinoid Berkovich analytic structure sheaf: Construct the affinoid Berkovich structure sheaf and local stalks #40;
• the ordinary locally ringed topological presentation of Berkovich spaces: Implement the ordinary Berkovich locally ringed core #37.

#38 should instantiate the reusable layer from this issue, not independently reimplement it. #40 should supply analytic sections to that instantiated site and derive its ordinary-open sheaf from the resulting analytic structure.

Required mathlib API

Build on:

• CategoryTheory.GrothendieckTopology and CategoryTheory.Sieve;
• CategoryTheory.Presieve and CategoryTheory.Pretopology;
• CategoryTheory.Pretopology.toGrothendieck;
• CategoryTheory.Sheaf J CommRingCat (or an appropriate category of commutative K-algebras);
• Presieve.IsSheaf / Presheaf.IsSheaf;
• the continuous-functor/site APIs for morphisms where applicable;
• Opens.grothendieckTopology, Opens.pretopology, and mathlib's ordinary LocallyRingedSpace as reference implementations, while keeping an admissible topology distinct from the ordinary topology of point sets.

Reusable G-site/G-ringed-space scope

1. Identify the minimal inputs needed from a thin category of domains and its admissible covering Pretopology; do not wrap or restate mathlib's topology axioms without need.
2. Package a G-ringed-space-style object from such a site and a mathlib sheaf of commutative rings or commutative K-algebras.
3. Derive sections and restriction maps from the sheaf functor and gluing from its IsSheaf property.
4. Define stalks as colimits over admissible neighborhoods of a point, or through a mathematically equivalent site-point construction, with canonical germ maps.
5. Define the local-ring condition and morphisms inducing local homomorphisms on stalks.
6. Provide identity, composition, and category structures reusable by the rigid and Berkovich instantiations.

Rigid admissible-site instantiation

1. Define the small category, or small basis category, of rigid admissible opens/domains with morphisms given by admissible inclusions.
2. Provide pullbacks corresponding to intersections/base change.
3. Encode rigid admissible covering families as a Precoverage or preferably a Pretopology.
4. Prove the isomorphism, pullback-stability, and transitivity axioms from the actual rigid-cover definitions.
5. Define the resulting GrothendieckTopology through the reusable layer and Pretopology.toGrothendieck.
6. Prove bridge lemmas between indexed covering families and membership of the generated Presieve/Sieve in the topology. These lemmas should support the comparator's AdmissibleOpen.IsCover API with index types in Type (u + 1).
7. Expose adapters for rigid StructureSheaf.Sections, restrictions, germs, stalks, and AnalyticMorphismData without changing comparator declarations prematurely.

Acceptance criteria

• The reusable layer is used by the rigid instantiation and is suitable for direct reuse in Instantiate the G-site framework for Berkovich analytic domains #38.
• No duplicate of mathlib's Grothendieck-topology axioms.
• No custom sheaf-gluing field where mathlib's Sheaf/IsSheaf API applies.
• No arbitrary stored stalks or germ maps.
• No finite-subcover definition masquerading as admissibility.
• Universe levels support the comparator API.
• Production modules contain no sorry and are directly imported by Rigid.lean.
• Include focused examples showing that indexed rigid admissible covers yield covering sieves and that a structure sheaf satisfies the corresponding sheaf condition.
• ./scripts/check_root_imports.sh, ./scripts/check_challenge_development.sh, and lake build Rigid pass.

Dependencies and follow-up

The rational/Laurent cover foundations in Rigid/AffinoidSpectrum/RationalCover.lean may provide the first generating covering families. Issue #22 remains blocked until this site and locally G-ringed-space layer is available. #38 is the corresponding Berkovich-domain instantiation; #40 supplies its affinoid analytic sheaf. Genuine local-affinoid atlases and canonical affinoid rigid spaces remain subsequent work in #22 and #25.