Limits of complete separated topological rings

The full subcategory TauCeti.CompleteSeparatedTopCommRingCat has products and equalizers, and the inclusion into TopCommRingCat creates them. Both come from the closure instances proved here: CategoryTheory.Limits.hasLimitsOfShape_of_closedUnderLimits supplies the limits, and CategoryTheory.Limits.createsLimitsOfShapeFullSubcategoryInclusion their creation by the inclusion. The equalizer closure is where separatedness of the codomain is used: the equalizing locus is closed in a Hausdorff codomain, and a closed subring of a complete separated ring is complete separated (IsCompleteSeparated.of_isClosedEmbedding, in CompleteSeparated/Basic.lean).

Main results

• HasLimits CompleteSeparatedTopCommRingCat: all small limits, obtained from the products and equalizers below through has_limits_of_hasEqualizers_and_products.
• The inclusion into TopCommRingCat preserves all small limits, so taking underlying sets commutes with the limits defining a structure presheaf.
• The IsClosedUnderLimitsOfShape instances for discrete shapes and parallel pairs. These are what the inclusion needs in order to create the limits, so TauCeti.CompleteSeparatedTopCommRingCat acquires products and equalizers, and its inclusion acquires CreatesLimitsOfShape for both shapes, by synthesis alone — as the examples below record.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1 — the structure presheaf of §8.1 takes values in complete separated topological rings, and the sheaf condition of §8.2 is an equalizer of a pair of maps between products in that category, so both shapes are needed there.

instance TauCeti.TopCommRingCat.instIsClosedUnderLimitsOfShapeTopCommRingCatIsCompleteSeparatedDiscrete {β : Type v} : isCompleteSeparated.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete β)

Complete separated objects are closed under products in TopCommRingCat.

instance TauCeti.TopCommRingCat.instIsClosedUnderLimitsOfShapeTopCommRingCatIsCompleteSeparatedWalkingParallelPair : isCompleteSeparated.IsClosedUnderLimitsOfShape CategoryTheory.Limits.WalkingParallelPair

Complete separated objects are closed under equalizers: the equalizing locus of two morphisms into a Hausdorff codomain is a closed subring.

instance TauCeti.CompleteSeparatedTopCommRingCat.instHasLimits : CategoryTheory.Limits.HasLimits CompleteSeparatedTopCommRingCat

All small limits, from the products and equalizers above. This is what lets a limit be formed over a general shape rather than only over discrete shapes and parallel pairs; the structure presheaf of an adic space is a limit over a category of rational presentations, which is neither.

instance TauCeti.CompleteSeparatedTopCommRingCat.instPreservesLimitsFullSubcategoryTopCommRingCatIsCompleteSeparatedι : CategoryTheory.Limits.PreservesLimits TopCommRingCat.isCompleteSeparated.ι

The inclusion of complete separated topological rings preserves all small limits.