mathlib documentation

topology.algebra.uniform_ring

Completion of topological rings: #

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.

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.

uniform_space.completion.extension_hom: extends a continuous ring morphism from R to a complete separated group S to completion R.
uniform_space.completion.map_ring_hom : promotes a continuous ring morphism from R to S into a continuous ring morphism from completion R to completion S.

@[protected, instance]

def uniform_space.completion.has_one (α : Type u_1) [ring α] [uniform_space α] :

has_one (uniform_space.completion α)

Equations

uniform_space.completion.has_one α = {one := ↑1}

@[protected, instance]

noncomputable def uniform_space.completion.has_mul (α : Type u_1) [ring α] [uniform_space α] :

has_mul (uniform_space.completion α)

Equations

uniform_space.completion.has_mul α = {mul := function.curry (_.extend (coe ∘ function.uncurry has_mul.mul))}

@[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 α] :

continuous (λ (p : uniform_space.completion α × uniform_space.completion α), (p.fst) * p.snd)

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]

noncomputable def uniform_space.completion.ring {α : Type u_1} [ring α] [uniform_space α] [topological_ring α] [uniform_add_group α] :

ring (uniform_space.completion α)

Equations

uniform_space.completion.ring = {add := add_comm_group.add uniform_space.completion.add_comm_group, add_assoc := _, zero := add_comm_group.zero uniform_space.completion.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul uniform_space.completion.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg uniform_space.completion.add_comm_group, sub := add_comm_group.sub uniform_space.completion.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul uniform_space.completion.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul (uniform_space.completion.has_mul α), mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow._default 1 has_mul.mul uniform_space.completion.ring._proof_15 uniform_space.completion.ring._proof_16, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}

def uniform_space.completion.coe_ring_hom {α : Type u_1} [ring α] [uniform_space α] [topological_ring α] [uniform_add_group α] :

α →+* uniform_space.completion α

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

Equations

uniform_space.completion.coe_ring_hom = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

theorem uniform_space.completion.continuous_coe_ring_hom {α : Type u_1} [ring α] [uniform_space α] [topological_ring α] [uniform_add_group α] :

continuous ⇑uniform_space.completion.coe_ring_hom

noncomputable def uniform_space.completion.extension_hom {α : Type u_1} [ring α] [uniform_space α] [topological_ring α] [uniform_add_group α] {β : Type u} [uniform_space β] [ring β] [uniform_add_group β] [topological_ring β] (f : α →+* β) (hf : continuous ⇑f) [complete_space β] [separated_space β] :

uniform_space.completion α →+* β

The completion extension as a ring morphism.

Equations

uniform_space.completion.extension_hom f hf = have hf' : continuous ⇑↑f, from hf, have hf : uniform_continuous ⇑f, from _, {to_fun := uniform_space.completion.extension ⇑f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

@[protected, instance]

def uniform_space.completion.top_ring_compl {α : Type u_1} [ring α] [uniform_space α] [topological_ring α] [uniform_add_group α] :

topological_ring (uniform_space.completion α)

noncomputable def uniform_space.completion.map_ring_hom {α : Type u_1} [ring α] [uniform_space α] [topological_ring α] [uniform_add_group α] {β : Type u} [uniform_space β] [ring β] [uniform_add_group β] [topological_ring β] (f : α →+* β) (hf : continuous ⇑f) :

uniform_space.completion α →+* uniform_space.completion β

The completion map as a ring morphism.

Equations

uniform_space.completion.map_ring_hom f hf = uniform_space.completion.extension_hom (uniform_space.completion.coe_ring_hom.comp f) _

@[protected, instance]

noncomputable def uniform_space.completion.comm_ring (R : Type u_2) [comm_ring R] [uniform_space R] [uniform_add_group R] [topological_ring R] :

comm_ring (uniform_space.completion R)

Equations

uniform_space.completion.comm_ring R = {add := ring.add uniform_space.completion.ring, add_assoc := _, zero := ring.zero uniform_space.completion.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul uniform_space.completion.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg uniform_space.completion.ring, sub := ring.sub uniform_space.completion.ring, sub_eq_add_neg := _, zsmul := ring.zsmul uniform_space.completion.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := ring.mul uniform_space.completion.ring, mul_assoc := _, one := ring.one uniform_space.completion.ring, one_mul := _, mul_one := _, npow := ring.npow uniform_space.completion.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

theorem uniform_space.ring_sep_rel (α : Type u_1) [comm_ring α] [uniform_space α] [uniform_add_group α] [topological_ring α] :

uniform_space.separation_setoid α = submodule.quotient_rel ⊥.closure

theorem uniform_space.ring_sep_quot (α : Type u) [r : comm_ring α] [uniform_space α] [uniform_add_group α] [topological_ring α] :

quotient (uniform_space.separation_setoid α) = (α ⧸ ⊥.closure)

def uniform_space.sep_quot_equiv_ring_quot (α : Type u_1) [r : comm_ring α] [uniform_space α] [uniform_add_group α] [topological_ring α] :

quotient (uniform_space.separation_setoid α) ≃ α ⧸ ⊥.closure

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

uniform_space.sep_quot_equiv_ring_quot α = quotient.congr_right _

@[protected, instance]

def uniform_space.comm_ring {α : Type u_1} [comm_ring α] [uniform_space α] [uniform_add_group α] [topological_ring α] :

comm_ring (quotient (uniform_space.separation_setoid α))

Equations

uniform_space.comm_ring = uniform_space.comm_ring._proof_1.mpr (ideal.quotient.comm_ring ⊥.closure)

@[protected, instance]

def uniform_space.topological_ring {α : Type u_1} [comm_ring α] [uniform_space α] [uniform_add_group α] [topological_ring α] :

topological_ring (quotient (uniform_space.separation_setoid α))