← Verification

.lake/packages/mathlib/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean

Download original source

Read-only source copy. Line numbers are navigation aids.

1/-
2Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
3Released under Apache 2.0 license as described in the file LICENSE.
4Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov, Frédéric Dupuis,
5 Heather Macbeth
6-/
7module
8
9public import Mathlib.Algebra.Module.LinearMap.DivisionRing
10public import Mathlib.Algebra.Module.Submodule.EqLocus
11public import Mathlib.Algebra.Module.Submodule.Invariant
12public import Mathlib.Data.FunLike.Module
13public import Mathlib.Data.FunLike.Ring
14public import Mathlib.Topology.Algebra.Group.ZPow
15public import Mathlib.Topology.Algebra.IsUniformGroup.Defs
16public import Mathlib.Topology.Algebra.Module.Basic
17
18/-!
19# Continuous linear maps
20
21In this file we define the type of continuous (semi)linear maps between topological
22modules that are continuous, and endow it with its algebraic structure.
23
24Later files endow it with a topological structure, see the docstring of
25`Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean`.
26
27## Main definitions
28
29* `ContinuousLinearMap` is the type of (semi)linear maps between two topological modules that are
30 continuous. It is denoted by `M →L[R] N` in the `R`-linear case, `M →SL[σ] N` in the
31 `σ`-semilinear case, and `M →L⋆[R] N` in the conjugate-linear (antilinear) case.
32* `StrongDual R M` is an abbreviation for `M →L[R] R`, the type of continuous `R`-linear forms on
33 `M`. As a vector space, it is often called the "topological dual of `M`". We use the name "strong
34 dual" because it will (in later files) be endowed with the strong-dual topology, namely the
35 topology of uniform convergence on bounded subsets.
36* `ContinuousLinearMap.addCommMonoid`, `ContinuousLinearMap.module`,... : the algebraic structures
37 on `M →SL[σ] N`.
38
39## Notation
40
41* `M →L[R] N`: the type of `R`-linear continuous maps from `M` to `N`;
42* `M →SL[σ] N`: the type of `σ`-semilinear continuous maps from `M` to `N`;
43* `M →L⋆[σ] N`: the type of conjugate-linear (antilinear) continuous maps from `M` to `N`;
44* `f ∘L g`: the composition of two continuous linear maps;
45* `f ∘SL g`: the composition of two continuous semilinear maps.
46
47-/
48
49@[expose] public section
50
51assert_not_exists TrivialStar
52
53open LinearMap (ker range)
54
55universe u v w u'
56
57/-- Continuous linear maps between modules. We only put the type classes that are necessary for the
58definition, although in applications `M` and `M₂` will be topological modules over the topological
59ring `R`. -/
60structure ContinuousLinearMap {R : Type*} {S : Type*} [Semiring R] [Semiring S] (σ : R →+* S)
61 (M : Type*) [TopologicalSpace M] [AddCommMonoid M] (M₂ : Type*) [TopologicalSpace M₂]
62 [AddCommMonoid M₂] [Module R M] [Module S M₂] extends M →ₛₗ[σ] M₂ where
63 cont : Continuous toFun := by
64 first | fun_prop | eta_expand; dsimp; fun_prop | skip
65
66attribute [inherit_doc ContinuousLinearMap] ContinuousLinearMap.cont
67
68@[inherit_doc]
69notation:25 M " →SL[" σ "] " M₂ => ContinuousLinearMap σ M M₂
70
71@[inherit_doc]
72notation:25 M " →L[" R "] " M₂ => ContinuousLinearMap (RingHom.id R) M M₂
73
74/-- `ContinuousSemilinearMapClass F σ M M₂` asserts `F` is a type of bundled continuous
75`σ`-semilinear maps `M → M₂`. See also `ContinuousLinearMapClass F R M M₂` for the case where
76`σ` is the identity map on `R`. A map `f` between an `R`-module and an `S`-module over a ring
77homomorphism `σ : R →+* S` is semilinear if it satisfies the two properties `f (x + y) = f x + f y`
78and `f (c • x) = (σ c) • f x`. -/
79class ContinuousSemilinearMapClass (F : Type*) {R S : outParam Type*} [Semiring R] [Semiring S]
80 (σ : outParam <| R →+* S) (M : outParam Type*) [TopologicalSpace M] [AddCommMonoid M]
81 (M₂ : outParam Type*) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M]
82 [Module S M₂] [FunLike F M M₂] : Prop
83 extends SemilinearMapClass F σ M M₂, ContinuousMapClass F M M₂
84
85/-- `ContinuousLinearMapClass F R M M₂` asserts `F` is a type of bundled continuous
86`R`-linear maps `M → M₂`. This is an abbreviation for
87`ContinuousSemilinearMapClass F (RingHom.id R) M M₂`. -/
88abbrev ContinuousLinearMapClass (F : Type*) (R : outParam Type*) [Semiring R]
89 (M : outParam Type*) [TopologicalSpace M] [AddCommMonoid M] (M₂ : outParam Type*)
90 [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M] [Module R M₂] [FunLike F M M₂] :=
91 ContinuousSemilinearMapClass F (RingHom.id R) M M₂
92
93/-- The *strong dual* of a topological vector space `M` over a ring `R`. This is the space of
94continuous linear functionals and is equipped with the topology of uniform convergence
95on bounded subsets. `StrongDual R M` is an abbreviation for `M →L[R] R`. -/
96abbrev StrongDual (R : Type*) [Semiring R] [TopologicalSpace R]
97 (M : Type*) [TopologicalSpace M] [AddCommMonoid M] [Module R M] : Type _ := M →L[R] R
98
99namespace ContinuousLinearMap
100
101section Semiring
102
103/-!
104### Properties that hold for non-necessarily commutative semirings.
105-/
106
107variable {R₁ : Type*} {R₂ : Type*} {R₃ : Type*} [Semiring R₁] [Semiring R₂] [Semiring R₃]
108 {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type*} [TopologicalSpace M₁]
109 [AddCommMonoid M₁] {M'₁ : Type*} [TopologicalSpace M'₁] [AddCommMonoid M'₁] {M₂ : Type*}
110 [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type*} [TopologicalSpace M₃] [AddCommMonoid M₃]
111 {M₄ : Type*} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R₁ M₁] [Module R₁ M'₁]
112 [Module R₂ M₂] [Module R₃ M₃]
113
114attribute [coe] ContinuousLinearMap.toLinearMap
115/-- Coerce continuous linear maps to linear maps. -/
116instance LinearMap.coe : Coe (M₁ →SL[σ₁₂] M₂) (M₁ →ₛₗ[σ₁₂] M₂) := ⟨toLinearMap⟩
117
118theorem coe_injective : Function.Injective ((↑) : (M₁ →SL[σ₁₂] M₂) → M₁ →ₛₗ[σ₁₂] M₂) := by
119 intro f g H
120 cases f
121 cases g
122 congr
123
124instance funLike : FunLike (M₁ →SL[σ₁₂] M₂) M₁ M₂ where
125 coe f := f.toLinearMap
126 coe_injective _ _ h := coe_injective (DFunLike.coe_injective h)
127
128instance continuousSemilinearMapClass :
129 ContinuousSemilinearMapClass (M₁ →SL[σ₁₂] M₂) σ₁₂ M₁ M₂ where
130 map_add f := map_add f.toLinearMap
131 map_continuous f := f.2
132 map_smulₛₗ f := f.toLinearMap.map_smul'
133
134theorem coe_mk (f : M₁ →ₛₗ[σ₁₂] M₂) (h) : (mk f h : M₁ →ₛₗ[σ₁₂] M₂) = f :=
135 rfl
136
137@[simp]
138theorem coe_mk' (f : M₁ →ₛₗ[σ₁₂] M₂) (h) : (mk f h : M₁ → M₂) = f :=
139 rfl
140
141@[continuity, fun_prop]
142protected theorem continuous (f : M₁ →SL[σ₁₂] M₂) : Continuous f :=
143 f.2
144
145@[continuity, fun_prop]
146protected theorem continuous_toLinearMap (f : M₁ →SL[σ₁₂] M₂) : Continuous f.toLinearMap :=
147 f.2
148
149@[simp]
150protected theorem uniformContinuous {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂]
151 [AddCommGroup E₁] [AddCommGroup E₂] [Module R₁ E₁] [Module R₂ E₂] [IsUniformAddGroup E₁]
152 [IsUniformAddGroup E₂] (f : E₁ →SL[σ₁₂] E₂) : UniformContinuous f :=
153 uniformContinuous_addMonoidHom_of_continuous f.continuous
154
155@[simp, norm_cast]
156theorem coe_inj {f g : M₁ →SL[σ₁₂] M₂} : (f : M₁ →ₛₗ[σ₁₂] M₂) = g ↔ f = g :=
157 coe_injective.eq_iff
158
159theorem coeFn_injective : @Function.Injective (M₁ →SL[σ₁₂] M₂) (M₁ → M₂) (↑) :=
160 DFunLike.coe_injective
161
162theorem toContinuousAddMonoidHom_injective :
163 Function.Injective ((↑) : (M₁ →SL[σ₁₂] M₂) → ContinuousAddMonoidHom M₁ M₂) :=
164 (DFunLike.coe_injective.of_comp_iff _).1 DFunLike.coe_injective
165
166@[simp, norm_cast]
167theorem toContinuousAddMonoidHom_inj {f g : M₁ →SL[σ₁₂] M₂} :
168 (f : ContinuousAddMonoidHom M₁ M₂) = g ↔ f = g :=
169 toContinuousAddMonoidHom_injective.eq_iff
170
171/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
172 because it is a composition of multiple projections. -/
173def Simps.apply (h : M₁ →SL[σ₁₂] M₂) : M₁ → M₂ :=
174 h
175
176/-- See Note [custom simps projection]. -/
177def Simps.coe (h : M₁ →SL[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂ :=
178 h
179
180initialize_simps_projections ContinuousLinearMap (toFun → apply, toLinearMap → coe, as_prefix coe)
181
182@[ext]
183theorem ext {f g : M₁ →SL[σ₁₂] M₂} (h : ∀ x, f x = g x) : f = g :=
184 DFunLike.ext f g h
185
186@[simp, norm_cast]
187theorem coe_coe (f : M₁ →SL[σ₁₂] M₂) : ⇑(f : M₁ →ₛₗ[σ₁₂] M₂) = f :=
188 rfl
189
190/-- Copy of a `ContinuousLinearMap` with a new `toFun` equal to the old one. Useful to fix
191definitional equalities. -/
192protected def copy (f : M₁ →SL[σ₁₂] M₂) (f' : M₁ → M₂) (h : f' = ⇑f) : M₁ →SL[σ₁₂] M₂ where
193 toLinearMap := f.toLinearMap.copy f' h
194 cont := show Continuous f' from h.symm ▸ f.continuous
195
196@[simp]
197theorem coe_copy (f : M₁ →SL[σ₁₂] M₂) (f' : M₁ → M₂) (h : f' = ⇑f) : ⇑(f.copy f' h) = f' :=
198 rfl
199
200theorem copy_eq (f : M₁ →SL[σ₁₂] M₂) (f' : M₁ → M₂) (h : f' = ⇑f) : f.copy f' h = f :=
201 DFunLike.ext' h
202
203theorem range_coeFn_eq :
204 Set.range ((⇑) : (M₁ →SL[σ₁₂] M₂) → (M₁ → M₂)) =
205 {f | Continuous f} ∩ Set.range ((⇑) : (M₁ →ₛₗ[σ₁₂] M₂) → (M₁ → M₂)) := by
206 ext f
207 constructor
208 · rintro ⟨f, rfl⟩
209 exact ⟨f.continuous, f, rfl⟩
210 · rintro ⟨hfc, f, rfl⟩
211 exact ⟨⟨f, hfc⟩, rfl⟩
212
213lemma range_toLinearMap (f : M₁ →SL[σ₁₂] M₂) : Set.range f.toLinearMap = Set.range f := by simp
214
215-- make some straightforward lemmas available to `simp`.
216protected theorem map_zero (f : M₁ →SL[σ₁₂] M₂) : f (0 : M₁) = 0 :=
217 map_zero f
218
219protected theorem map_add (f : M₁ →SL[σ₁₂] M₂) (x y : M₁) : f (x + y) = f x + f y :=
220 map_add f x y
221
222@[simp]
223protected theorem map_smulₛₗ (f : M₁ →SL[σ₁₂] M₂) (c : R₁) (x : M₁) : f (c • x) = σ₁₂ c • f x :=
224 (toLinearMap _).map_smulₛₗ _ _
225
226protected theorem map_smul [Module R₁ M₂] (f : M₁ →L[R₁] M₂) (c : R₁) (x : M₁) :
227 f (c • x) = c • f x := by simp only [RingHom.id_apply, map_smulₛₗ]
228
229@[simp]
230theorem map_smul_of_tower {R S : Type*} [Semiring S] [SMul R M₁] [Module S M₁] [SMul R M₂]
231 [Module S M₂] [LinearMap.CompatibleSMul M₁ M₂ R S] (f : M₁ →L[S] M₂) (c : R) (x : M₁) :
232 f (c • x) = c • f x :=
233 LinearMap.CompatibleSMul.map_smul (f : M₁ →ₗ[S] M₂) c x
234
235@[ext]
236theorem ext_ring [TopologicalSpace R₁] {f g : R₁ →L[R₁] M₁} (h : f 1 = g 1) : f = g :=
237 coe_inj.1 <| LinearMap.ext_ring h
238
239@[simp]
240theorem apply_val_ker (f : M₁ →SL[σ₁₂] M₂) (x : f.ker) : f x = 0 := x.2
241
242/-- If two continuous linear maps are equal on a set `s`, then they are equal on the closure
243of the `Submodule.span` of this set. -/
244theorem eqOn_closure_span [T2Space M₂] {s : Set M₁} {f g : M₁ →SL[σ₁₂] M₂} (h : Set.EqOn f g s) :
245 Set.EqOn f g (closure (Submodule.span R₁ s : Set M₁)) :=
246 (LinearMap.eqOn_span' h).closure f.continuous g.continuous
247
248/-- If the submodule generated by a set `s` is dense in the ambient module, then two continuous
249linear maps equal on `s` are equal. -/
250theorem ext_on [T2Space M₂] {s : Set M₁} (hs : Dense (Submodule.span R₁ s : Set M₁))
251 {f g : M₁ →SL[σ₁₂] M₂} (h : Set.EqOn f g s) : f = g :=
252 ext fun x => eqOn_closure_span h (hs x)
253
254/-- Under a continuous linear map, the image of the `TopologicalClosure` of a submodule is
255contained in the `TopologicalClosure` of its image. -/
256theorem _root_.Submodule.topologicalClosure_map [RingHomSurjective σ₁₂] [TopologicalSpace R₁]
257 [TopologicalSpace R₂] [ContinuousSMul R₁ M₁] [ContinuousAdd M₁] [ContinuousSMul R₂ M₂]
258 [ContinuousAdd M₂] (f : M₁ →SL[σ₁₂] M₂) (s : Submodule R₁ M₁) :
259 s.topologicalClosure.map (f : M₁ →ₛₗ[σ₁₂] M₂) ≤
260 (s.map (f : M₁ →ₛₗ[σ₁₂] M₂)).topologicalClosure :=
261 image_closure_subset_closure_image f.continuous
262
263/-- If a continuous linear map stabilizes a submodule, then it stabilizes its topological
264closure. -/
265theorem _root_.Submodule.topologicalClosure_mem_invtSubmodule [TopologicalSpace R₁]
266 [ContinuousSMul R₁ M₁] [ContinuousAdd M₁] {f : M₁ →L[R₁] M₁} {s : Submodule R₁ M₁}
267 (hs : s ∈ Module.End.invtSubmodule f) :
268 s.topologicalClosure ∈ Module.End.invtSubmodule f := by
269 rw [Module.End.mem_invtSubmodule_iff_map_le] at hs ⊢
270 exact (s.topologicalClosure_map f).trans (Submodule.topologicalClosure_mono hs)
271
272/-- Under a dense continuous linear map, a submodule whose `TopologicalClosure` is `⊤` is sent to
273another such submodule. That is, the image of a dense set under a map with dense range is dense.
274-/
275theorem _root_.DenseRange.topologicalClosure_map_submodule [RingHomSurjective σ₁₂]
276 [TopologicalSpace R₁] [TopologicalSpace R₂] [ContinuousSMul R₁ M₁] [ContinuousAdd M₁]
277 [ContinuousSMul R₂ M₂] [ContinuousAdd M₂] {f : M₁ →SL[σ₁₂] M₂} (hf' : DenseRange f)
278 {s : Submodule R₁ M₁} (hs : s.topologicalClosure = ⊤) :
279 (s.map (f : M₁ →ₛₗ[σ₁₂] M₂)).topologicalClosure = ⊤ := by
280 rw [SetLike.ext'_iff] at hs ⊢
281 simp only [Submodule.topologicalClosure_coe, Submodule.top_coe, ← dense_iff_closure_eq] at hs ⊢
282 exact hf'.dense_image f.continuous hs
283
284section SMul
285
286variable {S₂ T₂ : Type*}
287variable [DistribSMul S₂ M₂] [SMulCommClass R₂ S₂ M₂] [ContinuousConstSMul S₂ M₂]
288variable [DistribSMul T₂ M₂] [SMulCommClass R₂ T₂ M₂] [ContinuousConstSMul T₂ M₂]
289
290instance instSMul : SMul S₂ (M₁ →SL[σ₁₂] M₂) where
291 smul c f := ⟨c • (f : M₁ →ₛₗ[σ₁₂] M₂), (f.2.const_smul _ : Continuous fun x => c • f x)⟩
292
293instance : IsSMulApply S₂ (M₁ →SL[σ₁₂] M₂) M₁ M₂ where
294 smul_apply _ _ _ := rfl
295
296@[simp, norm_cast]
297theorem toLinearMap_smul (c : S₂) (f : M₁ →SL[σ₁₂] M₂) :
298 ↑(c • f) = c • (f : M₁ →ₛₗ[σ₁₂] M₂) :=
299 rfl
300
301@[deprecated (since := "2026-05-20")] protected alias smul_apply := _root_.smul_apply
302
303@[deprecated (since := "2026-05-20")] protected alias coe_smul := toLinearMap_smul
304
305@[deprecated (since := "2026-05-20")] alias coe_smul' := FunLike.coe_smul
306
307instance isScalarTower [SMul S₂ T₂] [IsScalarTower S₂ T₂ M₂] :
308 IsScalarTower S₂ T₂ (M₁ →SL[σ₁₂] M₂) := FunLike.isScalarTower
309
310instance smulCommClass [SMulCommClass S₂ T₂ M₂] : SMulCommClass S₂ T₂ (M₁ →SL[σ₁₂] M₂) :=
311 FunLike.smulCommClass
312
313end SMul
314
315section SMulMonoid
316
317variable {S₂ : Type*} [Monoid S₂]
318variable [DistribMulAction S₂ M₂] [SMulCommClass R₂ S₂ M₂] [ContinuousConstSMul S₂ M₂]
319
320instance mulAction : MulAction S₂ (M₁ →SL[σ₁₂] M₂) := fast_instance% FunLike.mulAction
321
322end SMulMonoid
323
324/-- The continuous map that is constantly zero. -/
325instance zero : Zero (M₁ →SL[σ₁₂] M₂) :=
326 ⟨⟨0, continuous_zero⟩⟩
327
328instance : IsZeroApply (M₁ →SL[σ₁₂] M₂) M₁ M₂ where
329 zero_apply _ := rfl
330
331instance inhabited : Inhabited (M₁ →SL[σ₁₂] M₂) :=
332 ⟨0⟩
333
334@[simp]
335theorem default_def : (default : M₁ →SL[σ₁₂] M₂) = 0 :=
336 rfl
337
338@[simp, norm_cast]
339theorem toLinearMap_zero : ((0 : M₁ →SL[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂) = 0 :=
340 rfl
341
342@[deprecated (since := "2026-05-20")] protected alias zero_apply := _root_.zero_apply
343
344@[deprecated (since := "2026-05-20")] protected alias coe_zero := toLinearMap_zero
345
346@[deprecated (since := "2026-05-20")] alias coe_zero' := FunLike.coe_zero
347
348@[simp, norm_cast]
349theorem toContinuousAddMonoidHom_zero :
350 ((0 : M₁ →SL[σ₁₂] M₂) : ContinuousAddMonoidHom M₁ M₂) = 0 := rfl
351
352instance uniqueOfLeft [Subsingleton M₁] : Unique (M₁ →SL[σ₁₂] M₂) :=
353 coe_injective.unique
354
355instance uniqueOfRight [Subsingleton M₂] : Unique (M₁ →SL[σ₁₂] M₂) :=
356 coe_injective.unique
357
358theorem exists_ne_zero {f : M₁ →SL[σ₁₂] M₂} (hf : f ≠ 0) : ∃ x, f x ≠ 0 := by
359 by_contra! h
360 exact hf (ContinuousLinearMap.ext h)
361
362section
363
364variable (R₁ M₁)
365
366/-- the identity map as a continuous linear map. -/
367protected def id : M₁ →L[R₁] M₁ :=
368 ⟨LinearMap.id, continuous_id⟩
369
370end
371
372instance one : One (M₁ →L[R₁] M₁) :=
373 ⟨.id R₁ M₁⟩
374
375theorem one_def : (1 : M₁ →L[R₁] M₁) = .id R₁ M₁ := rfl
376
377instance instIsOneApply : IsOneApplyEqSelf (M₁ →L[R₁] M₁) M₁ where
378 one_apply_eq_self _ := rfl
379
380@[simp]
381theorem id_apply (x : M₁) : ContinuousLinearMap.id R₁ M₁ x = x := rfl
382
383@[simp, norm_cast]
384theorem coe_id : (ContinuousLinearMap.id R₁ M₁ : M₁ →ₗ[R₁] M₁) = LinearMap.id :=
385 rfl
386
387@[simp, norm_cast]
388theorem coe_id' : ⇑(ContinuousLinearMap.id R₁ M₁) = id :=
389 rfl
390
391@[simp, norm_cast]
392theorem toLinearMap_one : ((1 : M₁ →L[R₁] M₁) : M₁ →ₗ[R₁] M₁) = 1 :=
393 rfl
394
395@[deprecated (since := "2026-05-20")] protected alias coe_one := toLinearMap_one
396
397@[simp] lemma mk_id : mk (.id : M₁ →ₗ[R₁] M₁) continuous_id = .id _ _ := rfl
398@[simp] lemma mk_one : mk (1 : M₁ →ₗ[R₁] M₁) continuous_id = 1 := rfl
399
400@[simp, norm_cast]
401theorem toContinuousAddMonoidHom_id :
402 (ContinuousLinearMap.id R₁ M₁ : ContinuousAddMonoidHom M₁ M₁) = .id _ := rfl
403
404@[simp, norm_cast]
405theorem coe_eq_id {f : M₁ →L[R₁] M₁} : (f : M₁ →ₗ[R₁] M₁) = LinearMap.id ↔ f = .id _ _ := by
406 rw [← coe_id, coe_inj]
407
408@[deprecated (since := "2026-05-20")] protected alias one_apply := one_apply_eq_self
409
410instance [Nontrivial M₁] : Nontrivial (M₁ →L[R₁] M₁) :=
411 ⟨0, 1, fun e ↦
412 have ⟨x, hx⟩ := exists_ne (0 : M₁); hx (by simpa using DFunLike.congr_fun e.symm x)⟩
413
414section Add
415
416variable [ContinuousAdd M₂]
417
418instance add : Add (M₁ →SL[σ₁₂] M₂) :=
419 ⟨fun f g => ⟨f + g, f.2.add g.2⟩⟩
420
421instance instIsAddApply : IsAddApply (M₁ →SL[σ₁₂] M₂) M₁ M₂ where
422 add_apply _ _ _ := rfl
423
424@[simp, norm_cast]
425theorem toLinearMap_add (f g : M₁ →SL[σ₁₂] M₂) : (↑(f + g) : M₁ →ₛₗ[σ₁₂] M₂) = f + g :=
426 rfl
427
428@[deprecated (since := "2026-05-20")] protected alias add_apply := _root_.add_apply
429
430@[deprecated (since := "2026-05-20")] protected alias coe_add := toLinearMap_add
431
432@[deprecated (since := "2026-05-20")] alias coe_add' := FunLike.coe_add
433
434@[simp, norm_cast]
435theorem toContinuousAddMonoidHom_add (f g : M₁ →SL[σ₁₂] M₂) :
436 ↑(f + g) = (f + g : ContinuousAddMonoidHom M₁ M₂) := rfl
437
438-- The `AddMonoid` instance exists to help speedup unification
439instance : AddMonoid (M₁ →SL[σ₁₂] M₂) := fast_instance% FunLike.addMonoid
440
441instance addCommMonoid : AddCommMonoid (M₁ →SL[σ₁₂] M₂) := fast_instance% FunLike.addCommMonoid
442
443@[simp, norm_cast]
444theorem toLinearMap_sum {ι : Type*} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) :
445 ↑(∑ d ∈ t, f d) = (∑ d ∈ t, f d : M₁ →ₛₗ[σ₁₂] M₂) :=
446 map_sum (AddMonoidHom.mk ⟨((↑) : (M₁ →SL[σ₁₂] M₂) → M₁ →ₛₗ[σ₁₂] M₂), rfl⟩ fun _ _ => rfl) _ _
447
448@[deprecated (since := "2026-05-20")] protected alias sum_apply := _root_.sum_apply
449
450@[deprecated (since := "2026-05-20")] protected alias coe_sum := toLinearMap_sum
451
452@[deprecated (since := "2026-05-20")] alias coe_sum' := FunLike.coe_sum
453
454end Add
455
456variable [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
457
458/-- Composition of continuous linear maps. -/
459def comp (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) : M₁ →SL[σ₁₃] M₃ :=
460 ⟨(g : M₂ →ₛₗ[σ₂₃] M₃).comp (f : M₁ →ₛₗ[σ₁₂] M₂), g.2.comp f.2⟩
461
462@[inherit_doc comp]
463infixr:80 " ∘L " =>
464 @ContinuousLinearMap.comp _ _ _ _ _ _ (RingHom.id _) (RingHom.id _) (RingHom.id _) _ _ _ _ _ _ _ _
465 _ _ _ _ RingHomCompTriple.ids
466
467@[inherit_doc comp]
468infixr:90 " ∘SL " =>
469 ContinuousLinearMap.comp
470
471@[simp, norm_cast]
472theorem toLinearMap_comp (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
473 (h ∘SL f : M₁ →ₛₗ[σ₁₃] M₃) = (h : M₂ →ₛₗ[σ₂₃] M₃) ∘ₛₗ (f : M₁ →ₛₗ[σ₁₂] M₂) :=
474 rfl
475
476@[norm_cast]
477theorem coe_comp (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) : ⇑(h ∘SL f) = h ∘ f :=
478 rfl
479
480@[deprecated (since := "2026-05-20")] alias coe_comp' := coe_comp
481
482@[simp, norm_cast]
483theorem toContinuousAddMonoidHom_comp (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
484 (↑(h ∘SL f) : ContinuousAddMonoidHom M₁ M₃) = (h : ContinuousAddMonoidHom M₂ M₃).comp f := rfl
485
486@[simp, grind =]
487theorem comp_apply (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) (x : M₁) : (g ∘SL f) x = g (f x) :=
488 rfl
489
490@[simp]
491theorem comp_id (f : M₁ →SL[σ₁₂] M₂) : f ∘SL .id R₁ M₁ = f :=
492 ext fun _x => rfl
493
494@[simp]
495theorem id_comp (f : M₁ →SL[σ₁₂] M₂) : .id R₂ M₂ ∘SL f = f :=
496 ext fun _x => rfl
497
498section
499
500variable {R E F : Type*} [Semiring R]
501 [TopologicalSpace E] [AddCommMonoid E] [Module R E]
502 [TopologicalSpace F] [AddCommMonoid F] [Module R F]
503
504/-- `g ∘ f = id` as `ContinuousLinearMap`s implies `g ∘ f = id` as functions. -/
505lemma leftInverse_of_comp {f : E →L[R] F} {g : F →L[R] E}
506 (hinv : g ∘L f = .id R E) : Function.LeftInverse g f := by
507 simpa [coe_comp, ← Function.leftInverse_iff_comp] using congr(⇑$hinv)
508
509/-- `f ∘ g = id` as `ContinuousLinearMap`s implies `f ∘ g = id` as functions. -/
510lemma rightInverse_of_comp {f : E →L[R] F} {g : F →L[R] E}
511 (hinv : f ∘L g = .id R F) : Function.RightInverse g f :=
512 leftInverse_of_comp hinv
513
514end
515
516@[simp]
517theorem comp_zero (g : M₂ →SL[σ₂₃] M₃) : g ∘SL (0 : M₁ →SL[σ₁₂] M₂) = 0 := by
518 ext
519 simp
520
521@[simp]
522theorem zero_comp (f : M₁ →SL[σ₁₂] M₂) : (0 : M₂ →SL[σ₂₃] M₃) ∘SL f = 0 := by
523 ext
524 simp
525
526@[simp]
527theorem comp_add [ContinuousAdd M₂] [ContinuousAdd M₃] (g : M₂ →SL[σ₂₃] M₃)
528 (f₁ f₂ : M₁ →SL[σ₁₂] M₂) : g ∘SL (f₁ + f₂) = g ∘SL f₁ + g ∘SL f₂ := by
529 ext
530 simp
531
532@[simp]
533theorem add_comp [ContinuousAdd M₃] (g₁ g₂ : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
534 (g₁ + g₂) ∘SL f = g₁ ∘SL f + g₂ ∘SL f := by
535 ext
536 simp
537
538theorem comp_finsetSum {ι : Type*} {s : Finset ι}
539 [ContinuousAdd M₂] [ContinuousAdd M₃] (g : M₂ →SL[σ₂₃] M₃)
540 (f : ι → M₁ →SL[σ₁₂] M₂) : g ∘SL (∑ i ∈ s, f i) = ∑ i ∈ s, g ∘SL (f i) := by
541 ext
542 simp
543
544@[deprecated (since := "2026-04-08")] alias comp_finset_sum := comp_finsetSum
545
546theorem finsetSum_comp {ι : Type*} {s : Finset ι}
547 [ContinuousAdd M₃] (g : ι → M₂ →SL[σ₂₃] M₃)
548 (f : M₁ →SL[σ₁₂] M₂) : (∑ i ∈ s, g i) ∘SL f = ∑ i ∈ s, (g i) ∘SL f := by
549 ext
550 simp only [comp_apply, sum_apply]
551
552@[deprecated (since := "2026-04-08")] alias finset_sum_comp := finsetSum_comp
553
554theorem comp_assoc {R₄ : Type*} [Semiring R₄] [Module R₄ M₄] {σ₁₄ : R₁ →+* R₄} {σ₂₄ : R₂ →+* R₄}
555 {σ₃₄ : R₃ →+* R₄} [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄]
556 [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (h : M₃ →SL[σ₃₄] M₄) (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
557 (h ∘SL g) ∘SL f = h ∘SL (g ∘SL f) :=
558 rfl
559
560theorem cancel_left {g : M₂ →SL[σ₂₃] M₃} {f₁ f₂ : M₁ →SL[σ₁₂] M₂} (hg : Function.Injective g)
561 (h : g ∘SL f₁ = g ∘SL f₂) : f₁ = f₂ := by
562 ext x
563 exact hg congr($h x)
564
565lemma cancel_left' {g : M₂ →SL[σ₂₃] M₃} {f₁ f₂ : M₁ →SL[σ₁₂] M₂} (hg : Function.Injective g) :
566 g ∘SL f₁ = g ∘SL f₂ ↔ f₁ = f₂ :=
567 ⟨cancel_left hg, congr_arg (fun f => g ∘SL f)⟩
568
569instance instMul : Mul (M₁ →L[R₁] M₁) :=
570 ⟨comp⟩
571
572instance : IsMulApplyEqComp (M₁ →L[R₁] M₁) M₁ where
573 mul_apply_eq_comp _ _ _ := rfl
574
575theorem mul_def (f g : M₁ →L[R₁] M₁) : f * g = f ∘L g :=
576 rfl
577
578@[simp, norm_cast]
579theorem toLinearMap_mul (f g : M₁ →L[R₁] M₁) : (↑(f * g) : M₁ →ₗ[R₁] M₁) = f * g :=
580 rfl
581
582@[deprecated (since := "2026-05-20")] alias coe_mul := toLinearMap_mul
583
584@[deprecated (since := "2026-05-20")] protected alias coe_mul' := FunLike.coe_mul
585
586@[deprecated (since := "2026-05-20")] protected alias mul_apply := mul_apply_eq_comp
587
588instance monoidWithZero : MonoidWithZero (M₁ →L[R₁] M₁) :=
589 fast_instance% FunLike.monoidWithZero
590
591@[deprecated (since := "2026-07-23")] alias coe_pow' := FunLike.coe_pow_eq_iterate
592
593@[simp, norm_cast]
594theorem toLinearMap_pow (f : M₁ →L[R₁] M₁) (n : ℕ) : (↑(f ^ n) : M₁ →ₗ[R₁] M₁) = f ^ n :=
595 DFunLike.ext' <| (FunLike.coe_pow_eq_iterate f n).trans
596 <| .symm <| hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _
597
598@[deprecated (since := "2026-07-24")] protected alias coe_pow := toLinearMap_pow
599
600instance instNatCast [ContinuousAdd M₁] : NatCast (M₁ →L[R₁] M₁) where
601 natCast n := n • (1 : M₁ →L[R₁] M₁)
602
603instance instIsNatCastApply [ContinuousAdd M₁] : IsNatCastApply (M₁ →L[R₁] M₁) M₁ where
604 natCast_apply _ _ := rfl
605
606instance semiring [ContinuousAdd M₁] : Semiring (M₁ →L[R₁] M₁) :=
607 fast_instance% FunLike.semiring
608
609/-- `ContinuousLinearMap.toLinearMap` as a `RingHom`. -/
610@[simps]
611def toLinearMapRingHom [ContinuousAdd M₁] : (M₁ →L[R₁] M₁) →+* M₁ →ₗ[R₁] M₁ where
612 toFun := toLinearMap
613 map_zero' := rfl
614 map_one' := rfl
615 map_add' _ _ := rfl
616 map_mul' _ _ := rfl
617
618@[simp]
619theorem natCast_apply [ContinuousAdd M₁] (n : ℕ) (m : M₁) : (↑n : M₁ →L[R₁] M₁) m = n • m :=
620 rfl
621
622@[simp]
623theorem ofNat_apply [ContinuousAdd M₁] (n : ℕ) [n.AtLeastTwo] (m : M₁) :
624 (ofNat(n) : M₁ →L[R₁] M₁) m = OfNat.ofNat n • m :=
625 rfl
626
627/-- Construct a homeomorphism from an invertible continuous linear map. -/
628@[simps]
629def homeomorphOfUnit (T : (M₁ →L[R₁] M₁)ˣ) : M₁ ≃ₜ M₁ where
630 toFun := T.1
631 invFun := T⁻¹.1
632 left_inv x := by rw [← mul_apply_eq_comp, Units.inv_mul, one_apply_eq_self]
633 right_inv x := by rw [← mul_apply_eq_comp, Units.mul_inv, one_apply_eq_self]
634
635theorem isHomeomorph_of_isUnit {T : M₁ →L[R₁] M₁} (hT : IsUnit T) : IsHomeomorph T := by
636 obtain ⟨T, rfl⟩ := hT
637 exact (homeomorphOfUnit T).isHomeomorph
638
639section ApplyAction
640
641variable [ContinuousAdd M₁]
642
643/-- The tautological action by `M₁ →L[R₁] M₁` on `M`.
644
645This generalizes `Function.End.applyMulAction`. -/
646instance applyModule : Module (M₁ →L[R₁] M₁) M₁ :=
647 Module.compHom _ toLinearMapRingHom
648
649@[simp]
650protected theorem smul_def (f : M₁ →L[R₁] M₁) (a : M₁) : f • a = f a :=
651 rfl
652
653/-- `ContinuousLinearMap.applyModule` is faithful. -/
654instance applyFaithfulSMul : FaithfulSMul (M₁ →L[R₁] M₁) M₁ :=
655 ⟨fun {_ _} => ContinuousLinearMap.ext⟩
656
657instance applySMulCommClass : SMulCommClass R₁ (M₁ →L[R₁] M₁) M₁ where
658 smul_comm r e m := (e.map_smul r m).symm
659
660instance applySMulCommClass' : SMulCommClass (M₁ →L[R₁] M₁) R₁ M₁ where
661 smul_comm := map_smul
662
663instance continuousConstSMul_apply : ContinuousConstSMul (M₁ →L[R₁] M₁) M₁ :=
664 ⟨ContinuousLinearMap.continuous⟩
665
666end ApplyAction
667
668theorem isClosed_ker [T1Space M₂] (f : M₁ →SL[σ₁₂] M₂) :
669 IsClosed (f.ker : Set M₁) :=
670 isClosed_singleton.preimage f.continuous
671
672theorem isClosed_eqLocus [T2Space M₂] (f g : M₁ →SL[σ₁₂] M₂) :
673 IsClosed (f.eqLocus g : Set M₁) :=
674 isClosed_eq f.continuous g.continuous
675
676theorem isComplete_ker {M' : Type*} [UniformSpace M'] [CompleteSpace M'] [AddCommMonoid M']
677 [Module R₁ M'] [T1Space M₂] (f : M' →SL[σ₁₂] M₂) :
678 IsComplete (f.ker : Set M') :=
679 (isClosed_ker f).isComplete
680
681theorem isComplete_eqLocus {M' : Type*} [UniformSpace M'] [CompleteSpace M'] [AddCommMonoid M']
682 [Module R₁ M'] [T2Space M₂] (f g : M' →SL[σ₁₂] M₂) :
683 IsComplete (f.eqLocus g : Set M') :=
684 (isClosed_eqLocus f g).isComplete
685
686instance completeSpace_ker {M' : Type*} [UniformSpace M'] [CompleteSpace M']
687 [AddCommMonoid M'] [Module R₁ M'] [T1Space M₂]
688 (f : M' →SL[σ₁₂] M₂) : CompleteSpace f.ker :=
689 (isComplete_ker f).completeSpace_coe
690
691instance completeSpace_eqLocus {M' : Type*} [UniformSpace M'] [CompleteSpace M']
692 [AddCommMonoid M'] [Module R₁ M'] [T2Space M₂]
693 (f g : M' →SL[σ₁₂] M₂) : CompleteSpace (f.toLinearMap.eqLocus g.toLinearMap) :=
694 (isComplete_eqLocus f g).completeSpace_coe
695
696section
697
698variable {R S : Type*} [Semiring R] [Semiring S] [Module R M₁] [Module R M₂] [Module R S]
699 [Module S M₂] [IsScalarTower R S M₂] [TopologicalSpace S] [ContinuousSMul S M₂]
700
701/-- The linear map `fun x => c x • f`. Associates to a scalar-valued linear map and an element of
702`M₂` the `M₂`-valued linear map obtained by multiplying the two (a.k.a. tensoring by `M₂`).
703See also `ContinuousLinearMap.smulRightₗ` and `ContinuousLinearMap.smulRightL`. -/
704@[simps coe]
705def smulRight (c : M₁ →L[R] S) (f : M₂) : M₁ →L[R] M₂ where
706 toLinearMap := c.toLinearMap.smulRight f
707
708@[simp]
709theorem smulRight_apply {c : M₁ →L[R] S} {f : M₂} {x : M₁} :
710 (smulRight c f : M₁ → M₂) x = c x • f :=
711 rfl
712
713@[simp]
714lemma smulRight_zero (f : M₁ →L[R] S) : f.smulRight (0 : M₂) = 0 := by ext; simp
715
716@[simp]
717theorem zero_smulRight {x : M₂} : (0 : M₁ →L[R] S).smulRight x = 0 := by ext; simp
718
719end
720
721variable [Module R₁ M₂] [TopologicalSpace R₁] [ContinuousSMul R₁ M₂]
722
723theorem smulRight_comp_smulRight {M₃ : Type*} [AddCommMonoid M₃] [Module R₁ M₃]
724 [TopologicalSpace M₃] [ContinuousSMul R₁ M₃] (f : M₃ →L[R₁] R₁) (g : M₁ →L[R₁] R₁) {x : M₂}
725 {y : M₃} : (smulRight f x) ∘L (smulRight g y) = smulRight g (f y • x) := by
726 ext
727 simp
728
729theorem range_smulRight_apply {R : Type*} [DivisionSemiring R] [Module R M₁] [Module R M₂]
730 [TopologicalSpace R] [ContinuousSMul R M₂] {f : M₁ →L[R] R} (hf : f ≠ 0) (x : M₂) :
731 range (f.smulRight x : M₁ →ₗ[R] M₂) = Submodule.span R {x} :=
732 LinearMap.range_smulRight_apply (by simpa [coe_inj, ← toLinearMap_zero] using hf) x
733
734section ToSpanSingleton
735
736variable (R₁)
737variable [ContinuousSMul R₁ M₁]
738
739set_option backward.defeqAttrib.useBackward true in
740/-- Given an element `x` of a topological space `M` over a semiring `R`, the natural continuous
741linear map from `R` to `M` by taking multiples of `x`. -/
742def toSpanSingleton (x : M₁) : R₁ →L[R₁] M₁ where
743 toLinearMap := LinearMap.toSpanSingleton R₁ M₁ x
744
745@[simp]
746theorem toSpanSingleton_apply (x : M₁) (r : R₁) : toSpanSingleton R₁ x r = r • x :=
747 rfl
748
749@[simp]
750theorem toSpanSingleton_zero : toSpanSingleton R₁ (0 : M₁) = 0 := by ext; simp
751
752theorem toSpanSingleton_apply_one (x : M₁) : toSpanSingleton R₁ x 1 = x :=
753 one_smul _ _
754
755@[simp] theorem toSpanSingleton_apply_map_one (c : R₁ →L[R₁] M₂) :
756 toSpanSingleton R₁ (c 1) = c := by
757 ext
758 simp [← ContinuousLinearMap.map_smul_of_tower]
759
760theorem toSpanSingleton_add [ContinuousAdd M₁] (x y : M₁) :
761 toSpanSingleton R₁ (x + y) = toSpanSingleton R₁ x + toSpanSingleton R₁ y :=
762 coe_inj.mp <| LinearMap.toSpanSingleton_add _ _
763
764theorem toSpanSingleton_smul {α} [Monoid α] [DistribMulAction α M₁] [ContinuousConstSMul α M₁]
765 [SMulCommClass R₁ α M₁] (c : α) (x : M₁) :
766 toSpanSingleton R₁ (c • x) = c • toSpanSingleton R₁ x :=
767 coe_inj.mp <| LinearMap.toSpanSingleton_smul _ _
768
769theorem smulRight_id : smulRight (.id R₁ R₁) = toSpanSingleton R₁ (M₁ := M₁) := rfl
770
771theorem smulRight_one_eq_toSpanSingleton (x : M₁) :
772 (1 : R₁ →L[R₁] R₁).smulRight x = toSpanSingleton R₁ x :=
773 rfl
774
775@[simp]
776theorem toLinearMap_toSpanSingleton (x : M₁) :
777 (toSpanSingleton R₁ x).toLinearMap = LinearMap.toSpanSingleton R₁ M₁ x := rfl
778
779variable {R₁}
780
781theorem comp_toSpanSingleton (f : M₁ →L[R₁] M₂) (x : M₁) :
782 f ∘L toSpanSingleton R₁ x = toSpanSingleton R₁ (f x) :=
783 coe_inj.mp <| LinearMap.comp_toSpanSingleton _ _
784
785omit [ContinuousSMul R₁ M₁] in
786theorem toSpanSingleton_comp (f : M₁ →L[R₁] R₁) (g : M₂) :
787 toSpanSingleton R₁ g ∘L f = f.smulRight g := rfl
788
789@[simp] theorem toSpanSingleton_inj {f f' : M₂} :
790 toSpanSingleton R₁ f = toSpanSingleton R₁ f' ↔ f = f' := by
791 simp [ContinuousLinearMap.ext_ring_iff]
792
793theorem toSpanSingleton_comp_toSpanSingleton [ContinuousMul R₁] {x : M₂} {c : R₁} :
794 (toSpanSingleton R₁ x) ∘L (toSpanSingleton R₁ c) =
795 toSpanSingleton R₁ (c • x) := smulRight_comp_smulRight 1 1
796
797end ToSpanSingleton
798
799end Semiring
800
801section Ring
802
803variable {R : Type*} [Ring R] {R₂ : Type*} [Ring R₂] {R₃ : Type*} [Ring R₃] {M : Type*}
804 [TopologicalSpace M] [AddCommGroup M] {M₂ : Type*} [TopologicalSpace M₂] [AddCommGroup M₂]
805 {M₃ : Type*} [TopologicalSpace M₃] [AddCommGroup M₃] {M₄ : Type*} [TopologicalSpace M₄]
806 [AddCommGroup M₄] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃}
807 {σ₁₃ : R →+* R₃}
808
809section
810
811protected theorem map_neg (f : M →SL[σ₁₂] M₂) (x : M) : f (-x) = -f x := by
812 exact map_neg f x
813
814protected theorem map_sub (f : M →SL[σ₁₂] M₂) (x y : M) : f (x - y) = f x - f y := by
815 exact map_sub f x y
816
817@[simp]
818theorem sub_apply' (f g : M →SL[σ₁₂] M₂) (x : M) : ((f : M →ₛₗ[σ₁₂] M₂) - g) x = f x - g x :=
819 rfl
820
821end
822
823section
824
825variable [IsTopologicalAddGroup M₂]
826
827instance neg : Neg (M →SL[σ₁₂] M₂) :=
828 ⟨fun f => ⟨-f, f.2.neg⟩⟩
829
830instance : IsNegApply (M →SL[σ₁₂] M₂) M M₂ where
831 neg_apply _ _ := rfl
832
833@[simp, norm_cast]
834theorem toLinearMap_neg (f : M →SL[σ₁₂] M₂) : (↑(-f) : M →ₛₗ[σ₁₂] M₂) = -f :=
835 rfl
836
837@[deprecated (since := "2026-05-20")] protected alias neg_apply := _root_.neg_apply
838
839@[deprecated (since := "2026-05-20")] protected alias coe_neg := toLinearMap_neg
840
841@[deprecated (since := "2026-05-20")] alias coe_neg' := FunLike.coe_neg
842
843@[simp, norm_cast]
844theorem toContinuousAddMonoidHom_neg (f : M →SL[σ₁₂] M₂) :
845 ↑(-f) = -(f : ContinuousAddMonoidHom M M₂) := rfl
846
847instance sub : Sub (M →SL[σ₁₂] M₂) :=
848 ⟨fun f g => ⟨f - g, f.2.sub g.2⟩⟩
849
850instance : IsSubApply (M →SL[σ₁₂] M₂) M M₂ where
851 sub_apply _ _ _ := rfl
852
853instance addCommGroup : AddCommGroup (M →SL[σ₁₂] M₂) := fast_instance% FunLike.addCommGroup
854
855@[simp, norm_cast]
856theorem toLinearMap_sub (f g : M →SL[σ₁₂] M₂) : (↑(f - g) : M →ₛₗ[σ₁₂] M₂) = f - g :=
857 rfl
858
859@[deprecated (since := "2026-05-20")] protected alias sub_apply := _root_.sub_apply
860
861@[deprecated (since := "2026-05-20")] protected alias coe_sub := toLinearMap_sub
862
863@[deprecated (since := "2026-05-20")] alias coe_sub' := FunLike.coe_sub
864
865@[simp, norm_cast]
866theorem toContinuousAddMonoidHom_sub (f g : M →SL[σ₁₂] M₂) :
867 ↑(f - g) = (f - g : ContinuousAddMonoidHom M M₂) := rfl
868
869end
870
871@[simp]
872theorem comp_neg [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [IsTopologicalAddGroup M₂]
873 [IsTopologicalAddGroup M₃] (g : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) :
874 g ∘SL (-f) = -g ∘SL f := by
875 ext x
876 simp
877
878@[simp]
879theorem neg_comp [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [IsTopologicalAddGroup M₃] (g : M₂ →SL[σ₂₃] M₃)
880 (f : M →SL[σ₁₂] M₂) : (-g) ∘SL f = -g ∘SL f := by
881 ext
882 simp
883
884@[simp]
885theorem comp_sub [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [IsTopologicalAddGroup M₂]
886 [IsTopologicalAddGroup M₃] (g : M₂ →SL[σ₂₃] M₃) (f₁ f₂ : M →SL[σ₁₂] M₂) :
887 g ∘SL (f₁ - f₂) = g ∘SL f₁ - g ∘SL f₂ := by
888 ext
889 simp
890
891@[simp]
892theorem sub_comp [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [IsTopologicalAddGroup M₃] (g₁ g₂ : M₂ →SL[σ₂₃] M₃)
893 (f : M →SL[σ₁₂] M₂) : (g₁ - g₂) ∘SL f = g₁ ∘SL f - g₂ ∘SL f := by
894 ext
895 simp
896
897instance [IsTopologicalAddGroup M] : IntCast (M →L[R] M) where
898 intCast z := z • (1 : M →L[R] M)
899
900instance instIsIntCastApply [IsTopologicalAddGroup M] : IsIntCastApply (M →L[R] M) M where
901 intCast_apply _ _ := rfl
902
903@[deprecated (since := "2026-05-20")] alias intCast_apply := _root_.intCast_apply
904
905instance ring [IsTopologicalAddGroup M] : Ring (M →L[R] M) := fast_instance% FunLike.ring
906
907theorem toSpanSingleton_pow [TopologicalSpace R] [IsTopologicalRing R] (c : R) (n : ℕ) :
908 toSpanSingleton R c ^ n = toSpanSingleton R (c ^ n) := by
909 induction n with
910 | zero => ext; simp
911 | succ n ihn =>
912 rw [pow_succ, ihn, mul_def, toSpanSingleton_comp_toSpanSingleton, smul_eq_mul, pow_succ']
913
914end Ring
915
916section DivisionRing
917
918variable {R M : Type*}
919
920/-- A nonzero continuous linear functional is open. -/
921protected theorem isOpenMap_of_ne_zero [TopologicalSpace R] [DivisionRing R] [ContinuousSub R]
922 [AddCommGroup M] [TopologicalSpace M] [ContinuousAdd M] [Module R M] [ContinuousSMul R M]
923 (f : StrongDual R M) (hf : f ≠ 0) : IsOpenMap f :=
924 let ⟨x, hx⟩ := exists_ne_zero hf
925 IsOpenMap.of_sections fun y =>
926 ⟨fun a => y + (a - f y) • (f x)⁻¹ • x, Continuous.continuousAt <| by fun_prop, by simp,
927 fun a => by simp [hx]⟩
928
929end DivisionRing
930
931section SMulMonoid
932
933-- The M's are used for semilinear maps, and the N's for plain linear maps
934variable {R R₂ R₃ S S₃ : Type*} [Semiring R] [Semiring R₂] [Semiring R₃] [Monoid S] [Monoid S₃]
935 {M : Type*} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {M₂ : Type*}
936 [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] {M₃ : Type*} [TopologicalSpace M₃]
937 [AddCommMonoid M₃] [Module R₃ M₃] {N₂ : Type*} [TopologicalSpace N₂] [AddCommMonoid N₂]
938 [Module R N₂] {N₃ : Type*} [TopologicalSpace N₃] [AddCommMonoid N₃] [Module R N₃]
939 [DistribMulAction S₃ M₃] [SMulCommClass R₃ S₃ M₃] [ContinuousConstSMul S₃ M₃]
940 [DistribMulAction S N₃] [SMulCommClass R S N₃] [ContinuousConstSMul S N₃] {σ₁₂ : R →+* R₂}
941 {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
942
943@[simp]
944theorem smul_comp (c : S₃) (h : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) :
945 (c • h) ∘SL f = c • h ∘SL f :=
946 rfl
947
948variable [DistribMulAction S₃ M₂] [ContinuousConstSMul S₃ M₂] [SMulCommClass R₂ S₃ M₂]
949variable [DistribMulAction S N₂] [ContinuousConstSMul S N₂] [SMulCommClass R S N₂]
950
951@[simp]
952theorem comp_smul [LinearMap.CompatibleSMul N₂ N₃ S R] (hₗ : N₂ →L[R] N₃) (c : S)
953 (fₗ : M →L[R] N₂) : hₗ ∘L (c • fₗ) = c • hₗ ∘L fₗ := by
954 ext x
955 exact hₗ.map_smul_of_tower c (fₗ x)
956
957@[simp]
958theorem comp_smulₛₗ [SMulCommClass R₂ R₂ M₂] [SMulCommClass R₃ R₃ M₃] [ContinuousConstSMul R₂ M₂]
959 [ContinuousConstSMul R₃ M₃] (h : M₂ →SL[σ₂₃] M₃) (c : R₂) (f : M →SL[σ₁₂] M₂) :
960 h ∘SL (c • f) = σ₂₃ c • h ∘SL f := by
961 ext x
962 simp
963
964instance distribMulAction [ContinuousAdd M₂] : DistribMulAction S₃ (M →SL[σ₁₂] M₂) :=
965 fast_instance% FunLike.distribMulAction
966
967end SMulMonoid
968
969section SMul
970
971-- The M's are used for semilinear maps, and the N's for plain linear maps
972variable {R R₂ R₃ S S₃ : Type*} [Semiring R] [Semiring R₂] [Semiring R₃] [Semiring S] [Semiring S₃]
973 {M : Type*} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {M₂ : Type*}
974 [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] {M₃ : Type*} [TopologicalSpace M₃]
975 [AddCommMonoid M₃] [Module R₃ M₃] {N₂ : Type*} [TopologicalSpace N₂] [AddCommMonoid N₂]
976 [Module R N₂] {N₃ : Type*} [TopologicalSpace N₃] [AddCommMonoid N₃] [Module R N₃] [Module S₃ M₃]
977 [SMulCommClass R₃ S₃ M₃] [ContinuousConstSMul S₃ M₃] [Module S N₂] [ContinuousConstSMul S N₂]
978 [SMulCommClass R S N₂] [Module S N₃] [SMulCommClass R S N₃] [ContinuousConstSMul S N₃]
979 {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (c : S)
980 (h : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂)
981
982variable [ContinuousAdd M₂] [ContinuousAdd M₃] [ContinuousAdd N₂]
983
984instance module : Module S₃ (M →SL[σ₁₃] M₃) := fast_instance% FunLike.module
985
986instance isCentralScalar [Module S₃ᵐᵒᵖ M₃] [IsCentralScalar S₃ M₃] :
987 IsCentralScalar S₃ (M →SL[σ₁₃] M₃) := FunLike.isCentralScalar
988
989variable (S) [ContinuousAdd N₃]
990
991/-- The coercion from `M →L[R] M₂` to `M →ₗ[R] M₂`, as a linear map. -/
992@[simps]
993def coeLM : (M →L[R] N₃) →ₗ[S] M →ₗ[R] N₃ where
994 toFun := (↑)
995 map_add' f g := toLinearMap_add f g
996 map_smul' c f := toLinearMap_smul c f
997
998variable {S} (σ₁₃)
999
1000/-- The coercion from `M →SL[σ] M₂` to `M →ₛₗ[σ] M₂`, as a linear map. -/
1001@[simps]
1002def coeLMₛₗ : (M →SL[σ₁₃] M₃) →ₗ[S₃] M →ₛₗ[σ₁₃] M₃ where
1003 toFun := (↑)
1004 map_add' f g := toLinearMap_add f g
1005 map_smul' c f := toLinearMap_smul c f
1006
1007end SMul
1008
1009section lcomp
1010
1011variable {R U V : Type*} (W : Type*) [CommSemiring R]
1012 [AddCommMonoid U] [Module R U] [TopologicalSpace U]
1013 [AddCommMonoid V] [Module R V] [TopologicalSpace V]
1014 [AddCommMonoid W] [Module R W] [TopologicalSpace W]
1015 [ContinuousAdd W] [ContinuousConstSMul R W]
1016
1017/-- Composition of continuous linear maps, as a linear map. Compare `LinearMap.lcomp`. -/
1018@[simps]
1019def lcomp (f : U →L[R] V) : (V →L[R] W) →ₗ[R] (U →L[R] W) where
1020 toFun l := l ∘L f
1021 map_add' _ _ := by simp
1022 map_smul' _ _ := by simp
1023
1024end lcomp
1025
1026section llcomp
1027
1028variable (R U V W : Type*) [CommSemiring R]
1029 [AddCommMonoid U] [Module R U] [TopologicalSpace U]
1030 [AddCommMonoid V] [Module R V] [TopologicalSpace V]
1031 [ContinuousAdd V] [ContinuousConstSMul R V]
1032 [AddCommMonoid W] [Module R W] [TopologicalSpace W]
1033 [ContinuousAdd W] [ContinuousConstSMul R W]
1034
1035/-- Composition of continuous linear maps, as a bilinear map. Compare `LinearMap.llcomp`. -/
1036@[simps]
1037def llcomp : (U →L[R] V) →ₗ[R] (V →L[R] W) →ₗ[R] (U →L[R] W) where
1038 toFun l := l.lcomp W
1039 map_add' _ _ := by ext; simp
1040 map_smul' _ _ := by ext; simp
1041
1042end llcomp
1043
1044section toSpanSingletonLE
1045
1046variable (R S M : Type*) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M]
1047 [SMulCommClass R S M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul S M]
1048 [TopologicalSpace R] [ContinuousSMul R M]
1049
1050/-- `ContinuousLinearMap.toSpanSingleton` as a linear equivalence. See
1051`ContinuousLinearMap.toSpanSingletonLIE` for the isometric version
1052and `ContinuousLinearMap.toSpanSingletonCLE` for the continuous version. -/
1053@[simps -fullyApplied]
1054def toSpanSingletonLE : M ≃ₗ[S] (R →L[R] M) where
1055 toFun := toSpanSingleton R
1056 invFun f := f 1
1057 map_add' := toSpanSingleton_add R
1058 map_smul' := toSpanSingleton_smul R
1059 left_inv x := by simp
1060 right_inv f := by ext; simp
1061
1062end toSpanSingletonLE
1063
1064section SMulRightₗ
1065
1066variable {R S T M M₂ : Type*} [Semiring R] [Semiring S] [Semiring T] [Module R S]
1067 [AddCommMonoid M₂] [Module R M₂] [Module S M₂] [IsScalarTower R S M₂] [TopologicalSpace S]
1068 [TopologicalSpace M₂] [ContinuousSMul S M₂] [TopologicalSpace M] [AddCommMonoid M] [Module R M]
1069 [ContinuousAdd M₂] [Module T M₂] [ContinuousConstSMul T M₂] [SMulCommClass R T M₂]
1070 [SMulCommClass S T M₂]
1071
1072/-- Given `c : E →L[R] S`, `c.smulRightₗ` is the linear map from `F` to `E →L[R] F`
1073sending `f` to `fun e => c e • f`. See also `ContinuousLinearMap.smulRightL`. -/
1074def smulRightₗ (c : M →L[R] S) : M₂ →ₗ[T] M →L[R] M₂ where
1075 toFun := c.smulRight
1076 map_add' x y := by
1077 ext e
1078 apply smul_add (c e)
1079 map_smul' a x := by
1080 ext e
1081 dsimp
1082 apply smul_comm
1083
1084@[simp]
1085theorem coe_smulRightₗ (c : M →L[R] S) : ⇑(smulRightₗ c : M₂ →ₗ[T] M →L[R] M₂) = c.smulRight :=
1086 rfl
1087
1088end SMulRightₗ
1089
1090section Semiring
1091variable {R S M : Type*} [Semiring R] [TopologicalSpace M] [AddCommGroup M] [Module R M]
1092 [CommSemiring S] [Module S M] [SMulCommClass R S M] [SMul S R] [IsScalarTower S R M]
1093 [ContinuousConstSMul S M] [IsTopologicalAddGroup M]
1094
1095instance algebra : Algebra S (M →L[R] M) :=
1096 Algebra.ofModule smul_comp fun _ _ _ => comp_smul _ _ _
1097
1098@[simp] theorem algebraMap_apply (r : S) (m : M) : algebraMap S (M →L[R] M) r m = r • m := rfl
1099
1100end Semiring
1101
1102end ContinuousLinearMap
1103
1104section topDualPairing
1105
1106variable {𝕜 E : Type*} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [AddCommMonoid E]
1107 [Module 𝕜 E] [TopologicalSpace E] [ContinuousConstSMul 𝕜 𝕜]
1108
1109variable (𝕜 E) in
1110/-- The canonical pairing of a vector space and its topological dual. -/
1111def topDualPairing : (E →L[𝕜] 𝕜) →ₗ[𝕜] E →ₗ[𝕜] 𝕜 :=
1112 ContinuousLinearMap.coeLM 𝕜
1113
1114@[simp]
1115theorem topDualPairing_apply (v : E →L[𝕜] 𝕜)
1116 (x : E) : topDualPairing 𝕜 E v x = v x :=
1117 rfl
1118
1119end topDualPairing