diff --git a/Mathlib.lean b/Mathlib.lean index 5fac66204eba26..a8e5a51b90dd4e 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2026,6 +2026,7 @@ public import Mathlib.Analysis.Fourier.Notation public import Mathlib.Analysis.Fourier.PoissonSummation public import Mathlib.Analysis.Fourier.RiemannLebesgueLemma public import Mathlib.Analysis.Fourier.ZMod +public import Mathlib.Analysis.FredholmOperator public import Mathlib.Analysis.FunctionalSpaces.SobolevInequality public import Mathlib.Analysis.Hofer public import Mathlib.Analysis.InnerProductSpace.Adjoint @@ -2254,6 +2255,7 @@ public import Mathlib.Analysis.Normed.Operator.LinearIsometry public import Mathlib.Analysis.Normed.Operator.Mul public import Mathlib.Analysis.Normed.Operator.NNNorm public import Mathlib.Analysis.Normed.Operator.NormedSpace +public import Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite public import Mathlib.Analysis.Normed.Operator.Prod public import Mathlib.Analysis.Normed.Order.Basic public import Mathlib.Analysis.Normed.Order.Hom.Basic @@ -7987,6 +7989,7 @@ public import Mathlib.Topology.Maps.Proper.CompactlyGenerated public import Mathlib.Topology.Maps.Proper.UniversallyClosed public import Mathlib.Topology.Maps.Strict.Basic public import Mathlib.Topology.Maps.Strict.Group +public import Mathlib.Topology.Maps.Strict.Module public import Mathlib.Topology.MetricSpace.Algebra public import Mathlib.Topology.MetricSpace.Antilipschitz public import Mathlib.Topology.MetricSpace.Basic diff --git a/Mathlib/Algebra/Module/Submodule/EqLocus.lean b/Mathlib/Algebra/Module/Submodule/EqLocus.lean index 9a6626da9d7b56..0691c6e537e6bb 100644 --- a/Mathlib/Algebra/Module/Submodule/EqLocus.lean +++ b/Mathlib/Algebra/Module/Submodule/EqLocus.lean @@ -68,6 +68,10 @@ theorem le_eqLocus {f g : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} : S ≤ eqLocus f g ↔ Set.EqOn f g S := Iff.rfl +theorem eqOn_eqLocus {f g : M →ₛₗ[τ₁₂] M₂} : + Set.EqOn f g (eqLocus f g) := + fun _ h ↦ h + variable {F : Type*} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] include τ₁₂ in diff --git a/Mathlib/Analysis/FredholmOperator.lean b/Mathlib/Analysis/FredholmOperator.lean new file mode 100644 index 00000000000000..430f8525f16e1f --- /dev/null +++ b/Mathlib/Analysis/FredholmOperator.lean @@ -0,0 +1,477 @@ +/- +Copyright (c) 2026 Filippo A. E. Nuccio. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jon Bannon, Anatole Dedecker, Yongxi Lin, Patrick Massot, Oliver Nash, Filippo A. E. Nuccio +-/ +module + +public import Mathlib.Analysis.Normed.Group.Quotient +public import Mathlib.Analysis.Normed.Module.HahnBanach +public import Mathlib.Analysis.Normed.Operator.Banach +public import Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite +public import Mathlib.Algebra.Module.LinearMap.Index + +/-! +# Fredholm operators between topological vector spaces + +Fix `𝕜` a complete `NontriviallyNormedField`, and `E`, `F` be two Hausdorff topological vector +spaces over `𝕜`. + +We say that a continuous linear map `T : E →L[𝕜] F` is a **Fredholm operator** if it satisfies +the following four equivalent conditions: + +1. `T` is strict, its range is closed and has finite codimension, and its kernel is (topologically) + complemented and has finite dimension. This is chosen as the definition, see `IsFredholm`. +2. `T` admits a continuous **quasi-inverse**, in the sense of `LinearMap.IsQuasiInverse`. +3. There are finite-codimension subspaces `E₁` and `F₁` of `E` and `F` between which `T` induces + an isomorphism. +4. `T` admits a `FredholmPackage`: there are topological decompositions `E = E₁ ⊕ E₀`, + `F = F₁ ⊕ F₀`, where `E₀` and `F₀` are finite dimensional, and an isomorphism `Φ : E₁ ≃L[𝕜] F₁` + such that `T` is zero on `E₀` and coincides with `Φ` on `E₁`; in other words, in these + decompositions, `T` is given by the matrix $$\begin{pmatrix} Φ & 0 \cr 0 & 0 \end{pmatrix}$$ + +## Main definitions + +* `ContinuousLinearMap.IsFredholm`: a continuous linear map `u : E →L[𝕜] F` is a + **Fredholm operator** if it is strict, its range is closed and has finite codimension, and its + kernel is (topologically) complemented and has finite dimension. +* `FredholmDecomposition`: a **Fredholm decomposition** of a topological vector space `E` is the + data of two subspaces `X₀` and `X₁` which are topological complements, and where `X₀` is finite + dimensional. +* `ContinuousLinearMap.FredholmPackage`: a **Fredholm package** for `u : E →L[𝕜] F` is the data of + Fredholm decompositions `decDom` and `decCodom` of `E` and `F` respectively, together with + a continuous linear equivalence `equiv : decDom.X₁ ≃ₗ[𝕜] decCodom.X₁` between the "essential" + (i.e finite codimension) parts of these decompositions, such that `u` equals the composition + `decCodom.X₁.subtypeL ∘L equiv ∘L decDom.proj`. + +Note that the data of a `FredholmPackage` for an operator is morally the strongest of the +equivalent ways to assume that `u` is Fredholm (for example, it is clear how to build a canonical +continuous quasi-inverse of `u` from such a package). + +Hence, you should not typically prove that an operator is Fredholm by building a Fredholm package +(consider using `IsFredholm.of_isInvertible_restrict`); instead, when you know that an operator is +Fredholm, you can obtain a `FredholmPackage` from `IsFredholm.nonempty_fredholmPackage` +in order to conveniently use the full strength of Fredholmness. + +## Main statements + +### Equivalent criterions + +* `ContinuousLinearMap.isFredholm_tfae`: the equivalence between conditions 1, 2, 3 and 4 above. + In practice, most of the interesting directions should be covered by specific API lemmas. +* `ContinuousLinearMap.FredholmPackage.isQuasiInverse`: given a `FredholmPackage` for `u`, + one can build a canonical continuous quasi-inverse of `u`. +* `ContinuousLinearMap.IsFredholm.of_isInvertible_restrict`: if a continuous linear map induces + an isomorphism between finite codimension subspaces, then it is Fredholm. +* `ContinuousLinearMap.IsFredholm.of_restrict` (not in Mathlib yet) is a generalization + of the above: if a continuous linear map induces a Fredholm operator between finite codimension + subspaces, then the original map is Fredholm as well. +* `IsFredholm.nonempty_fredholmPackage`: every Fredholm operator admits a Fredholm package. + This is the primary way to obtain Fredholm packages. + +## Implementation details + +We largely follow [N. Bourbaki, *Théories Spectrales*, Chapitre III, § 3, n° 2][bourbaki2023], +in particular for the proof of equivalence of the four conditions above. +Here are some notable changes : + +* Bourbaki restricts itself to locally convex spaces over `ℝ` or `ℂ`. Yet, under close inspection, + this assumption plays very little role in the beginning of the theory. In fact, at the very mild + cost of assuming that the kernel is complemented in the definition of `IsFredholm` (which follows + from the finiteness assumption if Hahn-Banach is available), we generalize the beginning of the + theory to topological vector spaces over any complete nontrivially normed field. In particular, + our theory naturally captures p-adic Fredholm operators. +* Bourbaki choses the existence of a continuous quasi-inverse as the definition of being Fredholm. + Our choice differs for a very practical reason: it is much simpler to spell out formally + "`u` has a continuous quasi-inverse" than "`u` is strict, its range is closed and has finite + codimension, and its kernel is complemented and has finite dimension". Hence we prefer to give + a name to the latter. + + +## References + +* [N. Bourbaki, *Théories Spectrales*, Chapitre III, § 3, n° 2][bourbaki2023] + +-/ + +@[expose] public noncomputable section + +open Topology Submodule LinearMap +open Set (MapsTo) +open LinearMap.FiniteRangeSetoid + +section TVS +namespace ContinuousLinearMap + +variable {𝕜 E F G : Type*} [NontriviallyNormedField 𝕜] + [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] + [Module 𝕜 E] [Module 𝕜 F] [Module 𝕜 G] + [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] + +/-! +## Definition and equivalent conditions +-/ + +section DefTFAE + +section IsFredholm + +/-- A continuous linear map `u : E →L[𝕜] F` is a **Fredholm operator** if it is strict, +its range is closed and has finite codimension, and its kernel is (topologically) complemented and +has finite dimension. + +See also `isFredholm_tfae` for other equivalent characterizations. +We will also prove later (not in Mathlib yet) that for maps between Banach (or even Fréchet) +spaces over `ℝ` or `ℂ`, all the conditions follow from the kernel and cokernel having finite +dimension. -/ +structure IsFredholm (u : E →L[𝕜] F) : Prop where + isStrictMap : IsStrictMap u + isClosed_range : IsClosed (u.range : Set F) + finite_ker : FiniteDimensional 𝕜 u.ker + finite_coker : u.range.CoFG + closedComplemented_ker : u.ker.ClosedComplemented + +variable [CompleteSpace 𝕜] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] in +/-- A Fredholm operator has (topologically) complemented range. -/ +lemma IsFredholm.closedComplemented_range {u : E →L[𝕜] F} (u_fred : IsFredholm u) : + u.range.ClosedComplemented := + have := u_fred.finite_coker + ClosedComplemented.of_finiteDimensional_quotient u_fred.isClosed_range + +end IsFredholm + +section FredholmDecomposition + +variable (𝕜 E) in +/-- A **Fredholm decomposition** of a topological vector space `E` is the data of two subspaces +`X₀` and `X₁` which are topological complements, and where `X₀` is finite dimensional. + +Note that we purposefully use the index `₀` for the "inessential" (i.e finite dimensional) +part of the decomposition. -/ +structure _root_.FredholmDecomposition where + /-- The inessential (i.e finite dimensional) part of a Fredholm decomposition. -/ + X₀ : Submodule 𝕜 E + /-- The essential (i.e finite co-dimensional) part of a Fredholm decomposition. -/ + X₁ : Submodule 𝕜 E + isTopCompl : IsTopCompl X₁ X₀ + finite_X₀ : FiniteDimensional 𝕜 X₀ + +/-- Given a fredhom decomposition `dec` of the space `E`, `dec.proj` is the (continuous linear) +projection onto the "essential part" `dec.X₁` along the "inessential part" `dec.X₀`. +This is a Fredholm operator. -/ +abbrev _root_.FredholmDecomposition.proj (dec : FredholmDecomposition 𝕜 E) : + E →L[𝕜] dec.X₁ := dec.X₁.projectionOntoL dec.X₀ dec.isTopCompl + +/-- Let `u : E →L[𝕜] F` be a continuous linear map. A **Fredholm package** for `u` is the data of +Fredholm decompositions `decDom` and `decCodom` of `E` and `F` respectively, together with +a continuous linear equivalence `equiv : decDom.X₁ ≃ₗ[𝕜] decCodom.X₁` between the "essential" +(i.e finite codimension) parts of these decompositions, such that `u` equals the composition +`decCodom.X₁.subtypeL ∘L equiv ∘L decDom.proj`. In other words, in these +"essential ⊕ inessential" decompositions, the matrix of `u` is +$$\begin{pmatrix} \texttt{equiv} & 0 \cr 0 & 0 \end{pmatrix}$$ + +We will show in `isFredholm_tfae` that an operator is Fredholm if and only if it admits +a Fredholm package. In practice, the condition that `u` is Fredholm is always easier to +prove, so if you need a Fredholm package you should probably get it from +`IsFredholm.nonempty_fredholmPackage` or `IsFredholm.fredholmPackage`. -/ +structure FredholmPackage (u : E →L[𝕜] F) where + /-- A `FredholmDecomposition` of the domain. -/ + decDom : FredholmDecomposition 𝕜 E + /-- A `FredholmDecomposition` of the codomain. -/ + decCodom : FredholmDecomposition 𝕜 F + /-- An isomorphism between the essential parts of `decDom` and `decCodom`. -/ + equiv : decDom.X₁ ≃L[𝕜] decCodom.X₁ + eq_equiv : u = decCodom.X₁.subtypeL ∘L equiv ∘L decDom.proj + +lemma FredholmPackage.ker_eq {u : E →L[𝕜] F} (pkg : FredholmPackage u) : + u.ker = pkg.decDom.X₀ := by simp [pkg.eq_equiv, ker_comp] + +lemma FredholmPackage.range_eq {u : E →L[𝕜] F} (pkg : FredholmPackage u) : + u.range = pkg.decCodom.X₁ := by + simp [pkg.eq_equiv, range_comp] + +lemma FredholmPackage.mapsTo {u : E →L[𝕜] F} (pkg : FredholmPackage u) : + MapsTo u pkg.decDom.X₁ pkg.decCodom.X₁ := by + simpa [← FredholmPackage.range_eq, LinearMap.coe_range] using Set.mapsTo_range _ _ + +lemma FredholmPackage.equiv_eq_restrict {u : E →L[𝕜] F} (pkg : FredholmPackage u) : + pkg.equiv = u.restrict pkg.mapsTo := by + ext x + simp [pkg.eq_equiv] + +lemma FredholmPackage.isInvertible_restrict {u : E →L[𝕜] F} (pkg : FredholmPackage u) : + u.restrict pkg.mapsTo |>.IsInvertible := + ⟨pkg.equiv, pkg.equiv_eq_restrict⟩ + +/-- The data of a Fredholm package for `u` determines a canonical quasi-inverse of `u`. -/ +def FredholmPackage.quasiInverse {u : E →L[𝕜] F} (pkg : FredholmPackage u) : + F →L[𝕜] E := + pkg.decDom.X₁.subtypeL ∘L pkg.equiv.symm ∘L pkg.decCodom.proj + +/-- The data of a Fredholm package for `u` determines a canonical quasi-inverse of `u`. -/ +lemma FredholmPackage.isQuasiInverse {u : E →L[𝕜] F} (pkg : FredholmPackage u) : + u.IsQuasiInverse pkg.quasiInverse := by + nth_rw 1 [pkg.eq_equiv, quasiInverse] + have hdom : IsQuasiInverse pkg.decDom.X₁.subtype pkg.decDom.proj := + have := pkg.decDom.finite_X₀ + isQuasiInverse_subtype_projectionOnto _ + have hcodom : IsQuasiInverse pkg.decCodom.X₁.subtype pkg.decCodom.proj := + have := pkg.decCodom.finite_X₀ + isQuasiInverse_subtype_projectionOnto _ + refine .of_comp_left hcodom.symm <| .of_comp_right hdom ?_ + simp_rw [FredholmDecomposition.proj, toLinearMap_comp, toLinearMap_subtypeL, + toLinearMap_projectionOntoL, LinearMap.comp_assoc, projectionOnto_comp_subtype, + LinearMap.comp_id, ← LinearMap.comp_assoc, projectionOnto_comp_subtype, LinearMap.id_comp] + simp [IsQuasiInverse, IsLeftQuasiInverse, IsRightQuasiInverse] + +end FredholmDecomposition + +section TFAE + +end TFAE + +variable [T2Space E] [T2Space F] in +/-- Assume that `u : E →L[𝕜] F` has a continuous quasi-invers. Then there are closed +subspaces of finite codimensions `E₁` and `F₁` between which `u` induces an isomorphism. + +This statement is private because it is superseded by later results: using `isFredholm_tfae`, +you can build a `FredholmPackage` for `u`, and then apply `FredholmPackage.isInvertible_restrict`. +-/ +private theorem exists_restrict_isInvertible_of_isQuasiInverse {u : E →L[𝕜] F} + {v : F →L[𝕜] E} (huv : u.IsQuasiInverse v) : + ∃ (E₁ : Submodule 𝕜 E) (F₁ : Submodule 𝕜 F), + IsClosed (E₁ : Set E) ∧ IsClosed (F₁ : Set F) ∧ + E₁.CoFG ∧ F₁.CoFG ∧ + ∃ h : MapsTo u E₁ F₁, (u.restrict h).IsInvertible := by + obtain ⟨huv, hvu⟩ := huv + rw [IsLeftQuasiInverse, Setoid.comm, equiv_iff_eqLocus_coFG] at huv + rw [IsRightQuasiInverse, Setoid.comm, equiv_iff_eqLocus_coFG] at hvu + set E₁ := (ContinuousLinearMap.id 𝕜 E).eqLocus (v ∘L u) + set F₁ := (ContinuousLinearMap.id 𝕜 F).eqLocus (u ∘L v) + have u_mapsto : MapsTo u E₁ F₁ := fun x hx ↦ congr(u $hx) + have v_mapsto : MapsTo v F₁ E₁ := fun x hx ↦ congr(v $hx) + refine ⟨E₁, F₁, isClosed_eqLocus _ _, isClosed_eqLocus _ _, hvu, huv, u_mapsto, ?_⟩ + refine .of_inverse (g := v.restrict v_mapsto) ?_ ?_ + · ext ⟨x, hx : x = u (v x)⟩; simp [← hx] + · ext ⟨x, hx : x = v (u x)⟩; simp [← hx] + +variable [CompleteSpace 𝕜] + [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] + [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] + +variable [T2Space F] in +/-- Assume that `u : E →L[𝕜] F` restricts to an isomorphism between closed finite co-dimension +subspaces `E₁` and `F₁`. Then `u` is Fredholm. + +In fact it is enough to assume that the restriction `E₁ →L[𝕜] F₁` is Fredholm, see +`IsFredholm.of_restrict` (not in Mathlib yet). -/ +theorem IsFredholm.of_isInvertible_restrict {u : E →L[𝕜] F} + {E₁ : Submodule 𝕜 E} (E₁_closed : IsClosed (E₁ : Set E)) [E₁_coFG : E₁.CoFG] + {F₁ : Submodule 𝕜 F} (F₁_closed : IsClosed (F₁ : Set F)) [F₁_coFG : F₁.CoFG] + (h_mapsto : MapsTo u E₁ F₁) (h_inv : (u.restrict h_mapsto).IsInvertible) : + IsFredholm u := by + obtain ⟨e, he⟩ := h_inv + have eqL : u.domRestrict E₁ = F₁.subtypeL ∘L e := congr(F₁.subtypeL ∘L $he).symm + have eqₗ : u.toLinearMap.domRestrict E₁ = F₁.subtype ∘ₗ e := congr(($eqL).toLinearMap) + have h : Topology.IsStrictMap u ∧ IsClosed (u.range : Set F) := by + rw [u.isStrictMap_isClosed_range_iff_restrict E₁ E₁_closed, ← LinearMap.range_domRestrict, + eqₗ, eqL] + exact ⟨F₁.isEmbedding_subtype.comp e.isHomeomorph.isEmbedding |>.isStrictMap, by simpa⟩ + have disj : Disjoint E₁ u.ker := by + rw [disjoint_iff_comap_eq_bot, ← LinearMap.ker_domRestrict, eqₗ, + LinearMap.ker_comp, ker_subtype, comap_bot, LinearEquiv.ker] + constructor + · exact h.1 + · exact h.2 + · rw [← Submodule.fg_iff_finiteDimensional] + exact E₁_coFG.fg_of_disjoint disj.symm + · refine F₁_coFG.of_le (le_trans ?_ (u.range_domRestrict_le_range E₁)) + rw [eqₗ, LinearMap.range_comp, LinearEquiv.range, Submodule.map_top, range_subtype] + · exact .of_disjoint_of_finiteDimensional_quotient E₁_closed disj.symm + +omit [ContinuousSMul 𝕜 E] in +/-- Let `u : E →L[𝕜] F` be a Fredholm operator. Given `dom₁` (resp. `codom₀`) be an arbitrary +topological complement of `u.ker` (resp. `u.range`), we get a `FredholmPackage` for `u` +by considering the decompositions `E = dom₁ ⊕ u.ker`, `F = u.range ⊕ codom₀`, and the isomorphism +`dom₁ ≃L[𝕜] u.range` induced by `u`. + +If you need control over the decompositions, this is the primary way to get a `FredholmPackage`. +Otherwise, see `IsFredholm.nonempty_fredholmPackage`. -/ +def IsFredholm.fredholmPackage {u : E →L[𝕜] F} + (u_fred : IsFredholm u) {dom₁ : Submodule 𝕜 E} {codom₀ : Submodule 𝕜 F} + (h_dom : IsTopCompl u.ker dom₁) (h_codom : IsTopCompl u.range codom₀) : + FredholmPackage u where + decDom := { + X₀ := u.ker + X₁ := dom₁ + isTopCompl := h_dom.symm + finite_X₀ := u_fred.finite_ker } + decCodom := { + X₀ := codom₀ + X₁ := u.range + isTopCompl := h_codom + finite_X₀ := .of_fg <| u_fred.finite_coker.fg_of_isCompl h_codom.isCompl } + equiv := + letI Φ : dom₁ ≃L[𝕜] E ⧸ u.ker := u.ker.quotientEquivOfIsTopCompl dom₁ h_dom |>.symm + letI Ψ : (E ⧸ u.ker) ≃L[𝕜] u.range := .quotKerEquivRange u_fred.isStrictMap + Φ.trans Ψ + eq_equiv := by + refine LinearMap.ext_on_codisjoint h_dom.isCompl.codisjoint ?_ ?_ + · intro x (hx : u x = 0) + simp [hx, projection_apply_of_mem_right] + · intro x (hx : x ∈ dom₁) + simp [hx, projection_apply_of_mem_left, ContinuousLinearEquiv.quotKerEquivRange] + +omit [ContinuousSMul 𝕜 E] in +/-- Every Fredholm operator admits a `FredholmPackage`. + +This is the primary way to get a `FredholmPackage` if you don't need control of the decompositions. +If you do, see `IsFredholm.fredholmPackage`. -/ +theorem IsFredholm.nonempty_fredholmPackage {u : E →L[𝕜] F} + (u_fred : IsFredholm u) : Nonempty (FredholmPackage u) := by + obtain ⟨codom₂, h_codom⟩ := u_fred.closedComplemented_range.exists_isTopCompl + obtain ⟨dom₁, h_dom⟩ := u_fred.closedComplemented_ker.exists_isTopCompl + exact ⟨u_fred.fredholmPackage h_dom h_codom⟩ + +variable [T2Space E] [T2Space F] + +/-- +Let `E`, `F` be two Hausdorff topological vector spaces over a complete `NontriviallyNormedField` +denoted `𝕜`, and `u : E →L[𝕜] F` a continuous linear map. The followng conditions are equivalent: + +1. `T` is a **Fredholm operator**, in the sense of `ContinuousLinearMap.IsFredholm`. +2. `T` admits a continuous **quasi-inverse**, in the sense of `LinearMap.IsQuasiInverse`. +3. There are finite-codimension subspaces `E₁` and `F₁` of `E` and `F` between which `T` induces + an isomorphism. +4. `T` admits a `FredholmPackage`. + +In practice, condition `4` is the "strongest", so you should probably not use it to *prove* that an +operator is Fredholm. +-/ +theorem isFredholm_tfae (u : E →L[𝕜] F) : List.TFAE + [ + IsFredholm u, + ∃ v : F →L[𝕜] E, u.IsQuasiInverse v, + ∃ (E₁ : Submodule 𝕜 E) (F₁ : Submodule 𝕜 F), + IsClosed (E₁ : Set E) ∧ IsClosed (F₁ : Set F) ∧ + E₁.CoFG ∧ F₁.CoFG ∧ + ∃ h : MapsTo u E₁ F₁, (u.restrict h).IsInvertible, + Nonempty (FredholmPackage u) + ] := by + tfae_have 1 → 4 := IsFredholm.nonempty_fredholmPackage + tfae_have 4 → 2 := by + rintro ⟨dec⟩ + exact ⟨dec.quasiInverse, dec.isQuasiInverse⟩ + tfae_have 2 → 3 := by + rintro ⟨v, huv⟩ + exact exists_restrict_isInvertible_of_isQuasiInverse huv + tfae_have 3 → 1 := by + rintro ⟨E₁, F₁, E₁_closed, F₁_closed, E₁_coFG, F₁_coFG, u_mapsto, u_invertible⟩ + exact .of_isInvertible_restrict E₁_closed F₁_closed u_mapsto u_invertible + tfae_finish + +/-- If `u` has a Fredholm package, it is Fredholm. -/ +theorem FredholmPackage.isFredholm {u : E →L[𝕜] F} (pkg : FredholmPackage u) : + IsFredholm u := + isFredholm_tfae u |>.out 3 0 |>.mp (Nonempty.intro pkg) + +theorem isFredholm_iff_exists_isQuasiInverse {u : E →L[𝕜] F} : + IsFredholm u ↔ ∃ v : F →L[𝕜] E, u.IsQuasiInverse v := + isFredholm_tfae u |>.out 0 1 + +end DefTFAE + +section Constructions + +theorem _root_.ContinuousLinearEquiv.isFredholm (e : E ≃L[𝕜] F) : + IsFredholm (e : E →L[𝕜] F) where + isStrictMap := e.isHomeomorph.isStrictMap + isClosed_range := by simp + finite_ker := by + rw [LinearMap.ker_eq_bot.2 (by exact e.injective)] + infer_instance + finite_coker := by simp + closedComplemented_ker := by simp + +theorem IsFredholm.id : IsFredholm (.id 𝕜 E) := + ContinuousLinearEquiv.refl 𝕜 E |>.isFredholm + +theorem _root_.Topology.IsClosedEmbedding.isFredholmStruct {f : E →L[𝕜] F} + (hf : IsClosedEmbedding f) (hcofg : f.range.CoFG) : + IsFredholm f where + isStrictMap := hf.isStrictMap + isClosed_range := hf.isClosed_range + finite_ker := by + rw [LinearMap.ker_eq_bot.2 hf.injective] + infer_instance + finite_coker := by simp [hcofg] + closedComplemented_ker := by + rw [LinearMap.ker_eq_bot.2 hf.injective] + exact closedComplemented_bot + +theorem _root_.Submodule.isFredholm_subtypeL {p : Submodule 𝕜 E} + (hp : IsClosed (p : Set E)) (hc : p.CoFG) : + IsFredholm p.subtypeL := + (IsClosedEmbedding.subtypeVal hp).isFredholmStruct (by simpa) + +theorem _root_.Topology.IsQuotientMap.isFredholm {f : E →L[𝕜] F} (hq : IsQuotientMap f) + (hfg : FiniteDimensional 𝕜 f.ker) (hcompl : f.ker.ClosedComplemented) : + IsFredholm f where + isStrictMap := hq.isStrictMap + isClosed_range := by + rw [LinearMap.range_eq_top.2 hq.surjective] + exact isClosed_univ + finite_ker := hfg + finite_coker := by + rw [LinearMap.range_eq_top.2 hq.surjective] + exact Submodule.CoFG.top + closedComplemented_ker := hcompl + +theorem _root_.Submodule.mkQL_isFredholmStruct {p : Submodule 𝕜 E} (hc : FiniteDimensional 𝕜 p) + (hcompl : p.ClosedComplemented) : + IsFredholm p.mkQL := + p.isQuotientMap_mkQL.isFredholm (by rwa [toLinearMap_mkQL, ker_mkQ]) (by simpa) + +variable [CompleteSpace 𝕜] [IsTopologicalAddGroup E] [IsTopologicalAddGroup F] + [IsTopologicalAddGroup G] [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] [ContinuousSMul 𝕜 G] + [T2Space E] [T2Space F] [T2Space G] + +theorem isFredholm_congr {u u' : E →L[𝕜] F} (h : u.toLinearMap ≈ u'.toLinearMap) : + IsFredholm u ↔ IsFredholm u' := by + simp_rw [isFredholm_iff_exists_isQuasiInverse] + refine exists_congr fun _ ↦ isQuasiInverse_congr (Setoid.symm h) (Setoid.refl _) + +theorem IsFredholm.congr {u u' : E →L[𝕜] F} (hu : IsFredholm u) + (h : u.toLinearMap ≈ u'.toLinearMap) : + IsFredholm u' := by + rwa [← isFredholm_congr h] + +theorem IsFredholm.comp {f' : F →L[𝕜] G} {f : E →L[𝕜] F} (hf' : IsFredholm f') + (hf : IsFredholm f) : IsFredholm (f' ∘L f) := by + rw [isFredholm_iff_exists_isQuasiInverse] at * + rcases hf with ⟨g, hg⟩ + rcases hf' with ⟨g', hg'⟩ + exact ⟨g ∘L g', hg'.comp hg⟩ + +theorem IsFredholm.comp_iff_left {f : E →L[𝕜] F} {f' : F →L[𝕜] G} (hf : IsFredholm f) : + IsFredholm (f' ∘L f) ↔ IsFredholm f' := by + refine ⟨fun hcomp ↦ ?_, fun hf' ↦ hf'.comp hf⟩ + rw [isFredholm_iff_exists_isQuasiInverse, toLinearMap_comp] at * + rcases hf with ⟨g, hg⟩ + rcases hcomp with ⟨w, hw⟩ + exact ⟨f ∘L w, .symm <| hg.symm.of_comp_left hw.symm⟩ + +theorem IsFredholm.comp_iff_right {f : E →L[𝕜] F} {f' : F →L[𝕜] G} (hf' : IsFredholm f') : + IsFredholm (f' ∘L f) ↔ IsFredholm f := by + refine ⟨fun hcomp ↦ ?_, fun hf ↦ hf'.comp hf⟩ + rw [isFredholm_iff_exists_isQuasiInverse, toLinearMap_comp] at * + rcases hf' with ⟨g', hg'⟩ + rcases hcomp with ⟨w, hw⟩ + exact ⟨w ∘L f', .symm <| hg'.symm.of_comp_right hw.symm⟩ + +end Constructions + +end ContinuousLinearMap +end TVS + +end diff --git a/Mathlib/Analysis/Normed/Operator/Perturbation/StrictByFinite.lean b/Mathlib/Analysis/Normed/Operator/Perturbation/StrictByFinite.lean new file mode 100644 index 00000000000000..e543095d44b422 --- /dev/null +++ b/Mathlib/Analysis/Normed/Operator/Perturbation/StrictByFinite.lean @@ -0,0 +1,349 @@ +/- +Copyright (c) 2026 Anatole Dedecker. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anatole Dedecker +-/ +module + +public import Mathlib.RingTheory.Finiteness.Cofinite +public import Mathlib.Topology.Maps.Strict.Module +public import Mathlib.Topology.LocalAtTarget +public import Mathlib.Topology.Algebra.Module.FiniteDimension +public import Mathlib.Algebra.Module.LinearMap.FiniteRange + +/-! +# Strict linear maps with closed range are closed under finite-rank perturbation + +Fix `𝕜` a complete nontrivially normed field, and `E`, `F` two topological vector spaces +over `𝕜`. This file contains various results expressing that the set of continuous +linear maps `u : E →L[𝕜] F` which are **strict** and have **closed range** is +"stable under finite-rank perturbations". + +More precisely, we prove the following statements: +* `ContinuousLinearMap.isStrictMap_isClosed_range_iff_restrict`: given a closed + subspace `A` of `E` of finite codimension, we have that `u` is strict with closed range + if and only if `u.domRestrict A` is strict with closed range. +* `ContinuousLinearMap.isStrictMap_isClosed_range_iff_of_finiteRangeSetoid`: if `u, v : E →L[𝕜] F` + differ by a finite rank continuous linear map, then `u` is strict with closed range if and only + if `v` is strict with closed range. +* `ContinuousLinearMap.isStrictMap_isClosed_range_iff_quotient`: given a *complemented* + finite dimensional subspace `B` of `F`, we have that `u` is strict with closed range + if and only if `B.mkQL ∘L u` is strict with closed range. + +These three results show up crucially when developing the theory of Fredholm operators +between topological vector spaces. Note that none of the results here use the Hahn-Banach +theorem, so there is no significant restriction on the field. + +## Implementation details + +There are two notable changes compared to Bourbaki. +* We treat all topological vector spaces over complete nontrivially normed fields, + where Bourbaki restricts to locally convex spaces over `ℝ` or `ℂ`. To do so, we have to + tweak one statement by assuming that a finite dimensional subspace is complemented, which + is always the case when you have Hahn-Banach available. +* We give a different proof, where we reduce the statement to + `AddMonoidHom.isStrictMap_prodMap_iff`. This gives a slightly longer proof, but we + claim that it is more natural. + +Note that these two changes are independent: the extra generality could have been achieved +with Bourbaki's proof. + +## References + +* [N. Bourbaki, *Théories Spectrales*, Chapitre III, § 3, n° 1][bourbaki2023] + +-/ + +open Topology Set Submodule Function ContinuousLinearMap + +variable {𝕜 : Type*} + [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] + +variable {E F : Type*} + [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] + [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] + [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] + +section FiniteCodimSubspace + +/-! +## Proof of `ContinuousLinearMap.isStrictMap_isClosed_range_iff_restrict` + +Let `u : E →L[𝕜] F` be a continuous linear map, and `A` a finite codimension closed +subspace of `E`. We want to show that `u` is strict with closed range if and only if +`u.domRestrict A` is strict with closed range. + +We do the proof in five steps. +-/ + +/-! +### Step 1 + +We prove the theorem under the assumptions that +- `u` is surjective +- `u.ker` is disjoint from `A` (i.e. `u` is injective on `A`) +- `map u A` is closed + +The strategy of proof is to decompose both spaces into complementary subspace, +with one of the spaces being finite dimensional and `u` preserving this decomposition. + +The result then follows from `AddMonoidHom.isStrictMap_prodMap_iff` and +`ContinuousLinearMap.isStrictMap_of_finiteDimensional`. +-/ + +theorem step1 [T2Space F] (u : E →L[𝕜] F) (A : Submodule 𝕜 E) + (A_closed : IsClosed (A : Set E)) [A_cofg : A.CoFG] + (h_ker : Disjoint u.ker A) (h_range : u.range = ⊤) + (uA_closed : IsClosed (map u.toLinearMap A : Set F)) : + IsStrictMap u ↔ IsStrictMap (u.domRestrict A) := by + -- Fix `S` an algebraic complement of `A` containing `u.ker`. It has finite dimension. + rcases h_ker.exists_isCompl with ⟨S, ker_le_S, S_compl_A⟩ + have : FiniteDimensional 𝕜 S := .of_fg <| A_cofg.fg_of_isCompl S_compl_A.symm + -- Because `u` is assumed surjective and `S ⊔ A = ⊤`, we have `map u S ⊔ map u A = ⊤`. + -- Furthermore, because the kernel of `u` is fully contained in `S`, we can show that + -- `map u S ⊓ map u A = ⊥`, so that `map u S` and `map u A` are in fact algebraic complements + -- of each other. + have uS_compl_uA : IsCompl (map u.toLinearMap S) (map u.toLinearMap A) := + ⟨disjoint_map_of_ker_le_left S_compl_A.disjoint ker_le_S, + codisjoint_map (LinearMap.range_eq_top.mp h_range) S_compl_A.codisjoint⟩ + -- Because `A` (resp. `map u A`) is closed and `S` (resp `map u S`) has finite dimension, + -- `A` and `S` (resp `map u A` and `map u S`) are in fact *topological* complements of each other. + replace S_compl_A : IsTopCompl S A := + S_compl_A.symm.isTopCompl_of_finiteDimensional_quotient A_closed |>.symm + replace uS_compl_uA : IsTopCompl (map u.toLinearMap S) (map u.toLinearMap A) := + uS_compl_uA.symm.isTopCompl_of_isClosed_of_finiteDimensional uA_closed |>.symm + -- Thus, we have decomposed both the domain and the codomain into topopological complements, + -- and `u` preserves this decomposition, inducing maps `uₛ : S → map u S` and `uₐ : A → map u A`. + set uₛ : S →L[𝕜] map u.toLinearMap S := u.restrict (fun _ ↦ mem_map_of_mem) + set uₐ : A →L[𝕜] map u.toLinearMap A := u.restrict (fun _ ↦ mem_map_of_mem) + -- Using the corresponding isomorphisms `(S × A) ≃L[𝕜] E` and `(map u S × map u A) ≃L[𝕜] F`, + -- we have to show that the map `uₛ.prodMap uₐ : S × A → map u S × map u A` is strict + -- if and only if `uₐ : A → map u A` is strict. + -- This follows from `AddMonoidHom.isStrictMap_prodMap_iff`, and the fact that `uₛ` is a + -- continuous linear map between finite dimensional spaces, hence a strict map. + set Φ : (S × A) ≃L[𝕜] E := prodEquivOfIsTopCompl S A S_compl_A + set Ψ : (map u.toLinearMap S × map u.toLinearMap A) ≃L[𝕜] F := + prodEquivOfIsTopCompl _ _ uS_compl_uA + have u_eq : u = Ψ ∘ (uₛ.prodMap uₐ) ∘ Φ.symm := by + ext x + simp [Φ, Ψ, uₛ, uₐ, ← map_add, projection_add_projection_eq_self] + have u_restr_eq : u.domRestrict A = (map u.toLinearMap A).subtypeL ∘ uₐ := rfl + suffices IsStrictMap (uₛ.prodMap uₐ) ↔ IsStrictMap uₐ by + rwa [u_restr_eq, u_eq, ← (isEmbedding_subtypeL _).isStrictMap_iff, + ← Ψ.isHomeomorph.isEmbedding.isStrictMap_iff, + ← Φ.symm.isHomeomorph.isQuotientMap.isStrictMap_iff] + simp_rw [← coe_coe, ContinuousLinearMap.coe_prodMap, LinearMap.isStrictMap_prodMap_iff, + coe_coe, uₛ.isStrictMap_of_finiteDimensional, true_and] + +/-! +### Step 2 + +We prove the theorem under the assumptions that +- `u` is surjective +- `u.ker` is disjoint from `A` (i.e. `u` is injective on `A`) +-/ + +theorem step2 [T2Space F] (u : E →L[𝕜] F) (A : Submodule 𝕜 E) + (A_closed : IsClosed (A : Set E)) [A_cofg : A.CoFG] + (h_ker : Disjoint u.ker A) (h_range : u.range = ⊤) : + IsStrictMap u ↔ IsStrictMap (u.domRestrict A) ∧ IsClosed (map u.toLinearMap A : Set F) := by + -- To reduce to step 1, it suffices to show that `IsStrictMap u → IsClosed (map u A)`. + suffices IsStrictMap u → IsClosed (map u.toLinearMap A : Set F) by grind only [step1] + -- So, we assume that `u` is strict. Because it is surjective, it is a quotient map. + intro u_strict + have u_quot : IsQuotientMap u := by + rw [LinearMap.range_eq_top, coe_coe] at h_range + simp [isQuotientMap_iff_isStrictMap_surjective, h_range, u_strict] + -- Hence, we have to check that `comap u (map u A)` is closed. This follows from + -- `A ≤ comap u (map u A)` and the fact that `A` is closed with finite codimension. + rw [← u_quot.isClosed_preimage, ← coe_coe, ← Submodule.comap_coe] + exact Submodule.isClosed_mono_of_finiteDimensional_quotient A_closed (le_comap_map _ _) + +/-! +### Step 3 + +We prove the theorem under the assumptions that +- `u` has closed range +- `u.ker` is disjoint from `A` (i.e. `u` is injective on `A`) +-/ + +theorem step3 [T2Space F] (u : E →L[𝕜] F) (A : Submodule 𝕜 E) + (A_closed : IsClosed (A : Set E)) [A_cofg : A.CoFG] + (h_ker : Disjoint u.ker A) (h_range : IsClosed (u.range : Set F)) : + IsStrictMap u ↔ IsStrictMap (u.domRestrict A) ∧ IsClosed (map u.toLinearMap A : Set F) := by + -- Let `F' := u.range` and `i : F' →L[𝕜] F` be the inclusion map. By assumption, + -- `i` is a closed embedding. + set F' : Submodule 𝕜 F := u.range + set i : F' →L[𝕜] F := F'.subtypeL + have i_clemb : IsClosedEmbedding i := F'.isClosedEmbedding_subtypeL h_range + -- Furthermore, `u` factors as `i ∘ u'` with `u' : E →L[𝕜] F'` surjective, + -- and we clearly have `u.domRestrict A = i ∘ u'.domRestrict A` as well. + set u' : E →L[𝕜] F' := u.rangeRestrict + have range_u' : u'.range = ⊤ := u.range_rangeRestrict + have eq1 : u = i ∘L u' := rfl + have eq2 : u.domRestrict A = i ∘L (u'.domRestrict A) := rfl + -- We can rewrite our goal in terms of `u'`. + simp_rw [eq2, eq1, coe_comp, ← i_clemb.isEmbedding.isStrictMap_iff, toLinearMap_comp, map_comp, + map_coe i.toLinearMap, coe_coe, ← i_clemb.isClosed_iff_image_isClosed] + -- We finish by applying step 2 (using that `u.ker = u'.ker`). + exact step2 u' A A_closed (u.ker_rangeRestrict ▸ h_ker) range_u' + +/-! +### Step 4 + +We prove the theorem under the assumption that `u.ker` is disjoint from `A` +(i.e. `u` is injective on `A`). +-/ + +theorem step4 [T2Space F] (u : E →L[𝕜] F) (A : Submodule 𝕜 E) (A_closed : IsClosed (A : Set E)) + [A_cofg : A.CoFG] (h_ker : Disjoint u.ker A) : + (IsStrictMap u ∧ IsClosed (u.range : Set F)) ↔ + IsStrictMap (u.domRestrict A) ∧ IsClosed (map u.toLinearMap A : Set F) := by + -- To reduce to step 3, it suffices to show that, if `map u A` is closed, then so is `u.range`. + suffices IsClosed (map u.toLinearMap A : Set F) → IsClosed (u.range : Set F) by + grind only [step3] + -- This follows from a general lemma, but we recall the proof below for completeness + exact u.toLinearMap.isClosed_range_of_isClosed_map_of_finiteDimensional_quotient + -- Assume that `map u A` is closed, and fix `S` an algebraic complement of `A`. + -- It has finite dimension. Then `u.range = map u A ⊔ map u S` is the supremum of + -- a closed subspace and a finite dimnsional subspace, hence it is closed. + +/-! +### Step 5 + +We now deduce from the previous steps the full strength of the theorem. +-/ + +/-- Consider `u : E →L[𝕜] F` and `A` a closed subspace of `E` of finite codimension. +We have that `u` is strict with closed range if and only if `u.domRestrict A` is strict with +closed range. + +This is [N. Bourbaki, *Théories Spectrales*, Chapitre III, § 3, n° 1, Prop. 1][bourbaki2023]. -/ +public theorem ContinuousLinearMap.isStrictMap_isClosed_range_iff_restrict [T2Space F] + (u : E →L[𝕜] F) (A : Submodule 𝕜 E) (A_closed : IsClosed (A : Set E)) + [A_cofg : A.CoFG] : + (IsStrictMap u ∧ IsClosed (u.range : Set F)) ↔ + (IsStrictMap (u.domRestrict A) ∧ IsClosed (map u.toLinearMap A : Set F)) := by + -- To reduce to step 4, we quotient by `N := A ⊓ u.ker`. Denoting by `π : E → E ⧸ N` + -- the (automatically open) quotient map, `u` factors as `v ∘ π` with `v : E ⧸ N → F`. + set N : Submodule 𝕜 E := A ⊓ u.ker + set π : E →L[𝕜] E ⧸ N := N.mkQL + set v : E ⧸ N →L[𝕜] F := N.liftQL u inf_le_right + have π_quot : IsOpenQuotientMap π := N.isOpenQuotientMap_mkQL + have u_eq : u = v ∘L π := rfl + -- We also consider the submodule `B := map π A` of `E ⧸ N`. It has finite codimension and, + -- by construction, it is disjoint from the kernel of `v`. + set B : Submodule 𝕜 (E ⧸ N) := map N.mkQ A + have B_cofg : B.CoFG := + quotientQuotientEquivQuotient N A inf_le_left |>.symm.finiteDimensional + have v_ker : Disjoint v.ker B := by + simp [disjoint_iff, v, B, toLinearMap_liftQL, ker_liftQ, + map_inf_eq_map_inf_comap, comap_map_mkQ, N, inf_comm] + -- Because `A` contains `N`, we have `A = comap π B`. In particular, `B` is closed. + have comap_B : comap π.toLinearMap B = A := by simp [B, N, π] + have A_mapsTo_B : MapsTo π A B := fun _ ↦ by simp [← comap_B] + have B_closed : IsClosed (B : Set <| E ⧸ N) := by + rwa [← π_quot.isQuotientMap.isClosed_preimage, ← π.coe_coe, ← comap_coe, comap_B] + -- Thus, we can apply step 4 to `v` and `B`: we get that `v` is strict with closed range if + -- and only if `v.domRestrict B` is strict with closed range. + have step4_output : (IsStrictMap v ∧ IsClosed (v.range : Set F)) ↔ + (IsStrictMap (v.domRestrict B) ∧ IsClosed (map v.toLinearMap B : Set F)) := + step4 v B B_closed v_ker + -- Now, we wish to reduce our statement about `u` and `u.domRestrict A` + -- to what we know about `v` and `v.domRestrict B`. + -- First, it is clear that `range u = range v` and `map u A = map v B`. + have range_eq : v.range = u.range := range_liftQ _ _ _ + have image_eq : map v.toLinearMap B = map u.toLinearMap A := by + simp [B, u_eq, π, ← map_comp] + -- Now, recall the equality `A = comap π B`; it ensures that the restriction + -- `π' : A → B` of the open quotient map `π` is *still* an (open) quotient map. + set π' : A →L[𝕜] B := π.restrict A_mapsTo_B + have π'_quot : IsOpenQuotientMap π' := by + let φ : (N.mkQL ⁻¹' B) ≃ₜ A := .setCongr congr(SetLike.coe $comap_B) + exact N.isOpenQuotientMap_mkQL.restrictPreimage B |>.comp + φ.symm.isOpenQuotientMap + -- Note that `u.domRestrict A` factors as `v.domRestrict B ∘ π'`. + have u_restr_eq : u.domRestrict A = v.domRestrict B ∘L π' := rfl + -- We conclude by invoking `IsQuotientMap.isStrictMap_iff` twice, to get that strictness of + -- `u` (resp. `u.domRestrict A`) is equivalent to strictness of `v` (resp. `v.domRestrict B`). + calc IsStrictMap u ∧ IsClosed (u.range : Set F) + ↔ IsStrictMap v ∧ IsClosed (v.range : Set F) := by + rw [← range_eq, u_eq, coe_comp, π_quot.isQuotientMap.isStrictMap_iff] + _ ↔ IsStrictMap (v.domRestrict B) ∧ IsClosed (map v.toLinearMap B : Set F) := + step4_output + _ ↔ IsStrictMap (u.domRestrict A) ∧ IsClosed (map u.toLinearMap A : Set F) := by + rw [← image_eq, u_restr_eq, coe_comp, π'_quot.isQuotientMap.isStrictMap_iff] + +end FiniteCodimSubspace + +/-! +## Consequences +-/ + +section FiniteRank + +/-- If `u, v : E →L[𝕜] F` agree on a closed subspace `A` of `E` with finite codimension, +then `u` is strict with closed range if and only if `v` is strict with closed range. -/ +public theorem ContinuousLinearMap.isStrictMap_isClosed_range_iff_of_eqOn [T2Space F] + (u v : E →L[𝕜] F) (A : Submodule 𝕜 E) (A_closed : IsClosed (A : Set E)) + [A_cofg : A.CoFG] (h_eqOn : EqOn u v A) : + (IsStrictMap u ∧ IsClosed (u.range : Set F)) ↔ + (IsStrictMap v ∧ IsClosed (v.range : Set F)) := by + simp_rw [u.isStrictMap_isClosed_range_iff_restrict A, + v.isStrictMap_isClosed_range_iff_restrict A, ← LinearMap.range_domRestrict, + LinearMap.coe_range, LinearMap.coe_domRestrict, ContinuousLinearMap.coe_domRestrict, + ContinuousLinearMap.coe_coe, restrict_eq_restrict_iff.mpr h_eqOn] + +open LinearMap.FiniteRangeSetoid + +/-- If `u, v : E →L[𝕜] F` differ by a finite rank linear map (recall that this is +denoted `u.toLinearMap ≈ v.toLinearMap` in scope `LinearMap.FiniteRangeSetoid`), then `u` is +strict with closed range if and only if `v` is strict with closed range. + +This is [N. Bourbaki, *Théories Spectrales*, Chapitre III, § 3, n° 1, Cor. 1][bourbaki2023]. -/ +public theorem ContinuousLinearMap.isStrictMap_isClosed_range_iff_of_finiteRangeSetoid [T2Space F] + (u v : E →L[𝕜] F) (h_equiv : u.toLinearMap ≈ v.toLinearMap) : + (IsStrictMap u ∧ IsClosed (u.range : Set F)) ↔ + (IsStrictMap v ∧ IsClosed (v.range : Set F)) := by + let A := u.toLinearMap.eqLocus v.toLinearMap + have A_closed : IsClosed (A : Set E) := u.isClosed_eqLocus v + have : A.CoFG := equiv_iff_eqLocus_coFG.mp h_equiv + exact ContinuousLinearMap.isStrictMap_isClosed_range_iff_of_eqOn u v A A_closed + LinearMap.eqOn_eqLocus + +end FiniteRank + +section FiniteDimQuotient + +open LinearMap.FiniteRangeSetoid + +/-- Consider `u : E →L[𝕜] F` and `B` a *complemented* finite dimensional subspace of `F`. We have +that `u` is strict with closed range if and only if `B.mkQL ∘L u` is strict with closed range. + +This is [N. Bourbaki, *Théories Spectrales*, Chapitre III, § 3, n° 1, Cor. 2][bourbaki2023]. -/ +public theorem ContinuousLinearMap.isStrictMap_isClosed_range_iff_quotient [T2Space F] + (u : E →L[𝕜] F) (A : Submodule 𝕜 F) [dim_A : FiniteDimensional 𝕜 A] + (A_compl : ClosedComplemented A) : + (IsStrictMap u ∧ IsClosed (u.range : Set F)) ↔ + (IsStrictMap (A.mkQL ∘L u) ∧ IsClosed ((A.mkQL ∘L u).range : Set (F ⧸ A))) := by + obtain ⟨S, A_compl_S⟩ := A_compl.exists_isTopCompl + let Φ : (F ⧸ A) ≃L[𝕜] S := A.quotientEquivOfIsTopCompl S A_compl_S + let i : S →L[𝕜] F := S.subtypeL + have i_clemb : IsClosedEmbedding i := S.isClosedEmbedding_subtypeL A_compl_S.symm.isClosed + set p : F →L[𝕜] F := S.projectionL A A_compl_S.symm with p_def + have eq : i ∘ Φ ∘ A.mkQ = p := rfl + have : u.toLinearMap ≈ (p ∘L u).toLinearMap := by + grw [toLinearMap_comp, p_def, toLinearMap_projectionL, projection_equiv_id, LinearMap.id_comp] + calc IsStrictMap u ∧ IsClosed (range u) + _ ↔ (IsStrictMap (p ∘ u) ∧ IsClosed (range (p ∘ u))) := + ContinuousLinearMap.isStrictMap_isClosed_range_iff_of_finiteRangeSetoid _ _ this + _ ↔ (IsStrictMap (i ∘ Φ ∘ A.mkQ ∘ u) ∧ IsClosed (range (i ∘ Φ ∘ A.mkQ ∘ u))) := by + simp_rw [← eq, Function.comp_assoc] + _ ↔ (IsStrictMap (Φ ∘ A.mkQ ∘ u) ∧ IsClosed (range (Φ ∘ A.mkQ ∘ u))) := by + rw [i_clemb.isStrictMap_iff, i_clemb.isClosed_iff_image_isClosed, ← range_comp] + _ ↔ (IsStrictMap (A.mkQ ∘ u) ∧ IsClosed (range (A.mkQ ∘ u))) := by + rw [Φ.isHomeomorph.isEmbedding.isStrictMap_iff, + Φ.isHomeomorph.isClosedEmbedding.isClosed_iff_image_isClosed, + ← range_comp] + +end FiniteDimQuotient diff --git a/Mathlib/Topology/Algebra/Module/FiniteDimension.lean b/Mathlib/Topology/Algebra/Module/FiniteDimension.lean index 9e16cef2540d80..2ecc959cdc91e9 100644 --- a/Mathlib/Topology/Algebra/Module/FiniteDimension.lean +++ b/Mathlib/Topology/Algebra/Module/FiniteDimension.lean @@ -553,6 +553,17 @@ theorem Submodule.isClosed_sup_finiteDimensional rw [← comap_map_mkQ] exact (map s.mkQ t).closed_of_finiteDimensional.preimage continuous_quot_mk +/-- Let `f : E →ₗ[𝕜] F` be a linear map, and `s` a subspace of `E` with finite codimension. +If the image of `s` by `f` is closed, the the range of `f` is closed. -/ +theorem LinearMap.isClosed_range_of_isClosed_map_of_finiteDimensional_quotient + {E : Type*} [AddCommGroup E] [Module 𝕜 E] {f : E →ₗ[𝕜] F} {s : Submodule 𝕜 E} + [hs : FiniteDimensional 𝕜 (E ⧸ s)] (h : IsClosed (s.map f : Set F)) : + IsClosed (f.range : Set F) := by + obtain ⟨t, s_compl_t⟩ := Submodule.exists_isCompl s + have : FiniteDimensional 𝕜 t := .of_fg <| Submodule.CoFG.fg_of_isCompl s_compl_t hs + rw [← Submodule.map_top, ← s_compl_t.sup_eq_top, Submodule.map_sup] + exact Submodule.isClosed_sup_finiteDimensional _ _ h + /-- An injective linear map with finite-dimensional domain is a closed embedding. -/ theorem LinearMap.isClosedEmbedding_of_injective [T2Space E] [FiniteDimensional 𝕜 E] [T2Space F] {f : E →ₗ[𝕜] F} (hf : LinearMap.ker f = ⊥) : IsClosedEmbedding f := diff --git a/Mathlib/Topology/Maps/Strict/Module.lean b/Mathlib/Topology/Maps/Strict/Module.lean new file mode 100644 index 00000000000000..d977ac68bfb395 --- /dev/null +++ b/Mathlib/Topology/Maps/Strict/Module.lean @@ -0,0 +1,74 @@ +/- +Copyright (c) 2026 Anatole Dedecker. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anatole Dedecker +-/ +module + +public import Mathlib.LinearAlgebra.Isomorphisms +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient +public import Mathlib.Topology.Algebra.Module.Equiv +public import Mathlib.Topology.Maps.Strict.Group + +/-! +# Strict Group Homomorphisms + +In this file, we study continuous linear maps which are *strict* in the sense of +`Topology.IsStrictMap`. So far, all the results in this file are direct +adaptations from the theory of strict homomorphisms of topological additive groups. +-/ + + +@[expose] public section + +open Function Set Topology QuotientGroup + +namespace LinearMap + +variable {R S M N Nₗ M' Nₗ' : Type*} [Ring R] [Ring S] {σ : R →+* S} + [AddCommGroup M] [AddCommGroup N] [AddCommGroup Nₗ] [AddCommGroup M'] [AddCommGroup Nₗ'] + [Module R M] [Module S N] [Module R Nₗ] [Module R M'] [Module R Nₗ'] + {f : M →ₛₗ[σ] N} {fₗ : M →ₗ[R] Nₗ} {gₗ : M' →ₗ[R] Nₗ'} + [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace Nₗ] + +/-- A linear map `f : E → F` is strict if and only the induced map `E ⧸ f.ker → F` is an +embedding. -/ +protected lemma isStrictMap_iff_isEmbedding_liftQ_ker : + IsStrictMap f ↔ IsEmbedding (f.ker.liftQ f le_rfl) := + f.toAddMonoidHom.isStrictMap_iff_isEmbedding_kerLift + +/-- A linear map `f : E → F` is strict if and only if the canonical isomorphism +`E ⧸ f.ker ≃ f.range` is a homeomorphism. -/ +protected lemma isStrictMap_iff_isHomeomorph_quotKerEquivRange : + IsStrictMap fₗ ↔ IsHomeomorph (fₗ.quotKerEquivRange) := by + simp_rw [isHomeomorph_iff_isStrictMap_bijective, EquivLike.bijective, and_true, + fₗ.ker.isQuotientMap_mkQ.isStrictMap_iff, IsEmbedding.subtypeVal.isStrictMap_iff] + rfl + +/-- The isomorphism of topological modules `E ⧸ f.ker ≃ f.range` given by a strict linear +map `f : E → F`. This is an avatar of the first isomorphism theorem. -/ +noncomputable def _root_.ContinuousLinearEquiv.quotKerEquivRange + (hf : IsStrictMap fₗ) : (M ⧸ fₗ.ker) ≃L[R] fₗ.range := + .ofIsHomeomorph fₗ.quotKerEquivRange (fₗ.isStrictMap_iff_isHomeomorph_quotKerEquivRange.mp hf) + +variable [IsTopologicalAddGroup M] + +/-- A linear map is strict if and only if its `rangeRestrict` is an open quotient map. -/ +protected lemma isStrictMap_iff_isOpenQuotientMap_rangeRestrict [RingHomSurjective σ] : + IsStrictMap f ↔ IsOpenQuotientMap f.rangeRestrict := + f.toAddMonoidHom.isStrictMap_iff_isOpenQuotientMap_rangeRestrict + +variable [TopologicalSpace M'] [IsTopologicalAddGroup M'] [TopologicalSpace Nₗ'] + +/-- The product (in the sense of `LinearMap.prodMap`) of linear maps is strict if and only if each +of the maps is strict. -/ +protected lemma isStrictMap_prodMap_iff : + IsStrictMap (fₗ.prodMap gₗ) ↔ IsStrictMap fₗ ∧ IsStrictMap gₗ := + AddMonoidHom.isStrictMap_prodMap_iff (f := fₗ.toAddMonoidHom) (g := gₗ.toAddMonoidHom) + +/-- The product (in the sense of `LinearMap.prodMap`) of strict linear maps is strict. -/ +protected lemma isStrictMap_prodMap (hf : IsStrictMap fₗ) + (hg : IsStrictMap gₗ) : IsStrictMap (fₗ.prodMap gₗ) := + LinearMap.isStrictMap_prodMap_iff.mpr ⟨hf, hg⟩ + +end LinearMap