The uniform structure on a subring

A subring carries the subspace uniformity, and the two facts one needs about it hold already for the underlying subobject: AddSubgroup.isUniformAddGroup gives the additive group structure at S.toAddSubgroup, and a countably generated uniformity is inherited by any subtype. Neither is keyed on Subring, so typeclass search reaches neither at ↥S.

That is the same keying gap TauCeti.Topology.Algebra.IsUniformGroup.Submodule fills for submodules, and this file is its Subring counterpart. Both are uniform-space facts, which is why they live beside each other here rather than in TauCeti.Topology.Algebra.Ring.Subring, whose subject is the topological structure of a subring.

Only NonAssocRing is needed: that is what Subring itself asks, and the proofs use nothing but the additive subgroup and the subtype uniformity.

Main results

• Subring.isUniformAddGroup: ↥S is a uniform additive group.
• Subring.isCountablyGenerated_uniformity: ↥S inherits a countably generated uniformity.

The consumer

Both are wanted at the ring of definition of a rational localisation, where TauCeti.Huber.PairOfDefinition.isStronglyNoetherian_completion needs the completion of a subring to be a uniform additive group with countably generated uniformity.

instance Subring.isUniformAddGroup {R : Type u_1} [NonAssocRing R] [UniformSpace R] [IsUniformAddGroup R] (S : Subring R) : IsUniformAddGroup ↥S

A subring of a uniform additive group is a uniform additive group. This is Mathlib's AddSubgroup.isUniformAddGroup at S.toAddSubgroup, which typeclass search does not reach from a Subring.

instance Subring.isCountablyGenerated_uniformity {R : Type u_1} [NonAssocRing R] [UniformSpace R] [(uniformity R).IsCountablyGenerated] (S : Subring R) : (uniformity ↥S).IsCountablyGenerated

A subring inherits a countably generated uniformity, its uniformity being the one comapped along the inclusion.