Completion of topological rings:

This files 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 UniformAddGroup. 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 (UniformSpace.Completion α)

Equations

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

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

Equations

• UniformSpace.Completion.mul α = { mul := Function.curry (DenseInducing.extend ⋯ (↑α ∘ Function.uncurry fun (x x_1 : α) => x * x_1)) }

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

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

theorem UniformSpace.Completion.continuous_mul {α : Type u_1} [Ring α] [UniformSpace α] [TopologicalRing α] [UniformAddGroup α] : Continuous fun (p : UniformSpace.Completion α × UniformSpace.Completion α) => p.1 * p.2

theorem UniformSpace.Completion.Continuous.mul {α : Type u_1} [Ring α] [UniformSpace α] [TopologicalRing α] [UniformAddGroup α] {β : Type u_2} [TopologicalSpace β] {f : β → UniformSpace.Completion α} {g : β → UniformSpace.Completion α} (hf : Continuous f) (hg : Continuous g) : Continuous fun (b : β) => f b * g b

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

Equations

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

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

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

Equations

• UniformSpace.Completion.coeRingHom = { toMonoidHom := { toOneHom := { toFun := ↑α, map_one' := ⋯ }, map_mul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

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

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

The completion extension as a ring morphism.

Equations

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

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

Equations

• ⋯ = ⋯

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

The completion map as a ring morphism.

Equations

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

@[simp]

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

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

Equations

• UniformSpace.Completion.algebra A R = let __src := RingHom.comp UniformSpace.Completion.coeRingHom (algebraMap R A); Algebra.mk __src ⋯ ⋯

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

instance UniformSpace.Completion.commRing (R : Type u_2) [CommRing R] [UniformSpace R] [UniformAddGroup R] [TopologicalRing R] : CommRing (UniformSpace.Completion R)

Equations

• UniformSpace.Completion.commRing R = let __src := UniformSpace.Completion.ring; CommRing.mk ⋯

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

A shortcut instance for the common case

Equations

• UniformSpace.Completion.algebra' R = inferInstance

theorem UniformSpace.ring_sep_rel (α : Type u_2) [CommRing α] [UniformSpace α] [UniformAddGroup α] [TopologicalRing α] : UniformSpace.separationSetoid α = Submodule.quotientRel (Ideal.closure ⊥)

theorem UniformSpace.ring_sep_quot (α : Type u) [r : CommRing α] [UniformSpace α] [UniformAddGroup α] [TopologicalRing α] : Quotient (UniformSpace.separationSetoid α) = (α ⧸ Ideal.closure ⊥)

def UniformSpace.sepQuotEquivRingQuot (α : Type u_2) [r : CommRing α] [UniformSpace α] [UniformAddGroup α] [TopologicalRing α] : Quotient (UniformSpace.separationSetoid α) ≃ α ⧸ Ideal.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.sepQuotEquivRingQuot α = Quotient.congrRight ⋯

instance UniformSpace.commRing {α : Type u_1} [CommRing α] [UniformSpace α] [UniformAddGroup α] [TopologicalRing α] : CommRing (Quotient (UniformSpace.separationSetoid α))

Equations

• UniformSpace.commRing = Eq.mpr ⋯ inferInstance

instance UniformSpace.topologicalRing {α : Type u_1} [CommRing α] [UniformSpace α] [UniformAddGroup α] [TopologicalRing α] : TopologicalRing (Quotient (UniformSpace.separationSetoid α))

Equations

• ⋯ = ⋯

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

The dense inducing extension as a ring homomorphism.

Equations

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