diff --git a/Mathlib.lean b/Mathlib.lean index d211bbdb619507..affc7f126e1cdd 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -7456,12 +7456,16 @@ 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.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 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 public import Mathlib.Topology.Algebra.Module.ModuleTopology 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/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/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 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/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 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/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/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/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..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.LinearMap +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient 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 74% rename from Mathlib/Topology/Algebra/Module/LinearMap.lean rename to Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean index b11c26e87dd3dd..675e0867659478 100644 --- a/Mathlib/Topology/Algebra/Module/LinearMap.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean @@ -1107,375 +1107,6 @@ instance algebra : Algebra S (M →L[R] M) := 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..cd073a5fc30887 --- /dev/null +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean @@ -0,0 +1,93 @@ +/- +Copyright (c) 2025 Monica Omar. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Monica Omar +-/ +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 + +namespace IsIdempotentElem + +/-- Idempotent operators are equal iff their range and kernels are. -/ +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 ⟨_, 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 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 ⟨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 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 ⟨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 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 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 range_eq_ker := + LinearMap.IsIdempotentElem.range_eq_ker +@[deprecated (since := "2025-12-27")] alias ker_eq_range := + LinearMap.IsIdempotentElem.ker_eq_range + +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/LinearMapPiProd.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean similarity index 99% rename from Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean rename to Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.lean index 18761b5b47885a..53d34c2cfe04da 100644 --- a/Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/PiProd.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/ContinuousLinearMap/Quotient.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean new file mode 100644 index 00000000000000..c1139c3d57e565 --- /dev/null +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Quotient.lean @@ -0,0 +1,67 @@ +/- +Copyright (c) 2026 Anatole Dedecker. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anatole Dedecker, Sharvil Kesarwani +-/ +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..6bddf0c74e3b03 --- /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 + +/-! +# Restrictions of continuous linear maps to submodules +-/ + +@[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..b5cd37255ab4f7 --- /dev/null +++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/RestrictScalars.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: Sébastien Gouëzel, Yury Kudryashov +-/ +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/Equiv.lean b/Mathlib/Topology/Algebra/Module/Equiv.lean index ee71f4f50d06a3..df054664cfcdf5 100644 --- a/Mathlib/Topology/Algebra/Module/Equiv.lean +++ b/Mathlib/Topology/Algebra/Module/Equiv.lean @@ -6,7 +6,8 @@ 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 /-! # Continuous linear equivalences 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/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/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 /-! 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 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`