English
The completion hat K inherits a topological division ring structure from the ambient field, with continuous inversion behavior near nonzero points.
Русский
Дополнение hat K наследует топологическое деление кольца, включающее непрерывность обращения около ненулевых элементов.
LaTeX
$$$IsTopologicalDivisionRing(\hat K)$$$
Lean4
/-- The pullback of a completable topological field along a uniform inducing
ring homomorphism is a completable topological field. -/
theorem completableTopField [UniformSpace α] [T0Space α] {f : α →+* β} (hf : IsUniformInducing f) :
CompletableTopField α := by
refine CompletableTopField.mk (fun F F_cau inf_F => ?_)
rw [← IsUniformInducing.cauchy_map_iff hf] at F_cau ⊢
have h_comm : (f ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ f := by ext; simp only [Function.comp_apply, map_inv₀]
rw [Filter.map_comm h_comm]
apply CompletableTopField.nice _ F_cau
rw [← Filter.push_pull', ← map_zero f, ← hf.isInducing.nhds_eq_comap, inf_F, Filter.map_bot]
