Uniform spaces #
In this file we prove that a UniformSpace.comap f b uniform structure defines a completable
topological field if the map f is a ring homomorphism between fields and if the codomain uniform
space b is a completable topological field.
Main results #
UniformInducing.completableTopField: if the codomain of a uniform inducing ring homomorphism between fields is a completable topological field, then the domain is also a completable topological field.
theorem
UniformInducing.completableTopField
{α : Type u_1}
{β : Type u_2}
[Field β]
[b : UniformSpace β]
[CompletableTopField β]
[Field α]
[UniformSpace α]
[T0Space α]
{f : α →+* β}
(hf : UniformInducing ⇑f)
:
The pullback of a completable topological field along a uniform inducing ring homomorphism is a completable topological field.
instance
UniformSpace.comap_completableTopField
{α : Type u_1}
{β : Type u_2}
[Field β]
[b : UniformSpace β]
[CompletableTopField β]
[Field α]
(f : α →+* β)
[T0Space α]
:
Equations
- ⋯ = ⋯