English
If 𝕜 is a nontrivially normed field, any T2 topology making it a topological vector space over itself with the norm topology equals the norm topology.
Русский
Если 𝕜 — ненулевое нормированное поле, любая T2-структура на 𝕜, делающая его векторным пространством над самим собой с нормальной топологией, совпадает с нормальной топологией.
LaTeX
$$$t = \text{norm topology on } 𝕜$ under given assumptions$$
Lean4
/-- If `𝕜` is a nontrivially normed field, any T2 topology on `𝕜` which makes it a topological
vector space over itself (with the norm topology) is *equal* to the norm topology. -/
theorem unique_topology_of_t2 {t : TopologicalSpace 𝕜} (h₁ : @IsTopologicalAddGroup 𝕜 t _)
(h₂ : @ContinuousSMul 𝕜 𝕜 _ hnorm.toUniformSpace.toTopologicalSpace t) (h₃ : @T2Space 𝕜 t) :
t = hnorm.toUniformSpace.toTopologicalSpace := by
-- Let `𝓣₀` denote the topology on `𝕜` induced by the norm, and `𝓣` be any T2 vector
-- topology on `𝕜`. To show that `𝓣₀ = 𝓣`, it suffices to show that they have the same
-- neighborhoods of 0.
refine IsTopologicalAddGroup.ext h₁ inferInstance (le_antisymm ?_ ?_)
· -- To show `𝓣 ≤ 𝓣₀`, we have to show that closed balls are `𝓣`-neighborhoods of 0.
rw [Metric.nhds_basis_closedBall.ge_iff]
-- Let `ε > 0`. Since `𝕜` is nontrivially normed, we have `0 < ‖ξ₀‖ < ε` for some `ξ₀ : 𝕜`.
intro ε hε
rcases NormedField.exists_norm_lt 𝕜 hε with
⟨ξ₀, hξ₀, hξ₀ε⟩
-- Since `ξ₀ ≠ 0` and `𝓣` is T2, we know that `{ξ₀}ᶜ` is a `𝓣`-neighborhood of 0.
have : { ξ₀ }ᶜ ∈ @nhds 𝕜 t 0 :=
IsOpen.mem_nhds isOpen_compl_singleton <|
mem_compl_singleton_iff.mpr <| Ne.symm <| norm_ne_zero_iff.mp hξ₀.ne.symm
have : balancedCore 𝕜 { ξ₀ }ᶜ ∈ @nhds 𝕜 t 0 := balancedCore_mem_nhds_zero this
refine
mem_of_superset this fun ξ hξ =>
?_
-- Let `ξ ∈ 𝓑`. We want to show `‖ξ‖ < ε`. If `ξ = 0`, this is trivial.
by_cases hξ0 : ξ = 0
· rw [hξ0]
exact Metric.mem_closedBall_self hε.le
· rw [mem_closedBall_zero_iff]
-- Now suppose `ξ ≠ 0`. By contradiction, let's assume `ε < ‖ξ‖`, and show that
-- `ξ₀ ∈ 𝓑 ⊆ {ξ₀}ᶜ`, which is a contradiction.
by_contra! h
suffices (ξ₀ * ξ⁻¹) • ξ ∈ balancedCore 𝕜 { ξ₀ }ᶜ
by
rw [smul_eq_mul, mul_assoc, inv_mul_cancel₀ hξ0, mul_one] at this
exact
notMem_compl_iff.mpr (mem_singleton ξ₀)
((balancedCore_subset _) this)
-- For that, we use that `𝓑` is balanced : since `‖ξ₀‖ < ε < ‖ξ‖`, we have `‖ξ₀ / ξ‖ ≤ 1`,
-- hence `ξ₀ = (ξ₀ / ξ) • ξ ∈ 𝓑` because `ξ ∈ 𝓑`.
refine (balancedCore_balanced _).smul_mem ?_ hξ
rw [norm_mul, norm_inv, mul_inv_le_iff₀ (norm_pos_iff.mpr hξ0), one_mul]
exact (hξ₀ε.trans h).le
· -- Finally, to show `𝓣₀ ≤ 𝓣`, we simply argue that `id = (fun x ↦ x • 1)` is continuous from
-- `(𝕜, 𝓣₀)` to `(𝕜, 𝓣)` because `(•) : (𝕜, 𝓣₀) × (𝕜, 𝓣) → (𝕜, 𝓣)` is continuous.
calc
@nhds 𝕜 hnorm.toUniformSpace.toTopologicalSpace 0 = map id (@nhds 𝕜 hnorm.toUniformSpace.toTopologicalSpace 0) :=
map_id.symm
_ = map (fun x => id x • (1 : 𝕜)) (@nhds 𝕜 hnorm.toUniformSpace.toTopologicalSpace 0) := by
conv_rhs =>
congr
ext
rw [smul_eq_mul, mul_one]
_ ≤ @nhds 𝕜 t ((0 : 𝕜) • (1 : 𝕜)) :=
(@Tendsto.smul_const _ _ _ hnorm.toUniformSpace.toTopologicalSpace t _ _ _ _ _ tendsto_id (1 : 𝕜))
_ = @nhds 𝕜 t 0 := by rw [zero_smul]
