Completion of topological rings:

This file endows the completion of a topological ring with a ring structure. More precisely, the instance UniformSpace.Completion.ring builds a ring structure on the completion of a ring endowed with a compatible uniform structure in the sense of IsUniformAddGroup. 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 UniformSpace.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.

• UniformSpace.Completion.extensionHom: extends a continuous ring morphism from R to a complete separated group S to Completion R.
• UniformSpace.Completion.mapRingHom: 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 AbstractCompletion.

instance UniformSpace.Completion.one (α : Type u_1) [Ring α] [UniformSpace α] : One (Completion α)

Equations

• UniformSpace.Completion.one α = { one := ↑1 }

instance UniformSpace.Completion.mul (α : Type u_1) [Ring α] [UniformSpace α] : Mul (Completion α)

Equations

• UniformSpace.Completion.mul α = { mul := Function.curry (⋯.extend (UniformSpace.Completion.coe' ∘ Function.uncurry fun (x1 x2 : α) => x1 * x2)) }

theorem UniformSpace.Completion.coe_one (α : Type u_1) [Ring α] [UniformSpace α] : ↑1 = 1

@[simp]

theorem UniformSpace.Completion.coe_eq_one_iff (α : Type u_1) [Ring α] [UniformSpace α] [T0Space α] {x : α} : ↑x = 1 ↔ x = 1

theorem UniformSpace.Completion.coe_mul {α : Type u_1} [Ring α] [UniformSpace α] [IsTopologicalRing α] (a b : α) : ↑(a * b) = ↑a * ↑b

instance UniformSpace.Completion.instContinuousMul {α : Type u_1} [Ring α] [UniformSpace α] [IsTopologicalRing α] [IsUniformAddGroup α] : ContinuousMul (Completion α)

instance UniformSpace.Completion.ring {α : Type u_1} [Ring α] [UniformSpace α] [IsTopologicalRing α] [IsUniformAddGroup α] : Ring (Completion α)

Equations

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

def UniformSpace.Completion.coeRingHom {α : Type u_1} [Ring α] [UniformSpace α] [IsTopologicalRing α] [IsUniformAddGroup α] : α →+* Completion α

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

Equations

• UniformSpace.Completion.coeRingHom = { toFun := UniformSpace.Completion.coe', map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem UniformSpace.Completion.continuous_coeRingHom {α : Type u_1} [Ring α] [UniformSpace α] [IsTopologicalRing α] [IsUniformAddGroup α] : Continuous ⇑coeRingHom

def UniformSpace.Completion.extensionHom {α : Type u_1} [Ring α] [UniformSpace α] [IsTopologicalRing α] [IsUniformAddGroup α] {β : Type u} [UniformSpace β] [Ring β] [IsUniformAddGroup β] [IsTopologicalRing β] (f : α →+* β) (hf : Continuous ⇑f) [CompleteSpace β] [T0Space β] : Completion α →+* β

The completion extension as a ring morphism.

Equations

• UniformSpace.Completion.extensionHom f hf = { toFun := UniformSpace.Completion.extension ⇑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem UniformSpace.Completion.extensionHom_coe {α : Type u_1} [Ring α] [UniformSpace α] [IsTopologicalRing α] [IsUniformAddGroup α] {β : Type u} [UniformSpace β] [Ring β] [IsUniformAddGroup β] [IsTopologicalRing β] (f : α →+* β) (hf : Continuous ⇑f) [CompleteSpace β] [T0Space β] (a : α) : (extensionHom f hf) ↑a = f a

instance UniformSpace.Completion.topologicalRing {α : Type u_1} [Ring α] [UniformSpace α] [IsTopologicalRing α] [IsUniformAddGroup α] : IsTopologicalRing (Completion α)

def UniformSpace.Completion.mapRingHom {α : Type u_1} [Ring α] [UniformSpace α] [IsTopologicalRing α] [IsUniformAddGroup α] {β : Type u} [UniformSpace β] [Ring β] [IsUniformAddGroup β] [IsTopologicalRing β] (f : α →+* β) (hf : Continuous ⇑f) : Completion α →+* Completion β

The completion map as a ring morphism.

Equations

• UniformSpace.Completion.mapRingHom f hf = UniformSpace.Completion.extensionHom (UniformSpace.Completion.coeRingHom.comp f) ⋯

@[simp]

theorem UniformSpace.Completion.mapRingHom_apply {α : Type u_1} [Ring α] [UniformSpace α] [IsTopologicalRing α] [IsUniformAddGroup α] {β : Type u} [UniformSpace β] [Ring β] [IsUniformAddGroup β] [IsTopologicalRing β] (f : α →+* β) (hf : Continuous ⇑f) {x : Completion α} : (mapRingHom f hf) x = Completion.map (⇑f) x

theorem UniformSpace.Completion.coe_mapRingHom {α : Type u_1} [Ring α] [UniformSpace α] [IsTopologicalRing α] [IsUniformAddGroup α] {β : Type u} [UniformSpace β] [Ring β] [IsUniformAddGroup β] [IsTopologicalRing β] (f : α →+* β) (hf : Continuous ⇑f) : ⇑(mapRingHom f hf) = Completion.map ⇑f

theorem UniformSpace.Completion.mapRingHom_coe {α : Type u_1} [Ring α] [UniformSpace α] [IsTopologicalRing α] [IsUniformAddGroup α] {β : Type u} [UniformSpace β] [Ring β] [IsUniformAddGroup β] [IsTopologicalRing β] {f : α →+* β} (hf : Continuous ⇑f) (a : α) : (mapRingHom f hf) ↑a = ↑(f a)

theorem UniformSpace.Completion.mapRingHom_comp {α : Type u_1} [Ring α] [UniformSpace α] [IsTopologicalRing α] [IsUniformAddGroup α] {β : Type u} [UniformSpace β] [Ring β] [IsUniformAddGroup β] [IsTopologicalRing β] {f : α →+* β} {γ : Type u_2} [UniformSpace γ] [Ring γ] [IsUniformAddGroup γ] [IsTopologicalRing γ] {g : β →+* γ} (hg : Continuous ⇑g) (hf : Continuous ⇑f) : (mapRingHom g hg).comp (mapRingHom f hf) = mapRingHom (g.comp f) ⋯

@[simp]

theorem UniformSpace.Completion.mapRingHom_id {α : Type u_1} [Ring α] [UniformSpace α] [IsTopologicalRing α] [IsUniformAddGroup α] : mapRingHom (RingHom.id α) ⋯ = RingHom.id (Completion α)

def UniformSpace.Completion.mapRingEquiv {α : Type u_1} [Ring α] [UniformSpace α] [IsTopologicalRing α] [IsUniformAddGroup α] {β : Type u} [UniformSpace β] [Ring β] [IsUniformAddGroup β] [IsTopologicalRing β] (f : α ≃+* β) (hf : Continuous ⇑f) (hf' : Continuous ⇑f.symm) : Completion α ≃+* Completion β

A ring isomorphism α ≃+* β between uniform rings, uniformly continuous in both directions, lifts to a ring isomorphism between corresponding uniform space completions.

Equations

• UniformSpace.Completion.mapRingEquiv f hf hf' = RingEquiv.ofRingHom (UniformSpace.Completion.mapRingHom f.toRingHom hf) (UniformSpace.Completion.mapRingHom f.symm.toRingHom hf') ⋯ ⋯

@[simp]

theorem UniformSpace.Completion.mapRingEquiv_apply {α : Type u_1} [Ring α] [UniformSpace α] [IsTopologicalRing α] [IsUniformAddGroup α] {β : Type u} [UniformSpace β] [Ring β] [IsUniformAddGroup β] [IsTopologicalRing β] (f : α ≃+* β) (hf : Continuous ⇑f) (hf' : Continuous ⇑f.symm) (a : Completion α) : (mapRingEquiv f hf hf') a = Completion.map (⇑f) a

@[simp]

theorem UniformSpace.Completion.mapRingEquiv_symm_apply {α : Type u_1} [Ring α] [UniformSpace α] [IsTopologicalRing α] [IsUniformAddGroup α] {β : Type u} [UniformSpace β] [Ring β] [IsUniformAddGroup β] [IsTopologicalRing β] (f : α ≃+* β) (hf : Continuous ⇑f) (hf' : Continuous ⇑f.symm) (a : Completion β) : (mapRingEquiv f hf hf').symm a = Completion.map (⇑f.symm) a

@[simp]

theorem UniformSpace.Completion.map_smul_eq_mul_coe (A : Type u_2) [Ring A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] (R : Type u_3) [CommSemiring R] [Algebra R A] [UniformContinuousConstSMul R A] (r : R) : (Completion.map fun (x : A) => r • x) = fun (x : Completion A) => ↑((algebraMap R A) r) * x

instance UniformSpace.Completion.algebra (A : Type u_2) [Ring A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] (R : Type u_3) [CommSemiring R] [Algebra R A] [UniformContinuousConstSMul R A] : Algebra R (Completion A)

Equations

• UniformSpace.Completion.algebra A R = { toSMul := UniformSpace.Completion.instSMul R A, algebraMap := UniformSpace.Completion.coeRingHom.comp (algebraMap R A), commutes' := ⋯, smul_def' := ⋯ }

theorem UniformSpace.Completion.algebraMap_def (A : Type u_2) [Ring A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] (R : Type u_3) [CommSemiring R] [Algebra R A] [UniformContinuousConstSMul R A] (r : R) : (algebraMap R (Completion A)) r = ↑((algebraMap R A) r)

instance UniformSpace.Completion.commRing (R : Type u_2) [CommRing R] [UniformSpace R] [IsUniformAddGroup R] [IsTopologicalRing R] : CommRing (Completion R)

Equations

• UniformSpace.Completion.commRing R = { toRing := UniformSpace.Completion.ring, mul_comm := ⋯ }

instance UniformSpace.Completion.algebra' (R : Type u_2) [CommRing R] [UniformSpace R] [IsUniformAddGroup R] [IsTopologicalRing R] : Algebra R (Completion R)

A shortcut instance for the common case

Equations

• UniformSpace.Completion.algebra' R = inferInstance

theorem UniformSpace.inseparableSetoid_ring (α : Type u_2) [Ring α] [TopologicalSpace α] [IsTopologicalRing α] : inseparableSetoid α = Submodule.quotientRel ⊥.closure

def UniformSpace.sepQuotHomeomorphRingQuot (α : Type u_2) [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] : SeparationQuotient α ≃ₜ α ⧸ ⊥.closure

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

Equations

• UniformSpace.sepQuotHomeomorphRingQuot α = { toEquiv := Quotient.congrRight ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

instance UniformSpace.commRing {α : Type u_1} [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] : CommRing (SeparationQuotient α)

Equations

• UniformSpace.commRing = (UniformSpace.sepQuotHomeomorphRingQuot α).commRing

def UniformSpace.sepQuotRingEquivRingQuot (α : Type u_2) [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] : SeparationQuotient α ≃+* α ⧸ ⊥.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

• UniformSpace.sepQuotRingEquivRingQuot α = (UniformSpace.sepQuotHomeomorphRingQuot α).ringEquiv

instance UniformSpace.topologicalRing {α : Type u_1} [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] : IsTopologicalRing (SeparationQuotient α)

noncomputable def IsDenseInducing.extendRingHom {α : Type u_1} [UniformSpace α] [Semiring α] {β : Type u_2} [UniformSpace β] [Semiring β] [IsTopologicalSemiring β] {γ : Type u_3} [UniformSpace γ] [Semiring γ] [IsTopologicalSemiring γ] [T2Space γ] [CompleteSpace γ] {i : α →+* β} {f : α →+* γ} (ue : IsUniformInducing ⇑i) (dr : DenseRange ⇑i) (hf : UniformContinuous ⇑f) : β →+* γ

The dense inducing extension as a ring homomorphism.

Equations

• IsDenseInducing.extendRingHom ue dr hf = { toFun := ⋯.extend ⇑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }