English
A linear form on a topology vector space is continuous if its kernel is closed, under nontrivial normed field 𝕜.
Русский
Линейная форма на топологическом векторном пространстве непрерывна, если её ядро замкнуто, над ненулевым нормированным полем 𝕜.
LaTeX
$$$\text{Continuous l}$ if $\ker l$ closed$$
Lean4
/-- Any linear form on a topological vector space over a nontrivially normed field is continuous if
its kernel is closed. -/
theorem continuous_of_isClosed_ker (l : E →ₗ[𝕜] 𝕜) (hl : IsClosed (LinearMap.ker l : Set E)) : Continuous l := by
-- `l` is either constant or surjective. If it is constant, the result is trivial.
by_cases H : finrank 𝕜 (LinearMap.range l) = 0
· rw [Submodule.finrank_eq_zero, LinearMap.range_eq_bot] at H
rw [H]
exact continuous_zero
· -- In the case where `l` is surjective, we factor it as `φ : (E ⧸ l.ker) ≃ₗ[𝕜] 𝕜`. Note that
-- `E ⧸ l.ker` is T2 since `l.ker` is closed.
have : finrank 𝕜 (LinearMap.range l) = 1 :=
le_antisymm (finrank_self 𝕜 ▸ (LinearMap.range l).finrank_le) (zero_lt_iff.mpr H)
have hi : Function.Injective ((LinearMap.ker l).liftQ l (le_refl _)) :=
by
rw [← LinearMap.ker_eq_bot]
exact Submodule.ker_liftQ_eq_bot _ _ _ (le_refl _)
have hs : Function.Surjective ((LinearMap.ker l).liftQ l (le_refl _)) :=
by
rw [← LinearMap.range_eq_top, Submodule.range_liftQ]
exact Submodule.eq_top_of_finrank_eq ((finrank_self 𝕜).symm ▸ this)
let φ : (E ⧸ LinearMap.ker l) ≃ₗ[𝕜] 𝕜 := LinearEquiv.ofBijective ((LinearMap.ker l).liftQ l (le_refl _)) ⟨hi, hs⟩
have hlφ : (l : E → 𝕜) = φ ∘ (LinearMap.ker l).mkQ := by ext;
rfl
-- Since the quotient map `E →ₗ[𝕜] (E ⧸ l.ker)` is continuous, the continuity of `l` will follow
-- form the continuity of `φ`.
suffices Continuous φ.toEquiv by
rw [hlφ]
exact this.comp continuous_quot_mk
have : induced φ.toEquiv.symm inferInstance = hnorm.toUniformSpace.toTopologicalSpace :=
by
refine
unique_topology_of_t2 (topologicalAddGroup_induced φ.symm.toLinearMap)
(continuousSMul_induced φ.symm.toMulActionHom) ?_
rw [t2Space_iff]
exact fun x y hxy =>
@separated_by_continuous _ _ (induced _ _) _ _ _ continuous_induced_dom _ _
(φ.toEquiv.symm.injective.ne hxy)
-- Finally, the pullback by `φ.symm` is exactly the pushforward by `φ`, so we have to prove
-- that `φ` is continuous when `𝕜` is endowed with the pushforward by `φ` of the quotient
-- topology, which is trivial by definition of the pushforward.
simp_rw [this.symm, Equiv.induced_symm]
exact continuous_coinduced_rng
