mathlib3 documentation

topology.algebra.uniform_ring

Completion of topological rings: #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This files endows the completion of a topological ring with a ring structure. More precisely the instance uniform_space.completion.ring builds a ring structure on the completion of a ring endowed with a compatible uniform structure in the sense of uniform_add_group. There is also a commutative version when the original ring is commutative. Moreover, if a topological ring is an algebra over a commutative semiring, then so is its uniform_space.completion.

The last part of the file builds a ring structure on the biggest separated quotient of a ring.

Main declarations: #

Beyond the instances explained above (that don't have to be explicitly invoked), the main constructions deal with continuous ring morphisms.

TODO: Generalise the results here from the concrete completion to any abstract_completion.

@[norm_cast]
theorem uniform_space.completion.coe_one (α : Type u_1) [ring α] [uniform_space α] :
1 = 1
@[norm_cast]
theorem uniform_space.completion.coe_mul {α : Type u_1} [ring α] [uniform_space α] [topological_ring α] (a b : α) :
(a * b) = a * b
theorem uniform_space.completion.continuous.mul {α : Type u_1} [ring α] [uniform_space α] [topological_ring α] [uniform_add_group α] {β : Type u_2} [topological_space β] {f g : β uniform_space.completion α} (hf : continuous f) (hg : continuous g) :
continuous (λ (b : β), f b * g b)
@[protected, instance]
Equations

The map from a uniform ring to its completion, as a ring homomorphism.

Equations

The completion extension as a ring morphism.

Equations
@[protected, instance]

A shortcut instance for the common case

Equations

Given a topological ring α equipped with a uniform structure that makes subtraction uniformly continuous, get an equivalence between the separated quotient of α and the quotient ring corresponding to the closure of zero.

Equations
noncomputable def dense_inducing.extend_ring_hom {α : Type u_1} [uniform_space α] [semiring α] {β : Type u_2} [uniform_space β] [semiring β] [topological_semiring β] {γ : Type u_3} [uniform_space γ] [semiring γ] [topological_semiring γ] [t2_space γ] [complete_space γ] {i : α →+* β} {f : α →+* γ} (ue : uniform_inducing i) (dr : dense_range i) (hf : uniform_continuous f) :
β →+* γ

The dense inducing extension as a ring homomorphism.

Equations