From 971a59a546a1b65ff5894b4080b270246c5d29e6 Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 13:43:35 +0200 Subject: [PATCH 01/26] chore: split Topology.Algebra.Module.LinearMap --- Mathlib.lean | 6 +- Mathlib/Analysis/Convex/Exposed.lean | 2 +- .../Analysis/Distribution/DerivNotation.lean | 2 +- .../Eigenspace/ContinuousLinearMap.lean | 2 +- Mathlib/Topology/Algebra/Algebra.lean | 2 +- .../Topology/Algebra/LinearMapCompletion.lean | 2 +- .../Topology/Algebra/Module/Complement.lean | 2 +- .../Basic.lean} | 381 ------------------ .../ContinuousLinearMap/Idempotent.lean | 90 +++++ .../Module/ContinuousLinearMap/Quotient.lean | 68 ++++ .../Module/ContinuousLinearMap/Restrict.lean | 198 +++++++++ .../ContinuousLinearMap/RestrictScalars.lean | 91 +++++ .../Algebra/Module/LinearMapPiProd.lean | 2 +- .../Algebra/Module/PerfectPairing.lean | 2 +- .../Algebra/Module/Spaces/WeakBilin.lean | 2 +- .../Algebra/Module/Spaces/WeakDual.lean | 2 +- .../Algebra/SeparationQuotient/Basic.lean | 2 +- Mathlib/Topology/ContinuousMap/Algebra.lean | 2 +- 18 files changed, 464 insertions(+), 394 deletions(-) rename Mathlib/Topology/Algebra/Module/{LinearMap.lean => ContinuousLinearMap/Basic.lean} (73%) create mode 100644 Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean create mode 100644 Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean create mode 100644 Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean create mode 100644 Mathlib/Topology/Algebra/Module/ContinuousLinearMap/RestrictScalars.lean diff --git a/Mathlib.lean b/Mathlib.lean index d211bbdb619507..e968e6ac84a538 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -7456,11 +7456,15 @@ public import Mathlib.Topology.Algebra.Module.Cardinality public import Mathlib.Topology.Algebra.Module.ClosedSubmodule public import Mathlib.Topology.Algebra.Module.Compact public import Mathlib.Topology.Algebra.Module.Complement +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars public import Mathlib.Topology.Algebra.Module.Determinant public import Mathlib.Topology.Algebra.Module.Equiv public import Mathlib.Topology.Algebra.Module.FiniteDimension public import Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear -public import Mathlib.Topology.Algebra.Module.LinearMap public import Mathlib.Topology.Algebra.Module.LinearMapPiProd public import Mathlib.Topology.Algebra.Module.LinearPMap public import Mathlib.Topology.Algebra.Module.LocallyConvex diff --git a/Mathlib/Analysis/Convex/Exposed.lean b/Mathlib/Analysis/Convex/Exposed.lean index d01762dabdb571..cd3e115303c64f 100644 --- a/Mathlib/Analysis/Convex/Exposed.lean +++ b/Mathlib/Analysis/Convex/Exposed.lean @@ -7,7 +7,7 @@ module public import Mathlib.Analysis.Convex.Extreme public import Mathlib.Analysis.Convex.Function -public import Mathlib.Topology.Algebra.Module.LinearMap +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic public import Mathlib.Topology.Order.OrderClosed /-! diff --git a/Mathlib/Analysis/Distribution/DerivNotation.lean b/Mathlib/Analysis/Distribution/DerivNotation.lean index 5b3e99323fe31c..ac41360aa6d623 100644 --- a/Mathlib/Analysis/Distribution/DerivNotation.lean +++ b/Mathlib/Analysis/Distribution/DerivNotation.lean @@ -7,7 +7,7 @@ module public import Mathlib.Algebra.Module.Equiv.Defs public import Mathlib.Data.Fin.Tuple.Basic -public import Mathlib.Topology.Algebra.Module.LinearMap +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic public import Mathlib.Analysis.InnerProductSpace.CanonicalTensor /-! # Type classes for derivatives and the Laplacian diff --git a/Mathlib/LinearAlgebra/Eigenspace/ContinuousLinearMap.lean b/Mathlib/LinearAlgebra/Eigenspace/ContinuousLinearMap.lean index 25da2a68704d5f..c04d7e8e20d63b 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/ContinuousLinearMap.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/ContinuousLinearMap.lean @@ -6,7 +6,7 @@ Authors: Thomas Browning module public import Mathlib.LinearAlgebra.Eigenspace.Basic -public import Mathlib.Topology.Algebra.Module.LinearMap +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic /-! # Eigenspaces of continuous linear maps diff --git a/Mathlib/Topology/Algebra/Algebra.lean b/Mathlib/Topology/Algebra/Algebra.lean index 2dd9efe165a15c..9ace4389aa5b0f 100644 --- a/Mathlib/Topology/Algebra/Algebra.lean +++ b/Mathlib/Topology/Algebra/Algebra.lean @@ -7,7 +7,7 @@ module public import Mathlib.Algebra.Algebra.Subalgebra.Lattice public import Mathlib.Algebra.Algebra.Tower -public import Mathlib.Topology.Algebra.Module.LinearMap +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic public import Mathlib.Algebra.Order.Interval.Set.Instances /-! diff --git a/Mathlib/Topology/Algebra/LinearMapCompletion.lean b/Mathlib/Topology/Algebra/LinearMapCompletion.lean index 72dcc710f0700d..9506ff449605a0 100644 --- a/Mathlib/Topology/Algebra/LinearMapCompletion.lean +++ b/Mathlib/Topology/Algebra/LinearMapCompletion.lean @@ -6,7 +6,7 @@ Authors: Gregory Wickham module public import Mathlib.Topology.Algebra.GroupCompletion -public import Mathlib.Topology.Algebra.Module.LinearMap +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic /-! # Completion of continuous (semi-)linear maps: diff --git a/Mathlib/Topology/Algebra/Module/Complement.lean b/Mathlib/Topology/Algebra/Module/Complement.lean index 04a11fce870f0f..823a1f26cf7037 100644 --- a/Mathlib/Topology/Algebra/Module/Complement.lean +++ b/Mathlib/Topology/Algebra/Module/Complement.lean @@ -5,7 +5,7 @@ Authors: Anatole Dedecker, Sharvil Kesarwani -/ module -public import Mathlib.Topology.Algebra.Module.LinearMap +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic public import Mathlib.Topology.Algebra.Module.Equiv /-! diff --git a/Mathlib/Topology/Algebra/Module/LinearMap.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean similarity index 73% rename from Mathlib/Topology/Algebra/Module/LinearMap.lean rename to Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean index b11c26e87dd3dd..55460a17b8a5b2 100644 --- a/Mathlib/Topology/Algebra/Module/LinearMap.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean @@ -1095,387 +1095,6 @@ theorem coe_smulRightₗ (c : M →L[R] S) : ⇑(smulRightₗ c : M₂ →ₗ[T] end SMulRightₗ -section Semiring -variable {R S M : Type*} [Semiring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] - [CommSemiring S] [Module S M] [SMulCommClass R S M] [SMul S R] [IsScalarTower S R M] - [ContinuousConstSMul S M] [IsTopologicalAddGroup M] - -instance algebra : Algebra S (M →L[R] M) := - Algebra.ofModule smul_comp fun _ _ _ => comp_smul _ _ _ - -@[simp] theorem algebraMap_apply (r : S) (m : M) : algebraMap S (M →L[R] M) r m = r • m := rfl - -end Semiring - -section RestrictScalars - -section Semiring -variable {A M₁ M₂ R S : Type*} [Semiring A] [Semiring R] [Semiring S] - [AddCommMonoid M₁] [Module A M₁] [Module R M₁] [TopologicalSpace M₁] - [AddCommMonoid M₂] [Module A M₂] [Module R M₂] [TopologicalSpace M₂] - [LinearMap.CompatibleSMul M₁ M₂ R A] - -variable (R) in -/-- If `A` is an `R`-algebra, then a continuous `A`-linear map can be interpreted as a continuous -`R`-linear map. We assume `LinearMap.CompatibleSMul M₁ M₂ R A` to match assumptions of -`LinearMap.map_smul_of_tower`. -/ -def restrictScalars (f : M₁ →L[A] M₂) : M₁ →L[R] M₂ := - ⟨(f : M₁ →ₗ[A] M₂).restrictScalars R, f.continuous⟩ - -@[simp] -theorem coe_restrictScalars (f : M₁ →L[A] M₂) : - (f.restrictScalars R : M₁ →ₗ[R] M₂) = (f : M₁ →ₗ[A] M₂).restrictScalars R := rfl - -@[simp] -theorem coe_restrictScalars' (f : M₁ →L[A] M₂) : ⇑(f.restrictScalars R) = f := rfl - -@[simp] -theorem toContinuousAddMonoidHom_restrictScalars (f : M₁ →L[A] M₂) : - ↑(f.restrictScalars R) = (f : ContinuousAddMonoidHom M₁ M₂) := rfl - -@[simp] lemma restrictScalars_zero : (0 : M₁ →L[A] M₂).restrictScalars R = 0 := rfl - -@[simp] -lemma restrictScalars_add [ContinuousAdd M₂] (f g : M₁ →L[A] M₂) : - (f + g).restrictScalars R = f.restrictScalars R + g.restrictScalars R := rfl - -variable [Module S M₂] [ContinuousConstSMul S M₂] [SMulCommClass A S M₂] [SMulCommClass R S M₂] - -@[simp] -theorem restrictScalars_smul (c : S) (f : M₁ →L[A] M₂) : - (c • f).restrictScalars R = c • f.restrictScalars R := - rfl - -variable [ContinuousAdd M₂] - -variable (A R S M₁ M₂) in -/-- `ContinuousLinearMap.restrictScalars` as a `LinearMap`. See also -`ContinuousLinearMap.restrictScalarsL`. -/ -def restrictScalarsₗ : (M₁ →L[A] M₂) →ₗ[S] M₁ →L[R] M₂ where - toFun := restrictScalars R - map_add' := restrictScalars_add - map_smul' := restrictScalars_smul - -@[simp] -theorem coe_restrictScalarsₗ : ⇑(restrictScalarsₗ A M₁ M₂ R S) = restrictScalars R := rfl - -end Semiring - -section Ring -variable {A R S M₁ M₂ : Type*} [Ring A] [Ring R] [Ring S] - [AddCommGroup M₁] [Module A M₁] [Module R M₁] [TopologicalSpace M₁] - [AddCommGroup M₂] [Module A M₂] [Module R M₂] [TopologicalSpace M₂] - [LinearMap.CompatibleSMul M₁ M₂ R A] [IsTopologicalAddGroup M₂] - -@[simp] -lemma restrictScalars_sub (f g : M₁ →L[A] M₂) : - (f - g).restrictScalars R = f.restrictScalars R - g.restrictScalars R := rfl - -@[simp] -lemma restrictScalars_neg (f : M₁ →L[A] M₂) : (-f).restrictScalars R = -f.restrictScalars R := rfl - -end Ring -end RestrictScalars - -end ContinuousLinearMap - -namespace Submodule - -section Semiring - -variable {R : Type*} [Semiring R] {M : Type*} [TopologicalSpace M] [AddCommMonoid M] [Module R M] - -/-- `Submodule.subtype` as a `ContinuousLinearMap`. -/ -def subtypeL (p : Submodule R M) : p →L[R] M where - toLinearMap := p.subtype - -@[simp, norm_cast] -theorem toLinearMap_subtypeL (p : Submodule R M) : (p.subtypeL : p →ₗ[R] M) = p.subtype := rfl - -@[simp] -theorem coe_subtypeL (p : Submodule R M) : ⇑p.subtypeL = p.subtype := rfl - -@[deprecated (since := "2026-05-06")] -alias coe_subtypeL' := coe_subtypeL - -theorem subtypeL_apply (p : Submodule R M) (x : p) : p.subtypeL x = x := by simp - -@[deprecated range_subtype (since := "2026-05-06")] -theorem range_subtypeL (p : Submodule R M) : (p.subtypeL : p →ₗ[R] M).range = p := - Submodule.range_subtype _ - -@[deprecated ker_subtype (since := "2026-05-06")] -theorem ker_subtypeL (p : Submodule R M) : (p.subtypeL : p →ₗ[R] M).ker = ⊥ := - Submodule.ker_subtype _ - -end Semiring - -section Ring - -variable {R R₂ : Type*} [Ring R] [Ring R₂] {σ : R →+* R₂} {M M₂ : Type*} - [TopologicalSpace M] [AddCommGroup M] [Module R M] - [TopologicalSpace M₂] [AddCommGroup M₂] [Module R₂ M₂] - (S : Submodule R M) - -open ContinuousLinearMap - -/-- `Submodule.mkQ` as a `ContinuousLinearMap`. -/ -def mkQL : M →L[R] M ⧸ S where - toLinearMap := S.mkQ - cont := continuous_quot_mk - -@[simp, norm_cast] -theorem toLinearMap_mkQL : (S.mkQL : M →ₗ[R] M ⧸ S) = S.mkQ := rfl - -@[simp] -theorem coe_mkQL : ⇑S.mkQL = S.mkQ := rfl - -theorem mkQL_apply (x : M) : S.mkQL x = S.mkQ x := by simp - -theorem isQuotientMap_mkQL : IsQuotientMap S.mkQL := isQuotientMap_quot_mk - -theorem isOpenQuotientMap_mkQL [ContinuousAdd M] : IsOpenQuotientMap S.mkQL := - S.isOpenQuotientMap_mkQ - -/-- `Submodule.liftQ` as a `ContinuousLinearMap`. -/ -def liftQL (f : M →SL[σ] M₂) (h : S ≤ f.ker) : M ⧸ S →SL[σ] M₂ where - toLinearMap := S.liftQ f h - cont := continuous_quot_lift _ f.continuous - -@[simp, norm_cast] -theorem toLinearMap_liftQL (f : M →SL[σ] M₂) (h : S ≤ f.ker) : - (S.liftQL f h).toLinearMap = S.liftQ f.toLinearMap h := rfl - -@[simp] -theorem coe_liftQL (f : M →SL[σ] M₂) (h : S ≤ f.ker) : - ⇑(S.liftQL f h) = S.liftQ f.toLinearMap h := - rfl - -theorem liftQL_apply (f : M →SL[σ] M₂) (h : S ≤ f.ker) (x : M ⧸ S) : - S.liftQL f h x = S.liftQ f.toLinearMap h x := by - simp - -end Ring - -end Submodule - -namespace ContinuousLinearMap - -section Restrict - -variable {R₁ R₂ R₃ : Type*} [Semiring R₁] [Semiring R₂] [Semiring R₃] - {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] - {M₁ M₂ M₃ : Type*} - [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] - [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] - [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₃ M₃] - -/-- The restriction of a linear map `f : M → M₂` to a submodule `p ⊆ M` gives a linear map -`p → M₂`. -/ -@[simps!] -def domRestrict (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₁ M₁) : p →SL[σ₁₂] M₂ := - f ∘SL p.subtypeL - -@[simp] -theorem toLinearMap_domRestrict (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₁ M₁) : - (f.domRestrict p).toLinearMap = f.toLinearMap.domRestrict p := - rfl - -lemma coe_domRestrict (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₁ M₁) : - ⇑(f.domRestrict p) = Set.restrict p f := - rfl - -/-- Restrict codomain of a continuous linear map. -/ -def codRestrict (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) : - M₁ →SL[σ₁₂] p where - cont := f.continuous.subtype_mk _ - toLinearMap := (f : M₁ →ₛₗ[σ₁₂] M₂).codRestrict p h - -@[simp, norm_cast] -theorem toLinearMap_codRestrict (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) : - (f.codRestrict p h).toLinearMap = f.toLinearMap.codRestrict p h := - rfl - -theorem coe_codRestrict (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) : - (f.codRestrict p h : M₁ → p) = Set.codRestrict (f : M₁ → M₂) p h := - rfl - -@[simp] -theorem coe_codRestrict_apply (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) (x) : - (f.codRestrict p h x : M₂) = f x := - rfl - -theorem ker_codRestrict (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) : - ker (f.codRestrict p h : M₁ →ₛₗ[σ₁₂] p) = ker (f : M₁ →ₛₗ[σ₁₂] M₂) := - f.toLinearMap.ker_codRestrict p h - -@[simp] -theorem domRestrict_comp_codRestrict (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) - (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) : - g.domRestrict p ∘SL f.codRestrict p h = g ∘SL f := - rfl - -/-- Restrict the codomain of a continuous linear map `f` to `f.range`. -/ -abbrev rangeRestrict [RingHomSurjective σ₁₂] (f : M₁ →SL[σ₁₂] M₂) := - f.codRestrict (LinearMap.range (f : M₁ →ₛₗ[σ₁₂] M₂)) (LinearMap.mem_range_self _) - -theorem toLinearMap_rangeRestrict [RingHomSurjective σ₁₂] (f : M₁ →SL[σ₁₂] M₂) : - f.rangeRestrict.toLinearMap = f.toLinearMap.rangeRestrict := by simp - -@[simp] -theorem coe_rangeRestrict [RingHomSurjective σ₁₂] (f : M₁ →SL[σ₁₂] M₂) : - (f.rangeRestrict : M₁ → f.range) = Set.rangeFactorization f := rfl - -/-- Restrict codomain of a continuous linear map. -/ -def restrict (f : M₁ →SL[σ₁₂] M₂) {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} - (h : ∀ x ∈ p, f x ∈ q) : p →SL[σ₁₂] q := - (f.domRestrict p).codRestrict q <| SetLike.forall.2 h - -@[simp, norm_cast] -theorem toLinearMap_restrict {f : M₁ →SL[σ₁₂] M₂} {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} - (h : ∀ x ∈ p, f x ∈ q) : - (f.restrict h).toLinearMap = f.toLinearMap.restrict h := - rfl - -@[simp] -theorem coe_restrict_apply {f : M₁ →SL[σ₁₂] M₂} {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} - (hf : ∀ x ∈ p, f x ∈ q) (x : p) : ↑(f.restrict hf x) = f x := - rfl - -theorem restrict_apply {f : M₁ →SL[σ₁₂] M₂} {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} - (hf : ∀ x ∈ p, f x ∈ q) (x : p) : f.restrict hf x = ⟨f x, hf x.1 x.2⟩ := - rfl - -open Set in -lemma restrict_comp {p : Submodule R₁ M₁} {p₂ : Submodule R₂ M₂} {p₃ : Submodule R₃ M₃} - {f : M₁ →SL[σ₁₂] M₂} {g : M₂ →SL[σ₂₃] M₃} - (hf : MapsTo f p p₂) (hg : MapsTo g p₂ p₃) (hfg : MapsTo (g ∘SL f) p p₃ := hg.comp hf) : - (g ∘SL f).restrict hfg = (g.restrict hg) ∘SL (f.restrict hf) := - rfl - -theorem subtypeL_comp_restrict {f : M₁ →SL[σ₁₂] M₂} {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} - (hf : ∀ x ∈ p, f x ∈ q) : q.subtypeL ∘SL (f.restrict hf) = f.domRestrict p := - rfl - -theorem restrict_eq_codRestrict_domRestrict {f : M₁ →SL[σ₁₂] M₂} {p : Submodule R₁ M₁} - {q : Submodule R₂ M₂} (hf : ∀ x ∈ p, f x ∈ q) : - f.restrict hf = (f.domRestrict p).codRestrict q fun x => hf x.1 x.2 := - rfl - -theorem restrict_eq_domRestrict_codRestrict {f : M₁ →SL[σ₁₂] M₂} {p : Submodule R₁ M₁} - {q : Submodule R₂ M₂} (hf : ∀ x, f x ∈ q) : - (f.restrict fun x _ => hf x) = (f.codRestrict q hf).domRestrict p := - rfl - -end Restrict - -section - -variable {R₁ R₂ R₃ : Type*} [Ring R₁] [Ring R₂] - {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] - {M₁ M₂ : Type*} - [TopologicalSpace M₁] [AddCommGroup M₁] [Module R₁ M₁] - [TopologicalSpace M₂] [AddCommGroup M₂] [Module R₂ M₂] - -/-- Given a right inverse `f₂ : M₂ →L[R] M₁` to `f₁ : M₁ →L[R] M₂`, -`projKerOfRightInverse f₁ f₂ h` is the projection `M₁ →L[R] LinearMap.ker f₁` along -`LinearMap.range f₂`. -/ -def projKerOfRightInverse [IsTopologicalAddGroup M₁] (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁) - (h : Function.RightInverse f₂ f₁) : M₁ →L[R₁] LinearMap.ker (f₁ : M₁ →ₛₗ[σ₁₂] M₂) := - (.id R₁ M₁ - f₂ ∘SL f₁).codRestrict (LinearMap.ker f₁.toLinearMap) fun x => by simp [h (f₁ x)] - -@[simp] -theorem coe_projKerOfRightInverse_apply [IsTopologicalAddGroup M₁] (f₁ : M₁ →SL[σ₁₂] M₂) - (f₂ : M₂ →SL[σ₂₁] M₁) (h : Function.RightInverse f₂ f₁) (x : M₁) : - (f₁.projKerOfRightInverse f₂ h x : M₁) = x - f₂ (f₁ x) := - rfl - -@[simp] -theorem projKerOfRightInverse_apply_idem [IsTopologicalAddGroup M₁] (f₁ : M₁ →SL[σ₁₂] M₂) - (f₂ : M₂ →SL[σ₂₁] M₁) (h : Function.RightInverse f₂ f₁) (x : f₁.ker) : - f₁.projKerOfRightInverse f₂ h x = x := by - ext1 - simp - -@[simp] -theorem projKerOfRightInverse_comp_inv [IsTopologicalAddGroup M₁] (f₁ : M₁ →SL[σ₁₂] M₂) - (f₂ : M₂ →SL[σ₂₁] M₁) (h : Function.RightInverse f₂ f₁) (y : M₂) : - f₁.projKerOfRightInverse f₂ h (f₂ y) = 0 := - Subtype.ext_iff.2 <| by simp [h y] - -end - -@[grind =] -theorem isIdempotentElem_toLinearMap_iff {R M : Type*} [Semiring R] [TopologicalSpace M] - [AddCommMonoid M] [Module R M] {f : M →L[R] M} : - IsIdempotentElem f.toLinearMap ↔ IsIdempotentElem f := by - simp only [IsIdempotentElem, Module.End.mul_eq_comp, ← coe_comp, mul_def, coe_inj] - -alias ⟨_, IsIdempotentElem.toLinearMap⟩ := isIdempotentElem_toLinearMap_iff - -variable {R M : Type*} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] - -open ContinuousLinearMap - -/-- Idempotent operators are equal iff their range and kernels are. -/ -lemma IsIdempotentElem.ext_iff {p q : M →L[R] M} - (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) : - p = q ↔ p.range = q.range ∧ p.ker = q.ker := by - simpa using LinearMap.IsIdempotentElem.ext_iff hp.toLinearMap hq.toLinearMap - -alias ⟨_, IsIdempotentElem.ext⟩ := IsIdempotentElem.ext_iff - -/-- `range f` is invariant under `T` if and only if `f ∘L T ∘L f = T ∘L f`, -for idempotent `f`. -/ -lemma IsIdempotentElem.range_mem_invtSubmodule_iff {f T : M →L[R] M} - (hf : IsIdempotentElem f) : - f.range ∈ Module.End.invtSubmodule T ↔ f ∘L T ∘L f = T ∘L f := by - simpa [← ContinuousLinearMap.coe_comp] using - LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff (T := T) hf.toLinearMap - -alias ⟨IsIdempotentElem.conj_eq_of_range_mem_invtSubmodule, - IsIdempotentElem.range_mem_invtSubmodule⟩ := IsIdempotentElem.range_mem_invtSubmodule_iff - -/-- `ker f` is invariant under `T` if and only if `f ∘L T ∘L f = f ∘L T`, -for idempotent `f`. -/ -lemma IsIdempotentElem.ker_mem_invtSubmodule_iff {f T : M →L[R] M} - (hf : IsIdempotentElem f) : - f.ker ∈ Module.End.invtSubmodule T ↔ f ∘L T ∘L f = f ∘L T := by - simpa [← ContinuousLinearMap.coe_comp] using - LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff (T := T) hf.toLinearMap - -alias ⟨IsIdempotentElem.conj_eq_of_ker_mem_invtSubmodule, - IsIdempotentElem.ker_mem_invtSubmodule⟩ := IsIdempotentElem.ker_mem_invtSubmodule_iff - -/-- An idempotent operator `f` commutes with `T` if and only if -both `range f` and `ker f` are invariant under `T`. -/ -lemma IsIdempotentElem.commute_iff {f T : M →L[R] M} - (hf : IsIdempotentElem f) : - Commute f T ↔ (f.range ∈ Module.End.invtSubmodule T ∧ f.ker ∈ Module.End.invtSubmodule T) := by - simpa [Commute, SemiconjBy, Module.End.mul_eq_comp, ← coe_comp] using - LinearMap.IsIdempotentElem.commute_iff (T := T) hf.toLinearMap - -variable [IsTopologicalAddGroup M] - -/-- An idempotent operator `f` commutes with a unit operator `T` if and only if -`T (range f) = range f` and `T (ker f) = ker f`. -/ -theorem IsIdempotentElem.commute_iff_of_isUnit {f T : M →L[R] M} (hT : IsUnit T) - (hf : IsIdempotentElem f) : - Commute f T ↔ f.range.map (T : M →ₗ[R] M) = f.range ∧ f.ker.map (T : M →ₗ[R] M) = f.ker := by - have := hT.map ContinuousLinearMap.toLinearMapRingHom - lift T to (M →L[R] M)ˣ using hT - simpa [Commute, SemiconjBy, Module.End.mul_eq_comp, ← ContinuousLinearMap.coe_comp] using - LinearMap.IsIdempotentElem.commute_iff_of_isUnit this hf.toLinearMap - -@[deprecated (since := "2025-12-27")] alias IsIdempotentElem.range_eq_ker := - LinearMap.IsIdempotentElem.range_eq_ker -@[deprecated (since := "2025-12-27")] alias IsIdempotentElem.ker_eq_range := - LinearMap.IsIdempotentElem.ker_eq_range - -theorem IsIdempotentElem.isClosed_range [T1Space M] {p : M →L[R] M} - (hp : IsIdempotentElem p) : IsClosed (p.range : Set M) := - LinearMap.IsIdempotentElem.range_eq_ker hp.toLinearMap ▸ isClosed_ker (.id R M - p) - end ContinuousLinearMap section topDualPairing diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean new file mode 100644 index 00000000000000..244eb1075050e4 --- /dev/null +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean @@ -0,0 +1,90 @@ +/- +Copyright (c) 2019 Sébastien Gouëzel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov, Frédéric Dupuis, + Heather Macbeth +-/ +module + +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic + +/-! +# Idempotent continuous linear maps +-/ + +@[expose] public section + +namespace ContinuousLinearMap + +@[grind =] +theorem isIdempotentElem_toLinearMap_iff {R M : Type*} [Semiring R] [TopologicalSpace M] + [AddCommMonoid M] [Module R M] {f : M →L[R] M} : + IsIdempotentElem f.toLinearMap ↔ IsIdempotentElem f := by + simp only [IsIdempotentElem, Module.End.mul_eq_comp, ← coe_comp, mul_def, coe_inj] + +alias ⟨_, IsIdempotentElem.toLinearMap⟩ := isIdempotentElem_toLinearMap_iff + +variable {R M : Type*} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] + +open ContinuousLinearMap + +/-- Idempotent operators are equal iff their range and kernels are. -/ +lemma IsIdempotentElem.ext_iff {p q : M →L[R] M} + (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) : + p = q ↔ p.range = q.range ∧ p.ker = q.ker := by + simpa using LinearMap.IsIdempotentElem.ext_iff hp.toLinearMap hq.toLinearMap + +alias ⟨_, IsIdempotentElem.ext⟩ := IsIdempotentElem.ext_iff + +/-- `range f` is invariant under `T` if and only if `f ∘L T ∘L f = T ∘L f`, +for idempotent `f`. -/ +lemma IsIdempotentElem.range_mem_invtSubmodule_iff {f T : M →L[R] M} + (hf : IsIdempotentElem f) : + f.range ∈ Module.End.invtSubmodule T ↔ f ∘L T ∘L f = T ∘L f := by + simpa [← ContinuousLinearMap.coe_comp] using + LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff (T := T) hf.toLinearMap + +alias ⟨IsIdempotentElem.conj_eq_of_range_mem_invtSubmodule, + IsIdempotentElem.range_mem_invtSubmodule⟩ := IsIdempotentElem.range_mem_invtSubmodule_iff + +/-- `ker f` is invariant under `T` if and only if `f ∘L T ∘L f = f ∘L T`, +for idempotent `f`. -/ +lemma IsIdempotentElem.ker_mem_invtSubmodule_iff {f T : M →L[R] M} + (hf : IsIdempotentElem f) : + f.ker ∈ Module.End.invtSubmodule T ↔ f ∘L T ∘L f = f ∘L T := by + simpa [← ContinuousLinearMap.coe_comp] using + LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff (T := T) hf.toLinearMap + +alias ⟨IsIdempotentElem.conj_eq_of_ker_mem_invtSubmodule, + IsIdempotentElem.ker_mem_invtSubmodule⟩ := IsIdempotentElem.ker_mem_invtSubmodule_iff + +/-- An idempotent operator `f` commutes with `T` if and only if +both `range f` and `ker f` are invariant under `T`. -/ +lemma IsIdempotentElem.commute_iff {f T : M →L[R] M} + (hf : IsIdempotentElem f) : + Commute f T ↔ (f.range ∈ Module.End.invtSubmodule T ∧ f.ker ∈ Module.End.invtSubmodule T) := by + simpa [Commute, SemiconjBy, Module.End.mul_eq_comp, ← coe_comp] using + LinearMap.IsIdempotentElem.commute_iff (T := T) hf.toLinearMap + +variable [IsTopologicalAddGroup M] + +/-- An idempotent operator `f` commutes with a unit operator `T` if and only if +`T (range f) = range f` and `T (ker f) = ker f`. -/ +theorem IsIdempotentElem.commute_iff_of_isUnit {f T : M →L[R] M} (hT : IsUnit T) + (hf : IsIdempotentElem f) : + Commute f T ↔ f.range.map (T : M →ₗ[R] M) = f.range ∧ f.ker.map (T : M →ₗ[R] M) = f.ker := by + have := hT.map ContinuousLinearMap.toLinearMapRingHom + lift T to (M →L[R] M)ˣ using hT + simpa [Commute, SemiconjBy, Module.End.mul_eq_comp, ← ContinuousLinearMap.coe_comp] using + LinearMap.IsIdempotentElem.commute_iff_of_isUnit this hf.toLinearMap + +@[deprecated (since := "2025-12-27")] alias IsIdempotentElem.range_eq_ker := + LinearMap.IsIdempotentElem.range_eq_ker +@[deprecated (since := "2025-12-27")] alias IsIdempotentElem.ker_eq_range := + LinearMap.IsIdempotentElem.ker_eq_range + +theorem IsIdempotentElem.isClosed_range [T1Space M] {p : M →L[R] M} + (hp : IsIdempotentElem p) : IsClosed (p.range : Set M) := + LinearMap.IsIdempotentElem.range_eq_ker hp.toLinearMap ▸ isClosed_ker (.id R M - p) + +end ContinuousLinearMap diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean new file mode 100644 index 00000000000000..0cafce34e288a8 --- /dev/null +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean @@ -0,0 +1,68 @@ +/- +Copyright (c) 2019 Sébastien Gouëzel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov, Frédéric Dupuis, + Heather Macbeth +-/ +module + +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic + +/-! +# Continuous linear maps and quotient topological modules +-/ + +@[expose] public section + +open Topology + +namespace Submodule + +section Ring + +variable {R R₂ : Type*} [Ring R] [Ring R₂] {σ : R →+* R₂} {M M₂ : Type*} + [TopologicalSpace M] [AddCommGroup M] [Module R M] + [TopologicalSpace M₂] [AddCommGroup M₂] [Module R₂ M₂] + (S : Submodule R M) + +open ContinuousLinearMap + +/-- `Submodule.mkQ` as a `ContinuousLinearMap`. -/ +def mkQL : M →L[R] M ⧸ S where + toLinearMap := S.mkQ + cont := continuous_quot_mk + +@[simp, norm_cast] +theorem toLinearMap_mkQL : (S.mkQL : M →ₗ[R] M ⧸ S) = S.mkQ := rfl + +@[simp] +theorem coe_mkQL : ⇑S.mkQL = S.mkQ := rfl + +theorem mkQL_apply (x : M) : S.mkQL x = S.mkQ x := by simp + +theorem isQuotientMap_mkQL : IsQuotientMap S.mkQL := isQuotientMap_quot_mk + +theorem isOpenQuotientMap_mkQL [ContinuousAdd M] : IsOpenQuotientMap S.mkQL := + S.isOpenQuotientMap_mkQ + +/-- `Submodule.liftQ` as a `ContinuousLinearMap`. -/ +def liftQL (f : M →SL[σ] M₂) (h : S ≤ f.ker) : M ⧸ S →SL[σ] M₂ where + toLinearMap := S.liftQ f h + cont := continuous_quot_lift _ f.continuous + +@[simp, norm_cast] +theorem toLinearMap_liftQL (f : M →SL[σ] M₂) (h : S ≤ f.ker) : + (S.liftQL f h).toLinearMap = S.liftQ f.toLinearMap h := rfl + +@[simp] +theorem coe_liftQL (f : M →SL[σ] M₂) (h : S ≤ f.ker) : + ⇑(S.liftQL f h) = S.liftQ f.toLinearMap h := + rfl + +theorem liftQL_apply (f : M →SL[σ] M₂) (h : S ≤ f.ker) (x : M ⧸ S) : + S.liftQL f h x = S.liftQ f.toLinearMap h x := by + simp + +end Ring + +end Submodule diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean new file mode 100644 index 00000000000000..fa91c3727cd1e1 --- /dev/null +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean @@ -0,0 +1,198 @@ +/- +Copyright (c) 2019 Sébastien Gouëzel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov, Frédéric Dupuis, + Heather Macbeth +-/ +module + +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic + +/-! +# Restriction operations on continuous linear maps +-/ + +@[expose] public section + +open LinearMap (ker range) + +namespace Submodule + +section Semiring + +variable {R : Type*} [Semiring R] {M : Type*} [TopologicalSpace M] [AddCommMonoid M] [Module R M] + +/-- `Submodule.subtype` as a `ContinuousLinearMap`. -/ +def subtypeL (p : Submodule R M) : p →L[R] M where + toLinearMap := p.subtype + +@[simp, norm_cast] +theorem toLinearMap_subtypeL (p : Submodule R M) : (p.subtypeL : p →ₗ[R] M) = p.subtype := rfl + +@[simp] +theorem coe_subtypeL (p : Submodule R M) : ⇑p.subtypeL = p.subtype := rfl + +@[deprecated (since := "2026-05-06")] +alias coe_subtypeL' := coe_subtypeL + +theorem subtypeL_apply (p : Submodule R M) (x : p) : p.subtypeL x = x := by simp + +@[deprecated range_subtype (since := "2026-05-06")] +theorem range_subtypeL (p : Submodule R M) : (p.subtypeL : p →ₗ[R] M).range = p := + Submodule.range_subtype _ + +@[deprecated ker_subtype (since := "2026-05-06")] +theorem ker_subtypeL (p : Submodule R M) : (p.subtypeL : p →ₗ[R] M).ker = ⊥ := + Submodule.ker_subtype _ + +end Semiring + +end Submodule + +namespace ContinuousLinearMap + +section Restrict + +variable {R₁ R₂ R₃ : Type*} [Semiring R₁] [Semiring R₂] [Semiring R₃] + {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] + {M₁ M₂ M₃ : Type*} + [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] + [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] + [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₃ M₃] + +/-- The restriction of a linear map `f : M → M₂` to a submodule `p ⊆ M` gives a linear map +`p → M₂`. -/ +@[simps!] +def domRestrict (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₁ M₁) : p →SL[σ₁₂] M₂ := + f ∘SL p.subtypeL + +@[simp] +theorem toLinearMap_domRestrict (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₁ M₁) : + (f.domRestrict p).toLinearMap = f.toLinearMap.domRestrict p := + rfl + +lemma coe_domRestrict (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₁ M₁) : + ⇑(f.domRestrict p) = Set.restrict p f := + rfl + +/-- Restrict codomain of a continuous linear map. -/ +def codRestrict (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) : + M₁ →SL[σ₁₂] p where + cont := f.continuous.subtype_mk _ + toLinearMap := (f : M₁ →ₛₗ[σ₁₂] M₂).codRestrict p h + +@[simp, norm_cast] +theorem toLinearMap_codRestrict (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) : + (f.codRestrict p h).toLinearMap = f.toLinearMap.codRestrict p h := + rfl + +theorem coe_codRestrict (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) : + (f.codRestrict p h : M₁ → p) = Set.codRestrict (f : M₁ → M₂) p h := + rfl + +@[simp] +theorem coe_codRestrict_apply (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) (x) : + (f.codRestrict p h x : M₂) = f x := + rfl + +theorem ker_codRestrict (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) : + ker (f.codRestrict p h : M₁ →ₛₗ[σ₁₂] p) = ker (f : M₁ →ₛₗ[σ₁₂] M₂) := + f.toLinearMap.ker_codRestrict p h + +@[simp] +theorem domRestrict_comp_codRestrict (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) + (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) : + g.domRestrict p ∘SL f.codRestrict p h = g ∘SL f := + rfl + +/-- Restrict the codomain of a continuous linear map `f` to `f.range`. -/ +abbrev rangeRestrict [RingHomSurjective σ₁₂] (f : M₁ →SL[σ₁₂] M₂) := + f.codRestrict (LinearMap.range (f : M₁ →ₛₗ[σ₁₂] M₂)) (LinearMap.mem_range_self _) + +theorem toLinearMap_rangeRestrict [RingHomSurjective σ₁₂] (f : M₁ →SL[σ₁₂] M₂) : + f.rangeRestrict.toLinearMap = f.toLinearMap.rangeRestrict := by simp + +@[simp] +theorem coe_rangeRestrict [RingHomSurjective σ₁₂] (f : M₁ →SL[σ₁₂] M₂) : + (f.rangeRestrict : M₁ → f.range) = Set.rangeFactorization f := rfl + +/-- Restrict codomain of a continuous linear map. -/ +def restrict (f : M₁ →SL[σ₁₂] M₂) {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} + (h : ∀ x ∈ p, f x ∈ q) : p →SL[σ₁₂] q := + (f.domRestrict p).codRestrict q <| SetLike.forall.2 h + +@[simp, norm_cast] +theorem toLinearMap_restrict {f : M₁ →SL[σ₁₂] M₂} {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} + (h : ∀ x ∈ p, f x ∈ q) : + (f.restrict h).toLinearMap = f.toLinearMap.restrict h := + rfl + +@[simp] +theorem coe_restrict_apply {f : M₁ →SL[σ₁₂] M₂} {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} + (hf : ∀ x ∈ p, f x ∈ q) (x : p) : ↑(f.restrict hf x) = f x := + rfl + +theorem restrict_apply {f : M₁ →SL[σ₁₂] M₂} {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} + (hf : ∀ x ∈ p, f x ∈ q) (x : p) : f.restrict hf x = ⟨f x, hf x.1 x.2⟩ := + rfl + +open Set in +lemma restrict_comp {p : Submodule R₁ M₁} {p₂ : Submodule R₂ M₂} {p₃ : Submodule R₃ M₃} + {f : M₁ →SL[σ₁₂] M₂} {g : M₂ →SL[σ₂₃] M₃} + (hf : MapsTo f p p₂) (hg : MapsTo g p₂ p₃) (hfg : MapsTo (g ∘SL f) p p₃ := hg.comp hf) : + (g ∘SL f).restrict hfg = (g.restrict hg) ∘SL (f.restrict hf) := + rfl + +theorem subtypeL_comp_restrict {f : M₁ →SL[σ₁₂] M₂} {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} + (hf : ∀ x ∈ p, f x ∈ q) : q.subtypeL ∘SL (f.restrict hf) = f.domRestrict p := + rfl + +theorem restrict_eq_codRestrict_domRestrict {f : M₁ →SL[σ₁₂] M₂} {p : Submodule R₁ M₁} + {q : Submodule R₂ M₂} (hf : ∀ x ∈ p, f x ∈ q) : + f.restrict hf = (f.domRestrict p).codRestrict q fun x => hf x.1 x.2 := + rfl + +theorem restrict_eq_domRestrict_codRestrict {f : M₁ →SL[σ₁₂] M₂} {p : Submodule R₁ M₁} + {q : Submodule R₂ M₂} (hf : ∀ x, f x ∈ q) : + (f.restrict fun x _ => hf x) = (f.codRestrict q hf).domRestrict p := + rfl + +end Restrict + +section + +variable {R₁ R₂ R₃ : Type*} [Ring R₁] [Ring R₂] + {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] + {M₁ M₂ : Type*} + [TopologicalSpace M₁] [AddCommGroup M₁] [Module R₁ M₁] + [TopologicalSpace M₂] [AddCommGroup M₂] [Module R₂ M₂] + +/-- Given a right inverse `f₂ : M₂ →L[R] M₁` to `f₁ : M₁ →L[R] M₂`, +`projKerOfRightInverse f₁ f₂ h` is the projection `M₁ →L[R] LinearMap.ker f₁` along +`LinearMap.range f₂`. -/ +def projKerOfRightInverse [IsTopologicalAddGroup M₁] (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁) + (h : Function.RightInverse f₂ f₁) : M₁ →L[R₁] LinearMap.ker (f₁ : M₁ →ₛₗ[σ₁₂] M₂) := + (.id R₁ M₁ - f₂ ∘SL f₁).codRestrict (LinearMap.ker f₁.toLinearMap) fun x => by simp [h (f₁ x)] + +@[simp] +theorem coe_projKerOfRightInverse_apply [IsTopologicalAddGroup M₁] (f₁ : M₁ →SL[σ₁₂] M₂) + (f₂ : M₂ →SL[σ₂₁] M₁) (h : Function.RightInverse f₂ f₁) (x : M₁) : + (f₁.projKerOfRightInverse f₂ h x : M₁) = x - f₂ (f₁ x) := + rfl + +@[simp] +theorem projKerOfRightInverse_apply_idem [IsTopologicalAddGroup M₁] (f₁ : M₁ →SL[σ₁₂] M₂) + (f₂ : M₂ →SL[σ₂₁] M₁) (h : Function.RightInverse f₂ f₁) (x : f₁.ker) : + f₁.projKerOfRightInverse f₂ h x = x := by + ext1 + simp + +@[simp] +theorem projKerOfRightInverse_comp_inv [IsTopologicalAddGroup M₁] (f₁ : M₁ →SL[σ₁₂] M₂) + (f₂ : M₂ →SL[σ₂₁] M₁) (h : Function.RightInverse f₂ f₁) (y : M₂) : + f₁.projKerOfRightInverse f₂ h (f₂ y) = 0 := + Subtype.ext_iff.2 <| by simp [h y] + +end + +end ContinuousLinearMap diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/RestrictScalars.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/RestrictScalars.lean new file mode 100644 index 00000000000000..863c5dd58b0b87 --- /dev/null +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/RestrictScalars.lean @@ -0,0 +1,91 @@ +/- +Copyright (c) 2019 Sébastien Gouëzel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov, Frédéric Dupuis, + Heather Macbeth +-/ +module + +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic + +/-! +# Restriction of scalars for continuous linear maps +-/ + +@[expose] public section + +section RestrictScalars + +namespace ContinuousLinearMap + +section Semiring + +variable {A M₁ M₂ R S : Type*} [Semiring A] [Semiring R] [Semiring S] + [AddCommMonoid M₁] [Module A M₁] [Module R M₁] [TopologicalSpace M₁] + [AddCommMonoid M₂] [Module A M₂] [Module R M₂] [TopologicalSpace M₂] + [LinearMap.CompatibleSMul M₁ M₂ R A] + +variable (R) in +/-- If `A` is an `R`-algebra, then a continuous `A`-linear map can be interpreted as a continuous +`R`-linear map. We assume `LinearMap.CompatibleSMul M₁ M₂ R A` to match assumptions of +`LinearMap.map_smul_of_tower`. -/ +def restrictScalars (f : M₁ →L[A] M₂) : M₁ →L[R] M₂ := + ⟨(f : M₁ →ₗ[A] M₂).restrictScalars R, f.continuous⟩ + +@[simp] +theorem coe_restrictScalars (f : M₁ →L[A] M₂) : + (f.restrictScalars R : M₁ →ₗ[R] M₂) = (f : M₁ →ₗ[A] M₂).restrictScalars R := rfl + +@[simp] +theorem coe_restrictScalars' (f : M₁ →L[A] M₂) : ⇑(f.restrictScalars R) = f := rfl + +@[simp] +theorem toContinuousAddMonoidHom_restrictScalars (f : M₁ →L[A] M₂) : + ↑(f.restrictScalars R) = (f : ContinuousAddMonoidHom M₁ M₂) := rfl + +@[simp] lemma restrictScalars_zero : (0 : M₁ →L[A] M₂).restrictScalars R = 0 := rfl + +@[simp] +lemma restrictScalars_add [ContinuousAdd M₂] (f g : M₁ →L[A] M₂) : + (f + g).restrictScalars R = f.restrictScalars R + g.restrictScalars R := rfl + +variable [Module S M₂] [ContinuousConstSMul S M₂] [SMulCommClass A S M₂] [SMulCommClass R S M₂] + +@[simp] +theorem restrictScalars_smul (c : S) (f : M₁ →L[A] M₂) : + (c • f).restrictScalars R = c • f.restrictScalars R := + rfl + +variable [ContinuousAdd M₂] + +variable (A R S M₁ M₂) in +/-- `ContinuousLinearMap.restrictScalars` as a `LinearMap`. See also +`ContinuousLinearMap.restrictScalarsL`. -/ +def restrictScalarsₗ : (M₁ →L[A] M₂) →ₗ[S] M₁ →L[R] M₂ where + toFun := restrictScalars R + map_add' := restrictScalars_add + map_smul' := restrictScalars_smul + +@[simp] +theorem coe_restrictScalarsₗ : ⇑(restrictScalarsₗ A M₁ M₂ R S) = restrictScalars R := rfl + +end Semiring + +section Ring +variable {A R S M₁ M₂ : Type*} [Ring A] [Ring R] [Ring S] + [AddCommGroup M₁] [Module A M₁] [Module R M₁] [TopologicalSpace M₁] + [AddCommGroup M₂] [Module A M₂] [Module R M₂] [TopologicalSpace M₂] + [LinearMap.CompatibleSMul M₁ M₂ R A] [IsTopologicalAddGroup M₂] + +@[simp] +lemma restrictScalars_sub (f g : M₁ →L[A] M₂) : + (f - g).restrictScalars R = f.restrictScalars R - g.restrictScalars R := rfl + +@[simp] +lemma restrictScalars_neg (f : M₁ →L[A] M₂) : (-f).restrictScalars R = -f.restrictScalars R := rfl + +end Ring + +end ContinuousLinearMap + +end RestrictScalars diff --git a/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean b/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean index 18761b5b47885a..53d34c2cfe04da 100644 --- a/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean +++ b/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean @@ -6,7 +6,7 @@ Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov, Fréd -/ module -public import Mathlib.Topology.Algebra.Module.LinearMap +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic /-! # Continuous linear maps on products and Pi types diff --git a/Mathlib/Topology/Algebra/Module/PerfectPairing.lean b/Mathlib/Topology/Algebra/Module/PerfectPairing.lean index 879bd305d91f77..3206adb8589429 100644 --- a/Mathlib/Topology/Algebra/Module/PerfectPairing.lean +++ b/Mathlib/Topology/Algebra/Module/PerfectPairing.lean @@ -6,7 +6,7 @@ Authors: Yaël Dillies, Andrew Yang module public import Mathlib.LinearAlgebra.BilinearMap -public import Mathlib.Topology.Algebra.Module.LinearMap +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic /-! # Continuous perfect pairings diff --git a/Mathlib/Topology/Algebra/Module/Spaces/WeakBilin.lean b/Mathlib/Topology/Algebra/Module/Spaces/WeakBilin.lean index 927b1f8f09d894..1f7fa9d634c3e0 100644 --- a/Mathlib/Topology/Algebra/Module/Spaces/WeakBilin.lean +++ b/Mathlib/Topology/Algebra/Module/Spaces/WeakBilin.lean @@ -5,7 +5,7 @@ Authors: Kalle Kytölä, Moritz Doll -/ module -public import Mathlib.Topology.Algebra.Module.LinearMap +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic public import Mathlib.LinearAlgebra.BilinearMap /-! diff --git a/Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean b/Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean index ae02942e1b3dc0..b9932eb857911c 100644 --- a/Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean +++ b/Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean @@ -6,7 +6,7 @@ Authors: Kalle Kytölä, Moritz Doll module public import Mathlib.LinearAlgebra.BilinearMap -public import Mathlib.Topology.Algebra.Module.LinearMap +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic public import Mathlib.Topology.Algebra.Module.Spaces.WeakBilin /-! diff --git a/Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean b/Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean index 6fc3769c7ddf82..a1816f2c3badd6 100644 --- a/Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean +++ b/Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean @@ -5,7 +5,7 @@ Authors: Yury Kudryashov -/ module -public import Mathlib.Topology.Algebra.Module.LinearMap +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic /-! # Algebraic operations on `SeparationQuotient` diff --git a/Mathlib/Topology/ContinuousMap/Algebra.lean b/Mathlib/Topology/ContinuousMap/Algebra.lean index 066b64e473d1e1..5d39eabc7e3970 100644 --- a/Mathlib/Topology/ContinuousMap/Algebra.lean +++ b/Mathlib/Topology/ContinuousMap/Algebra.lean @@ -9,7 +9,7 @@ public import Mathlib.Algebra.Algebra.Pi public import Mathlib.Algebra.Algebra.Subalgebra.Basic public import Mathlib.Tactic.FieldSimp public import Mathlib.Topology.Algebra.InfiniteSum.Basic -public import Mathlib.Topology.Algebra.Module.LinearMap +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic public import Mathlib.Topology.Algebra.Ring.Basic public import Mathlib.Topology.UniformSpace.CompactConvergence From 0bc6f531e74023deea2b49b2384b5f4c6590250d Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 14:09:44 +0200 Subject: [PATCH 02/26] fix + extra move --- .../{LinearMapPiProd.lean => ContinuousLinearMap/PiProd.lean} | 0 Mathlib/Topology/Algebra/Module/Equiv.lean | 1 + 2 files changed, 1 insertion(+) rename Mathlib/Topology/Algebra/Module/{LinearMapPiProd.lean => ContinuousLinearMap/PiProd.lean} (100%) diff --git a/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean similarity index 100% rename from Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean rename to Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean diff --git a/Mathlib/Topology/Algebra/Module/Equiv.lean b/Mathlib/Topology/Algebra/Module/Equiv.lean index ee71f4f50d06a3..8ce7236f242d97 100644 --- a/Mathlib/Topology/Algebra/Module/Equiv.lean +++ b/Mathlib/Topology/Algebra/Module/Equiv.lean @@ -7,6 +7,7 @@ Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov, Fréd module public import Mathlib.Topology.Algebra.Module.LinearMapPiProd +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict /-! # Continuous linear equivalences From 17e676a297a347d13fe95de1805e95692906f95b Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 14:10:01 +0200 Subject: [PATCH 03/26] mk_all --- Mathlib.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib.lean b/Mathlib.lean index e968e6ac84a538..affc7f126e1cdd 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -7458,6 +7458,7 @@ public import Mathlib.Topology.Algebra.Module.Compact public import Mathlib.Topology.Algebra.Module.Complement public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars @@ -7465,7 +7466,6 @@ public import Mathlib.Topology.Algebra.Module.Determinant public import Mathlib.Topology.Algebra.Module.Equiv public import Mathlib.Topology.Algebra.Module.FiniteDimension public import Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear -public import Mathlib.Topology.Algebra.Module.LinearMapPiProd public import Mathlib.Topology.Algebra.Module.LinearPMap public import Mathlib.Topology.Algebra.Module.LocallyConvex public import Mathlib.Topology.Algebra.Module.ModuleTopology From 98f43b30aebd9d18a11e138b4df64226bbd0cd27 Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 14:12:50 +0200 Subject: [PATCH 04/26] import fixes --- Mathlib/Analysis/Asymptotics/TVS.lean | 2 +- Mathlib/Topology/Algebra/ContinuousAffineMap.lean | 2 +- Mathlib/Topology/Algebra/Module/Equiv.lean | 2 +- Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean | 2 +- Mathlib/Topology/Instances/TrivSqZeroExt.lean | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/Analysis/Asymptotics/TVS.lean b/Mathlib/Analysis/Asymptotics/TVS.lean index 50c5e8a599a193..68a1ea4eb5be46 100644 --- a/Mathlib/Analysis/Asymptotics/TVS.lean +++ b/Mathlib/Analysis/Asymptotics/TVS.lean @@ -9,7 +9,7 @@ public import Mathlib.Analysis.Convex.EGauge public import Mathlib.Analysis.LocallyConvex.BalancedCoreHull public import Mathlib.Analysis.Seminorm public import Mathlib.Analysis.Asymptotics.Defs -public import Mathlib.Topology.Algebra.Module.LinearMapPiProd +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd import Mathlib.Tactic.Peel public import Mathlib.Tactic.Bound public import Mathlib.Topology.Instances.ENNReal.Lemmas diff --git a/Mathlib/Topology/Algebra/ContinuousAffineMap.lean b/Mathlib/Topology/Algebra/ContinuousAffineMap.lean index 901f4bf7b59131..7b17d45f64d353 100644 --- a/Mathlib/Topology/Algebra/ContinuousAffineMap.lean +++ b/Mathlib/Topology/Algebra/ContinuousAffineMap.lean @@ -6,7 +6,7 @@ Authors: Oliver Nash module public import Mathlib.LinearAlgebra.AffineSpace.AffineMap -public import Mathlib.Topology.Algebra.Module.LinearMapPiProd +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd public import Mathlib.Topology.Algebra.Affine /-! diff --git a/Mathlib/Topology/Algebra/Module/Equiv.lean b/Mathlib/Topology/Algebra/Module/Equiv.lean index 8ce7236f242d97..df054664cfcdf5 100644 --- a/Mathlib/Topology/Algebra/Module/Equiv.lean +++ b/Mathlib/Topology/Algebra/Module/Equiv.lean @@ -6,7 +6,7 @@ Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov, Fréd -/ module -public import Mathlib.Topology.Algebra.Module.LinearMapPiProd +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict /-! diff --git a/Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean b/Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean index 603c79fc335d7b..cc01bf7e1b5bdd 100644 --- a/Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean +++ b/Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean @@ -5,7 +5,7 @@ Authors: Sébastien Gouëzel -/ module -public import Mathlib.Topology.Algebra.Module.LinearMapPiProd +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd public import Mathlib.LinearAlgebra.Multilinear.Basic public import Mathlib.Algebra.BigOperators.Fin diff --git a/Mathlib/Topology/Instances/TrivSqZeroExt.lean b/Mathlib/Topology/Instances/TrivSqZeroExt.lean index fcdfa7292550d7..81f2888fb6ddcd 100644 --- a/Mathlib/Topology/Instances/TrivSqZeroExt.lean +++ b/Mathlib/Topology/Instances/TrivSqZeroExt.lean @@ -8,7 +8,7 @@ module public import Mathlib.Algebra.TrivSqZeroExt.Basic public import Mathlib.Topology.Algebra.InfiniteSum.Basic public import Mathlib.Topology.Algebra.IsUniformGroup.Constructions -public import Mathlib.Topology.Algebra.Module.LinearMapPiProd +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd /-! # Topology on `TrivSqZeroExt R M` From 5c235df55dd4ef8c76d1c764ec2d32374c0b3f8b Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 14:16:23 +0200 Subject: [PATCH 05/26] fix --- Mathlib/Topology/Algebra/Module/Complement.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Topology/Algebra/Module/Complement.lean b/Mathlib/Topology/Algebra/Module/Complement.lean index 823a1f26cf7037..86076b328f6388 100644 --- a/Mathlib/Topology/Algebra/Module/Complement.lean +++ b/Mathlib/Topology/Algebra/Module/Complement.lean @@ -5,7 +5,8 @@ Authors: Anatole Dedecker, Sharvil Kesarwani -/ module -public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient public import Mathlib.Topology.Algebra.Module.Equiv /-! From 640cb0ec5f09d5d2c4cd851287e89c5d149c82ec Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 14:17:24 +0200 Subject: [PATCH 06/26] fix --- Mathlib/Analysis/Convex/Cone/Basic.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Analysis/Convex/Cone/Basic.lean b/Mathlib/Analysis/Convex/Cone/Basic.lean index b00f4e199c21e0..4c250d39c8419a 100644 --- a/Mathlib/Analysis/Convex/Cone/Basic.lean +++ b/Mathlib/Analysis/Convex/Cone/Basic.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.Convex.Cone.Closure public import Mathlib.Geometry.Convex.Cone.Pointed public import Mathlib.Topology.Algebra.Module.ClosedSubmodule +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars public import Mathlib.Topology.Algebra.Order.Module public import Mathlib.Topology.Order.DenselyOrdered From e18d6cd0cd17441f44dae8cd5670bc9f04df130b Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 14:20:23 +0200 Subject: [PATCH 07/26] Restore mistake --- .../Algebra/Module/ContinuousLinearMap/Basic.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean index 55460a17b8a5b2..675e0867659478 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean @@ -1095,6 +1095,18 @@ theorem coe_smulRightₗ (c : M →L[R] S) : ⇑(smulRightₗ c : M₂ →ₗ[T] end SMulRightₗ +section Semiring +variable {R S M : Type*} [Semiring R] [TopologicalSpace M] [AddCommGroup M] [Module R M] + [CommSemiring S] [Module S M] [SMulCommClass R S M] [SMul S R] [IsScalarTower S R M] + [ContinuousConstSMul S M] [IsTopologicalAddGroup M] + +instance algebra : Algebra S (M →L[R] M) := + Algebra.ofModule smul_comp fun _ _ _ => comp_smul _ _ _ + +@[simp] theorem algebraMap_apply (r : S) (m : M) : algebraMap S (M →L[R] M) r m = r • m := rfl + +end Semiring + end ContinuousLinearMap section topDualPairing From e8fcf4469c0cf5aa6de2973e23c2c7620b70ace4 Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 14:37:09 +0200 Subject: [PATCH 08/26] fixes --- Mathlib/Analysis/Complex/Basic.lean | 1 + Mathlib/Analysis/RCLike/Extend.lean | 1 + Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean | 1 + 3 files changed, 3 insertions(+) diff --git a/Mathlib/Analysis/Complex/Basic.lean b/Mathlib/Analysis/Complex/Basic.lean index 2891c136085179..2d43bd75916f75 100644 --- a/Mathlib/Analysis/Complex/Basic.lean +++ b/Mathlib/Analysis/Complex/Basic.lean @@ -11,6 +11,7 @@ public import Mathlib.Data.Complex.BigOperators public import Mathlib.LinearAlgebra.Complex.Module public import Mathlib.Topology.Algebra.Algebra.Equiv public import Mathlib.Topology.Algebra.InfiniteSum.Module +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars public import Mathlib.Topology.Instances.RealVectorSpace /-! diff --git a/Mathlib/Analysis/RCLike/Extend.lean b/Mathlib/Analysis/RCLike/Extend.lean index a78208e983ee03..9bfd56a416bf36 100644 --- a/Mathlib/Analysis/RCLike/Extend.lean +++ b/Mathlib/Analysis/RCLike/Extend.lean @@ -8,6 +8,7 @@ module public import Mathlib.Algebra.Algebra.RestrictScalars public import Mathlib.Analysis.RCLike.Basic public import Mathlib.LinearAlgebra.Dual.Defs +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars /-! # Extending an `ℝ`-linear functional to a `𝕜`-linear functional diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean index d965e396a95b34..efeec28683bac1 100644 --- a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean +++ b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean @@ -5,6 +5,7 @@ Authors: Anatole Dedecker, Yury Kudryashov -/ module +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars public import Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM /-! From 100dd8d071cfc511f75c683c115371a5388cb6f9 Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 14:55:19 +0200 Subject: [PATCH 09/26] fix --- Mathlib/Analysis/InnerProductSpace/Symmetric.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean index 17f5ccaed2136e..4960be18dc355d 100644 --- a/Mathlib/Analysis/InnerProductSpace/Symmetric.lean +++ b/Mathlib/Analysis/InnerProductSpace/Symmetric.lean @@ -9,6 +9,7 @@ public import Mathlib.Analysis.InnerProductSpace.Subspace public import Mathlib.Analysis.Normed.Operator.Banach public import Mathlib.LinearAlgebra.SesquilinearForm.Basic public import Mathlib.Analysis.InnerProductSpace.Orthogonal +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent /-! # Symmetric linear maps in an inner product space From 5ab265c4e59af14bd559c6e7e4be688cab6f2d31 Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 15:26:26 +0200 Subject: [PATCH 10/26] fix authors --- .../Algebra/Module/ContinuousLinearMap/Quotient.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean index 0cafce34e288a8..c1139c3d57e565 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean @@ -1,8 +1,7 @@ /- -Copyright (c) 2019 Sébastien Gouëzel. All rights reserved. +Copyright (c) 2026 Anatole Dedecker. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov, Frédéric Dupuis, - Heather Macbeth +Authors: Anatole Dedecker, Sharvil Kesarwani -/ module From c73fdbc67ce98390a27e86b5eece3a5673226614 Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 15:30:20 +0200 Subject: [PATCH 11/26] fix authors --- .../Algebra/Module/ContinuousLinearMap/Idempotent.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean index 244eb1075050e4..797960eac36b26 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean @@ -1,8 +1,7 @@ /- -Copyright (c) 2019 Sébastien Gouëzel. All rights reserved. +Copyright (c) 2025 Monica Omar. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov, Frédéric Dupuis, - Heather Macbeth +Authors: Monica Omar -/ module From 22a8619a86551bfd4af048d15767288d9a323f56 Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 15:50:55 +0200 Subject: [PATCH 12/26] Archaeology --- .../Algebra/Module/ContinuousLinearMap/RestrictScalars.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/RestrictScalars.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/RestrictScalars.lean index 863c5dd58b0b87..b5cd37255ab4f7 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/RestrictScalars.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/RestrictScalars.lean @@ -1,8 +1,7 @@ /- Copyright (c) 2019 Sébastien Gouëzel. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov, Frédéric Dupuis, - Heather Macbeth +Authors: Sébastien Gouëzel, Yury Kudryashov -/ module From 8647f20159be6cd268e5dce1765add569827327c Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 21:58:08 +0200 Subject: [PATCH 13/26] suggestions from review --- .../ContinuousLinearMap/Idempotent.lean | 30 +++++++++++-------- .../Module/ContinuousLinearMap/Restrict.lean | 2 +- 2 files changed, 18 insertions(+), 14 deletions(-) diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean index 797960eac36b26..cd073a5fc30887 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean @@ -27,39 +27,41 @@ variable {R M : Type*} [Ring R] [TopologicalSpace M] [AddCommGroup M] [Module R open ContinuousLinearMap +namespace IsIdempotentElem + /-- Idempotent operators are equal iff their range and kernels are. -/ -lemma IsIdempotentElem.ext_iff {p q : M →L[R] M} +lemma ext_iff {p q : M →L[R] M} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) : p = q ↔ p.range = q.range ∧ p.ker = q.ker := by simpa using LinearMap.IsIdempotentElem.ext_iff hp.toLinearMap hq.toLinearMap -alias ⟨_, IsIdempotentElem.ext⟩ := IsIdempotentElem.ext_iff +alias ⟨_, ext⟩ := IsIdempotentElem.ext_iff /-- `range f` is invariant under `T` if and only if `f ∘L T ∘L f = T ∘L f`, for idempotent `f`. -/ -lemma IsIdempotentElem.range_mem_invtSubmodule_iff {f T : M →L[R] M} +lemma range_mem_invtSubmodule_iff {f T : M →L[R] M} (hf : IsIdempotentElem f) : f.range ∈ Module.End.invtSubmodule T ↔ f ∘L T ∘L f = T ∘L f := by simpa [← ContinuousLinearMap.coe_comp] using LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff (T := T) hf.toLinearMap -alias ⟨IsIdempotentElem.conj_eq_of_range_mem_invtSubmodule, - IsIdempotentElem.range_mem_invtSubmodule⟩ := IsIdempotentElem.range_mem_invtSubmodule_iff +alias ⟨conj_eq_of_range_mem_invtSubmodule, + range_mem_invtSubmodule⟩ := IsIdempotentElem.range_mem_invtSubmodule_iff /-- `ker f` is invariant under `T` if and only if `f ∘L T ∘L f = f ∘L T`, for idempotent `f`. -/ -lemma IsIdempotentElem.ker_mem_invtSubmodule_iff {f T : M →L[R] M} +lemma ker_mem_invtSubmodule_iff {f T : M →L[R] M} (hf : IsIdempotentElem f) : f.ker ∈ Module.End.invtSubmodule T ↔ f ∘L T ∘L f = f ∘L T := by simpa [← ContinuousLinearMap.coe_comp] using LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff (T := T) hf.toLinearMap -alias ⟨IsIdempotentElem.conj_eq_of_ker_mem_invtSubmodule, - IsIdempotentElem.ker_mem_invtSubmodule⟩ := IsIdempotentElem.ker_mem_invtSubmodule_iff +alias ⟨conj_eq_of_ker_mem_invtSubmodule, + ker_mem_invtSubmodule⟩ := IsIdempotentElem.ker_mem_invtSubmodule_iff /-- An idempotent operator `f` commutes with `T` if and only if both `range f` and `ker f` are invariant under `T`. -/ -lemma IsIdempotentElem.commute_iff {f T : M →L[R] M} +lemma commute_iff {f T : M →L[R] M} (hf : IsIdempotentElem f) : Commute f T ↔ (f.range ∈ Module.End.invtSubmodule T ∧ f.ker ∈ Module.End.invtSubmodule T) := by simpa [Commute, SemiconjBy, Module.End.mul_eq_comp, ← coe_comp] using @@ -69,7 +71,7 @@ variable [IsTopologicalAddGroup M] /-- An idempotent operator `f` commutes with a unit operator `T` if and only if `T (range f) = range f` and `T (ker f) = ker f`. -/ -theorem IsIdempotentElem.commute_iff_of_isUnit {f T : M →L[R] M} (hT : IsUnit T) +theorem commute_iff_of_isUnit {f T : M →L[R] M} (hT : IsUnit T) (hf : IsIdempotentElem f) : Commute f T ↔ f.range.map (T : M →ₗ[R] M) = f.range ∧ f.ker.map (T : M →ₗ[R] M) = f.ker := by have := hT.map ContinuousLinearMap.toLinearMapRingHom @@ -77,13 +79,15 @@ theorem IsIdempotentElem.commute_iff_of_isUnit {f T : M →L[R] M} (hT : IsUnit simpa [Commute, SemiconjBy, Module.End.mul_eq_comp, ← ContinuousLinearMap.coe_comp] using LinearMap.IsIdempotentElem.commute_iff_of_isUnit this hf.toLinearMap -@[deprecated (since := "2025-12-27")] alias IsIdempotentElem.range_eq_ker := +@[deprecated (since := "2025-12-27")] alias range_eq_ker := LinearMap.IsIdempotentElem.range_eq_ker -@[deprecated (since := "2025-12-27")] alias IsIdempotentElem.ker_eq_range := +@[deprecated (since := "2025-12-27")] alias ker_eq_range := LinearMap.IsIdempotentElem.ker_eq_range -theorem IsIdempotentElem.isClosed_range [T1Space M] {p : M →L[R] M} +theorem isClosed_range [T1Space M] {p : M →L[R] M} (hp : IsIdempotentElem p) : IsClosed (p.range : Set M) := LinearMap.IsIdempotentElem.range_eq_ker hp.toLinearMap ▸ isClosed_ker (.id R M - p) +end IsIdempotentElem + end ContinuousLinearMap diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean index fa91c3727cd1e1..6bddf0c74e3b03 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean @@ -9,7 +9,7 @@ module public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic /-! -# Restriction operations on continuous linear maps +# Restrictions of continuous linear maps to submodules -/ @[expose] public section From 5bebadf73e97acdaeff047ffa341ce7ffc4548a9 Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 22:15:30 +0200 Subject: [PATCH 14/26] doc1 --- .../Module/ContinuousLinearMap/Basic.lean | 59 +++++++++++++++++-- 1 file changed, 55 insertions(+), 4 deletions(-) diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean index 675e0867659478..670f955728606a 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean @@ -16,12 +16,63 @@ public import Mathlib.Topology.Algebra.Module.Basic /-! # Continuous linear maps -In this file we define continuous (semi-)linear maps, as semilinear maps between topological -modules which are continuous. The set of continuous semilinear maps between the topological -`R₁`-module `M` and `R₂`-module `M₂` with respect to the `RingHom` `σ` is denoted by `M →SL[σ] M₂`. -Plain linear maps are denoted by `M →L[R] M₂` and star-linear maps by `M →L⋆[R] M₂`. +In this file we define the type of continuous (semi-)linear maps between topological +modules which are continuous, and endow it with its algebraic structure. + +Later files endow it with a topological structure, see the docstring of +`Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap`. + +## Main definitions + +* `ContinuousLinearMap` is the type of (semi)linear maps between two topological modules which are + continuous. It is denoted by `M →L[R] N` in the `R`-linear case, `M →SL[σ] N` in the + `σ`-semilinear case, and `M →L⋆[R] N` in the star-linear case. +* `StrongDual R M` is an abbrev for `M →L[R] R`, the type of continuous `R`-linear forms on `M`. + As a vector space, it is often called the "topological dual of `M`". We use the name "strong + dual" because it will (in later files) be endowed with the strong-dual topology, namely the + topology of uniform convergence on bounded subsets. +* `ContinuousLinearMap.addCommMonoid`, `ContinuousLinearMap.module`,... : algebraic structure + on `M →SL[σ] N` + +## Notation + +* `M →L[R] N`: the type of `R`-linear continuous maps from `M` to `N`; +* `M →SL[σ] N`: the type of `σ`-semilinear continuous maps from `M` to `N`; +* `M →L⋆[σ] N`: the type of star-linear continuous maps from `M` to `N`; +* `f ∘L g`: the composition of two continuous linear maps; +* `f ∘SL g`: the composition of two continuous semilinear maps. + +-/ + +/-! +# Basic + +## Main definitions + +* `FooBar` + +## Main statements + +* `fooBar_unique` + +## Notation + + + +## Implementation details + + + +## References + +* [F. Bar, *Quuxes*][bibkey] + +## Tags + +Foobars, barfoos -/ + @[expose] public section assert_not_exists TrivialStar From 6ab5be179737dcb2a5dc1e8db3e341c6ad860432 Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 22:27:04 +0200 Subject: [PATCH 15/26] doc 2 --- .../ContinuousLinearMap/Idempotent.lean | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean index cd073a5fc30887..0b32bb0927bbf3 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean @@ -9,8 +9,27 @@ public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic /-! # Idempotent continuous linear maps + +In this file, we study the idempotent elements (`IsIdempotentElem`) of the ring `M →L[R] M` of +continuous endomorphisms of a topological `R`-module `M`. + +## Main statements + +* `ContinuousLinearMap.isIdempotentElem_toLinearMap_iff`: `T` is idempotent as an element of + `M →L[R] M` if and only if it is as an element of `M →ₗ[R] M`; +* `ContinuousLinearMap.IsIdempotentElem.ext_iff`: idempotent elements of `M →L[R] M` are determined + by their range and kernel; +* `ContinuousLinearMap.IsIdempotentElem.commute_iff`: a continuous linear map `S` commutes with + an idempotent `T` if and only if the range and kernel of `T` are `S`-invariant; +* `ContinuousLinearMap.IsIdempotentElem.isCLosed_range`: an idempotent continuous linear map + has closed range. + +Further results can be found in the `Mathlib.Topology.Algebra.Module.Complement` module, where +we show that idempotent elements of `M →L[R] M` are precisely the projections associated to +topological complement submodules. -/ + @[expose] public section namespace ContinuousLinearMap From 98ea62163887cc7a5edb765a7cc9ef44f08c9a7a Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 22:31:51 +0200 Subject: [PATCH 16/26] doc3 --- .../Algebra/Module/ContinuousLinearMap/Quotient.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean index c1139c3d57e565..c6ffe1c9ae2728 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean @@ -9,6 +9,16 @@ public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic /-! # Continuous linear maps and quotient topological modules + +In this file, we collect various continuous linear maps associated to quotient spaces. + +## Main definitions + +* `Submodule.mkQL S` is the canonical quotient map `M →L[R] M ⧸ S`. In other words, it is + `Submodule.mkQ S` bundled as a `ContinuousLinearMap`. +* `Submodule.liftQL S f h` is the map `M ⧸ S →SL[σ] N` given by `f : M →SL[σ] N` and a proof + `h : S ≤ f.ker` that `f` vanishes on `S`. In other words, it is `Submodule.liftQ S f h` bundled + as a `ContinuousLinearMap`. -/ @[expose] public section From e864b11c3a608052a1820aee1be383bfafc29156 Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 22:32:31 +0200 Subject: [PATCH 17/26] ++ --- .../Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean index c6ffe1c9ae2728..842a576bd9b1b0 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean @@ -19,6 +19,10 @@ In this file, we collect various continuous linear maps associated to quotient s * `Submodule.liftQL S f h` is the map `M ⧸ S →SL[σ] N` given by `f : M →SL[σ] N` and a proof `h : S ≤ f.ker` that `f` vanishes on `S`. In other words, it is `Submodule.liftQ S f h` bundled as a `ContinuousLinearMap`. + +## TODO + +* Define `Submodule.mapQL`, the continuous linear bundling of `Submodule.mapQ`. -/ @[expose] public section From 86ec3b61e97058ee222b8978db5cc2d2fee7089b Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 23:28:25 +0200 Subject: [PATCH 18/26] PiProd --- .../Module/ContinuousLinearMap/PiProd.lean | 45 +++++++++++++++++++ .../Module/ContinuousLinearMap/Restrict.lean | 17 +++++++ 2 files changed, 62 insertions(+) diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean index 53d34c2cfe04da..b88c537110343c 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean @@ -10,6 +10,51 @@ public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic /-! # Continuous linear maps on products and Pi types + +In this file, we collect various constructions relating continuous linear maps with (binary or +arbitrary) products. + +## Main definitions + +Binary products (viewed as categorical products): + +* `ContinuousLinearMap.fst R M₁ M₂ : M₁ × M₂ →L[R] M₁` and + `ContinuousLinearMap.snd R M₁ M₂ : M₁ × M₂ →L[R] M₂` are the two canonical projections, given + respectively by `fst (x, y) = x` and `snd (x, y) = y`. These are the continuous versions + of `LinearMap.fst` and `LinearMap.snd`. +* `ContinuousLinearMap.prod f₁ f₂` is the continuous linear map `M →L[R] N₁ × N₂` given by two + continuous linear maps `f₁ : M →L[R] N₁` and `f₂ : M →L[R] N₂`. This is the continuous version + of `LinearMap.prod`. +* `ContinuousLinearMap.prodEquiv` shows that the above is a bijection: every continuous linear + map to a product is obtained this way. In other words, this is the universal property of the + product. +* `ContinuousLinearMap.prodMap f₁ f₂` is the continuous linear map `M₁ × M₂ →L[R] N₁ × N₂` given by + two continuous linear maps `f₁ : M₁ →L[R] N₁` and `f₂ : M₂ →L[R] N₂`. This is the continuous + version of `LinearMap.prodMap`. + +Binary products (viewed as categorical coproducts): + +* `ContinuousLinearMap.inl R M₁ M₂ : M₁ →L[R] M₁ × M₂` and + `ContinuousLinearMap.inr R M₁ M₂ : M₂ →L[R] M₁ × M₂` are the two canonical inclusions, given + respectively by `inl x = (x, 0)` and `inr x = (0, x)`. These are the continuous versions + of `LinearMap.inl` and `LinearMap.inr`. +* `ContinuousLinearMap.coprod f₁ f₂` is the continuous linear map ` M₁ × M₂ →L[R] N` given by + two continuous linear maps `f₁ : M₁ →L[R] N` and `f₂ : M₂ →L[R] N`. This is the continuous + version of `LinearMap.coprod`. +* `ContinuousLinearMap.coprodEquiv` shows that the above is a bijection: every continuous linear + map from a (binary) product is obtained this way. In other words, this is the universal property + of the coproduct. + +Indexed products: + +* `ContinuousLinearMap.pi f` is the continuous linear map `M →L[R] (Π i, N i)` given by a family + `f₁ : Π i, M →L[R] N i` of continuous linear maps. This is the continuous version + of `LinearMap.pi`. +* `ContinuousLinearMap.piMap f` is the continuous linear map `(Π i, M i) →L[R] (Π i, N i)` given by + a family `f : Π i, M i →L[R] N i` of continuous linear maps. This is the continuous + version of `LinearMap.piMap`. +* `ContinuousLinearMap.proj j : (Π i, M i) → L[R] M j` is the canonical projection given by + `proj i f = f i`. This is the continuous version of `LinearMap.proj`. -/ @[expose] public section diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean index 6bddf0c74e3b03..ffc5d82f41cb0f 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean @@ -10,6 +10,23 @@ public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic /-! # Restrictions of continuous linear maps to submodules + +In this file, we collect the various operations of restrictions of `ContinuousLinearMap`s +to subspaces of the domain/codomain. + +## Main definitions + +* `Submodule.subtypeL S` is the canonical inclusion `S →L[R] M` when `S : Submodule R M`. + In other words, it is `Submodule.subtype S` bundled as a `ContinuousLinearMap`. +* `ContinuousLinearMap.domRestrict f S` is the map `S →SL[σ] N` obtained by restricting + `f : M →SL[σ] N` to a subspace `S` of the *domain*. +* `ContinuousLinearMap.codRestrict f S h` is the map `M →SL[σ] S` obtained by co-restricting + `f : M →SL[σ] N` to a subspace `S` of the *codomain*; this requires a proof `h` that all values + of `f` indeed belong to `S`. +* `ContinuousLinearMap.rangeRestrict f` is an abbrev for + `f.codRestrict f.range ⋯ : M →SL[σ] f.range`. +* `ContinuousLinearMap.restrict f h` is the map `S →SL[σ] T` obtained by restricting from + `f : M →SL[σ] N` and a proof `h` that `f` maps `S` inside `T`. -/ @[expose] public section From 71478330099186e4a792ea441a0a54bc02bef89e Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 23:30:50 +0200 Subject: [PATCH 19/26] Done ? --- .../Algebra/Module/ContinuousLinearMap/RestrictScalars.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/RestrictScalars.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/RestrictScalars.lean index b5cd37255ab4f7..7c57f0b68852a3 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/RestrictScalars.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/RestrictScalars.lean @@ -9,6 +9,10 @@ public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic /-! # Restriction of scalars for continuous linear maps + +In this file, we define and study `ContinuousLinearMap.restrictScalars`, which reinterprets +a continuous `R`-linear map as a continuous `S`-linear map, for suitable `R` and `S`. +This is the continuous version of `LinearMap.restrictScalars`. -/ @[expose] public section From ab334094a52f717b58e3a288bb64b27245f0f2be Mon Sep 17 00:00:00 2001 From: ADedecker Date: Wed, 20 May 2026 23:35:22 +0200 Subject: [PATCH 20/26] forgot --- .../Module/ContinuousLinearMap/Basic.lean | 29 ------------------- 1 file changed, 29 deletions(-) diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean index 670f955728606a..468a1b57eeff8e 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean @@ -44,35 +44,6 @@ Later files endow it with a topological structure, see the docstring of -/ -/-! -# Basic - -## Main definitions - -* `FooBar` - -## Main statements - -* `fooBar_unique` - -## Notation - - - -## Implementation details - - - -## References - -* [F. Bar, *Quuxes*][bibkey] - -## Tags - -Foobars, barfoos --/ - - @[expose] public section assert_not_exists TrivialStar From 808bcbf8d98ebb56d39f07b4b62f060b236538af Mon Sep 17 00:00:00 2001 From: ADedecker Date: Thu, 21 May 2026 10:23:28 +0200 Subject: [PATCH 21/26] abbreviation --- .../Topology/Algebra/Module/ContinuousLinearMap/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean index 468a1b57eeff8e..0a007918348513 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean @@ -27,8 +27,8 @@ Later files endow it with a topological structure, see the docstring of * `ContinuousLinearMap` is the type of (semi)linear maps between two topological modules which are continuous. It is denoted by `M →L[R] N` in the `R`-linear case, `M →SL[σ] N` in the `σ`-semilinear case, and `M →L⋆[R] N` in the star-linear case. -* `StrongDual R M` is an abbrev for `M →L[R] R`, the type of continuous `R`-linear forms on `M`. - As a vector space, it is often called the "topological dual of `M`". We use the name "strong +* `StrongDual R M` is an abbreviation for `M →L[R] R`, the type of continuous `R`-linear forms on + `M`. As a vector space, it is often called the "topological dual of `M`". We use the name "strong dual" because it will (in later files) be endowed with the strong-dual topology, namely the topology of uniform convergence on bounded subsets. * `ContinuousLinearMap.addCommMonoid`, `ContinuousLinearMap.module`,... : algebraic structure From a35b86e6c875e2bdc1bc8c45093348e6af88fbff Mon Sep 17 00:00:00 2001 From: Anatole Dedecker Date: Thu, 21 May 2026 10:26:53 +0200 Subject: [PATCH 22/26] Apply suggestions from code review Co-authored-by: Filippo A. E. Nuccio --- .../Algebra/Module/ContinuousLinearMap/Basic.lean | 8 ++++---- .../Algebra/Module/ContinuousLinearMap/Idempotent.lean | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean index 0a007918348513..9ef29f3161265d 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean @@ -16,22 +16,22 @@ public import Mathlib.Topology.Algebra.Module.Basic /-! # Continuous linear maps -In this file we define the type of continuous (semi-)linear maps between topological -modules which are continuous, and endow it with its algebraic structure. +In this file we define the type of continuous (semi)linear maps between topological +modules that are continuous, and endow it with its algebraic structure. Later files endow it with a topological structure, see the docstring of `Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap`. ## Main definitions -* `ContinuousLinearMap` is the type of (semi)linear maps between two topological modules which are +* `ContinuousLinearMap` is the type of (semi)linear maps between two topological modules that are continuous. It is denoted by `M →L[R] N` in the `R`-linear case, `M →SL[σ] N` in the `σ`-semilinear case, and `M →L⋆[R] N` in the star-linear case. * `StrongDual R M` is an abbreviation for `M →L[R] R`, the type of continuous `R`-linear forms on `M`. As a vector space, it is often called the "topological dual of `M`". We use the name "strong dual" because it will (in later files) be endowed with the strong-dual topology, namely the topology of uniform convergence on bounded subsets. -* `ContinuousLinearMap.addCommMonoid`, `ContinuousLinearMap.module`,... : algebraic structure +* `ContinuousLinearMap.addCommMonoid`, `ContinuousLinearMap.module`,... : the algebraic structures on `M →SL[σ] N` ## Notation diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean index 876fccf30be15c..14ec31c07dbc39 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean @@ -16,7 +16,7 @@ continuous endomorphisms of a topological `R`-module `M`. ## Main statements * `ContinuousLinearMap.isIdempotentElem_toLinearMap_iff`: `T` is idempotent as an element of - `M →L[R] M` if and only if it is as an element of `M →ₗ[R] M`; + `M →L[R] M` if and only if it is such as an element of `M →ₗ[R] M`; * `ContinuousLinearMap.IsIdempotentElem.ext_iff`: idempotent elements of `M →L[R] M` are determined by their range and kernel; * `ContinuousLinearMap.IsIdempotentElem.commute_iff`: a continuous linear map `S` commutes with From 40266b6264a1851234c57a2f6c7c79d54a05ddec Mon Sep 17 00:00:00 2001 From: ADedecker Date: Thu, 21 May 2026 10:29:59 +0200 Subject: [PATCH 23/26] less canonical --- .../Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean | 6 +++--- .../Algebra/Module/ContinuousLinearMap/Quotient.lean | 2 +- .../Algebra/Module/ContinuousLinearMap/Restrict.lean | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean index b88c537110343c..026d2988cc4c86 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean @@ -19,7 +19,7 @@ arbitrary) products. Binary products (viewed as categorical products): * `ContinuousLinearMap.fst R M₁ M₂ : M₁ × M₂ →L[R] M₁` and - `ContinuousLinearMap.snd R M₁ M₂ : M₁ × M₂ →L[R] M₂` are the two canonical projections, given + `ContinuousLinearMap.snd R M₁ M₂ : M₁ × M₂ →L[R] M₂` are the two projections, given respectively by `fst (x, y) = x` and `snd (x, y) = y`. These are the continuous versions of `LinearMap.fst` and `LinearMap.snd`. * `ContinuousLinearMap.prod f₁ f₂` is the continuous linear map `M →L[R] N₁ × N₂` given by two @@ -35,7 +35,7 @@ Binary products (viewed as categorical products): Binary products (viewed as categorical coproducts): * `ContinuousLinearMap.inl R M₁ M₂ : M₁ →L[R] M₁ × M₂` and - `ContinuousLinearMap.inr R M₁ M₂ : M₂ →L[R] M₁ × M₂` are the two canonical inclusions, given + `ContinuousLinearMap.inr R M₁ M₂ : M₂ →L[R] M₁ × M₂` are the two inclusions, given respectively by `inl x = (x, 0)` and `inr x = (0, x)`. These are the continuous versions of `LinearMap.inl` and `LinearMap.inr`. * `ContinuousLinearMap.coprod f₁ f₂` is the continuous linear map ` M₁ × M₂ →L[R] N` given by @@ -53,7 +53,7 @@ Indexed products: * `ContinuousLinearMap.piMap f` is the continuous linear map `(Π i, M i) →L[R] (Π i, N i)` given by a family `f : Π i, M i →L[R] N i` of continuous linear maps. This is the continuous version of `LinearMap.piMap`. -* `ContinuousLinearMap.proj j : (Π i, M i) → L[R] M j` is the canonical projection given by +* `ContinuousLinearMap.proj j : (Π i, M i) → L[R] M j` is the projection given by `proj i f = f i`. This is the continuous version of `LinearMap.proj`. -/ diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean index 842a576bd9b1b0..db51786e65a5db 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean @@ -14,7 +14,7 @@ In this file, we collect various continuous linear maps associated to quotient s ## Main definitions -* `Submodule.mkQL S` is the canonical quotient map `M →L[R] M ⧸ S`. In other words, it is +* `Submodule.mkQL S` is the quotient map `M →L[R] M ⧸ S`. In other words, it is `Submodule.mkQ S` bundled as a `ContinuousLinearMap`. * `Submodule.liftQL S f h` is the map `M ⧸ S →SL[σ] N` given by `f : M →SL[σ] N` and a proof `h : S ≤ f.ker` that `f` vanishes on `S`. In other words, it is `Submodule.liftQ S f h` bundled diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean index ffc5d82f41cb0f..9a1da7187a5278 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean @@ -16,14 +16,14 @@ to subspaces of the domain/codomain. ## Main definitions -* `Submodule.subtypeL S` is the canonical inclusion `S →L[R] M` when `S : Submodule R M`. +* `Submodule.subtypeL S` is the inclusion map `S →L[R] M` when `S : Submodule R M`. In other words, it is `Submodule.subtype S` bundled as a `ContinuousLinearMap`. * `ContinuousLinearMap.domRestrict f S` is the map `S →SL[σ] N` obtained by restricting `f : M →SL[σ] N` to a subspace `S` of the *domain*. * `ContinuousLinearMap.codRestrict f S h` is the map `M →SL[σ] S` obtained by co-restricting `f : M →SL[σ] N` to a subspace `S` of the *codomain*; this requires a proof `h` that all values of `f` indeed belong to `S`. -* `ContinuousLinearMap.rangeRestrict f` is an abbrev for +* `ContinuousLinearMap.rangeRestrict f` is an abbreviation for `f.codRestrict f.range ⋯ : M →SL[σ] f.range`. * `ContinuousLinearMap.restrict f h` is the map `S →SL[σ] T` obtained by restricting from `f : M →SL[σ] N` and a proof `h` that `f` maps `S` inside `T`. From 8421bdf228c97a660fc185ad12b9de8db585db89 Mon Sep 17 00:00:00 2001 From: ADedecker Date: Thu, 21 May 2026 11:19:26 +0200 Subject: [PATCH 24/26] dot --- Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean index 9ef29f3161265d..d29ad782307898 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean @@ -32,7 +32,7 @@ Later files endow it with a topological structure, see the docstring of dual" because it will (in later files) be endowed with the strong-dual topology, namely the topology of uniform convergence on bounded subsets. * `ContinuousLinearMap.addCommMonoid`, `ContinuousLinearMap.module`,... : the algebraic structures - on `M →SL[σ] N` + on `M →SL[σ] N`. ## Notation From ba2ce945937236054554afbef0fb414780c04682 Mon Sep 17 00:00:00 2001 From: Anatole Dedecker Date: Thu, 21 May 2026 11:20:20 +0200 Subject: [PATCH 25/26] Apply suggestions from code review Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- .../Topology/Algebra/Module/ContinuousLinearMap/Basic.lean | 6 +++--- .../Algebra/Module/ContinuousLinearMap/Idempotent.lean | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean index d29ad782307898..5b71e302d72c81 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean @@ -20,13 +20,13 @@ In this file we define the type of continuous (semi)linear maps between topologi modules that are continuous, and endow it with its algebraic structure. Later files endow it with a topological structure, see the docstring of -`Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap`. +`Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean`. ## Main definitions * `ContinuousLinearMap` is the type of (semi)linear maps between two topological modules that are continuous. It is denoted by `M →L[R] N` in the `R`-linear case, `M →SL[σ] N` in the - `σ`-semilinear case, and `M →L⋆[R] N` in the star-linear case. + `σ`-semilinear case, and `M →L⋆[R] N` in the conjugate-linear (antilinear) case. * `StrongDual R M` is an abbreviation for `M →L[R] R`, the type of continuous `R`-linear forms on `M`. As a vector space, it is often called the "topological dual of `M`". We use the name "strong dual" because it will (in later files) be endowed with the strong-dual topology, namely the @@ -38,7 +38,7 @@ Later files endow it with a topological structure, see the docstring of * `M →L[R] N`: the type of `R`-linear continuous maps from `M` to `N`; * `M →SL[σ] N`: the type of `σ`-semilinear continuous maps from `M` to `N`; -* `M →L⋆[σ] N`: the type of star-linear continuous maps from `M` to `N`; +* `M →L⋆[σ] N`: the type of conjugate-linear (antilinear) continuous maps from `M` to `N`; * `f ∘L g`: the composition of two continuous linear maps; * `f ∘SL g`: the composition of two continuous semilinear maps. diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean index 14ec31c07dbc39..fc0781b504f45e 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean @@ -24,7 +24,7 @@ continuous endomorphisms of a topological `R`-module `M`. * `ContinuousLinearMap.IsIdempotentElem.isCLosed_range`: an idempotent continuous linear map has closed range. -Further results can be found in the `Mathlib.Topology.Algebra.Module.Complement` module, where +Further results can be found in the `Mathlib/Topology/Algebra/Module/Complement.lean` module, where we show that idempotent elements of `M →L[R] M` are precisely the projections associated to topological complement submodules. -/ From 8cdcb5f867c23b74ddfe2666be7fd59cd3efffdf Mon Sep 17 00:00:00 2001 From: Anatole Dedecker Date: Thu, 21 May 2026 11:39:48 +0200 Subject: [PATCH 26/26] Apply suggestions from code review Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- .../Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean | 2 +- .../Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean index 026d2988cc4c86..e5d262bec8c0df 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean @@ -53,7 +53,7 @@ Indexed products: * `ContinuousLinearMap.piMap f` is the continuous linear map `(Π i, M i) →L[R] (Π i, N i)` given by a family `f : Π i, M i →L[R] N i` of continuous linear maps. This is the continuous version of `LinearMap.piMap`. -* `ContinuousLinearMap.proj j : (Π i, M i) → L[R] M j` is the projection given by +* `ContinuousLinearMap.proj j : (Π i, M i) →L[R] M j` is the projection given by `proj i f = f i`. This is the continuous version of `LinearMap.proj`. -/ diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean index 9a1da7187a5278..d441ec3c01472a 100644 --- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean @@ -20,13 +20,17 @@ to subspaces of the domain/codomain. In other words, it is `Submodule.subtype S` bundled as a `ContinuousLinearMap`. * `ContinuousLinearMap.domRestrict f S` is the map `S →SL[σ] N` obtained by restricting `f : M →SL[σ] N` to a subspace `S` of the *domain*. + This is the continuous version of `LinearMap.domRestrict`. * `ContinuousLinearMap.codRestrict f S h` is the map `M →SL[σ] S` obtained by co-restricting `f : M →SL[σ] N` to a subspace `S` of the *codomain*; this requires a proof `h` that all values of `f` indeed belong to `S`. + This is the continuous version of `LinearMap.codRestrict`. * `ContinuousLinearMap.rangeRestrict f` is an abbreviation for `f.codRestrict f.range ⋯ : M →SL[σ] f.range`. + This is the continuous version of `LinearMap.rangeRestrict`. * `ContinuousLinearMap.restrict f h` is the map `S →SL[σ] T` obtained by restricting from `f : M →SL[σ] N` and a proof `h` that `f` maps `S` inside `T`. + This is the continuous version of `LinearMap.restrict`. -/ @[expose] public section