Theorems · Theorem · operator theory

ContinuousLinearMap.isStrictMap_isClosed_range_iff_quotient

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3}
  [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [inst_9 : TopologicalSpace F]
  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [T2Space F] (u : E →L[𝕜] F) (A : Submodule 𝕜 F)
  [FiniteDimensional 𝕜 ↥A],
  A.ClosedComplemented →
    (Topology.IsStrictMap ⇑u ∧ IsClosed ↑(↑u).range ↔
      Topology.IsStrictMap ⇑(A.mkQL ∘SL u) ∧ IsClosed ↑(↑(A.mkQL ∘SL u)).range)

Let u : E → F be a continuous linear map, and A a complemented finite dimensional subspace of F. Then u is strict with closed range if and only if the induced map E → F ⧸ A is strict with closed range. This is [N. Bourbaki, Théories Spectrales, Chapitre III, § 3, n° 1, Cor. 2][bourbaki2023].

Defined in

Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite

Cited by

0 results in Mathlib

Foundations

Depth 183 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldCompleteSpaceAddCommGroupModuleAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMulTopologicalSpaceIsTopologicalAddGroupContinuousSMulT2SpaceFiniteDimensional