Products and equalizers of topological commutative rings

Mathlib's TopCommRingCat carries no limit constructions at all. This file provides the two shapes the sheaf condition consumes — products and equalizers — by exhibiting the explicit cones: the pointwise ring with the product topology, and the agreement subring with the subspace topology.

The forgetful functor to CommRingCat does not create these limits in the technical sense: it does not reflect them, since the topology on a cone apex is not determined by the underlying ring — the same reason TopCat's own forgetful functor does not create products or arbitrary limits (it does create some shapes, such as terminal objects). What is true, and what later files use, is that the constructions below have the expected underlying rings, which is plain from their statements.

Main definitions

• TauCeti.TopCommRingCat.piFan and TauCeti.TopCommRingCat.piFanIsLimit : the product of a family, as the pointwise ring under the product topology.
• TauCeti.TopCommRingCat.equalizerFork and TauCeti.TopCommRingCat.equalizerForkIsLimit : the equalizer of a parallel pair, as the agreement subring under the subspace topology.
• The resulting HasProducts and HasEqualizers instances.

The equalizer fork's inclusion is, as a function, the subtype coercion of the agreement subring, and by rfl; consumers state closedness of its range against the coercion and let that definitional equality carry it to the categorical morphism, rather than going through a named lemma here.

The closedness of the agreement subring over a Hausdorff codomain — what will keep equalizers of complete separated rings complete — is Mathlib's isClosed_eq applied to the two morphisms' continuity fields; consumers use it directly rather than through a named specialization here.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1 — the sheaf condition of §8.2 is stated in complete Hausdorff topological rings, whose products and equalizers this file prepares.
• The constructions adapt Mathlib's to continuous ring homomorphisms: piFan/piFanIsLimit follow TopCat.piFan/TopCat.piFanIsLimit (Mathlib/Topology/Category/TopCat/Limits/Products.lean) on the topological side and CommRingCat.piFan/CommRingCat.piFanIsLimit on the algebraic side, and equalizerFork/equalizerForkIsLimit follow CommRingCat.equalizerFork/ CommRingCat.equalizerForkIsLimit (Mathlib/Algebra/Category/Ring/Constructions.lean), with the topology carried through each construction.

def TauCeti.TopCommRingCat.piFan {β : Type v} (f : β → TopCommRingCat) : CategoryTheory.Limits.Fan f

The explicit product fan of a family of topological commutative rings: the pointwise ring under the product topology, with the evaluation projections.

Equations

• TauCeti.TopCommRingCat.piFan f = CategoryTheory.Limits.Fan.mk (TopCommRingCat.of ((b : β) → (f b).α)) fun (b : β) => ⟨Pi.evalRingHom (fun (b : β) => (f b).α) b, ⋯⟩

@[simp]

theorem TauCeti.TopCommRingCat.piFan_π_app {β : Type v} (f : β → TopCommRingCat) (X : CategoryTheory.Discrete β) : (piFan f).π.app X = ⟨Pi.evalRingHom (fun (b : β) => (f b).α) X.as, ⋯⟩

@[simp]

theorem TauCeti.TopCommRingCat.piFan_pt {β : Type v} (f : β → TopCommRingCat) : (piFan f).pt = TopCommRingCat.of ((b : β) → (f b).α)

def TauCeti.TopCommRingCat.piFanIsLimit {β : Type v} (f : β → TopCommRingCat) : CategoryTheory.Limits.IsLimit (piFan f)

The pointwise ring under the product topology is the product in TopCommRingCat.

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.TopCommRingCat.instHasProductTopCommRingCat_tauCeti {β : Type v} (f : β → TopCommRingCat) : CategoryTheory.Limits.HasProduct f

instance TauCeti.TopCommRingCat.instHasProductsTopCommRingCat_tauCeti : CategoryTheory.Limits.HasProducts TopCommRingCat

def TauCeti.TopCommRingCat.equalizerFork {R S : TopCommRingCat} (f g : R ⟶ S) : CategoryTheory.Limits.Fork f g

The explicit equalizer fork of a parallel pair: the agreement subring RingHom.eqLocus under the subspace topology.

Equations

• TauCeti.TopCommRingCat.equalizerFork f g = CategoryTheory.Limits.Fork.ofι ⟨((↑f).eqLocus ↑g).subtype, ⋯⟩ ⋯

@[simp]

theorem TauCeti.TopCommRingCat.equalizerFork_π_app {R S : TopCommRingCat} (f g : R ⟶ S) (X : CategoryTheory.Limits.WalkingParallelPair) : (equalizerFork f g).π.app X = CategoryTheory.Limits.WalkingParallelPair.rec (motive := fun (t : CategoryTheory.Limits.WalkingParallelPair) => X = t → (TopCommRingCat.of ↥((↑f).eqLocus ↑g) ⟶ (CategoryTheory.Limits.parallelPair f g).obj X)) (fun (h : X = CategoryTheory.Limits.WalkingParallelPair.zero) => ⋯ ▸ ⟨((↑f).eqLocus ↑g).subtype, ⋯⟩) (fun (h : X = CategoryTheory.Limits.WalkingParallelPair.one) => ⋯ ▸ CategoryTheory.CategoryStruct.comp ⟨((↑f).eqLocus ↑g).subtype, ⋯⟩ f) X ⋯

@[simp]

theorem TauCeti.TopCommRingCat.equalizerFork_pt {R S : TopCommRingCat} (f g : R ⟶ S) : (equalizerFork f g).pt = TopCommRingCat.of ↥((↑f).eqLocus ↑g)

def TauCeti.TopCommRingCat.equalizerForkIsLimit {R S : TopCommRingCat} (f g : R ⟶ S) : CategoryTheory.Limits.IsLimit (equalizerFork f g)

The agreement subring under the subspace topology is the equalizer in TopCommRingCat.

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.TopCommRingCat.instHasLimitWalkingParallelPairTopCommRingCatParallelPair_tauCeti {R S : TopCommRingCat} (f g : R ⟶ S) : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g)

instance TauCeti.TopCommRingCat.instHasEqualizersTopCommRingCat_tauCeti : CategoryTheory.Limits.HasEqualizers TopCommRingCat