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.comap_completableTopField: if the codomain of a ring homomorphism between fields is a completable topological field, then the domain is also a completable topological field.
theorem
UniformSpace.comap_completableTopField
{α : Type u}
{β : Type v}
[Field β]
[Field α]
{f : α →+* β}
[b : UniformSpace β]
[T0Space α]
[CompletableTopField β]
:
The pullback of a completable topological field along a ring homomorphism is a completable topological field.