Completions of uniform topological rings

Results about UniformSpace.Completion as a ring: extensionality for continuous ring homomorphisms, comparison across equal uniformities, and the identification of a complete Hausdorff ring with its completion.

UniformSpace.Completion.ringHom_ext_of_continuous is UniformSpace.Completion.ext for ring homomorphisms: two continuous ring homomorphisms out of Completion R that agree after composing with the coercion from R are equal. R is a topological ring carrying a compatible uniform additive-group structure, and nothing more: neither CompleteSpace nor T0Space is required, and R need not be commutative. This extensionality principle lets consumers state uniqueness on the base ring instead of on the completion.

The completion of a complete separated ring is itself

UniformSpace.Completion.completeRingEquivSelf: for a complete Hausdorff topological ring S, the extension of the identity is a ring isomorphism UniformSpace.Completion S ≃+* S. Its underlying function is that of the uniform bijection UniformCompletion.completeEquivSelf, and its inverse is the canonical map from S into its completion.

The rest of the self-equivalence material is read off that identification. The isomorphism is uniformly continuous because UniformCompletion.completeEquivSelf is a uniform equivalence, and its inverse is uniformly continuous because it is the canonical map into the completion. Over a base ring R acting by uniformly continuous scalar multiplication the same map is R-linear, giving UniformSpace.Completion.completeAlgEquivSelf. Uniform continuity of the action is not a convenience: it is what makes the completion an R-algebra in the first place, since that is what UniformSpace.Completion.algebra requires.

Comparison across equal uniformities

RingHom.completionCoe_comp_heq compares the coercion for two equal uniformities on the same ring: following a fixed map by the coercion gives heterogeneously equal composites. It uses HEq because the completion types depend on their uniformities.

TauCeti.completionRingHom_heq_of_uniformSpace_eq transports the characterization of a continuous ring homomorphism between completions across equal source and target uniformities. The completed rings may be noncommutative, and the fixed source of their structure maps may be a nonassociative semiring. TauCeti.ringHom_flat_of_completion_heq transports flatness across such a heterogeneous equality of maps, and TauCeti.ringHom_flat_of_heq_of_uniformSpace_eq gives the same transport for maps from a fixed commutative ring into completions.

Main definitions

• UniformSpace.Completion.completeRingEquivSelf: the ring isomorphism UniformSpace.Completion S ≃+* S.
• UniformSpace.Completion.completeAlgEquivSelf: the same map as an R-algebra equivalence, for a complete Hausdorff topological R-algebra S whose scalar multiplication by R is uniformly continuous (UniformContinuousConstSMul R S).

Main results

• RingHom.completionCoe_comp_heq: equal uniformities on the codomain give heterogeneously equal composites with the coercion into the completion.
• TauCeti.completionRingHom_heq_of_uniformSpace_eq: compares continuous ring homomorphisms between completions for equal source and target uniformities.
• TauCeti.ringHom_flat_of_completion_heq and TauCeti.ringHom_flat_of_heq_of_uniformSpace_eq: transport flatness across heterogeneous map equalities between completions, or from a fixed ring into completions.
• UniformSpace.Completion.ringHom_ext_of_continuous: two continuous ring homomorphisms out of a completion that agree on the image of the coercion are equal.
• UniformSpace.Completion.continuous_mapRingEquiv and UniformSpace.Completion.continuous_mapRingEquiv_symm: the isomorphism of completions induced by a topological ring isomorphism is continuous in both directions.
• UniformSpace.Completion.coe_completeRingEquivSelf and UniformSpace.Completion.coe_completeRingEquivSelf_symm: the isomorphism is UniformCompletion.completeEquivSelf and its inverse is the coercion into the completion.
• UniformSpace.Completion.uniformContinuous_completeRingEquivSelf and UniformSpace.Completion.uniformContinuous_completeRingEquivSelf_symm: both directions are uniformly continuous, hence continuous by UniformContinuous.continuous.

theorem RingHom.completionCoe_comp_heq {R : Type u_1} {S : Type u_2} [NonAssocSemiring R] [Ring S] (f : R →+* S) {u₁ u₂ : UniformSpace S} (hu : u₁ = u₂) (t₁ : IsTopologicalRing S) (t₂ : IsTopologicalRing S) (g₁ : IsUniformAddGroup S) (g₂ : IsUniformAddGroup S) : UniformSpace.Completion.coeRingHom.comp f ≍ UniformSpace.Completion.coeRingHom.comp f

Following a fixed map by the coercion into a completion depends on the uniformity only through the instance. For two equal uniformities on S, the composites R →+* S → UniformSpace.Completion S agree.

The conclusion is HEq rather than = because the type UniformSpace.Completion S mentions the uniformity on S, so the two composites do not share a codomain. A caller holding an equation between uniformities — rather than a defeq — is the intended consumer.

theorem UniformSpace.Completion.ringHom_ext_of_continuous {R : Type u_1} [Ring R] [UniformSpace R] [IsTopologicalRing R] [IsUniformAddGroup R] {B : Type u_2} [NonAssocSemiring B] [TopologicalSpace B] [T2Space B] {g h : Completion R →+* B} (hg : Continuous ⇑g) (hh : Continuous ⇑h) (hcomp : g.comp coeRingHom = h.comp coeRingHom) : g = h

Maps out of a completion are determined on the image of the coercion. Two continuous ring homomorphisms R̂ → B into a non-associative semiring carrying a Hausdorff topology that agree after composing with coeRingHom are equal.

This is UniformSpace.Completion.ext packaged for ring homomorphisms: composing with coeRingHom is restriction along the coercion, and density of the image does the rest. Nothing is asked of B beyond a non-associative semiring structure and a Hausdorff topology — no compatibility between the two is used — and R need not be commutative.

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

The ring isomorphism of completions induced by a topological ring isomorphism is continuous: its underlying map is UniformSpace.Completion.map.

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

The inverse of the ring isomorphism of completions induced by a topological ring isomorphism is continuous.

noncomputable def UniformSpace.Completion.completeRingEquivSelf (S : Type u_1) [Ring S] [UniformSpace S] [IsTopologicalRing S] [IsUniformAddGroup S] [CompleteSpace S] [T0Space S] : Completion S ≃+* S

For a complete Hausdorff topological ring, the extension of the identity is a ring isomorphism from the completion.

Equations

• UniformSpace.Completion.completeRingEquivSelf S = RingEquiv.ofBijective (UniformSpace.Completion.extensionHom (RingHom.id S) ⋯) ⋯

@[simp]

theorem UniformSpace.Completion.completeRingEquivSelf_coe (S : Type u_1) [Ring S] [UniformSpace S] [IsTopologicalRing S] [IsUniformAddGroup S] [CompleteSpace S] [T0Space S] (a : S) : (completeRingEquivSelf S) ↑a = a

The isomorphism undoes the canonical inclusion: on an element of S regarded as an element of the completion, it returns that element.

@[simp]

theorem UniformSpace.Completion.completeRingEquivSelf_symm_apply (S : Type u_1) [Ring S] [UniformSpace S] [IsTopologicalRing S] [IsUniformAddGroup S] [CompleteSpace S] [T0Space S] (a : S) : (completeRingEquivSelf S).symm a = ↑a

The inverse isomorphism is the canonical inclusion: it sends an element of S to itself, regarded as an element of the completion.

theorem UniformSpace.Completion.coe_completeRingEquivSelf (S : Type u_1) [Ring S] [UniformSpace S] [IsTopologicalRing S] [IsUniformAddGroup S] [CompleteSpace S] [T0Space S] : ⇑(completeRingEquivSelf S) = ⇑UniformCompletion.completeEquivSelf

The isomorphism is the uniform bijection UniformCompletion.completeEquivSelf, as a function: both are UniformSpace.Completion.extension id.

theorem UniformSpace.Completion.coe_completeRingEquivSelf_symm (S : Type u_1) [Ring S] [UniformSpace S] [IsTopologicalRing S] [IsUniformAddGroup S] [CompleteSpace S] [T0Space S] : ⇑(completeRingEquivSelf S).symm = coe'

The inverse isomorphism is the canonical map into the completion, as a function.

theorem UniformSpace.Completion.uniformContinuous_completeRingEquivSelf (S : Type u_1) [Ring S] [UniformSpace S] [IsTopologicalRing S] [IsUniformAddGroup S] [CompleteSpace S] [T0Space S] : UniformContinuous ⇑(completeRingEquivSelf S)

The isomorphism is uniformly continuous: it is the uniform bijection UniformCompletion.completeEquivSelf.

theorem UniformSpace.Completion.uniformContinuous_completeRingEquivSelf_symm (S : Type u_1) [Ring S] [UniformSpace S] [IsTopologicalRing S] [IsUniformAddGroup S] [CompleteSpace S] [T0Space S] : UniformContinuous ⇑(completeRingEquivSelf S).symm

The inverse isomorphism is uniformly continuous: it is the canonical map into the completion.

noncomputable def UniformSpace.Completion.completeAlgEquivSelf (S : Type u_1) [Ring S] [UniformSpace S] [IsTopologicalRing S] [IsUniformAddGroup S] [CompleteSpace S] [T0Space S] (R : Type u_2) [CommSemiring R] [Algebra R S] [UniformContinuousConstSMul R S] : Completion S ≃ₐ[R] S

For a complete Hausdorff topological R-algebra S whose scalar multiplication by R is uniformly continuous (UniformContinuousConstSMul R S, which is what gives the completion its R-algebra structure), the extension of the identity is an R-algebra equivalence from the completion: completeRingEquivSelf is R-linear, since it fixes the image of R.

Equations

• UniformSpace.Completion.completeAlgEquivSelf S R = AlgEquiv.ofRingEquiv ⋯

@[simp]

theorem UniformSpace.Completion.coe_completeAlgEquivSelf (S : Type u_1) [Ring S] [UniformSpace S] [IsTopologicalRing S] [IsUniformAddGroup S] [CompleteSpace S] [T0Space S] (R : Type u_2) [CommSemiring R] [Algebra R S] [UniformContinuousConstSMul R S] : ⇑(completeAlgEquivSelf S R) = ⇑(completeRingEquivSelf S)

The algebra equivalence has the same underlying map as the ring isomorphism, so simp normalises the R-algebra bundling onto the ring one.

@[simp]

theorem UniformSpace.Completion.coe_completeAlgEquivSelf_symm (S : Type u_1) [Ring S] [UniformSpace S] [IsTopologicalRing S] [IsUniformAddGroup S] [CompleteSpace S] [T0Space S] (R : Type u_2) [CommSemiring R] [Algebra R S] [UniformContinuousConstSMul R S] : ⇑(completeAlgEquivSelf S R).symm = ⇑(completeRingEquivSelf S).symm

The inverses agree too, so the two bundlings normalise together in both directions.

theorem TauCeti.completionRingHom_heq_of_uniformSpace_eq {A : Type u_1} {S : Type u_2} {S' : Type u_3} [NonAssocSemiring A] [Ring S] [Ring S'] {u₁ u₂ : UniformSpace S} (hu : u₂ = u₁) {v₁ v₂ : UniformSpace S'} (hv : v₂ = v₁) (g₁ : IsUniformAddGroup S) (g₂ : IsUniformAddGroup S) (t₁ : IsTopologicalRing S) (t₂ : IsTopologicalRing S) (g₁' : IsUniformAddGroup S') (g₂' : IsUniformAddGroup S') (t₁' : IsTopologicalRing S') (t₂' : IsTopologicalRing S') : let B₁ := UniformSpace.Completion S; let B₂ := UniformSpace.Completion S; let C₁ := UniformSpace.Completion S'; let C₂ := UniformSpace.Completion S'; have b₁ := UniformSpace.Completion.ring; have b₂ := UniformSpace.Completion.ring; have c₁ := UniformSpace.Completion.ring; have c₂ := UniformSpace.Completion.ring; ∀ (f₂ : B₂ →+* C₂) (f₁ : B₁ →+* C₁) (a₂ : A →+* B₂) (a₁ : A →+* B₁) (d₂ : A →+* C₂) (d₁ : A →+* C₁), Continuous ⇑f₂ → a₂ ≍ a₁ → d₂ ≍ d₁ → f₂.comp a₂ = d₂ → (∀ (f : B₁ →+* C₁), Continuous ⇑f → f.comp a₁ = d₁ → f = f₁) → f₂ ≍ f₁

Two completion ring homomorphisms are heterogeneously equal when their source and target uniformities agree and the first map satisfies the characterization that uniquely determines the second. The rings being completed need not be commutative, and the fixed source of the structure maps need only be a nonassociative semiring.

theorem TauCeti.ringHom_flat_of_completion_heq {S : Type u_1} {S' : Type u_2} [CommRing S] [CommRing S'] {u₁ u₂ : UniformSpace S} (hu : u₂ = u₁) {v₁ v₂ : UniformSpace S'} (hv : v₂ = v₁) (g₁ : IsUniformAddGroup S) (g₂ : IsUniformAddGroup S) (t₁ : IsTopologicalRing S) (t₂ : IsTopologicalRing S) (g₁' : IsUniformAddGroup S') (g₂' : IsUniformAddGroup S') (t₁' : IsTopologicalRing S') (t₂' : IsTopologicalRing S') : let R₁ := UniformSpace.Completion S; let R₂ := UniformSpace.Completion S; let B₁ := UniformSpace.Completion S'; let B₂ := UniformSpace.Completion S'; let r₁ := UniformSpace.Completion.commRing S; let r₂ := UniformSpace.Completion.commRing S; let b₁ := UniformSpace.Completion.commRing S'; let b₂ := UniformSpace.Completion.commRing S'; ∀ (f₂ : R₂ →+* B₂) (f₁ : R₁ →+* B₁), f₂ ≍ f₁ → f₂.Flat → f₁.Flat

Flatness passes across a heterogeneous equality between ring homomorphisms of completions whose source and target uniformities agree.

theorem TauCeti.ringHom_flat_of_heq_of_uniformSpace_eq {A : Type u_1} {S : Type u_2} [CommRing A] [CommRing S] {u₁ u₂ : UniformSpace S} (hu : u₂ = u₁) (g₁ : IsUniformAddGroup S) (g₂ : IsUniformAddGroup S) (t₁ : IsTopologicalRing S) (t₂ : IsTopologicalRing S) : let B₁ := UniformSpace.Completion S; let B₂ := UniformSpace.Completion S; let b₁ := UniformSpace.Completion.commRing S; let b₂ := UniformSpace.Completion.commRing S; ∀ (f₂ : A →+* B₂) (f₁ : A →+* B₁), f₂ ≍ f₁ → f₂.Flat → f₁.Flat

Flatness of a ring homomorphism from A into a completion passes across a heterogeneous equality with a ring homomorphism into the completion for an equal uniformity. This is the fixed-source form of TauCeti.ringHom_flat_of_completion_heq: A keeps its ring structure, and only the uniformity of S, hence its completion, varies. For instance, it compares the canonical maps from A into two completions of a localisation S whose uniformities agree.