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.

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.

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

@[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_monoid_with_one.add add_monoid_with_one.unary, add_assoc := _, zero := add_monoid_with_one.zero add_monoid_with_one.unary, zero_add := _, add_zero := _, nsmul := add_monoid_with_one.nsmul add_monoid_with_one.unary, 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 := _, int_cast := add_comm_group_with_one.int_cast._default add_monoid_with_one.nat_cast add_monoid_with_one.add uniform_space.completion.ring._proof_12 add_monoid_with_one.zero uniform_space.completion.ring._proof_13 uniform_space.completion.ring._proof_14 add_monoid_with_one.nsmul uniform_space.completion.ring._proof_15 uniform_space.completion.ring._proof_16 add_monoid_with_one.one uniform_space.completion.ring._proof_17 uniform_space.completion.ring._proof_18 add_comm_group.neg add_comm_group.sub uniform_space.completion.ring._proof_19 add_comm_group.zsmul uniform_space.completion.ring._proof_20 uniform_space.completion.ring._proof_21 uniform_space.completion.ring._proof_22 uniform_space.completion.ring._proof_23, nat_cast := add_monoid_with_one.nat_cast add_monoid_with_one.unary, one := add_monoid_with_one.one add_monoid_with_one.unary, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul (uniform_space.completion.has_mul α), mul_assoc := _, one_mul := _, mul_one := _, npow := monoid.npow._default add_monoid_with_one.one has_mul.mul uniform_space.completion.ring._proof_31 uniform_space.completion.ring._proof_32, 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) _

@[simp]

theorem uniform_space.completion.map_smul_eq_mul_coe (A : Type u_2) [ring A] [uniform_space A] [uniform_add_group A] [topological_ring A] (R : Type u_3) [comm_semiring R] [algebra R A] [has_uniform_continuous_const_smul R A] (r : R) :

uniform_space.completion.map (has_smul.smul r) = has_mul.mul ↑(⇑(algebra_map R A) r)

@[protected, instance]

noncomputable def uniform_space.completion.algebra (A : Type u_2) [ring A] [uniform_space A] [uniform_add_group A] [topological_ring A] (R : Type u_3) [comm_semiring R] [algebra R A] [has_uniform_continuous_const_smul R A] :

algebra R (uniform_space.completion A)

Equations

uniform_space.completion.algebra A R = {to_has_smul := uniform_space.completion.has_smul R A smul_zero_class.to_has_smul, to_ring_hom := {to_fun := (uniform_space.completion.coe_ring_hom.comp (algebra_map R A)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}

theorem uniform_space.completion.algebra_map_def (A : Type u_2) [ring A] [uniform_space A] [uniform_add_group A] [topological_ring A] (R : Type u_3) [comm_semiring R] [algebra R A] [has_uniform_continuous_const_smul R A] (r : R) :

⇑(algebra_map R (uniform_space.completion A)) r = ↑(⇑(algebra_map R A) r)

@[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 := _, int_cast := ring.int_cast uniform_space.completion.ring, nat_cast := ring.nat_cast uniform_space.completion.ring, one := ring.one uniform_space.completion.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul uniform_space.completion.ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow uniform_space.completion.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

@[protected, instance]

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

algebra R (uniform_space.completion R)

A shortcut instance for the common case

Equations

uniform_space.completion.algebra' R = uniform_space.completion.algebra R R

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 α))

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

dense_inducing.extend_ring_hom ue dr hf = {to_fun := _.extend ⇑f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}