Skip to content

Commit

Permalink
feat(topology/algebra/module/finite_dimension): all linear maps from …
Browse files Browse the repository at this point in the history 
…a finite dimensional T2 TVS are continuous (#13460)

Summary of the changes :
- generalize a bunch of results from `analysis/normed_space/finite_dimension` (main ones are : `continuous_equiv_fun_basis`, `linear_map.continuous_of_finite_dimensional`, and related constructions like `linear_map.to_continuous_linear_map`) to arbitrary TVSs, and move them to a new file `topology/algebra/module/finite_dimension`
- generalize `linear_map.continuous_iff_is_closed_ker` to arbitrary TVSs, and move it from `analysis/normed_space/operator_norm` to the new file
- as needed by the generalizations, add lemma `unique_topology_of_t2` : if `𝕜` is a nondiscrete 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
- finally, change `pi_eq_sum_univ` to take any `decidable_eq` instance (not just the classical ones), and fix later uses
  • Loading branch information
@ADedecker
ADedecker committed Jun 3, 2022
1 parent 31cbfbb commit c9d69a4
Show file tree
Hide file tree
Showing 6 changed files with 370 additions and 273 deletions.
201 changes: 1 addition & 200 deletions src/analysis/normed_space/finite_dimension.lean
View file
Expand Up @@ -8,6 +8,7 @@ import analysis.normed_space.affine_isometry
import analysis.normed_space.operator_norm
import analysis.normed_space.riesz_lemma
import linear_algebra.matrix.to_lin
import topology.algebra.module.finite_dimension
import topology.instances.matrix

/-!
Expand All @@ -18,8 +19,6 @@ are continuous. Moreover, a finite-dimensional subspace is always complete and c
## Main results:
* `linear_map.continuous_of_finite_dimensional` : a linear map on a finite-dimensional space over a
complete field is continuous.
* `finite_dimensional.complete` : a finite-dimensional space over a complete field is complete. This
is not registered as an instance, as the field would be an unknown metavariable in typeclass
resolution.
Expand Down Expand Up @@ -109,31 +108,6 @@ affine_isometry_equiv.mk' li (li.linear_isometry.to_linear_isometry_equiv h) (ar

end affine_isometry

/-- A linear map on `ι → 𝕜` (where `ι` is a fintype) is continuous -/
lemma linear_map.continuous_on_pi {ι : Type w} [fintype ι] {𝕜 : Type u} [normed_field 𝕜]
{E : Type v} [add_comm_group E] [module 𝕜 E] [topological_space E]
[topological_add_group E] [has_continuous_smul 𝕜 E] (f : (ι → 𝕜) →ₗ[𝕜] E) : continuous f :=
begin
-- for the proof, write `f` in the standard basis, and use that each coordinate is a continuous
-- function.
have : (f : (ι → 𝕜) → E) =
(λx, ∑ i : ι, x i • (f (λj, if i = j then 1 else 0))),
by { ext x, exact f.pi_apply_eq_sum_univ x },
rw this,
refine continuous_finset_sum _ (λi hi, _),
exact (continuous_apply i).smul continuous_const
end

/-- The space of continuous linear maps between finite-dimensional spaces is finite-dimensional. -/
instance {𝕜 E F : Type*} [field 𝕜] [topological_space 𝕜]
[topological_space E] [add_comm_group E] [module 𝕜 E] [finite_dimensional 𝕜 E]
[topological_space F] [add_comm_group F] [module 𝕜 F] [topological_add_group F]
[has_continuous_smul 𝕜 F] [finite_dimensional 𝕜 F] :
finite_dimensional 𝕜 (E →L[𝕜] F) :=
finite_dimensional.of_injective
(continuous_linear_map.coe_lm 𝕜 : (E →L[𝕜] F) →ₗ[𝕜] (E →ₗ[𝕜] F))
continuous_linear_map.coe_injective

section complete_field

variables {𝕜 : Type u} [nondiscrete_normed_field 𝕜]
Expand All @@ -143,98 +117,6 @@ variables {𝕜 : Type u} [nondiscrete_normed_field 𝕜]
[topological_add_group F'] [has_continuous_smul 𝕜 F']
[complete_space 𝕜]

/-- In finite dimension over a complete field, the canonical identification (in terms of a basis)
with `𝕜^n` together with its sup norm is continuous. This is the nontrivial part in the fact that
all norms are equivalent in finite dimension.
This statement is superceded by the fact that every linear map on a finite-dimensional space is
continuous, in `linear_map.continuous_of_finite_dimensional`. -/
lemma continuous_equiv_fun_basis {ι : Type v} [fintype ι] (ξ : basis ι 𝕜 E) :
continuous ξ.equiv_fun :=
begin
unfreezingI { induction hn : fintype.card ι with n IH generalizing ι E },
{ apply ξ.equiv_fun.to_linear_map.continuous_of_bound 0 (λx, _),
have : ξ.equiv_fun x = 0,
by { ext i, exact (fintype.card_eq_zero_iff.1 hn).elim i },
change ∥ξ.equiv_fun x∥ ≤ 0 * ∥x∥,
rw this,
simp [norm_nonneg] },
{ haveI : finite_dimensional 𝕜 E := of_fintype_basis ξ,
-- first step: thanks to the inductive assumption, any n-dimensional subspace is equivalent
-- to a standard space of dimension n, hence it is complete and therefore closed.
have H₁ : ∀s : submodule 𝕜 E, finrank 𝕜 s = n → is_closed (s : set E),
{ assume s s_dim,
let b := basis.of_vector_space 𝕜 s,
have U : uniform_embedding b.equiv_fun.symm.to_equiv,
{ have : fintype.card (basis.of_vector_space_index 𝕜 s) = n,
by { rw ← s_dim, exact (finrank_eq_card_basis b).symm },
have : continuous b.equiv_fun := IH b this,
exact b.equiv_fun.symm.uniform_embedding b.equiv_fun.symm.to_linear_map.continuous_on_pi
this },
have : is_complete (s : set E),
from complete_space_coe_iff_is_complete.1 ((complete_space_congr U).1 (by apply_instance)),
exact this.is_closed },
-- second step: any linear form is continuous, as its kernel is closed by the first step
have H₂ : ∀f : E →ₗ[𝕜] 𝕜, continuous f,
{ assume f,
have : finrank 𝕜 f.ker = n ∨ finrank 𝕜 f.ker = n.succ,
{ have Z := f.finrank_range_add_finrank_ker,
rw [finrank_eq_card_basis ξ, hn] at Z,
by_cases H : finrank 𝕜 f.range = 0,
{ right,
rw H at Z,
simpa using Z },
{ left,
have : finrank 𝕜 f.range = 1,
{ refine le_antisymm _ (zero_lt_iff.mpr H),
simpa [finrank_self] using f.range.finrank_le },
rw [this, add_comm, nat.add_one] at Z,
exact nat.succ.inj Z } },
have : is_closed (f.ker : set E),
{ cases this,
{ exact H₁ _ this },
{ have : f.ker = ⊤,
by { apply eq_top_of_finrank_eq, rw [finrank_eq_card_basis ξ, hn, this] },
simp [this] } },
exact linear_map.continuous_iff_is_closed_ker.2 this },
-- third step: applying the continuity to the linear form corresponding to a coefficient in the
-- basis decomposition, deduce that all such coefficients are controlled in terms of the norm
have : ∀i:ι, ∃C, 0 ≤ C ∧ ∀(x:E), ∥ξ.equiv_fun x i∥ ≤ C * ∥x∥,
{ assume i,
let f : E →ₗ[𝕜] 𝕜 := (linear_map.proj i) ∘ₗ ↑ξ.equiv_fun,
let f' : E →L[𝕜] 𝕜 := { cont := H₂ f, ..f },
exact ⟨∥f'∥, norm_nonneg _, λx, continuous_linear_map.le_op_norm f' x⟩ },
-- fourth step: combine the bound on each coefficient to get a global bound and the continuity
choose C0 hC0 using this,
let C := ∑ i, C0 i,
have C_nonneg : 0 ≤ C := finset.sum_nonneg (λi hi, (hC0 i).1),
have C0_le : ∀i, C0 i ≤ C :=
λi, finset.single_le_sum (λj hj, (hC0 j).1) (finset.mem_univ _),
apply ξ.equiv_fun.to_linear_map.continuous_of_bound C (λx, _),
rw pi_norm_le_iff,
{ exact λi, le_trans ((hC0 i).2 x) (mul_le_mul_of_nonneg_right (C0_le i) (norm_nonneg _)) },
{ exact mul_nonneg C_nonneg (norm_nonneg _) } }
end

/-- Any linear map on a finite dimensional space over a complete field is continuous. -/
theorem linear_map.continuous_of_finite_dimensional [finite_dimensional 𝕜 E] (f : E →ₗ[𝕜] F') :
continuous f :=
begin
-- for the proof, go to a model vector space `b → 𝕜` thanks to `continuous_equiv_fun_basis`, and
-- argue that all linear maps there are continuous.
let b := basis.of_vector_space 𝕜 E,
have A : continuous b.equiv_fun :=
continuous_equiv_fun_basis b,
have B : continuous (f.comp (b.equiv_fun.symm : (basis.of_vector_space_index 𝕜 E → 𝕜) →ₗ[𝕜] E)) :=
linear_map.continuous_on_pi _,
have : continuous ((f.comp (b.equiv_fun.symm : (basis.of_vector_space_index 𝕜 E → 𝕜) →ₗ[𝕜] E))
∘ b.equiv_fun) := B.comp A,
convert this,
ext x,
dsimp,
rw [basis.equiv_fun_symm_apply, basis.sum_repr]
end

section affine

variables {PE PF : Type*} [metric_space PE] [normed_add_torsor E PE] [metric_space PF]
Expand Down Expand Up @@ -281,87 +163,6 @@ begin
simpa only [h, monoid_hom.one_apply, dif_neg, not_false_iff] using continuous_const }
end

namespace linear_map

variables [finite_dimensional 𝕜 E]

/-- The continuous linear map induced by a linear map on a finite dimensional space -/
def to_continuous_linear_map : (E →ₗ[𝕜] F') ≃ₗ[𝕜] E →L[𝕜] F' :=
{ to_fun := λ f, ⟨f, f.continuous_of_finite_dimensional⟩,
inv_fun := coe,
map_add' := λ f g, rfl,
map_smul' := λ c f, rfl,
left_inv := λ f, rfl,
right_inv := λ f, continuous_linear_map.coe_injective rfl }

@[simp] lemma coe_to_continuous_linear_map' (f : E →ₗ[𝕜] F') :
⇑f.to_continuous_linear_map = f := rfl

@[simp] lemma coe_to_continuous_linear_map (f : E →ₗ[𝕜] F') :
(f.to_continuous_linear_map : E →ₗ[𝕜] F') = f := rfl

@[simp] lemma coe_to_continuous_linear_map_symm :
⇑(to_continuous_linear_map : (E →ₗ[𝕜] F') ≃ₗ[𝕜] E →L[𝕜] F').symm = coe := rfl

end linear_map

namespace linear_equiv

variables [finite_dimensional 𝕜 E]

/-- The continuous linear equivalence induced by a linear equivalence on a finite dimensional
space. -/
def to_continuous_linear_equiv (e : E ≃ₗ[𝕜] F) : E ≃L[𝕜] F :=
{ continuous_to_fun := e.to_linear_map.continuous_of_finite_dimensional,
continuous_inv_fun := begin
haveI : finite_dimensional 𝕜 F := e.finite_dimensional,
exact e.symm.to_linear_map.continuous_of_finite_dimensional
end,
..e }

@[simp] lemma coe_to_continuous_linear_equiv (e : E ≃ₗ[𝕜] F) :
(e.to_continuous_linear_equiv : E →ₗ[𝕜] F) = e := rfl

@[simp] lemma coe_to_continuous_linear_equiv' (e : E ≃ₗ[𝕜] F) :
(e.to_continuous_linear_equiv : E → F) = e := rfl

@[simp] lemma coe_to_continuous_linear_equiv_symm (e : E ≃ₗ[𝕜] F) :
(e.to_continuous_linear_equiv.symm : F →ₗ[𝕜] E) = e.symm := rfl

@[simp] lemma coe_to_continuous_linear_equiv_symm' (e : E ≃ₗ[𝕜] F) :
(e.to_continuous_linear_equiv.symm : F → E) = e.symm := rfl

@[simp] lemma to_linear_equiv_to_continuous_linear_equiv (e : E ≃ₗ[𝕜] F) :
e.to_continuous_linear_equiv.to_linear_equiv = e :=
by { ext x, refl }

@[simp] lemma to_linear_equiv_to_continuous_linear_equiv_symm (e : E ≃ₗ[𝕜] F) :
e.to_continuous_linear_equiv.symm.to_linear_equiv = e.symm :=
by { ext x, refl }

end linear_equiv

namespace continuous_linear_map

variable [finite_dimensional 𝕜 E]

/-- Builds a continuous linear equivalence from a continuous linear map on a finite-dimensional
vector space whose determinant is nonzero. -/
def to_continuous_linear_equiv_of_det_ne_zero
(f : E →L[𝕜] E) (hf : f.det ≠ 0) : E ≃L[𝕜] E :=
((f : E →ₗ[𝕜] E).equiv_of_det_ne_zero hf).to_continuous_linear_equiv

@[simp] lemma coe_to_continuous_linear_equiv_of_det_ne_zero (f : E →L[𝕜] E) (hf : f.det ≠ 0) :
(f.to_continuous_linear_equiv_of_det_ne_zero hf : E →L[𝕜] E) = f :=
by { ext x, refl }

@[simp] lemma to_continuous_linear_equiv_of_det_ne_zero_apply
(f : E →L[𝕜] E) (hf : f.det ≠ 0) (x : E) :
f.to_continuous_linear_equiv_of_det_ne_zero hf x = f x :=
rfl

end continuous_linear_map

/-- Any `K`-Lipschitz map from a subset `s` of a metric space `α` to a finite-dimensional real
vector space `E'` can be extended to a Lipschitz map on the whole space `α`, with a slightly worse
constant `C * K` where `C` only depends on `E'`. We record a working value for this constant `C`
Expand Down
60 changes: 0 additions & 60 deletions src/analysis/normed_space/operator_norm.lean
View file
Expand Up @@ -1155,66 +1155,6 @@ variables [normed_group E] [normed_group F] [normed_group G] [normed_group Fₗ]

open metric continuous_linear_map

section normed_field

variables [normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (f : E →ₗ[𝕜] F)

lemma linear_map.continuous_iff_is_closed_ker {f : E →ₗ[𝕜] 𝕜} :
continuous f ↔ is_closed (f.ker : set E) :=
begin
-- the continuity of f obviously implies that its kernel is closed
refine ⟨λh, (t1_space.t1 (0 : 𝕜)).preimage h, λh, _⟩,
-- for the other direction, we assume that the kernel is closed
by_cases hf : ∀x, x ∈ f.ker,
{ -- if `f = 0`, its continuity is obvious
have : (f : E → 𝕜) = (λx, 0), by { ext x, simpa using hf x },
rw this,
exact continuous_const },
{ /- if `f` is not zero, we use an element `x₀ ∉ ker f` such that `∥x₀∥ ≤ 2 ∥x₀ - y∥` for all
`y ∈ ker f`, given by Riesz's lemma, and prove that `2 ∥f x₀∥ / ∥x₀∥` gives a bound on the
operator norm of `f`. For this, start from an arbitrary `x` and note that
`y = x₀ - (f x₀ / f x) x` belongs to the kernel of `f`. Applying the above inequality to `x₀`
and `y` readily gives the conclusion. -/
push_neg at hf,
let r : ℝ := (2 : ℝ)⁻¹,
have : 0 ≤ r, by norm_num [r],
have : r < 1, by norm_num [r],
obtain ⟨x₀, x₀ker, h₀⟩ : ∃ (x₀ : E), x₀ ∉ f.ker ∧ ∀ y ∈ linear_map.ker f,
r * ∥x₀∥ ≤ ∥x₀ - y∥, from riesz_lemma h hf this,
have : x₀ ≠ 0,
{ assume h,
have : x₀ ∈ f.ker, by { rw h, exact (linear_map.ker f).zero_mem },
exact x₀ker this },
have rx₀_ne_zero : r * ∥x₀∥ ≠ 0, by { simp [norm_eq_zero, this], },
have : ∀x, ∥f x∥ ≤ (((r * ∥x₀∥)⁻¹) * ∥f x₀∥) * ∥x∥,
{ assume x,
by_cases hx : f x = 0,
{ rw [hx, norm_zero],
apply_rules [mul_nonneg, norm_nonneg, inv_nonneg.2] },
{ let y := x₀ - (f x₀ * (f x)⁻¹ ) • x,
have fy_zero : f y = 0, by calc
f y = f x₀ - (f x₀ * (f x)⁻¹ ) * f x : by simp [y]
... = 0 :
by { rw [mul_assoc, inv_mul_cancel hx, mul_one, sub_eq_zero_of_eq], refl },
have A : r * ∥x₀∥ ≤ ∥f x₀∥ * ∥f x∥⁻¹ * ∥x∥, from calc
r * ∥x₀∥ ≤ ∥x₀ - y∥ : h₀ _ (linear_map.mem_ker.2 fy_zero)
... = ∥(f x₀ * (f x)⁻¹ ) • x∥ : by { dsimp [y], congr, abel }
... = ∥f x₀∥ * ∥f x∥⁻¹ * ∥x∥ :
by rw [norm_smul, norm_mul, norm_inv],
calc
∥f x∥ = (r * ∥x₀∥)⁻¹ * (r * ∥x₀∥) * ∥f x∥ : by rwa [inv_mul_cancel, one_mul]
... ≤ (r * ∥x₀∥)⁻¹ * (∥f x₀∥ * ∥f x∥⁻¹ * ∥x∥) * ∥f x∥ : begin
apply mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left A _) (norm_nonneg _),
exact inv_nonneg.2 (mul_nonneg (by norm_num) (norm_nonneg _))
end
... = (∥f x∥ ⁻¹ * ∥f x∥) * (((r * ∥x₀∥)⁻¹) * ∥f x₀∥) * ∥x∥ : by ring
... = (((r * ∥x₀∥)⁻¹) * ∥f x₀∥) * ∥x∥ :
by { rw [inv_mul_cancel, one_mul], simp [norm_eq_zero, hx] } } },
exact linear_map.continuous_of_bound f _ this }
end

end normed_field

section
variables [nondiscrete_normed_field 𝕜] [nondiscrete_normed_field 𝕜₂] [nondiscrete_normed_field 𝕜₃]
[normed_space 𝕜 E] [normed_space 𝕜₂ F] [normed_space 𝕜₃ G] [normed_space 𝕜 Fₗ] (c : 𝕜)
Expand Down
14 changes: 2 additions & 12 deletions src/linear_algebra/basic.lean
View file
Expand Up @@ -119,16 +119,11 @@ by { ext, simp [linear_equiv_fun_on_fintype], }

end finsupp

section
open_locale classical

/-- decomposing `x : ι → R` as a sum along the canonical basis -/
lemma pi_eq_sum_univ {ι : Type*} [fintype ι] {R : Type*} [semiring R] (x : ι → R) :
lemma pi_eq_sum_univ {ι : Type*} [fintype ι] [decidable_eq ι] {R : Type*} [semiring R] (x : ι → R) :
x = ∑ i, x i • (λj, if i = j then 1 else 0) :=
by { ext, simp }

end

/-! ### Properties of linear maps -/
namespace linear_map

Expand Down Expand Up @@ -317,21 +312,16 @@ end

end

section
open_locale classical

/-- A linear map `f` applied to `x : ι → R` can be computed using the image under `f` of elements
of the canonical basis. -/
lemma pi_apply_eq_sum_univ [fintype ι] (f : (ι → R) →ₗ[R] M) (x : ι → R) :
lemma pi_apply_eq_sum_univ [fintype ι] [decidable_eq ι] (f : (ι → R) →ₗ[R] M) (x : ι → R) :
f x = ∑ i, x i • (f (λj, if i = j then 1 else 0)) :=
begin
conv_lhs { rw [pi_eq_sum_univ x, f.map_sum] },
apply finset.sum_congr rfl (λl hl, _),
rw map_smul
end

end

end add_comm_monoid

section module
Expand Down
2 changes: 1 addition & 1 deletion src/linear_algebra/matrix/adjugate.lean
View file
Expand Up @@ -220,7 +220,7 @@ begin
nth_rewrite 1 ← A.transpose_transpose,
rw [← adjugate_transpose, adjugate_def],
have : b = ∑ i, (b i) • (pi.single i 1),
{ refine (pi_eq_sum_univ b).trans _, congr' with j, simp [pi.single_apply, eq_comm], congr, },
{ refine (pi_eq_sum_univ b).trans _, congr' with j, simp [pi.single_apply, eq_comm] },
nth_rewrite 0 this, ext k,
simp [mul_vec, dot_product, mul_comm],
end
Expand Down
1 change: 1 addition & 0 deletions src/ring_theory/ideal/quotient.lean
View file
Expand Up @@ -305,6 +305,7 @@ noncomputable def pi_quot_equiv : ((ι → R) ⧸ I.pi ι) ≃ₗ[(R ⧸ I)] (ι
lemma map_pi {ι} [fintype ι] {ι' : Type w} (x : ι → R) (hi : ∀ i, x i ∈ I)
(f : (ι → R) →ₗ[R] (ι' → R)) (i : ι') : f x i ∈ I :=
begin
classical,
rw pi_eq_sum_univ x,
simp only [finset.sum_apply, smul_eq_mul, linear_map.map_sum, pi.smul_apply, linear_map.map_smul],
exact I.sum_mem (λ j hj, I.mul_mem_right _ (hi j))
Expand Down

0 comments on commit c9d69a4

Please sign in to comment.