Documentation

Mathlib.Topology.Algebra.Module.Basic

Theory of topological modules and continuous linear maps. #

We use the class ContinuousSMul for topological (semi) modules and topological vector spaces.

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₂.

The corresponding notation for equivalences is M ≃SL[σ] M₂, M ≃L[R] M₂ and M ≃L⋆[R] M₂.

theorem ContinuousSMul.of_nhds_zero {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace R] [TopologicalSpace M] [AddCommGroup M] [Module R M] [TopologicalRing R] [TopologicalAddGroup M] (hmul : Filter.Tendsto (fun (p : R × M) => p.1 • p.2) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hmulleft : ∀ (m : M), Filter.Tendsto (fun (a : R) => a • m) (nhds 0) (nhds 0)) (hmulright : ∀ (a : R), Filter.Tendsto (fun (m : M) => a • m) (nhds 0) (nhds 0)) :

ContinuousSMul R M

theorem Submodule.eq_top_of_nonempty_interior' {R : Type u_1} {M : Type u_2} [Ring R] [TopologicalSpace R] [TopologicalSpace M] [AddCommGroup M] [ContinuousAdd M] [Module R M] [ContinuousSMul R M] [Filter.NeBot (nhdsWithin 0 {x : R | IsUnit x})] (s : Submodule R M) (hs : Set.Nonempty (interior ↑s)) :

If M is a topological module over R and 0 is a limit of invertible elements of R, then ⊤ is the only submodule of M with a nonempty interior. This is the case, e.g., if R is a nontrivially normed field.

theorem Module.punctured_nhds_neBot (R : Type u_1) (M : Type u_2) [Ring R] [TopologicalSpace R] [TopologicalSpace M] [AddCommGroup M] [ContinuousAdd M] [Module R M] [ContinuousSMul R M] [Nontrivial M] [Filter.NeBot (nhdsWithin 0 {0}ᶜ)] [NoZeroSMulDivisors R M] (x : M) :

Filter.NeBot (nhdsWithin x {x}ᶜ)

Let R be a topological ring such that zero is not an isolated point (e.g., a nontrivially normed field, see NormedField.punctured_nhds_neBot). Let M be a nontrivial module over R such that c • x = 0 implies c = 0 ∨ x = 0. Then M has no isolated points. We formulate this using NeBot (𝓝[≠] x).

This lemma is not an instance because Lean would need to find [ContinuousSMul ?m_1 M] with unknown ?m_1. We register this as an instance for R = ℝ in Real.punctured_nhds_module_neBot. One can also use haveI := Module.punctured_nhds_neBot R M in a proof.

theorem continuousSMul_induced {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [u : TopologicalSpace R] {t : TopologicalSpace M₂} [ContinuousSMul R M₂] (f : M₁ →ₗ[R] M₂) :

ContinuousSMul R M₁

theorem TopologicalSpace.IsSeparable.span {R : Type u_1} {M : Type u_2} [AddCommMonoid M] [Semiring R] [Module R M] [TopologicalSpace M] [TopologicalSpace R] [TopologicalSpace.SeparableSpace R] [ContinuousAdd M] [ContinuousSMul R M] {s : Set M} (hs : TopologicalSpace.IsSeparable s) :

TopologicalSpace.IsSeparable ↑(Submodule.span R s)

The span of a separable subset with respect to a separable scalar ring is again separable.

instance Submodule.topologicalAddGroup {α : Type u_1} {β : Type u_2} [TopologicalSpace β] [Ring α] [AddCommGroup β] [Module α β] [TopologicalAddGroup β] (S : Submodule α β) :

TopologicalAddGroup ↥S

Equations

⋯ = ⋯

theorem Submodule.mapsTo_smul_closure {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] (s : Submodule R M) (c : R) :

Set.MapsTo (fun (x : M) => c • x) (closure ↑s) (closure ↑s)

theorem Submodule.smul_closure_subset {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] (s : Submodule R M) (c : R) :

c • closure ↑s ⊆ closure ↑s

def Submodule.topologicalClosure {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (s : Submodule R M) :

The (topological-space) closure of a submodule of a topological R-module M is itself a submodule.

Equations

Submodule.topologicalClosure s = let __src := AddSubmonoid.topologicalClosure s.toAddSubmonoid; { toAddSubmonoid := __src, smul_mem' := ⋯ }

@[simp]

theorem Submodule.topologicalClosure_coe {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (s : Submodule R M) :

↑(Submodule.topologicalClosure s) = closure ↑s

theorem Submodule.le_topologicalClosure {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (s : Submodule R M) :

s ≤ Submodule.topologicalClosure s

theorem Submodule.closure_subset_topologicalClosure_span {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (s : Set M) :

closure s ⊆ ↑(Submodule.topologicalClosure (Submodule.span R s))

theorem Submodule.isClosed_topologicalClosure {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (s : Submodule R M) :

IsClosed ↑(Submodule.topologicalClosure s)

theorem Submodule.topologicalClosure_minimal {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (s : Submodule R M) {t : Submodule R M} (h : s ≤ t) (ht : IsClosed ↑t) :

Submodule.topologicalClosure s ≤ t

theorem Submodule.topologicalClosure_mono {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] {s : Submodule R M} {t : Submodule R M} (h : s ≤ t) :

Submodule.topologicalClosure s ≤ Submodule.topologicalClosure t

theorem IsClosed.submodule_topologicalClosure_eq {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] {s : Submodule R M} (hs : IsClosed ↑s) :

Submodule.topologicalClosure s = s

The topological closure of a closed submodule s is equal to s.

theorem Submodule.dense_iff_topologicalClosure_eq_top {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] {s : Submodule R M} :

Dense ↑s ↔ Submodule.topologicalClosure s = ⊤

A subspace is dense iff its topological closure is the entire space.

instance Submodule.topologicalClosure.completeSpace {R : Type u} [Semiring R] {M' : Type u_1} [AddCommMonoid M'] [Module R M'] [UniformSpace M'] [ContinuousAdd M'] [ContinuousConstSMul R M'] [CompleteSpace M'] (U : Submodule R M') :

CompleteSpace ↥(Submodule.topologicalClosure U)

Equations

⋯ = ⋯

theorem Submodule.isClosed_or_dense_of_isCoatom {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (s : Submodule R M) (hs : IsCoatom s) :

IsClosed ↑s ∨ Dense ↑s

A maximal proper subspace of a topological module (i.e a Submodule satisfying IsCoatom) is either closed or dense.

theorem LinearMap.continuous_on_pi {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Finite ι] [Semiring R] [TopologicalSpace R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousSMul R M] (f : (ι → R) →ₗ[R] M) :

Continuous ⇑f

structure ContinuousLinearMap {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type u_3) [TopologicalSpace M] [AddCommMonoid M] (M₂ : Type u_4) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends LinearMap :

Type (max u_3 u_4)

Continuous linear maps between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological ring R.

toFun : M → M₂
map_add' : ∀ (x y : M), self.toFun (x + y) = self.toFun x + self.toFun y
map_smul' : ∀ (r : R) (x : M), self.toFun (r • x) = σ r • self.toFun x
cont : Continuous self.toFun
Continuous linear maps between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological ring R.

Instances For

def «term_→SL[_]_» :

Lean.TrailingParserDescr

Continuous linear maps between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological ring R.

Equations

One or more equations did not get rendered due to their size.

def «term_→L[_]_» :

Lean.TrailingParserDescr

Continuous linear maps between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological ring R.

Equations

One or more equations did not get rendered due to their size.

def «term_→L⋆[_]_» :

Lean.TrailingParserDescr

Continuous linear maps between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological ring R.

Equations

One or more equations did not get rendered due to their size.

class ContinuousSemilinearMapClass (F : Type u_1) {R : outParam (Type u_2)} {S : outParam (Type u_3)} [Semiring R] [Semiring S] (σ : outParam (R →+* S)) (M : outParam (Type u_4)) [TopologicalSpace M] [AddCommMonoid M] (M₂ : outParam (Type u_5)) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M] [Module S M₂] [FunLike F M M₂] extends SemilinearMapClass , ContinuousMapClass :

ContinuousSemilinearMapClass F σ M M₂ asserts F is a type of bundled continuous σ-semilinear maps M → M₂. See also ContinuousLinearMapClass F R M M₂ for the case where σ is the identity map on R. A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

Instances

@[inline, reducible]

abbrev ContinuousLinearMapClass (F : Type u_1) (R : outParam (Type u_2)) [Semiring R] (M : outParam (Type u_3)) [TopologicalSpace M] [AddCommMonoid M] (M₂ : outParam (Type u_4)) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M] [Module R M₂] [FunLike F M M₂] :

ContinuousLinearMapClass F R M M₂ asserts F is a type of bundled continuous R-linear maps M → M₂. This is an abbreviation for ContinuousSemilinearMapClass F (RingHom.id R) M M₂.

Equations

ContinuousLinearMapClass F R M M₂ = ContinuousSemilinearMapClass F (RingHom.id R) M M₂

structure ContinuousLinearEquiv {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (σ : R →+* S) {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M : Type u_3) [TopologicalSpace M] [AddCommMonoid M] (M₂ : Type u_4) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends LinearEquiv :

Type (max u_3 u_4)

Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological semiring R.

toFun : M → M₂
map_add' : ∀ (x y : M), self.toFun (x + y) = self.toFun x + self.toFun y
map_smul' : ∀ (r : R) (x : M), self.toFun (r • x) = σ r • self.toFun x
invFun : M₂ → M
left_inv : Function.LeftInverse self.invFun self.toFun
right_inv : Function.RightInverse self.invFun self.toFun
continuous_toFun : Continuous self.toFun
Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological semiring R.
continuous_invFun : Continuous self.invFun
Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological semiring R.

Instances For

def «term_≃SL[_]_» :

Lean.TrailingParserDescr

Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological semiring R.

Equations

One or more equations did not get rendered due to their size.

def «term_≃L[_]_» :

Lean.TrailingParserDescr

Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological semiring R.

Equations

One or more equations did not get rendered due to their size.

def «term_≃L⋆[_]_» :

Lean.TrailingParserDescr

Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological semiring R.

Equations

One or more equations did not get rendered due to their size.

class ContinuousSemilinearEquivClass (F : Type u_1) {R : outParam (Type u_2)} {S : outParam (Type u_3)} [Semiring R] [Semiring S] (σ : outParam (R →+* S)) {σ' : outParam (S →+* R)} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M : outParam (Type u_4)) [TopologicalSpace M] [AddCommMonoid M] (M₂ : outParam (Type u_5)) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M] [Module S M₂] [EquivLike F M M₂] extends SemilinearEquivClass :

ContinuousSemilinearEquivClass F σ M M₂ asserts F is a type of bundled continuous σ-semilinear equivs M → M₂. See also ContinuousLinearEquivClass F R M M₂ for the case where σ is the identity map on R. A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

map_add : ∀ (f : F) (a b : M), f (a + b) = f a + f b
map_smulₛₗ : ∀ (f : F) (r : R) (x : M), f (r • x) = σ r • f x
map_continuous : ∀ (f : F), Continuous ⇑f
ContinuousSemilinearEquivClass F σ M M₂ asserts F is a type of bundled continuous σ-semilinear equivs M → M₂. See also ContinuousLinearEquivClass F R M M₂ for the case where σ is the identity map on R. A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.
inv_continuous : ∀ (f : F), Continuous (EquivLike.inv f)
ContinuousSemilinearEquivClass F σ M M₂ asserts F is a type of bundled continuous σ-semilinear equivs M → M₂. See also ContinuousLinearEquivClass F R M M₂ for the case where σ is the identity map on R. A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

Instances

ContinuousLinearEquiv.continuousSemilinearEquivClass

@[inline, reducible]

abbrev ContinuousLinearEquivClass (F : Type u_1) (R : outParam (Type u_2)) [Semiring R] (M : outParam (Type u_3)) [TopologicalSpace M] [AddCommMonoid M] (M₂ : outParam (Type u_4)) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M] [Module R M₂] [EquivLike F M M₂] :

ContinuousLinearEquivClass F σ M M₂ asserts F is a type of bundled continuous R-linear equivs M → M₂. This is an abbreviation for ContinuousSemilinearEquivClass F (RingHom.id R) M M₂.

Equations

ContinuousLinearEquivClass F R M M₂ = ContinuousSemilinearEquivClass F (RingHom.id R) M M₂

instance ContinuousSemilinearEquivClass.continuousSemilinearMapClass (F : Type u_1) {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (σ : R →+* S) {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M : Type u_4) [TopologicalSpace M] [AddCommMonoid M] (M₂ : Type u_5) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M] [Module S M₂] [EquivLike F M M₂] [s : ContinuousSemilinearEquivClass F σ M M₂] :

ContinuousSemilinearMapClass F σ M M₂

Equations

⋯ = ⋯

@[simp]

theorem linearMapOfMemClosureRangeCoe_apply {M₁ : Type u_1} {M₂ : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace M₂] [T2Space M₂] [Semiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module S M₂] [ContinuousConstSMul S M₂] [ContinuousAdd M₂] {σ : R →+* S} (f : M₁ → M₂) (hf : f ∈ closure (Set.range DFunLike.coe)) :

⇑(linearMapOfMemClosureRangeCoe f hf) = (addMonoidHomOfMemClosureRangeCoe f hf).toFun

def linearMapOfMemClosureRangeCoe {M₁ : Type u_1} {M₂ : Type u_2} {R : Type u_4} {S : Type u_5} [TopologicalSpace M₂] [T2Space M₂] [Semiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module S M₂] [ContinuousConstSMul S M₂] [ContinuousAdd M₂] {σ : R →+* S} (f : M₁ → M₂) (hf : f ∈ closure (Set.range DFunLike.coe)) :

M₁ →ₛₗ[σ] M₂

Constructs a bundled linear map from a function and a proof that this function belongs to the closure of the set of linear maps.

Equations

linearMapOfMemClosureRangeCoe f hf = let __src := addMonoidHomOfMemClosureRangeCoe f hf; { toAddHom := { toFun := __src.toFun, map_add' := ⋯ }, map_smul' := ⋯ }

@[simp]

theorem linearMapOfTendsto_apply {M₁ : Type u_1} {M₂ : Type u_2} {α : Type u_3} {R : Type u_4} {S : Type u_5} [TopologicalSpace M₂] [T2Space M₂] [Semiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module S M₂] [ContinuousConstSMul S M₂] [ContinuousAdd M₂] {σ : R →+* S} {l : Filter α} (f : M₁ → M₂) (g : α → M₁ →ₛₗ[σ] M₂) [Filter.NeBot l] (h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f)) :

⇑(linearMapOfTendsto f g h) = f

def linearMapOfTendsto {M₁ : Type u_1} {M₂ : Type u_2} {α : Type u_3} {R : Type u_4} {S : Type u_5} [TopologicalSpace M₂] [T2Space M₂] [Semiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module S M₂] [ContinuousConstSMul S M₂] [ContinuousAdd M₂] {σ : R →+* S} {l : Filter α} (f : M₁ → M₂) (g : α → M₁ →ₛₗ[σ] M₂) [Filter.NeBot l] (h : Filter.Tendsto (fun (a : α) (x : M₁) => (g a) x) l (nhds f)) :

M₁ →ₛₗ[σ] M₂

Construct a bundled linear map from a pointwise limit of linear maps

Equations

linearMapOfTendsto f g h = linearMapOfMemClosureRangeCoe f ⋯

theorem LinearMap.isClosed_range_coe (M₁ : Type u_1) (M₂ : Type u_2) {R : Type u_4} {S : Type u_5} [TopologicalSpace M₂] [T2Space M₂] [Semiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module S M₂] [ContinuousConstSMul S M₂] [ContinuousAdd M₂] (σ : R →+* S) :

IsClosed (Set.range DFunLike.coe)

Properties that hold for non-necessarily commutative semirings. #

instance ContinuousLinearMap.LinearMap.coe {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] :

Coe (M₁ →SL[σ₁₂] M₂) (M₁ →ₛₗ[σ₁₂] M₂)

Coerce continuous linear maps to linear maps.

Equations

ContinuousLinearMap.LinearMap.coe = { coe := ContinuousLinearMap.toLinearMap }

theorem ContinuousLinearMap.coe_injective {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] :

Function.Injective ContinuousLinearMap.toLinearMap

instance ContinuousLinearMap.funLike {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] :

FunLike (M₁ →SL[σ₁₂] M₂) M₁ M₂

Equations

ContinuousLinearMap.funLike = { coe := fun (f : M₁ →SL[σ₁₂] M₂) => ⇑↑f, coe_injective' := ⋯ }

instance ContinuousLinearMap.continuousSemilinearMapClass {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] :

ContinuousSemilinearMapClass (M₁ →SL[σ₁₂] M₂) σ₁₂ M₁ M₂

Equations

⋯ = ⋯

theorem ContinuousLinearMap.coe_mk {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →ₛₗ[σ₁₂] M₂) (h : Continuous f.toFun) :

↑{ toLinearMap := f, cont := h } = f

Coerce continuous linear maps to functions.

@[simp]

theorem ContinuousLinearMap.coe_mk' {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →ₛₗ[σ₁₂] M₂) (h : Continuous f.toFun) :

⇑{ toLinearMap := f, cont := h } = ⇑f

theorem ContinuousLinearMap.continuous {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) :

Continuous ⇑f

theorem ContinuousLinearMap.uniformContinuous {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {E₁ : Type u_9} {E₂ : Type u_10} [UniformSpace E₁] [UniformSpace E₂] [AddCommGroup E₁] [AddCommGroup E₂] [Module R₁ E₁] [Module R₂ E₂] [UniformAddGroup E₁] [UniformAddGroup E₂] (f : E₁ →SL[σ₁₂] E₂) :

UniformContinuous ⇑f

@[simp]

theorem ContinuousLinearMap.coe_inj {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂} {g : M₁ →SL[σ₁₂] M₂} :

↑f = ↑g ↔ f = g

theorem ContinuousLinearMap.coeFn_injective {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] :

Function.Injective DFunLike.coe

def ContinuousLinearMap.Simps.apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (h : M₁ →SL[σ₁₂] M₂) :

M₁ → M₂

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations

ContinuousLinearMap.Simps.apply h = ⇑h

def ContinuousLinearMap.Simps.coe {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (h : M₁ →SL[σ₁₂] M₂) :

M₁ →ₛₗ[σ₁₂] M₂

See Note [custom simps projection].

Equations

ContinuousLinearMap.Simps.coe h = ↑h

theorem ContinuousLinearMap.ext {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂} {g : M₁ →SL[σ₁₂] M₂} (h : ∀ (x : M₁), f x = g x) :

f = g

theorem ContinuousLinearMap.ext_iff {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂} {g : M₁ →SL[σ₁₂] M₂} :

f = g ↔ ∀ (x : M₁), f x = g x

def ContinuousLinearMap.copy {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (f' : M₁ → M₂) (h : f' = ⇑f) :

M₁ →SL[σ₁₂] M₂

Copy of a ContinuousLinearMap with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

ContinuousLinearMap.copy f f' h = { toLinearMap := LinearMap.copy (↑f) f' h, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.coe_copy {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (f' : M₁ → M₂) (h : f' = ⇑f) :

⇑(ContinuousLinearMap.copy f f' h) = f'

theorem ContinuousLinearMap.copy_eq {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (f' : M₁ → M₂) (h : f' = ⇑f) :

ContinuousLinearMap.copy f f' h = f

theorem ContinuousLinearMap.map_zero {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) :

f 0 = 0

theorem ContinuousLinearMap.map_add {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (x : M₁) (y : M₁) :

f (x + y) = f x + f y

theorem ContinuousLinearMap.map_smulₛₗ {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (c : R₁) (x : M₁) :

f (c • x) = σ₁₂ c • f x

theorem ContinuousLinearMap.map_smul {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] (f : M₁ →L[R₁] M₂) (c : R₁) (x : M₁) :

f (c • x) = c • f x

@[simp]

theorem ContinuousLinearMap.map_smul_of_tower {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {R : Type u_9} {S : Type u_10} [Semiring S] [SMul R M₁] [Module S M₁] [SMul R M₂] [Module S M₂] [LinearMap.CompatibleSMul M₁ M₂ R S] (f : M₁ →L[S] M₂) (c : R) (x : M₁) :

f (c • x) = c • f x

@[deprecated map_sum]

theorem ContinuousLinearMap.map_sum {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {ι : Type u_9} (f : M₁ →SL[σ₁₂] M₂) (s : Finset ι) (g : ι → M₁) :

f (Finset.sum s fun (i : ι) => g i) = Finset.sum s fun (i : ι) => f (g i)

@[simp]

theorem ContinuousLinearMap.coe_coe {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) :

⇑↑f = ⇑f

theorem ContinuousLinearMap.ext_ring {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace R₁] {f : R₁ →L[R₁] M₁} {g : R₁ →L[R₁] M₁} (h : f 1 = g 1) :

f = g

theorem ContinuousLinearMap.ext_ring_iff {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace R₁] {f : R₁ →L[R₁] M₁} {g : R₁ →L[R₁] M₁} :

f = g ↔ f 1 = g 1

theorem ContinuousLinearMap.eqOn_closure_span {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] [T2Space M₂] {s : Set M₁} {f : M₁ →SL[σ₁₂] M₂} {g : M₁ →SL[σ₁₂] M₂} (h : Set.EqOn (⇑f) (⇑g) s) :

Set.EqOn (⇑f) (⇑g) (closure ↑(Submodule.span R₁ s))

If two continuous linear maps are equal on a set s, then they are equal on the closure of the Submodule.span of this set.

theorem ContinuousLinearMap.ext_on {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] [T2Space M₂] {s : Set M₁} (hs : Dense ↑(Submodule.span R₁ s)) {f : M₁ →SL[σ₁₂] M₂} {g : M₁ →SL[σ₁₂] M₂} (h : Set.EqOn (⇑f) (⇑g) s) :

f = g

If the submodule generated by a set s is dense in the ambient module, then two continuous linear maps equal on s are equal.

theorem Submodule.topologicalClosure_map {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] [RingHomSurjective σ₁₂] [TopologicalSpace R₁] [TopologicalSpace R₂] [ContinuousSMul R₁ M₁] [ContinuousAdd M₁] [ContinuousSMul R₂ M₂] [ContinuousAdd M₂] (f : M₁ →SL[σ₁₂] M₂) (s : Submodule R₁ M₁) :

Submodule.map (↑f) (Submodule.topologicalClosure s) ≤ Submodule.topologicalClosure (Submodule.map (↑f) s)

Under a continuous linear map, the image of the TopologicalClosure of a submodule is contained in the TopologicalClosure of its image.

theorem DenseRange.topologicalClosure_map_submodule {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] [RingHomSurjective σ₁₂] [TopologicalSpace R₁] [TopologicalSpace R₂] [ContinuousSMul R₁ M₁] [ContinuousAdd M₁] [ContinuousSMul R₂ M₂] [ContinuousAdd M₂] {f : M₁ →SL[σ₁₂] M₂} (hf' : DenseRange ⇑f) {s : Submodule R₁ M₁} (hs : Submodule.topologicalClosure s = ⊤) :

Submodule.topologicalClosure (Submodule.map (↑f) s) = ⊤

Under a dense continuous linear map, a submodule whose TopologicalClosure is ⊤ is sent to another such submodule. That is, the image of a dense set under a map with dense range is dense.

instance ContinuousLinearMap.mulAction {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {S₂ : Type u_9} [Monoid S₂] [DistribMulAction S₂ M₂] [SMulCommClass R₂ S₂ M₂] [ContinuousConstSMul S₂ M₂] :

MulAction S₂ (M₁ →SL[σ₁₂] M₂)

Equations

ContinuousLinearMap.mulAction = MulAction.mk ⋯ ⋯

theorem ContinuousLinearMap.smul_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {S₂ : Type u_9} [Monoid S₂] [DistribMulAction S₂ M₂] [SMulCommClass R₂ S₂ M₂] [ContinuousConstSMul S₂ M₂] (c : S₂) (f : M₁ →SL[σ₁₂] M₂) (x : M₁) :

(c • f) x = c • f x

@[simp]

theorem ContinuousLinearMap.coe_smul {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {S₂ : Type u_9} [Monoid S₂] [DistribMulAction S₂ M₂] [SMulCommClass R₂ S₂ M₂] [ContinuousConstSMul S₂ M₂] (c : S₂) (f : M₁ →SL[σ₁₂] M₂) :

↑(c • f) = c • ↑f

@[simp]

theorem ContinuousLinearMap.coe_smul' {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {S₂ : Type u_9} [Monoid S₂] [DistribMulAction S₂ M₂] [SMulCommClass R₂ S₂ M₂] [ContinuousConstSMul S₂ M₂] (c : S₂) (f : M₁ →SL[σ₁₂] M₂) :

⇑(c • f) = c • ⇑f

instance ContinuousLinearMap.isScalarTower {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {S₂ : Type u_9} {T₂ : Type u_10} [Monoid S₂] [Monoid T₂] [DistribMulAction S₂ M₂] [SMulCommClass R₂ S₂ M₂] [ContinuousConstSMul S₂ M₂] [DistribMulAction T₂ M₂] [SMulCommClass R₂ T₂ M₂] [ContinuousConstSMul T₂ M₂] [SMul S₂ T₂] [IsScalarTower S₂ T₂ M₂] :

IsScalarTower S₂ T₂ (M₁ →SL[σ₁₂] M₂)

Equations

⋯ = ⋯

instance ContinuousLinearMap.smulCommClass {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {S₂ : Type u_9} {T₂ : Type u_10} [Monoid S₂] [Monoid T₂] [DistribMulAction S₂ M₂] [SMulCommClass R₂ S₂ M₂] [ContinuousConstSMul S₂ M₂] [DistribMulAction T₂ M₂] [SMulCommClass R₂ T₂ M₂] [ContinuousConstSMul T₂ M₂] [SMulCommClass S₂ T₂ M₂] :

SMulCommClass S₂ T₂ (M₁ →SL[σ₁₂] M₂)

Equations

⋯ = ⋯

instance ContinuousLinearMap.zero {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] :

Zero (M₁ →SL[σ₁₂] M₂)

The continuous map that is constantly zero.

Equations

ContinuousLinearMap.zero = { zero := { toLinearMap := 0, cont := ⋯ } }

instance ContinuousLinearMap.inhabited {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] :

Inhabited (M₁ →SL[σ₁₂] M₂)

Equations

ContinuousLinearMap.inhabited = { default := 0 }

@[simp]

theorem ContinuousLinearMap.default_def {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] :

default = 0

@[simp]

theorem ContinuousLinearMap.zero_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (x : M₁) :

0 x = 0

@[simp]

theorem ContinuousLinearMap.coe_zero {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] :

↑0 = 0

theorem ContinuousLinearMap.coe_zero' {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] :

⇑0 = 0

instance ContinuousLinearMap.uniqueOfLeft {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] [Subsingleton M₁] :

Unique (M₁ →SL[σ₁₂] M₂)

Equations

ContinuousLinearMap.uniqueOfLeft = Function.Injective.unique ⋯

instance ContinuousLinearMap.uniqueOfRight {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] [Subsingleton M₂] :

Unique (M₁ →SL[σ₁₂] M₂)

Equations

ContinuousLinearMap.uniqueOfRight = Function.Injective.unique ⋯

theorem ContinuousLinearMap.exists_ne_zero {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂} (hf : f ≠ 0) :

∃ (x : M₁), f x ≠ 0

def ContinuousLinearMap.id (R₁ : Type u_1) [Semiring R₁] (M₁ : Type u_4) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :

M₁ →L[R₁] M₁

the identity map as a continuous linear map.

Equations

ContinuousLinearMap.id R₁ M₁ = { toLinearMap := LinearMap.id, cont := ⋯ }

instance ContinuousLinearMap.one {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :

One (M₁ →L[R₁] M₁)

Equations

ContinuousLinearMap.one = { one := ContinuousLinearMap.id R₁ M₁ }

theorem ContinuousLinearMap.one_def {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :

1 = ContinuousLinearMap.id R₁ M₁

theorem ContinuousLinearMap.id_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] (x : M₁) :

(ContinuousLinearMap.id R₁ M₁) x = x

@[simp]

theorem ContinuousLinearMap.coe_id {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :

↑(ContinuousLinearMap.id R₁ M₁) = LinearMap.id

@[simp]

theorem ContinuousLinearMap.coe_id' {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :

⇑(ContinuousLinearMap.id R₁ M₁) = id

@[simp]

theorem ContinuousLinearMap.coe_eq_id {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] {f : M₁ →L[R₁] M₁} :

↑f = LinearMap.id ↔ f = ContinuousLinearMap.id R₁ M₁

@[simp]

theorem ContinuousLinearMap.one_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] (x : M₁) :

1 x = x

instance ContinuousLinearMap.instNontrivialContinuousLinearMapIdToNonAssocSemiring {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [Nontrivial M₁] :

Nontrivial (M₁ →L[R₁] M₁)

Equations

⋯ = ⋯

instance ContinuousLinearMap.add {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] [ContinuousAdd M₂] :

Add (M₁ →SL[σ₁₂] M₂)

Equations

ContinuousLinearMap.add = { add := fun (f g : M₁ →SL[σ₁₂] M₂) => { toLinearMap := ↑f + ↑g, cont := ⋯ } }

@[simp]

theorem ContinuousLinearMap.add_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] [ContinuousAdd M₂] (f : M₁ →SL[σ₁₂] M₂) (g : M₁ →SL[σ₁₂] M₂) (x : M₁) :

(f + g) x = f x + g x

@[simp]

theorem ContinuousLinearMap.coe_add {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] [ContinuousAdd M₂] (f : M₁ →SL[σ₁₂] M₂) (g : M₁ →SL[σ₁₂] M₂) :

↑(f + g) = ↑f + ↑g

theorem ContinuousLinearMap.coe_add' {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] [ContinuousAdd M₂] (f : M₁ →SL[σ₁₂] M₂) (g : M₁ →SL[σ₁₂] M₂) :

⇑(f + g) = ⇑f + ⇑g

instance ContinuousLinearMap.addCommMonoid {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] [ContinuousAdd M₂] :

AddCommMonoid (M₁ →SL[σ₁₂] M₂)

Equations

ContinuousLinearMap.addCommMonoid = AddCommMonoid.mk ⋯

@[simp]

theorem ContinuousLinearMap.coe_sum {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] [ContinuousAdd M₂] {ι : Type u_9} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) :

↑(Finset.sum t fun (d : ι) => f d) = Finset.sum t fun (d : ι) => ↑(f d)

@[simp]

theorem ContinuousLinearMap.coe_sum' {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] [ContinuousAdd M₂] {ι : Type u_9} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) :

⇑(Finset.sum t fun (d : ι) => f d) = Finset.sum t fun (d : ι) => ⇑(f d)

theorem ContinuousLinearMap.sum_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] [ContinuousAdd M₂] {ι : Type u_9} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) (b : M₁) :

(Finset.sum t fun (d : ι) => f d) b = Finset.sum t fun (d : ι) => (f d) b

def ContinuousLinearMap.comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :

M₁ →SL[σ₁₃] M₃

Composition of bounded linear maps.

Equations

ContinuousLinearMap.comp g f = { toLinearMap := LinearMap.comp ↑g ↑f, cont := ⋯ }

def ContinuousLinearMap.«term_∘L_» :

Lean.TrailingParserDescr

Composition of bounded linear maps.

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousLinearMap.coe_comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :

↑(ContinuousLinearMap.comp h f) = LinearMap.comp ↑h ↑f

@[simp]

theorem ContinuousLinearMap.coe_comp' {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :

⇑(ContinuousLinearMap.comp h f) = ⇑h ∘ ⇑f

theorem ContinuousLinearMap.comp_apply {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) (x : M₁) :

(ContinuousLinearMap.comp g f) x = g (f x)

@[simp]

theorem ContinuousLinearMap.comp_id {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) :

ContinuousLinearMap.comp f (ContinuousLinearMap.id R₁ M₁) = f

@[simp]

theorem ContinuousLinearMap.id_comp {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) :

ContinuousLinearMap.comp (ContinuousLinearMap.id R₂ M₂) f = f

@[simp]

theorem ContinuousLinearMap.comp_zero {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →SL[σ₂₃] M₃) :

ContinuousLinearMap.comp g 0 = 0

@[simp]

theorem ContinuousLinearMap.zero_comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₁ →SL[σ₁₂] M₂) :

ContinuousLinearMap.comp 0 f = 0

@[simp]

theorem ContinuousLinearMap.comp_add {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [ContinuousAdd M₂] [ContinuousAdd M₃] (g : M₂ →SL[σ₂₃] M₃) (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₁ →SL[σ₁₂] M₂) :

ContinuousLinearMap.comp g (f₁ + f₂) = ContinuousLinearMap.comp g f₁ + ContinuousLinearMap.comp g f₂

@[simp]

theorem ContinuousLinearMap.add_comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [ContinuousAdd M₃] (g₁ : M₂ →SL[σ₂₃] M₃) (g₂ : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :

ContinuousLinearMap.comp (g₁ + g₂) f = ContinuousLinearMap.comp g₁ f + ContinuousLinearMap.comp g₂ f

theorem ContinuousLinearMap.comp_assoc {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] {M₄ : Type u_8} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {R₄ : Type u_9} [Semiring R₄] [Module R₄ M₄] {σ₁₄ : R₁ →+* R₄} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄} [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (h : M₃ →SL[σ₃₄] M₄) (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :

ContinuousLinearMap.comp (ContinuousLinearMap.comp h g) f = ContinuousLinearMap.comp h (ContinuousLinearMap.comp g f)

instance ContinuousLinearMap.instMul {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :

Mul (M₁ →L[R₁] M₁)

Equations

ContinuousLinearMap.instMul = { mul := ContinuousLinearMap.comp }

theorem ContinuousLinearMap.mul_def {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] (f : M₁ →L[R₁] M₁) (g : M₁ →L[R₁] M₁) :

f * g = ContinuousLinearMap.comp f g

@[simp]

theorem ContinuousLinearMap.coe_mul {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] (f : M₁ →L[R₁] M₁) (g : M₁ →L[R₁] M₁) :

⇑(f * g) = ⇑f ∘ ⇑g

theorem ContinuousLinearMap.mul_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] (f : M₁ →L[R₁] M₁) (g : M₁ →L[R₁] M₁) (x : M₁) :

(f * g) x = f (g x)

instance ContinuousLinearMap.monoidWithZero {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :

MonoidWithZero (M₁ →L[R₁] M₁)

Equations

ContinuousLinearMap.monoidWithZero = MonoidWithZero.mk ⋯ ⋯

theorem ContinuousLinearMap.coe_pow {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] (f : M₁ →L[R₁] M₁) (n : ℕ) :

⇑(f ^ n) = (⇑f)^[n]

instance ContinuousLinearMap.semiring {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [ContinuousAdd M₁] :

Semiring (M₁ →L[R₁] M₁)

Equations

ContinuousLinearMap.semiring = let __spread.0 := ContinuousLinearMap.monoidWithZero; let __spread.1 := ContinuousLinearMap.addCommMonoid; Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯

@[simp]

theorem ContinuousLinearMap.toLinearMapRingHom_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [ContinuousAdd M₁] (self : M₁ →L[R₁] M₁) :

ContinuousLinearMap.toLinearMapRingHom self = ↑self

def ContinuousLinearMap.toLinearMapRingHom {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [ContinuousAdd M₁] :

(M₁ →L[R₁] M₁) →+* M₁ →ₗ[R₁] M₁

ContinuousLinearMap.toLinearMap as a RingHom.

Equations

ContinuousLinearMap.toLinearMapRingHom = { toMonoidHom := { toOneHom := { toFun := ContinuousLinearMap.toLinearMap, map_one' := ⋯ }, map_mul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem ContinuousLinearMap.natCast_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [ContinuousAdd M₁] (n : ℕ) (m : M₁) :

↑n m = n • m

@[simp]

theorem ContinuousLinearMap.ofNat_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [ContinuousAdd M₁] (n : ℕ) [Nat.AtLeastTwo n] (m : M₁) :

(OfNat.ofNat n) m = OfNat.ofNat n • m

instance ContinuousLinearMap.applyModule {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [ContinuousAdd M₁] :

Module (M₁ →L[R₁] M₁) M₁

The tautological action by M₁ →L[R₁] M₁ on M.

This generalizes Function.End.applyMulAction.

Equations

ContinuousLinearMap.applyModule = Module.compHom M₁ ContinuousLinearMap.toLinearMapRingHom

@[simp]

theorem ContinuousLinearMap.smul_def {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [ContinuousAdd M₁] (f : M₁ →L[R₁] M₁) (a : M₁) :

f • a = f a

instance ContinuousLinearMap.applyFaithfulSMul {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [ContinuousAdd M₁] :

FaithfulSMul (M₁ →L[R₁] M₁) M₁

ContinuousLinearMap.applyModule is faithful.

Equations

⋯ = ⋯

instance ContinuousLinearMap.applySMulCommClass {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [ContinuousAdd M₁] :

SMulCommClass R₁ (M₁ →L[R₁] M₁) M₁

Equations

⋯ = ⋯

instance ContinuousLinearMap.applySMulCommClass' {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [ContinuousAdd M₁] :

SMulCommClass (M₁ →L[R₁] M₁) R₁ M₁

Equations

⋯ = ⋯

instance ContinuousLinearMap.continuousConstSMul_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [ContinuousAdd M₁] :

ContinuousConstSMul (M₁ →L[R₁] M₁) M₁

Equations

⋯ = ⋯

def ContinuousLinearMap.prod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₁ →L[R₁] M₃) :

M₁ →L[R₁] M₂ × M₃

The cartesian product of two bounded linear maps, as a bounded linear map.

Equations

ContinuousLinearMap.prod f₁ f₂ = { toLinearMap := LinearMap.prod ↑f₁ ↑f₂, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.coe_prod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₁ →L[R₁] M₃) :

↑(ContinuousLinearMap.prod f₁ f₂) = LinearMap.prod ↑f₁ ↑f₂

@[simp]

theorem ContinuousLinearMap.prod_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₁ →L[R₁] M₃) (x : M₁) :

(ContinuousLinearMap.prod f₁ f₂) x = (f₁ x, f₂ x)

def ContinuousLinearMap.inl (R₁ : Type u_1) [Semiring R₁] (M₁ : Type u_4) [TopologicalSpace M₁] [AddCommMonoid M₁] (M₂ : Type u_6) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] :

M₁ →L[R₁] M₁ × M₂

The left injection into a product is a continuous linear map.

Equations

ContinuousLinearMap.inl R₁ M₁ M₂ = ContinuousLinearMap.prod (ContinuousLinearMap.id R₁ M₁) 0

def ContinuousLinearMap.inr (R₁ : Type u_1) [Semiring R₁] (M₁ : Type u_4) [TopologicalSpace M₁] [AddCommMonoid M₁] (M₂ : Type u_6) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] :

M₂ →L[R₁] M₁ × M₂

The right injection into a product is a continuous linear map.

Equations

ContinuousLinearMap.inr R₁ M₁ M₂ = ContinuousLinearMap.prod 0 (ContinuousLinearMap.id R₁ M₂)

@[simp]

theorem ContinuousLinearMap.inl_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] (x : M₁) :

(ContinuousLinearMap.inl R₁ M₁ M₂) x = (x, 0)

@[simp]

theorem ContinuousLinearMap.inr_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] (x : M₂) :

(ContinuousLinearMap.inr R₁ M₁ M₂) x = (0, x)

@[simp]

theorem ContinuousLinearMap.coe_inl {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] :

↑(ContinuousLinearMap.inl R₁ M₁ M₂) = LinearMap.inl R₁ M₁ M₂

@[simp]

theorem ContinuousLinearMap.coe_inr {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] :

↑(ContinuousLinearMap.inr R₁ M₁ M₂) = LinearMap.inr R₁ M₁ M₂

theorem ContinuousLinearMap.isClosed_ker {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {F : Type u_9} [T1Space M₂] [FunLike F M₁ M₂] [ContinuousSemilinearMapClass F σ₁₂ M₁ M₂] (f : F) :

IsClosed ↑(LinearMap.ker f)

theorem ContinuousLinearMap.isComplete_ker {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_9} {M' : Type u_10} [UniformSpace M'] [CompleteSpace M'] [AddCommMonoid M'] [Module R₁ M'] [T1Space M₂] [FunLike F M' M₂] [ContinuousSemilinearMapClass F σ₁₂ M' M₂] (f : F) :

IsComplete ↑(LinearMap.ker f)

instance ContinuousLinearMap.completeSpace_ker {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_9} {M' : Type u_10} [UniformSpace M'] [CompleteSpace M'] [AddCommMonoid M'] [Module R₁ M'] [T1Space M₂] [FunLike F M' M₂] [ContinuousSemilinearMapClass F σ₁₂ M' M₂] (f : F) :

CompleteSpace ↥(LinearMap.ker f)

Equations

⋯ = ⋯

instance ContinuousLinearMap.completeSpace_eqLocus {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_9} {M' : Type u_10} [UniformSpace M'] [CompleteSpace M'] [AddCommMonoid M'] [Module R₁ M'] [T2Space M₂] [FunLike F M' M₂] [ContinuousSemilinearMapClass F σ₁₂ M' M₂] (f : F) (g : F) :

CompleteSpace ↥(LinearMap.eqLocus f g)

Equations

⋯ = ⋯

@[simp]

theorem ContinuousLinearMap.ker_prod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] (f : M₁ →L[R₁] M₂) (g : M₁ →L[R₁] M₃) :

LinearMap.ker (ContinuousLinearMap.prod f g) = LinearMap.ker f ⊓ LinearMap.ker g

def ContinuousLinearMap.codRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x ∈ p) :

M₁ →SL[σ₁₂] ↥p

Restrict codomain of a continuous linear map.

Equations

ContinuousLinearMap.codRestrict f p h = { toLinearMap := LinearMap.codRestrict p (↑f) h, cont := ⋯ }

theorem ContinuousLinearMap.coe_codRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x ∈ p) :

↑(ContinuousLinearMap.codRestrict f p h) = LinearMap.codRestrict p (↑f) h

@[simp]

theorem ContinuousLinearMap.coe_codRestrict_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x ∈ p) (x : M₁) :

↑((ContinuousLinearMap.codRestrict f p h) x) = f x

@[simp]

theorem ContinuousLinearMap.ker_codRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x ∈ p) :

LinearMap.ker (ContinuousLinearMap.codRestrict f p h) = LinearMap.ker f

@[reducible]

def ContinuousLinearMap.rangeRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] [RingHomSurjective σ₁₂] (f : M₁ →SL[σ₁₂] M₂) :

M₁ →SL[σ₁₂] ↥(LinearMap.range f)

Restrict the codomain of a continuous linear map f to f.range.

Equations

ContinuousLinearMap.rangeRestrict f = ContinuousLinearMap.codRestrict f (LinearMap.range f) ⋯

@[simp]

theorem ContinuousLinearMap.coe_rangeRestrict {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] [RingHomSurjective σ₁₂] (f : M₁ →SL[σ₁₂] M₂) :

↑(ContinuousLinearMap.rangeRestrict f) = LinearMap.rangeRestrict ↑f

def Submodule.subtypeL {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] (p : Submodule R₁ M₁) :

↥p →L[R₁] M₁

Submodule.subtype as a ContinuousLinearMap.

Equations

Submodule.subtypeL p = { toLinearMap := Submodule.subtype p, cont := ⋯ }

@[simp]

theorem Submodule.coe_subtypeL {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] (p : Submodule R₁ M₁) :

↑(Submodule.subtypeL p) = Submodule.subtype p

@[simp]

theorem Submodule.coe_subtypeL' {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] (p : Submodule R₁ M₁) :

⇑(Submodule.subtypeL p) = ⇑(Submodule.subtype p)

@[simp]

theorem Submodule.subtypeL_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] (p : Submodule R₁ M₁) (x : ↥p) :

(Submodule.subtypeL p) x = ↑x

@[simp]

theorem Submodule.range_subtypeL {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] (p : Submodule R₁ M₁) :

LinearMap.range (Submodule.subtypeL p) = p

@[simp]

theorem Submodule.ker_subtypeL {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] (p : Submodule R₁ M₁) :

LinearMap.ker (Submodule.subtypeL p) = ⊥

def ContinuousLinearMap.fst (R₁ : Type u_1) [Semiring R₁] (M₁ : Type u_4) [TopologicalSpace M₁] [AddCommMonoid M₁] (M₂ : Type u_6) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] :

M₁ × M₂ →L[R₁] M₁

Prod.fst as a ContinuousLinearMap.

Equations

ContinuousLinearMap.fst R₁ M₁ M₂ = { toLinearMap := LinearMap.fst R₁ M₁ M₂, cont := ⋯ }

def ContinuousLinearMap.snd (R₁ : Type u_1) [Semiring R₁] (M₁ : Type u_4) [TopologicalSpace M₁] [AddCommMonoid M₁] (M₂ : Type u_6) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] :

M₁ × M₂ →L[R₁] M₂

Prod.snd as a ContinuousLinearMap.

Equations

ContinuousLinearMap.snd R₁ M₁ M₂ = { toLinearMap := LinearMap.snd R₁ M₁ M₂, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.coe_fst {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] :

↑(ContinuousLinearMap.fst R₁ M₁ M₂) = LinearMap.fst R₁ M₁ M₂

@[simp]

theorem ContinuousLinearMap.coe_fst' {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] :

⇑(ContinuousLinearMap.fst R₁ M₁ M₂) = Prod.fst

@[simp]

theorem ContinuousLinearMap.coe_snd {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] :

↑(ContinuousLinearMap.snd R₁ M₁ M₂) = LinearMap.snd R₁ M₁ M₂

@[simp]

theorem ContinuousLinearMap.coe_snd' {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] :

⇑(ContinuousLinearMap.snd R₁ M₁ M₂) = Prod.snd

@[simp]

theorem ContinuousLinearMap.fst_prod_snd {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] :

ContinuousLinearMap.prod (ContinuousLinearMap.fst R₁ M₁ M₂) (ContinuousLinearMap.snd R₁ M₁ M₂) = ContinuousLinearMap.id R₁ (M₁ × M₂)

@[simp]

theorem ContinuousLinearMap.fst_comp_prod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] (f : M₁ →L[R₁] M₂) (g : M₁ →L[R₁] M₃) :

ContinuousLinearMap.comp (ContinuousLinearMap.fst R₁ M₂ M₃) (ContinuousLinearMap.prod f g) = f

@[simp]

theorem ContinuousLinearMap.snd_comp_prod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] (f : M₁ →L[R₁] M₂) (g : M₁ →L[R₁] M₃) :

ContinuousLinearMap.comp (ContinuousLinearMap.snd R₁ M₂ M₃) (ContinuousLinearMap.prod f g) = g

def ContinuousLinearMap.prodMap {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] {M₄ : Type u_8} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [Module R₁ M₄] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₃ →L[R₁] M₄) :

M₁ × M₃ →L[R₁] M₂ × M₄

Prod.map of two continuous linear maps.

Equations

ContinuousLinearMap.prodMap f₁ f₂ = ContinuousLinearMap.prod (ContinuousLinearMap.comp f₁ (ContinuousLinearMap.fst R₁ M₁ M₃)) (ContinuousLinearMap.comp f₂ (ContinuousLinearMap.snd R₁ M₁ M₃))

@[simp]

theorem ContinuousLinearMap.coe_prodMap {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] {M₄ : Type u_8} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [Module R₁ M₄] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₃ →L[R₁] M₄) :

↑(ContinuousLinearMap.prodMap f₁ f₂) = LinearMap.prodMap ↑f₁ ↑f₂

@[simp]

theorem ContinuousLinearMap.coe_prodMap' {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] {M₄ : Type u_8} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [Module R₁ M₄] (f₁ : M₁ →L[R₁] M₂) (f₂ : M₃ →L[R₁] M₄) :

⇑(ContinuousLinearMap.prodMap f₁ f₂) = Prod.map ⇑f₁ ⇑f₂

def ContinuousLinearMap.coprod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [ContinuousAdd M₃] (f₁ : M₁ →L[R₁] M₃) (f₂ : M₂ →L[R₁] M₃) :

M₁ × M₂ →L[R₁] M₃

The continuous linear map given by (x, y) ↦ f₁ x + f₂ y.

Equations

ContinuousLinearMap.coprod f₁ f₂ = { toLinearMap := LinearMap.coprod ↑f₁ ↑f₂, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.coe_coprod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [ContinuousAdd M₃] (f₁ : M₁ →L[R₁] M₃) (f₂ : M₂ →L[R₁] M₃) :

↑(ContinuousLinearMap.coprod f₁ f₂) = LinearMap.coprod ↑f₁ ↑f₂

@[simp]

theorem ContinuousLinearMap.coprod_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [ContinuousAdd M₃] (f₁ : M₁ →L[R₁] M₃) (f₂ : M₂ →L[R₁] M₃) (x : M₁ × M₂) :

(ContinuousLinearMap.coprod f₁ f₂) x = f₁ x.1 + f₂ x.2

theorem ContinuousLinearMap.range_coprod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [ContinuousAdd M₃] (f₁ : M₁ →L[R₁] M₃) (f₂ : M₂ →L[R₁] M₃) :

LinearMap.range (ContinuousLinearMap.coprod f₁ f₂) = LinearMap.range f₁ ⊔ LinearMap.range f₂

theorem ContinuousLinearMap.comp_fst_add_comp_snd {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [ContinuousAdd M₃] (f : M₁ →L[R₁] M₃) (g : M₂ →L[R₁] M₃) :

ContinuousLinearMap.comp f (ContinuousLinearMap.fst R₁ M₁ M₂) + ContinuousLinearMap.comp g (ContinuousLinearMap.snd R₁ M₁ M₂) = ContinuousLinearMap.coprod f g

theorem ContinuousLinearMap.coprod_inl_inr {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M'₁ : Type u_5} [TopologicalSpace M'₁] [AddCommMonoid M'₁] [Module R₁ M₁] [Module R₁ M'₁] [ContinuousAdd M₁] [ContinuousAdd M'₁] :

ContinuousLinearMap.coprod (ContinuousLinearMap.inl R₁ M₁ M'₁) (ContinuousLinearMap.inr R₁ M₁ M'₁) = ContinuousLinearMap.id R₁ (M₁ × M'₁)

def ContinuousLinearMap.smulRight {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {R : Type u_10} {S : Type u_11} [Semiring R] [Semiring S] [Module R M₁] [Module R M₂] [Module R S] [Module S M₂] [IsScalarTower R S M₂] [TopologicalSpace S] [ContinuousSMul S M₂] (c : M₁ →L[R] S) (f : M₂) :

M₁ →L[R] M₂

The linear map fun x => c x • f. Associates to a scalar-valued linear map and an element of M₂ the M₂-valued linear map obtained by multiplying the two (a.k.a. tensoring by M₂). See also ContinuousLinearMap.smulRightₗ and ContinuousLinearMap.smulRightL.

Equations

ContinuousLinearMap.smulRight c f = let __src := LinearMap.smulRight (↑c) f; { toLinearMap := __src, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.smulRight_apply {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {R : Type u_10} {S : Type u_11} [Semiring R] [Semiring S] [Module R M₁] [Module R M₂] [Module R S] [Module S M₂] [IsScalarTower R S M₂] [TopologicalSpace S] [ContinuousSMul S M₂] {c : M₁ →L[R] S} {f : M₂} {x : M₁} :

(ContinuousLinearMap.smulRight c f) x = c x • f

@[simp]

theorem ContinuousLinearMap.smulRight_one_one {R₁ : Type u_1} [Semiring R₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₂] [TopologicalSpace R₁] [ContinuousSMul R₁ M₂] (c : R₁ →L[R₁] M₂) :

ContinuousLinearMap.smulRight 1 (c 1) = c

@[simp]

theorem ContinuousLinearMap.smulRight_one_eq_iff {R₁ : Type u_1} [Semiring R₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₂] [TopologicalSpace R₁] [ContinuousSMul R₁ M₂] {f : M₂} {f' : M₂} :

ContinuousLinearMap.smulRight 1 f = ContinuousLinearMap.smulRight 1 f' ↔ f = f'

theorem ContinuousLinearMap.smulRight_comp {R₁ : Type u_1} [Semiring R₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₂] [TopologicalSpace R₁] [ContinuousSMul R₁ M₂] [ContinuousMul R₁] {x : M₂} {c : R₁} :

ContinuousLinearMap.comp (ContinuousLinearMap.smulRight 1 x) (ContinuousLinearMap.smulRight 1 c) = ContinuousLinearMap.smulRight 1 (c • x)

def ContinuousLinearMap.toSpanSingleton (R₁ : Type u_1) [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace R₁] [ContinuousSMul R₁ M₁] (x : M₁) :

R₁ →L[R₁] M₁

Given an element x of a topological space M over a semiring R, the natural continuous linear map from R to M by taking multiples of x.

Equations

ContinuousLinearMap.toSpanSingleton R₁ x = { toLinearMap := LinearMap.toSpanSingleton R₁ M₁ x, cont := ⋯ }

theorem ContinuousLinearMap.toSpanSingleton_apply (R₁ : Type u_1) [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace R₁] [ContinuousSMul R₁ M₁] (x : M₁) (r : R₁) :

(ContinuousLinearMap.toSpanSingleton R₁ x) r = r • x

theorem ContinuousLinearMap.toSpanSingleton_add (R₁ : Type u_1) [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace R₁] [ContinuousSMul R₁ M₁] [ContinuousAdd M₁] (x : M₁) (y : M₁) :

ContinuousLinearMap.toSpanSingleton R₁ (x + y) = ContinuousLinearMap.toSpanSingleton R₁ x + ContinuousLinearMap.toSpanSingleton R₁ y

theorem ContinuousLinearMap.toSpanSingleton_smul' (R₁ : Type u_1) [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace R₁] [ContinuousSMul R₁ M₁] {α : Type u_10} [Monoid α] [DistribMulAction α M₁] [ContinuousConstSMul α M₁] [SMulCommClass R₁ α M₁] (c : α) (x : M₁) :

ContinuousLinearMap.toSpanSingleton R₁ (c • x) = c • ContinuousLinearMap.toSpanSingleton R₁ x

theorem ContinuousLinearMap.toSpanSingleton_smul (R : Type u_10) {M₁ : Type u_11} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [TopologicalSpace R] [TopologicalSpace M₁] [ContinuousSMul R M₁] (c : R) (x : M₁) :

ContinuousLinearMap.toSpanSingleton R (c • x) = c • ContinuousLinearMap.toSpanSingleton R x

A special case of to_span_singleton_smul' for when R is commutative.

def ContinuousLinearMap.pi {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {ι : Type u_4} {φ : ι → Type u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M →L[R] φ i) :

M →L[R] (i : ι) → φ i

pi construction for continuous linear functions. From a family of continuous linear functions it produces a continuous linear function into a family of topological modules.

Equations

ContinuousLinearMap.pi f = { toLinearMap := LinearMap.pi fun (i : ι) => ↑(f i), cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.coe_pi' {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {ι : Type u_4} {φ : ι → Type u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M →L[R] φ i) :

⇑(ContinuousLinearMap.pi f) = fun (c : M) (i : ι) => (f i) c

@[simp]

theorem ContinuousLinearMap.coe_pi {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {ι : Type u_4} {φ : ι → Type u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M →L[R] φ i) :

↑(ContinuousLinearMap.pi f) = LinearMap.pi fun (i : ι) => ↑(f i)

theorem ContinuousLinearMap.pi_apply {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {ι : Type u_4} {φ : ι → Type u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M →L[R] φ i) (c : M) (i : ι) :

(ContinuousLinearMap.pi f) c i = (f i) c

theorem ContinuousLinearMap.pi_eq_zero {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {ι : Type u_4} {φ : ι → Type u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M →L[R] φ i) :

ContinuousLinearMap.pi f = 0 ↔ ∀ (i : ι), f i = 0

theorem ContinuousLinearMap.pi_zero {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {ι : Type u_4} {φ : ι → Type u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] :

(ContinuousLinearMap.pi fun (x : ι) => 0) = 0

theorem ContinuousLinearMap.pi_comp {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {ι : Type u_4} {φ : ι → Type u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M →L[R] φ i) (g : M₂ →L[R] M) :

ContinuousLinearMap.comp (ContinuousLinearMap.pi f) g = ContinuousLinearMap.pi fun (i : ι) => ContinuousLinearMap.comp (f i) g

def ContinuousLinearMap.proj {R : Type u_1} [Semiring R] {ι : Type u_4} {φ : ι → Type u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) :

((i : ι) → φ i) →L[R] φ i

The projections from a family of topological modules are continuous linear maps.

Equations

ContinuousLinearMap.proj i = { toLinearMap := LinearMap.proj i, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.proj_apply {R : Type u_1} [Semiring R] {ι : Type u_4} {φ : ι → Type u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) (b : (i : ι) → φ i) :

(ContinuousLinearMap.proj i) b = b i

theorem ContinuousLinearMap.proj_pi {R : Type u_1} [Semiring R] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {ι : Type u_4} {φ : ι → Type u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (f : (i : ι) → M₂ →L[R] φ i) (i : ι) :

ContinuousLinearMap.comp (ContinuousLinearMap.proj i) (ContinuousLinearMap.pi f) = f i

theorem ContinuousLinearMap.iInf_ker_proj {R : Type u_1} [Semiring R] {ι : Type u_4} {φ : ι → Type u_5} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] :

⨅ (i : ι), LinearMap.ker (ContinuousLinearMap.proj i) = ⊥

def ContinuousLinearMap.iInfKerProjEquiv (R : Type u_1) [Semiring R] {ι : Type u_4} (φ : ι → Type u_5) [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {I : Set ι} {J : Set ι} [DecidablePred fun (i : ι) => i ∈ I] (hd : Disjoint I J) (hu : Set.univ ⊆ I ∪ J) :

↥(⨅ i ∈ J, LinearMap.ker (ContinuousLinearMap.proj i)) ≃L[R] (i : ↑I) → φ ↑i

If I and J are complementary index sets, the product of the kernels of the Jth projections of φ is linearly equivalent to the product over I.

Equations

ContinuousLinearMap.iInfKerProjEquiv R φ hd hu = { toLinearEquiv := LinearMap.iInfKerProjEquiv R φ hd hu, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem ContinuousLinearMap.map_neg {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →SL[σ₁₂] M₂) (x : M) :

f (-x) = -f x

theorem ContinuousLinearMap.map_sub {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →SL[σ₁₂] M₂) (x : M) (y : M) :

f (x - y) = f x - f y

@[simp]

theorem ContinuousLinearMap.sub_apply' {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →SL[σ₁₂] M₂) (g : M →SL[σ₁₂] M₂) (x : M) :

(↑f - ↑g) x = f x - g x

theorem ContinuousLinearMap.range_prod_eq {R : Type u_1} [Ring R] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] {M₃ : Type u_6} [TopologicalSpace M₃] [AddCommGroup M₃] [Module R M] [Module R M₂] [Module R M₃] {f : M →L[R] M₂} {g : M →L[R] M₃} (h : LinearMap.ker f ⊔ LinearMap.ker g = ⊤) :

LinearMap.range (ContinuousLinearMap.prod f g) = Submodule.prod (LinearMap.range f) (LinearMap.range g)

theorem ContinuousLinearMap.ker_prod_ker_le_ker_coprod {R : Type u_1} [Ring R] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] {M₃ : Type u_6} [TopologicalSpace M₃] [AddCommGroup M₃] [Module R M] [Module R M₂] [Module R M₃] [ContinuousAdd M₃] (f : M →L[R] M₃) (g : M₂ →L[R] M₃) :

Submodule.prod (LinearMap.ker f) (LinearMap.ker g) ≤ LinearMap.ker (ContinuousLinearMap.coprod f g)

theorem ContinuousLinearMap.ker_coprod_of_disjoint_range {R : Type u_1} [Ring R] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] {M₃ : Type u_6} [TopologicalSpace M₃] [AddCommGroup M₃] [Module R M] [Module R M₂] [Module R M₃] [ContinuousAdd M₃] (f : M →L[R] M₃) (g : M₂ →L[R] M₃) (hd : Disjoint (LinearMap.range f) (LinearMap.range g)) :

LinearMap.ker (ContinuousLinearMap.coprod f g) = Submodule.prod (LinearMap.ker f) (LinearMap.ker g)

instance ContinuousLinearMap.neg {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [TopologicalAddGroup M₂] :

Neg (M →SL[σ₁₂] M₂)

Equations

ContinuousLinearMap.neg = { neg := fun (f : M →SL[σ₁₂] M₂) => { toLinearMap := -↑f, cont := ⋯ } }

@[simp]

theorem ContinuousLinearMap.neg_apply {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [TopologicalAddGroup M₂] (f : M →SL[σ₁₂] M₂) (x : M) :

(-f) x = -f x

@[simp]

theorem ContinuousLinearMap.coe_neg {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [TopologicalAddGroup M₂] (f : M →SL[σ₁₂] M₂) :

↑(-f) = -↑f

theorem ContinuousLinearMap.coe_neg' {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [TopologicalAddGroup M₂] (f : M →SL[σ₁₂] M₂) :

⇑(-f) = -⇑f

instance ContinuousLinearMap.sub {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [TopologicalAddGroup M₂] :

Sub (M →SL[σ₁₂] M₂)

Equations

ContinuousLinearMap.sub = { sub := fun (f g : M →SL[σ₁₂] M₂) => { toLinearMap := ↑f - ↑g, cont := ⋯ } }

instance ContinuousLinearMap.addCommGroup {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [TopologicalAddGroup M₂] :

AddCommGroup (M →SL[σ₁₂] M₂)

Equations

ContinuousLinearMap.addCommGroup = let __src := ContinuousLinearMap.addCommMonoid; AddCommGroup.mk ⋯

theorem ContinuousLinearMap.sub_apply {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [TopologicalAddGroup M₂] (f : M →SL[σ₁₂] M₂) (g : M →SL[σ₁₂] M₂) (x : M) :

(f - g) x = f x - g x

@[simp]

theorem ContinuousLinearMap.coe_sub {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [TopologicalAddGroup M₂] (f : M →SL[σ₁₂] M₂) (g : M →SL[σ₁₂] M₂) :

↑(f - g) = ↑f - ↑g

@[simp]

theorem ContinuousLinearMap.coe_sub' {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [TopologicalAddGroup M₂] (f : M →SL[σ₁₂] M₂) (g : M →SL[σ₁₂] M₂) :

⇑(f - g) = ⇑f - ⇑g

@[simp]

theorem ContinuousLinearMap.comp_neg {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {R₃ : Type u_3} [Ring R₃] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] {M₃ : Type u_6} [TopologicalSpace M₃] [AddCommGroup M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [TopologicalAddGroup M₂] [TopologicalAddGroup M₃] (g : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) :

ContinuousLinearMap.comp g (-f) = -ContinuousLinearMap.comp g f

@[simp]

theorem ContinuousLinearMap.neg_comp {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {R₃ : Type u_3} [Ring R₃] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] {M₃ : Type u_6} [TopologicalSpace M₃] [AddCommGroup M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [TopologicalAddGroup M₃] (g : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) :

ContinuousLinearMap.comp (-g) f = -ContinuousLinearMap.comp g f

@[simp]

theorem ContinuousLinearMap.comp_sub {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {R₃ : Type u_3} [Ring R₃] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] {M₃ : Type u_6} [TopologicalSpace M₃] [AddCommGroup M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [TopologicalAddGroup M₂] [TopologicalAddGroup M₃] (g : M₂ →SL[σ₂₃] M₃) (f₁ : M →SL[σ₁₂] M₂) (f₂ : M →SL[σ₁₂] M₂) :

ContinuousLinearMap.comp g (f₁ - f₂) = ContinuousLinearMap.comp g f₁ - ContinuousLinearMap.comp g f₂

@[simp]

theorem ContinuousLinearMap.sub_comp {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {R₃ : Type u_3} [Ring R₃] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] {M₃ : Type u_6} [TopologicalSpace M₃] [AddCommGroup M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [TopologicalAddGroup M₃] (g₁ : M₂ →SL[σ₂₃] M₃) (g₂ : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) :

ContinuousLinearMap.comp (g₁ - g₂) f = ContinuousLinearMap.comp g₁ f - ContinuousLinearMap.comp g₂ f

instance ContinuousLinearMap.ring {R : Type u_1} [Ring R] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] [Module R M] [TopologicalAddGroup M] :

Ring (M →L[R] M)

Equations

ContinuousLinearMap.ring = let __spread.0 := ContinuousLinearMap.semiring; let __spread.1 := ContinuousLinearMap.addCommGroup; Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem ContinuousLinearMap.intCast_apply {R : Type u_1} [Ring R] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] [Module R M] [TopologicalAddGroup M] (z : ℤ) (m : M) :

↑z m = z • m

theorem ContinuousLinearMap.smulRight_one_pow {R : Type u_1} [Ring R] [TopologicalSpace R] [TopologicalRing R] (c : R) (n : ℕ) :

ContinuousLinearMap.smulRight 1 c ^ n = ContinuousLinearMap.smulRight 1 (c ^ n)

def ContinuousLinearMap.projKerOfRightInverse {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [TopologicalAddGroup M] (f₁ : M →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M) (h : Function.RightInverse ⇑f₂ ⇑f₁) :

M →L[R] ↥(LinearMap.ker f₁)

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₂.

Equations

ContinuousLinearMap.projKerOfRightInverse f₁ f₂ h = ContinuousLinearMap.codRestrict (ContinuousLinearMap.id R M - ContinuousLinearMap.comp f₂ f₁) (LinearMap.ker f₁) ⋯

@[simp]

theorem ContinuousLinearMap.coe_projKerOfRightInverse_apply {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [TopologicalAddGroup M] (f₁ : M →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M) (h : Function.RightInverse ⇑f₂ ⇑f₁) (x : M) :

↑((ContinuousLinearMap.projKerOfRightInverse f₁ f₂ h) x) = x - f₂ (f₁ x)

@[simp]

theorem ContinuousLinearMap.projKerOfRightInverse_apply_idem {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [TopologicalAddGroup M] (f₁ : M →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M) (h : Function.RightInverse ⇑f₂ ⇑f₁) (x : ↥(LinearMap.ker f₁)) :

(ContinuousLinearMap.projKerOfRightInverse f₁ f₂ h) ↑x = x

@[simp]

theorem ContinuousLinearMap.projKerOfRightInverse_comp_inv {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_4} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_5} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [TopologicalAddGroup M] (f₁ : M →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M) (h : Function.RightInverse ⇑f₂ ⇑f₁) (y : M₂) :

(ContinuousLinearMap.projKerOfRightInverse f₁ f₂ h) (f₂ y) = 0

theorem ContinuousLinearMap.isOpenMap_of_ne_zero {R : Type u_1} {M : Type u_2} [TopologicalSpace R] [DivisionRing R] [ContinuousSub R] [AddCommGroup M] [TopologicalSpace M] [ContinuousAdd M] [Module R M] [ContinuousSMul R M] (f : M →L[R] R) (hf : f ≠ 0) :

A nonzero continuous linear functional is open.

@[simp]

theorem ContinuousLinearMap.smul_comp {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {S₃ : Type u_5} [Semiring R] [Semiring R₂] [Semiring R₃] [Monoid S₃] {M : Type u_6} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {M₂ : Type u_7} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] {M₃ : Type u_8} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₃ M₃] [DistribMulAction S₃ M₃] [SMulCommClass R₃ S₃ M₃] [ContinuousConstSMul S₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (c : S₃) (h : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) :

ContinuousLinearMap.comp (c • h) f = c • ContinuousLinearMap.comp h f

@[simp]

theorem ContinuousLinearMap.comp_smul {R : Type u_1} {S : Type u_4} [Semiring R] [Monoid S] {M : Type u_6} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {N₂ : Type u_9} [TopologicalSpace N₂] [AddCommMonoid N₂] [Module R N₂] {N₃ : Type u_10} [TopologicalSpace N₃] [AddCommMonoid N₃] [Module R N₃] [DistribMulAction S N₃] [SMulCommClass R S N₃] [ContinuousConstSMul S N₃] [DistribMulAction S N₂] [ContinuousConstSMul S N₂] [SMulCommClass R S N₂] [LinearMap.CompatibleSMul N₂ N₃ S R] (hₗ : N₂ →L[R] N₃) (c : S) (fₗ : M →L[R] N₂) :

ContinuousLinearMap.comp hₗ (c • fₗ) = c • ContinuousLinearMap.comp hₗ fₗ

@[simp]

theorem ContinuousLinearMap.comp_smulₛₗ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R] [Semiring R₂] [Semiring R₃] {M : Type u_6} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {M₂ : Type u_7} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] {M₃ : Type u_8} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [SMulCommClass R₂ R₂ M₂] [SMulCommClass R₃ R₃ M₃] [ContinuousConstSMul R₂ M₂] [ContinuousConstSMul R₃ M₃] (h : M₂ →SL[σ₂₃] M₃) (c : R₂) (f : M →SL[σ₁₂] M₂) :

ContinuousLinearMap.comp h (c • f) = σ₂₃ c • ContinuousLinearMap.comp h f

instance ContinuousLinearMap.distribMulAction {R : Type u_1} {R₂ : Type u_2} {S₃ : Type u_5} [Semiring R] [Semiring R₂] [Monoid S₃] {M : Type u_6} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {M₂ : Type u_7} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [DistribMulAction S₃ M₂] [ContinuousConstSMul S₃ M₂] [SMulCommClass R₂ S₃ M₂] [ContinuousAdd M₂] :

DistribMulAction S₃ (M →SL[σ₁₂] M₂)

Equations

ContinuousLinearMap.distribMulAction = DistribMulAction.mk ⋯ ⋯

@[simp]

theorem ContinuousLinearMap.prodEquiv_apply {R : Type u_1} [Semiring R] {M : Type u_6} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {N₂ : Type u_9} [TopologicalSpace N₂] [AddCommMonoid N₂] [Module R N₂] {N₃ : Type u_10} [TopologicalSpace N₃] [AddCommMonoid N₃] [Module R N₃] (f : (M →L[R] N₂) × (M →L[R] N₃)) :

ContinuousLinearMap.prodEquiv f = ContinuousLinearMap.prod f.1 f.2

def ContinuousLinearMap.prodEquiv {R : Type u_1} [Semiring R] {M : Type u_6} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {N₂ : Type u_9} [TopologicalSpace N₂] [AddCommMonoid N₂] [Module R N₂] {N₃ : Type u_10} [TopologicalSpace N₃] [AddCommMonoid N₃] [Module R N₃] :

(M →L[R] N₂) × (M →L[R] N₃) ≃ (M →L[R] N₂ × N₃)

ContinuousLinearMap.prod as an Equiv.

Equations

One or more equations did not get rendered due to their size.

theorem ContinuousLinearMap.prod_ext_iff {R : Type u_1} [Semiring R] {M : Type u_6} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {N₂ : Type u_9} [TopologicalSpace N₂] [AddCommMonoid N₂] [Module R N₂] {N₃ : Type u_10} [TopologicalSpace N₃] [AddCommMonoid N₃] [Module R N₃] {f : M × N₂ →L[R] N₃} {g : M × N₂ →L[R] N₃} :

f = g ↔ ContinuousLinearMap.comp f (ContinuousLinearMap.inl R M N₂) = ContinuousLinearMap.comp g (ContinuousLinearMap.inl R M N₂) ∧ ContinuousLinearMap.comp f (ContinuousLinearMap.inr R M N₂) = ContinuousLinearMap.comp g (ContinuousLinearMap.inr R M N₂)

theorem ContinuousLinearMap.prod_ext {R : Type u_1} [Semiring R] {M : Type u_6} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {N₂ : Type u_9} [TopologicalSpace N₂] [AddCommMonoid N₂] [Module R N₂] {N₃ : Type u_10} [TopologicalSpace N₃] [AddCommMonoid N₃] [Module R N₃] {f : M × N₂ →L[R] N₃} {g : M × N₂ →L[R] N₃} (hl : ContinuousLinearMap.comp f (ContinuousLinearMap.inl R M N₂) = ContinuousLinearMap.comp g (ContinuousLinearMap.inl R M N₂)) (hr : ContinuousLinearMap.comp f (ContinuousLinearMap.inr R M N₂) = ContinuousLinearMap.comp g (ContinuousLinearMap.inr R M N₂)) :

f = g

instance ContinuousLinearMap.module {R : Type u_1} {R₃ : Type u_3} {S₃ : Type u_5} [Semiring R] [Semiring R₃] [Semiring S₃] {M : Type u_6} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {M₃ : Type u_8} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₃ M₃] [Module S₃ M₃] [SMulCommClass R₃ S₃ M₃] [ContinuousConstSMul S₃ M₃] {σ₁₃ : R →+* R₃} [ContinuousAdd M₃] :

Module S₃ (M →SL[σ₁₃] M₃)

Equations

ContinuousLinearMap.module = Module.mk ⋯ ⋯

instance ContinuousLinearMap.isCentralScalar {R : Type u_1} {R₃ : Type u_3} {S₃ : Type u_5} [Semiring R] [Semiring R₃] [Semiring S₃] {M : Type u_6} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {M₃ : Type u_8} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₃ M₃] [Module S₃ M₃] [SMulCommClass R₃ S₃ M₃] [ContinuousConstSMul S₃ M₃] {σ₁₃ : R →+* R₃} [ContinuousAdd M₃] [Module S₃ᵐᵒᵖ M₃] [IsCentralScalar S₃ M₃] :

IsCentralScalar S₃ (M →SL[σ₁₃] M₃)

Equations

⋯ = ⋯

@[simp]

theorem ContinuousLinearMap.prodₗ_apply {R : Type u_1} (S : Type u_4) [Semiring R] [Semiring S] {M : Type u_6} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {N₂ : Type u_9} [TopologicalSpace N₂] [AddCommMonoid N₂] [Module R N₂] {N₃ : Type u_10} [TopologicalSpace N₃] [AddCommMonoid N₃] [Module R N₃] [Module S N₂] [ContinuousConstSMul S N₂] [SMulCommClass R S N₂] [Module S N₃] [SMulCommClass R S N₃] [ContinuousConstSMul S N₃] [ContinuousAdd N₂] [ContinuousAdd N₃] :

∀ (a : (M →L[R] N₂) × (M →L[R] N₃)), (ContinuousLinearMap.prodₗ S) a = ContinuousLinearMap.prodEquiv.toFun a

def ContinuousLinearMap.prodₗ {R : Type u_1} (S : Type u_4) [Semiring R] [Semiring S] {M : Type u_6} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {N₂ : Type u_9} [TopologicalSpace N₂] [AddCommMonoid N₂] [Module R N₂] {N₃ : Type u_10} [TopologicalSpace N₃] [AddCommMonoid N₃] [Module R N₃] [Module S N₂] [ContinuousConstSMul S N₂] [SMulCommClass R S N₂] [Module S N₃] [SMulCommClass R S N₃] [ContinuousConstSMul S N₃] [ContinuousAdd N₂] [ContinuousAdd N₃] :

((M →L[R] N₂) × (M →L[R] N₃)) ≃ₗ[S] M →L[R] N₂ × N₃

ContinuousLinearMap.prod as a LinearEquiv.

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousLinearMap.coeLM_apply {R : Type u_1} (S : Type u_4) [Semiring R] [Semiring S] {M : Type u_6} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {N₃ : Type u_10} [TopologicalSpace N₃] [AddCommMonoid N₃] [Module R N₃] [Module S N₃] [SMulCommClass R S N₃] [ContinuousConstSMul S N₃] [ContinuousAdd N₃] (self : M →L[R] N₃) :

(ContinuousLinearMap.coeLM S) self = ↑self

def ContinuousLinearMap.coeLM {R : Type u_1} (S : Type u_4) [Semiring R] [Semiring S] {M : Type u_6} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {N₃ : Type u_10} [TopologicalSpace N₃] [AddCommMonoid N₃] [Module R N₃] [Module S N₃] [SMulCommClass R S N₃] [ContinuousConstSMul S N₃] [ContinuousAdd N₃] :

(M →L[R] N₃) →ₗ[S] M →ₗ[R] N₃

The coercion from M →L[R] M₂ to M →ₗ[R] M₂, as a linear map.

Equations

ContinuousLinearMap.coeLM S = { toAddHom := { toFun := ContinuousLinearMap.toLinearMap, map_add' := ⋯ }, map_smul' := ⋯ }

@[simp]

theorem ContinuousLinearMap.coeLMₛₗ_apply {R : Type u_1} {R₃ : Type u_3} {S₃ : Type u_5} [Semiring R] [Semiring R₃] [Semiring S₃] {M : Type u_6} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {M₃ : Type u_8} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₃ M₃] [Module S₃ M₃] [SMulCommClass R₃ S₃ M₃] [ContinuousConstSMul S₃ M₃] (σ₁₃ : R →+* R₃) [ContinuousAdd M₃] (self : M →SL[σ₁₃] M₃) :

(ContinuousLinearMap.coeLMₛₗ σ₁₃) self = ↑self

def ContinuousLinearMap.coeLMₛₗ {R : Type u_1} {R₃ : Type u_3} {S₃ : Type u_5} [Semiring R] [Semiring R₃] [Semiring S₃] {M : Type u_6} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {M₃ : Type u_8} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₃ M₃] [Module S₃ M₃] [SMulCommClass R₃ S₃ M₃] [ContinuousConstSMul S₃ M₃] (σ₁₃ : R →+* R₃) [ContinuousAdd M₃] :

(M →SL[σ₁₃] M₃) →ₗ[S₃] M →ₛₗ[σ₁₃] M₃

The coercion from M →SL[σ] M₂ to M →ₛₗ[σ] M₂, as a linear map.

Equations

ContinuousLinearMap.coeLMₛₗ σ₁₃ = { toAddHom := { toFun := ContinuousLinearMap.toLinearMap, map_add' := ⋯ }, map_smul' := ⋯ }

def ContinuousLinearMap.smulRightₗ {R : Type u_1} {S : Type u_2} {T : Type u_3} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring S] [Semiring T] [Module R S] [AddCommMonoid M₂] [Module R M₂] [Module S M₂] [IsScalarTower R S M₂] [TopologicalSpace S] [TopologicalSpace M₂] [ContinuousSMul S M₂] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousAdd M₂] [Module T M₂] [ContinuousConstSMul T M₂] [SMulCommClass R T M₂] [SMulCommClass S T M₂] (c : M →L[R] S) :

M₂ →ₗ[T] M →L[R] M₂

Given c : E →L[𝕜] 𝕜, c.smulRightₗ is the linear map from F to E →L[𝕜] F sending f to fun e => c e • f. See also ContinuousLinearMap.smulRightL.

Equations

ContinuousLinearMap.smulRightₗ c = { toAddHom := { toFun := ContinuousLinearMap.smulRight c, map_add' := ⋯ }, map_smul' := ⋯ }

@[simp]

theorem ContinuousLinearMap.coe_smulRightₗ {R : Type u_1} {S : Type u_2} {T : Type u_3} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring S] [Semiring T] [Module R S] [AddCommMonoid M₂] [Module R M₂] [Module S M₂] [IsScalarTower R S M₂] [TopologicalSpace S] [TopologicalSpace M₂] [ContinuousSMul S M₂] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousAdd M₂] [Module T M₂] [ContinuousConstSMul T M₂] [SMulCommClass R T M₂] [SMulCommClass S T M₂] (c : M →L[R] S) :

⇑(ContinuousLinearMap.smulRightₗ c) = ContinuousLinearMap.smulRight c

instance ContinuousLinearMap.algebra {R : Type u_1} [CommRing R] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M₂] [TopologicalAddGroup M₂] [ContinuousConstSMul R M₂] :

Algebra R (M₂ →L[R] M₂)

Equations

ContinuousLinearMap.algebra = Algebra.ofModule ⋯ ⋯

@[simp]

theorem ContinuousLinearMap.algebraMap_apply {R : Type u_1} [CommRing R] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M₂] [TopologicalAddGroup M₂] [ContinuousConstSMul R M₂] (r : R) (m : M₂) :

((algebraMap R (M₂ →L[R] M₂)) r) m = r • m

def ContinuousLinearMap.restrictScalars {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring A] [AddCommGroup M] [AddCommGroup M₂] [Module A M] [Module A M₂] [TopologicalSpace M] [TopologicalSpace M₂] (R : Type u_4) [Ring R] [Module R M] [Module R M₂] [LinearMap.CompatibleSMul M M₂ R A] (f : M →L[A] M₂) :

M →L[R] M₂

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.

Equations

ContinuousLinearMap.restrictScalars R f = { toLinearMap := ↑R ↑f, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.coe_restrictScalars {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring A] [AddCommGroup M] [AddCommGroup M₂] [Module A M] [Module A M₂] [TopologicalSpace M] [TopologicalSpace M₂] {R : Type u_4} [Ring R] [Module R M] [Module R M₂] [LinearMap.CompatibleSMul M M₂ R A] (f : M →L[A] M₂) :

↑(ContinuousLinearMap.restrictScalars R f) = ↑R ↑f

@[simp]

theorem ContinuousLinearMap.coe_restrictScalars' {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring A] [AddCommGroup M] [AddCommGroup M₂] [Module A M] [Module A M₂] [TopologicalSpace M] [TopologicalSpace M₂] {R : Type u_4} [Ring R] [Module R M] [Module R M₂] [LinearMap.CompatibleSMul M M₂ R A] (f : M →L[A] M₂) :

⇑(ContinuousLinearMap.restrictScalars R f) = ⇑f

@[simp]

theorem ContinuousLinearMap.restrictScalars_zero {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring A] [AddCommGroup M] [AddCommGroup M₂] [Module A M] [Module A M₂] [TopologicalSpace M] [TopologicalSpace M₂] {R : Type u_4} [Ring R] [Module R M] [Module R M₂] [LinearMap.CompatibleSMul M M₂ R A] :

ContinuousLinearMap.restrictScalars R 0 = 0

@[simp]

theorem ContinuousLinearMap.restrictScalars_add {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring A] [AddCommGroup M] [AddCommGroup M₂] [Module A M] [Module A M₂] [TopologicalSpace M] [TopologicalSpace M₂] {R : Type u_4} [Ring R] [Module R M] [Module R M₂] [LinearMap.CompatibleSMul M M₂ R A] [TopologicalAddGroup M₂] (f : M →L[A] M₂) (g : M →L[A] M₂) :

ContinuousLinearMap.restrictScalars R (f + g) = ContinuousLinearMap.restrictScalars R f + ContinuousLinearMap.restrictScalars R g

@[simp]

theorem ContinuousLinearMap.restrictScalars_neg {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring A] [AddCommGroup M] [AddCommGroup M₂] [Module A M] [Module A M₂] [TopologicalSpace M] [TopologicalSpace M₂] {R : Type u_4} [Ring R] [Module R M] [Module R M₂] [LinearMap.CompatibleSMul M M₂ R A] [TopologicalAddGroup M₂] (f : M →L[A] M₂) :

ContinuousLinearMap.restrictScalars R (-f) = -ContinuousLinearMap.restrictScalars R f

@[simp]

theorem ContinuousLinearMap.restrictScalars_smul {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring A] [AddCommGroup M] [AddCommGroup M₂] [Module A M] [Module A M₂] [TopologicalSpace M] [TopologicalSpace M₂] {R : Type u_4} [Ring R] [Module R M] [Module R M₂] [LinearMap.CompatibleSMul M M₂ R A] {S : Type u_5} [Ring S] [Module S M₂] [ContinuousConstSMul S M₂] [SMulCommClass A S M₂] [SMulCommClass R S M₂] (c : S) (f : M →L[A] M₂) :

ContinuousLinearMap.restrictScalars R (c • f) = c • ContinuousLinearMap.restrictScalars R f

def ContinuousLinearMap.restrictScalarsₗ (A : Type u_1) (M : Type u_2) (M₂ : Type u_3) [Ring A] [AddCommGroup M] [AddCommGroup M₂] [Module A M] [Module A M₂] [TopologicalSpace M] [TopologicalSpace M₂] (R : Type u_4) [Ring R] [Module R M] [Module R M₂] [LinearMap.CompatibleSMul M M₂ R A] (S : Type u_5) [Ring S] [Module S M₂] [ContinuousConstSMul S M₂] [SMulCommClass A S M₂] [SMulCommClass R S M₂] [TopologicalAddGroup M₂] :

(M →L[A] M₂) →ₗ[S] M →L[R] M₂

ContinuousLinearMap.restrictScalars as a LinearMap. See also ContinuousLinearMap.restrictScalarsL.

Equations

ContinuousLinearMap.restrictScalarsₗ A M M₂ R S = { toAddHom := { toFun := ContinuousLinearMap.restrictScalars R, map_add' := ⋯ }, map_smul' := ⋯ }

@[simp]

theorem ContinuousLinearMap.coe_restrictScalarsₗ {A : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring A] [AddCommGroup M] [AddCommGroup M₂] [Module A M] [Module A M₂] [TopologicalSpace M] [TopologicalSpace M₂] {R : Type u_4} [Ring R] [Module R M] [Module R M₂] [LinearMap.CompatibleSMul M M₂ R A] {S : Type u_5} [Ring S] [Module S M₂] [ContinuousConstSMul S M₂] [SMulCommClass A S M₂] [SMulCommClass R S M₂] [TopologicalAddGroup M₂] :

⇑(ContinuousLinearMap.restrictScalarsₗ A M M₂ R S) = ContinuousLinearMap.restrictScalars R

def ContinuousLinearEquiv.toContinuousLinearMap {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) :

M₁ →SL[σ₁₂] M₂

A continuous linear equivalence induces a continuous linear map.

Equations

↑e = let __src := ↑e.toLinearEquiv; { toLinearMap := __src, cont := ⋯ }

instance ContinuousLinearEquiv.ContinuousLinearMap.coe {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] :

Coe (M₁ ≃SL[σ₁₂] M₂) (M₁ →SL[σ₁₂] M₂)

Coerce continuous linear equivs to continuous linear maps.

Equations

ContinuousLinearEquiv.ContinuousLinearMap.coe = { coe := ContinuousLinearEquiv.toContinuousLinearMap }

instance ContinuousLinearEquiv.equivLike {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] :

EquivLike (M₁ ≃SL[σ₁₂] M₂) M₁ M₂

Equations

ContinuousLinearEquiv.equivLike = { coe := fun (f : M₁ ≃SL[σ₁₂] M₂) => f.toFun, inv := fun (f : M₁ ≃SL[σ₁₂] M₂) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

instance ContinuousLinearEquiv.continuousSemilinearEquivClass {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] :

ContinuousSemilinearEquivClass (M₁ ≃SL[σ₁₂] M₂) σ₁₂ M₁ M₂

Equations

⋯ = ⋯

theorem ContinuousLinearEquiv.coe_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (b : M₁) :

↑e b = e b

@[simp]

theorem ContinuousLinearEquiv.coe_toLinearEquiv {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f : M₁ ≃SL[σ₁₂] M₂) :

⇑f.toLinearEquiv = ⇑f

@[simp]

theorem ContinuousLinearEquiv.coe_coe {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) :

⇑↑e = ⇑e

theorem ContinuousLinearEquiv.toLinearEquiv_injective {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] :

Function.Injective ContinuousLinearEquiv.toLinearEquiv

theorem ContinuousLinearEquiv.ext {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {f : M₁ ≃SL[σ₁₂] M₂} {g : M₁ ≃SL[σ₁₂] M₂} (h : ⇑f = ⇑g) :

f = g

theorem ContinuousLinearEquiv.coe_injective {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] :

Function.Injective ContinuousLinearEquiv.toContinuousLinearMap

@[simp]

theorem ContinuousLinearEquiv.coe_inj {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {e : M₁ ≃SL[σ₁₂] M₂} {e' : M₁ ≃SL[σ₁₂] M₂} :

↑e = ↑e' ↔ e = e'

def ContinuousLinearEquiv.toHomeomorph {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) :

M₁ ≃ₜ M₂

A continuous linear equivalence induces a homeomorphism.

Equations

ContinuousLinearEquiv.toHomeomorph e = { toEquiv := LinearEquiv.toEquiv e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.coe_toHomeomorph {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) :

⇑(ContinuousLinearEquiv.toHomeomorph e) = ⇑e

theorem ContinuousLinearEquiv.isOpenMap {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) :

theorem ContinuousLinearEquiv.image_closure {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₁) :

⇑e '' closure s = closure (⇑e '' s)

theorem ContinuousLinearEquiv.preimage_closure {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₂) :

⇑e ⁻¹' closure s = closure (⇑e ⁻¹' s)

@[simp]

theorem ContinuousLinearEquiv.isClosed_image {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) {s : Set M₁} :

IsClosed (⇑e '' s) ↔ IsClosed s

theorem ContinuousLinearEquiv.map_nhds_eq {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (x : M₁) :

Filter.map (⇑e) (nhds x) = nhds (e x)

theorem ContinuousLinearEquiv.map_zero {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) :

e 0 = 0

theorem ContinuousLinearEquiv.map_add {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (x : M₁) (y : M₁) :

e (x + y) = e x + e y

theorem ContinuousLinearEquiv.map_smulₛₗ {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (c : R₁) (x : M₁) :

e (c • x) = σ₁₂ c • e x

theorem ContinuousLinearEquiv.map_smul {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] (e : M₁ ≃L[R₁] M₂) (c : R₁) (x : M₁) :

e (c • x) = c • e x

theorem ContinuousLinearEquiv.map_eq_zero_iff {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) {x : M₁} :

e x = 0 ↔ x = 0

theorem ContinuousLinearEquiv.continuous {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) :

Continuous ⇑e

theorem ContinuousLinearEquiv.continuousOn {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) {s : Set M₁} :

ContinuousOn (⇑e) s

theorem ContinuousLinearEquiv.continuousAt {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) {x : M₁} :

ContinuousAt (⇑e) x

theorem ContinuousLinearEquiv.continuousWithinAt {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) {s : Set M₁} {x : M₁} :

ContinuousWithinAt (⇑e) s x

theorem ContinuousLinearEquiv.comp_continuousOn_iff {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {α : Type u_9} [TopologicalSpace α] (e : M₁ ≃SL[σ₁₂] M₂) {f : α → M₁} {s : Set α} :

ContinuousOn (⇑e ∘ f) s ↔ ContinuousOn f s

theorem ContinuousLinearEquiv.comp_continuous_iff {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {α : Type u_9} [TopologicalSpace α] (e : M₁ ≃SL[σ₁₂] M₂) {f : α → M₁} :

Continuous (⇑e ∘ f) ↔ Continuous f

theorem ContinuousLinearEquiv.ext₁ {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [TopologicalSpace R₁] {f : R₁ ≃L[R₁] M₁} {g : R₁ ≃L[R₁] M₁} (h : f 1 = g 1) :

f = g

An extensionality lemma for R ≃L[R] M.

def ContinuousLinearEquiv.refl (R₁ : Type u_1) [Semiring R₁] (M₁ : Type u_4) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :

M₁ ≃L[R₁] M₁

The identity map as a continuous linear equivalence.

Equations

ContinuousLinearEquiv.refl R₁ M₁ = let __src := LinearEquiv.refl R₁ M₁; { toLinearEquiv := __src, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.coe_refl {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :

↑(ContinuousLinearEquiv.refl R₁ M₁) = ContinuousLinearMap.id R₁ M₁

@[simp]

theorem ContinuousLinearEquiv.coe_refl' {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :

⇑(ContinuousLinearEquiv.refl R₁ M₁) = id

def ContinuousLinearEquiv.symm {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) :

M₂ ≃SL[σ₂₁] M₁

The inverse of a continuous linear equivalence as a continuous linear equivalence

Equations

ContinuousLinearEquiv.symm e = let __src := LinearEquiv.symm e.toLinearEquiv; { toLinearEquiv := __src, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.symm_toLinearEquiv {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) :

(ContinuousLinearEquiv.symm e).toLinearEquiv = LinearEquiv.symm e.toLinearEquiv

@[simp]

theorem ContinuousLinearEquiv.symm_toHomeomorph {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) :

Homeomorph.symm (ContinuousLinearEquiv.toHomeomorph e) = ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm e)

def ContinuousLinearEquiv.Simps.apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (h : M₁ ≃SL[σ₁₂] M₂) :

M₁ → M₂

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations

ContinuousLinearEquiv.Simps.apply h = ⇑h

def ContinuousLinearEquiv.Simps.symm_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (h : M₁ ≃SL[σ₁₂] M₂) :

M₂ → M₁

See Note [custom simps projection]

Equations

ContinuousLinearEquiv.Simps.symm_apply h = ⇑(ContinuousLinearEquiv.symm h)

theorem ContinuousLinearEquiv.symm_map_nhds_eq {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (x : M₁) :

Filter.map (⇑(ContinuousLinearEquiv.symm e)) (nhds (e x)) = nhds x

def ContinuousLinearEquiv.trans {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] (e₁ : M₁ ≃SL[σ₁₂] M₂) (e₂ : M₂ ≃SL[σ₂₃] M₃) :

M₁ ≃SL[σ₁₃] M₃

The composition of two continuous linear equivalences as a continuous linear equivalence.

Equations

ContinuousLinearEquiv.trans e₁ e₂ = let __src := LinearEquiv.trans e₁.toLinearEquiv e₂.toLinearEquiv; { toLinearEquiv := __src, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.trans_toLinearEquiv {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] (e₁ : M₁ ≃SL[σ₁₂] M₂) (e₂ : M₂ ≃SL[σ₂₃] M₃) :

(ContinuousLinearEquiv.trans e₁ e₂).toLinearEquiv = LinearEquiv.trans e₁.toLinearEquiv e₂.toLinearEquiv

def ContinuousLinearEquiv.prod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] {M₄ : Type u_8} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [Module R₁ M₄] (e : M₁ ≃L[R₁] M₂) (e' : M₃ ≃L[R₁] M₄) :

(M₁ × M₃) ≃L[R₁] M₂ × M₄

Product of two continuous linear equivalences. The map comes from Equiv.prodCongr.

Equations

ContinuousLinearEquiv.prod e e' = let __src := LinearEquiv.prod e.toLinearEquiv e'.toLinearEquiv; { toLinearEquiv := __src, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.prod_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] {M₄ : Type u_8} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [Module R₁ M₄] (e : M₁ ≃L[R₁] M₂) (e' : M₃ ≃L[R₁] M₄) (x : M₁ × M₃) :

(ContinuousLinearEquiv.prod e e') x = (e x.1, e' x.2)

@[simp]

theorem ContinuousLinearEquiv.coe_prod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] {M₄ : Type u_8} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [Module R₁ M₄] (e : M₁ ≃L[R₁] M₂) (e' : M₃ ≃L[R₁] M₄) :

↑(ContinuousLinearEquiv.prod e e') = ContinuousLinearMap.prodMap ↑e ↑e'

theorem ContinuousLinearEquiv.prod_symm {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] {M₄ : Type u_8} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R₁ M₁] [Module R₁ M₂] [Module R₁ M₃] [Module R₁ M₄] (e : M₁ ≃L[R₁] M₂) (e' : M₃ ≃L[R₁] M₄) :

ContinuousLinearEquiv.symm (ContinuousLinearEquiv.prod e e') = ContinuousLinearEquiv.prod (ContinuousLinearEquiv.symm e) (ContinuousLinearEquiv.symm e')

@[simp]

theorem ContinuousLinearEquiv.prodComm_toLinearEquiv (R₁ : Type u_1) [Semiring R₁] (M₁ : Type u_4) [TopologicalSpace M₁] [AddCommMonoid M₁] (M₂ : Type u_6) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] :

(ContinuousLinearEquiv.prodComm R₁ M₁ M₂).toLinearEquiv = LinearEquiv.prodComm R₁ M₁ M₂

@[simp]

theorem ContinuousLinearEquiv.prodComm_apply (R₁ : Type u_1) [Semiring R₁] (M₁ : Type u_4) [TopologicalSpace M₁] [AddCommMonoid M₁] (M₂ : Type u_6) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] :

∀ (a : M₁ × M₂), (ContinuousLinearEquiv.prodComm R₁ M₁ M₂) a = Prod.swap a

def ContinuousLinearEquiv.prodComm (R₁ : Type u_1) [Semiring R₁] (M₁ : Type u_4) [TopologicalSpace M₁] [AddCommMonoid M₁] (M₂ : Type u_6) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] :

(M₁ × M₂) ≃L[R₁] M₂ × M₁

Product of modules is commutative up to continuous linear isomorphism.

Equations

ContinuousLinearEquiv.prodComm R₁ M₁ M₂ = let __src := LinearEquiv.prodComm R₁ M₁ M₂; { toLinearEquiv := __src, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.prodComm_symm (R₁ : Type u_1) [Semiring R₁] (M₁ : Type u_4) [TopologicalSpace M₁] [AddCommMonoid M₁] (M₂ : Type u_6) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] :

ContinuousLinearEquiv.symm (ContinuousLinearEquiv.prodComm R₁ M₁ M₂) = ContinuousLinearEquiv.prodComm R₁ M₂ M₁

theorem ContinuousLinearEquiv.bijective {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) :

Function.Bijective ⇑e

theorem ContinuousLinearEquiv.injective {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) :

Function.Injective ⇑e

theorem ContinuousLinearEquiv.surjective {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) :

Function.Surjective ⇑e

@[simp]

theorem ContinuousLinearEquiv.trans_apply {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] (e₁ : M₁ ≃SL[σ₁₂] M₂) (e₂ : M₂ ≃SL[σ₂₃] M₃) (c : M₁) :

(ContinuousLinearEquiv.trans e₁ e₂) c = e₂ (e₁ c)

@[simp]

theorem ContinuousLinearEquiv.apply_symm_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (c : M₂) :

e ((ContinuousLinearEquiv.symm e) c) = c

@[simp]

theorem ContinuousLinearEquiv.symm_apply_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (b : M₁) :

(ContinuousLinearEquiv.symm e) (e b) = b

@[simp]

theorem ContinuousLinearEquiv.symm_trans_apply {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] (e₁ : M₂ ≃SL[σ₂₁] M₁) (e₂ : M₃ ≃SL[σ₃₂] M₂) (c : M₁) :

(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.trans e₂ e₁)) c = (ContinuousLinearEquiv.symm e₂) ((ContinuousLinearEquiv.symm e₁) c)

@[simp]

theorem ContinuousLinearEquiv.symm_image_image {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₁) :

⇑(ContinuousLinearEquiv.symm e) '' (⇑e '' s) = s

@[simp]

theorem ContinuousLinearEquiv.image_symm_image {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₂) :

⇑e '' (⇑(ContinuousLinearEquiv.symm e) '' s) = s

@[simp]

theorem ContinuousLinearEquiv.comp_coe {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] (f : M₁ ≃SL[σ₁₂] M₂) (f' : M₂ ≃SL[σ₂₃] M₃) :

ContinuousLinearMap.comp ↑f' ↑f = ↑(ContinuousLinearEquiv.trans f f')

@[simp]

theorem ContinuousLinearEquiv.coe_comp_coe_symm {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) :

ContinuousLinearMap.comp ↑e ↑(ContinuousLinearEquiv.symm e) = ContinuousLinearMap.id R₂ M₂

@[simp]

theorem ContinuousLinearEquiv.coe_symm_comp_coe {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) :

ContinuousLinearMap.comp ↑(ContinuousLinearEquiv.symm e) ↑e = ContinuousLinearMap.id R₁ M₁

@[simp]

theorem ContinuousLinearEquiv.symm_comp_self {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) :

⇑(ContinuousLinearEquiv.symm e) ∘ ⇑e = id

@[simp]

theorem ContinuousLinearEquiv.self_comp_symm {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) :

⇑e ∘ ⇑(ContinuousLinearEquiv.symm e) = id

@[simp]

theorem ContinuousLinearEquiv.symm_symm {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) :

ContinuousLinearEquiv.symm (ContinuousLinearEquiv.symm e) = e

@[simp]

theorem ContinuousLinearEquiv.refl_symm {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :

ContinuousLinearEquiv.symm (ContinuousLinearEquiv.refl R₁ M₁) = ContinuousLinearEquiv.refl R₁ M₁

theorem ContinuousLinearEquiv.symm_symm_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (x : M₁) :

(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.symm e)) x = e x

theorem ContinuousLinearEquiv.symm_apply_eq {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) {x : M₂} {y : M₁} :

(ContinuousLinearEquiv.symm e) x = y ↔ x = e y

theorem ContinuousLinearEquiv.eq_symm_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) {x : M₂} {y : M₁} :

y = (ContinuousLinearEquiv.symm e) x ↔ e y = x

theorem ContinuousLinearEquiv.image_eq_preimage {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₁) :

⇑e '' s = ⇑(ContinuousLinearEquiv.symm e) ⁻¹' s

theorem ContinuousLinearEquiv.image_symm_eq_preimage {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₂) :

⇑(ContinuousLinearEquiv.symm e) '' s = ⇑e ⁻¹' s

@[simp]

theorem ContinuousLinearEquiv.symm_preimage_preimage {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₂) :

⇑(ContinuousLinearEquiv.symm e) ⁻¹' (⇑e ⁻¹' s) = s

@[simp]

theorem ContinuousLinearEquiv.preimage_symm_preimage {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₁) :

⇑e ⁻¹' (⇑(ContinuousLinearEquiv.symm e) ⁻¹' s) = s

theorem ContinuousLinearEquiv.uniformEmbedding {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {E₁ : Type u_9} {E₂ : Type u_10} [UniformSpace E₁] [UniformSpace E₂] [AddCommGroup E₁] [AddCommGroup E₂] [Module R₁ E₁] [Module R₂ E₂] [UniformAddGroup E₁] [UniformAddGroup E₂] (e : E₁ ≃SL[σ₁₂] E₂) :

UniformEmbedding ⇑e

theorem LinearEquiv.uniformEmbedding {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {E₁ : Type u_9} {E₂ : Type u_10} [UniformSpace E₁] [UniformSpace E₂] [AddCommGroup E₁] [AddCommGroup E₂] [Module R₁ E₁] [Module R₂ E₂] [UniformAddGroup E₁] [UniformAddGroup E₂] (e : E₁ ≃ₛₗ[σ₁₂] E₂) (h₁ : Continuous ⇑e) (h₂ : Continuous ⇑(LinearEquiv.symm e)) :

UniformEmbedding ⇑e

def ContinuousLinearEquiv.equivOfInverse {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁) (h₁ : Function.LeftInverse ⇑f₂ ⇑f₁) (h₂ : Function.RightInverse ⇑f₂ ⇑f₁) :

M₁ ≃SL[σ₁₂] M₂

Create a ContinuousLinearEquiv from two ContinuousLinearMaps that are inverse of each other.

Equations

ContinuousLinearEquiv.equivOfInverse f₁ f₂ h₁ h₂ = { toLinearEquiv := { toLinearMap := ↑f₁, invFun := ⇑f₂, left_inv := h₁, right_inv := h₂ }, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.equivOfInverse_apply {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁) (h₁ : Function.LeftInverse ⇑f₂ ⇑f₁) (h₂ : Function.RightInverse ⇑f₂ ⇑f₁) (x : M₁) :

(ContinuousLinearEquiv.equivOfInverse f₁ f₂ h₁ h₂) x = f₁ x

@[simp]

theorem ContinuousLinearEquiv.symm_equivOfInverse {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁) (h₁ : Function.LeftInverse ⇑f₂ ⇑f₁) (h₂ : Function.RightInverse ⇑f₂ ⇑f₁) :

ContinuousLinearEquiv.symm (ContinuousLinearEquiv.equivOfInverse f₁ f₂ h₁ h₂) = ContinuousLinearEquiv.equivOfInverse f₂ f₁ h₂ h₁

instance ContinuousLinearEquiv.automorphismGroup {R₁ : Type u_1} [Semiring R₁] (M₁ : Type u_4) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :

Group (M₁ ≃L[R₁] M₁)

The continuous linear equivalences from M to itself form a group under composition.

Equations

ContinuousLinearEquiv.automorphismGroup M₁ = Group.mk ⋯

def ContinuousLinearEquiv.ulift {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :

ULift.{u_10, u_4} M₁ ≃L[R₁] M₁

The continuous linear equivalence between ULift M₁ and M₁.

This is a continuous version of ULift.moduleEquiv.

Equations

ContinuousLinearEquiv.ulift = let __src := ULift.moduleEquiv; { toLinearEquiv := __src, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.arrowCongrEquiv_symm_apply {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] {M₄ : Type u_8} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] {R₄ : Type u_9} [Semiring R₄] [Module R₄ M₄] {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃} [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄} [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] (e₁₂ : M₁ ≃SL[σ₁₂] M₂) (e₄₃ : M₄ ≃SL[σ₄₃] M₃) (f : M₂ →SL[σ₂₃] M₃) :

(ContinuousLinearEquiv.arrowCongrEquiv e₁₂ e₄₃).symm f = ContinuousLinearMap.comp (↑(ContinuousLinearEquiv.symm e₄₃)) (ContinuousLinearMap.comp f ↑e₁₂)

@[simp]

theorem ContinuousLinearEquiv.arrowCongrEquiv_apply {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] {M₄ : Type u_8} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] {R₄ : Type u_9} [Semiring R₄] [Module R₄ M₄] {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃} [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄} [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] (e₁₂ : M₁ ≃SL[σ₁₂] M₂) (e₄₃ : M₄ ≃SL[σ₄₃] M₃) (f : M₁ →SL[σ₁₄] M₄) :

(ContinuousLinearEquiv.arrowCongrEquiv e₁₂ e₄₃) f = ContinuousLinearMap.comp (↑e₄₃) (ContinuousLinearMap.comp f ↑(ContinuousLinearEquiv.symm e₁₂))

def ContinuousLinearEquiv.arrowCongrEquiv {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [Semiring R₁] [Semiring R₂] [Semiring R₃] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_7} [TopologicalSpace M₃] [AddCommMonoid M₃] {M₄ : Type u_8} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] {R₄ : Type u_9} [Semiring R₄] [Module R₄ M₄] {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃} [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄} [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] (e₁₂ : M₁ ≃SL[σ₁₂] M₂) (e₄₃ : M₄ ≃SL[σ₄₃] M₃) :

(M₁ →SL[σ₁₄] M₄) ≃ (M₂ →SL[σ₂₃] M₃)

A pair of continuous (semi)linear equivalences generates an equivalence between the spaces of continuous linear maps. See also ContinuousLinearEquiv.arrowCongr.

Equations

One or more equations did not get rendered due to their size.

def ContinuousLinearEquiv.skewProd {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommGroup M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommGroup M₃] {M₄ : Type u_5} [TopologicalSpace M₄] [AddCommGroup M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] [TopologicalAddGroup M₄] (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (f : M →L[R] M₄) :

(M × M₃) ≃L[R] M₂ × M₄

Equivalence given by a block lower diagonal matrix. e and e' are diagonal square blocks, and f is a rectangular block below the diagonal.

Equations

ContinuousLinearEquiv.skewProd e e' f = let __src := LinearEquiv.skewProd e.toLinearEquiv e'.toLinearEquiv ↑f; { toLinearEquiv := __src, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.skewProd_apply {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommGroup M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommGroup M₃] {M₄ : Type u_5} [TopologicalSpace M₄] [AddCommGroup M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] [TopologicalAddGroup M₄] (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (f : M →L[R] M₄) (x : M × M₃) :

(ContinuousLinearEquiv.skewProd e e' f) x = (e x.1, e' x.2 + f x.1)

@[simp]

theorem ContinuousLinearEquiv.skewProd_symm_apply {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommGroup M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommGroup M₃] {M₄ : Type u_5} [TopologicalSpace M₄] [AddCommGroup M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] [TopologicalAddGroup M₄] (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (f : M →L[R] M₄) (x : M₂ × M₄) :

(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.skewProd e e' f)) x = ((ContinuousLinearEquiv.symm e) x.1, (ContinuousLinearEquiv.symm e') (x.2 - f ((ContinuousLinearEquiv.symm e) x.1)))

theorem ContinuousLinearEquiv.map_sub {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [Module R M] {M₂ : Type u_4} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : M ≃SL[σ₁₂] M₂) (x : M) (y : M) :

e (x - y) = e x - e y

theorem ContinuousLinearEquiv.map_neg {R : Type u_1} [Ring R] {R₂ : Type u_2} [Ring R₂] {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [Module R M] {M₂ : Type u_4} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : M ≃SL[σ₁₂] M₂) (x : M) :

e (-x) = -e x

The next theorems cover the identification between M ≃L[𝕜] Mand the group of units of the ring M →L[R] M.

def ContinuousLinearEquiv.ofUnit {R : Type u_1} [Ring R] {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [Module R M] (f : (M →L[R] M)ˣ) :

An invertible continuous linear map f determines a continuous equivalence from M to itself.

Equations

One or more equations did not get rendered due to their size.

def ContinuousLinearEquiv.toUnit {R : Type u_1} [Ring R] {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [Module R M] (f : M ≃L[R] M) :

(M →L[R] M)ˣ

A continuous equivalence from M to itself determines an invertible continuous linear map.

Equations

ContinuousLinearEquiv.toUnit f = { val := ↑f, inv := ↑(ContinuousLinearEquiv.symm f), val_inv := ⋯, inv_val := ⋯ }

def ContinuousLinearEquiv.unitsEquiv (R : Type u_1) [Ring R] (M : Type u_3) [TopologicalSpace M] [AddCommGroup M] [Module R M] :

(M →L[R] M)ˣ ≃* M ≃L[R] M

The units of the algebra of continuous R-linear endomorphisms of M is multiplicatively equivalent to the type of continuous linear equivalences between M and itself.

Equations

ContinuousLinearEquiv.unitsEquiv R M = { toEquiv := { toFun := ContinuousLinearEquiv.ofUnit, invFun := ContinuousLinearEquiv.toUnit, left_inv := ⋯, right_inv := ⋯ }, map_mul' := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.unitsEquiv_apply (R : Type u_1) [Ring R] (M : Type u_3) [TopologicalSpace M] [AddCommGroup M] [Module R M] (f : (M →L[R] M)ˣ) (x : M) :

((ContinuousLinearEquiv.unitsEquiv R M) f) x = ↑f x

def ContinuousLinearEquiv.unitsEquivAut (R : Type u_1) [Ring R] [TopologicalSpace R] [ContinuousMul R] :

Rˣ ≃ R ≃L[R] R

Continuous linear equivalences R ≃L[R] R are enumerated by Rˣ.

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousLinearEquiv.unitsEquivAut_apply {R : Type u_1} [Ring R] [TopologicalSpace R] [ContinuousMul R] (u : Rˣ) (x : R) :

((ContinuousLinearEquiv.unitsEquivAut R) u) x = x * ↑u

@[simp]

theorem ContinuousLinearEquiv.unitsEquivAut_apply_symm {R : Type u_1} [Ring R] [TopologicalSpace R] [ContinuousMul R] (u : Rˣ) (x : R) :

(ContinuousLinearEquiv.symm ((ContinuousLinearEquiv.unitsEquivAut R) u)) x = x * ↑u⁻¹

@[simp]

theorem ContinuousLinearEquiv.unitsEquivAut_symm_apply {R : Type u_1} [Ring R] [TopologicalSpace R] [ContinuousMul R] (e : R ≃L[R] R) :

↑((ContinuousLinearEquiv.unitsEquivAut R).symm e) = e 1

def ContinuousLinearEquiv.equivOfRightInverse {R : Type u_1} [Ring R] {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [Module R M] {M₂ : Type u_4} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M₂] [TopologicalAddGroup M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : Function.RightInverse ⇑f₂ ⇑f₁) :

M ≃L[R] M₂ × ↥(LinearMap.ker f₁)

A pair of continuous linear maps such that f₁ ∘ f₂ = id generates a continuous linear equivalence e between M and M₂ × f₁.ker such that (e x).2 = x for x ∈ f₁.ker, (e x).1 = f₁ x, and (e (f₂ y)).2 = 0. The map is given by e x = (f₁ x, x - f₂ (f₁ x)).

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousLinearEquiv.fst_equivOfRightInverse {R : Type u_1} [Ring R] {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [Module R M] {M₂ : Type u_4} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M₂] [TopologicalAddGroup M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : Function.RightInverse ⇑f₂ ⇑f₁) (x : M) :

((ContinuousLinearEquiv.equivOfRightInverse f₁ f₂ h) x).1 = f₁ x

@[simp]

theorem ContinuousLinearEquiv.snd_equivOfRightInverse {R : Type u_1} [Ring R] {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [Module R M] {M₂ : Type u_4} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M₂] [TopologicalAddGroup M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : Function.RightInverse ⇑f₂ ⇑f₁) (x : M) :

↑((ContinuousLinearEquiv.equivOfRightInverse f₁ f₂ h) x).2 = x - f₂ (f₁ x)

@[simp]

theorem ContinuousLinearEquiv.equivOfRightInverse_symm_apply {R : Type u_1} [Ring R] {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [Module R M] {M₂ : Type u_4} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M₂] [TopologicalAddGroup M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : Function.RightInverse ⇑f₂ ⇑f₁) (y : M₂ × ↥(LinearMap.ker f₁)) :

(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.equivOfRightInverse f₁ f₂ h)) y = f₂ y.1 + ↑y.2

def ContinuousLinearEquiv.funUnique (ι : Type u_1) (R : Type u_2) (M : Type u_3) [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] :

(ι → M) ≃L[R] M

If ι has a unique element, then ι → M is continuously linear equivalent to M.

Equations

ContinuousLinearEquiv.funUnique ι R M = let __src := Homeomorph.funUnique ι M; { toLinearEquiv := LinearEquiv.funUnique ι R M, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.coe_funUnique {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] :

⇑(ContinuousLinearEquiv.funUnique ι R M) = Function.eval default

@[simp]

theorem ContinuousLinearEquiv.coe_funUnique_symm {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] :

⇑(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.funUnique ι R M)) = Function.const ι

@[simp]

theorem ContinuousLinearEquiv.piFinTwo_apply (R : Type u_2) [Semiring R] (M : Fin 2 → Type u_4) [(i : Fin 2) → AddCommMonoid (M i)] [(i : Fin 2) → Module R (M i)] [(i : Fin 2) → TopologicalSpace (M i)] :

⇑(ContinuousLinearEquiv.piFinTwo R M) = fun (f : (i : Fin 2) → M i) => (f 0, f 1)

@[simp]

theorem ContinuousLinearEquiv.piFinTwo_symm_apply (R : Type u_2) [Semiring R] (M : Fin 2 → Type u_4) [(i : Fin 2) → AddCommMonoid (M i)] [(i : Fin 2) → Module R (M i)] [(i : Fin 2) → TopologicalSpace (M i)] :

⇑(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.piFinTwo R M)) = fun (p : M 0 × M 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)

def ContinuousLinearEquiv.piFinTwo (R : Type u_2) [Semiring R] (M : Fin 2 → Type u_4) [(i : Fin 2) → AddCommMonoid (M i)] [(i : Fin 2) → Module R (M i)] [(i : Fin 2) → TopologicalSpace (M i)] :

((i : Fin 2) → M i) ≃L[R] M 0 × M 1

Continuous linear equivalence between dependent functions (i : Fin 2) → M i and M 0 × M 1.

Equations

ContinuousLinearEquiv.piFinTwo R M = let __src := Homeomorph.piFinTwo M; { toLinearEquiv := LinearEquiv.piFinTwo R M, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.finTwoArrow_symm_apply (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] :

⇑(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.finTwoArrow R M)) = fun (x : M × M) => ![x.1, x.2]

@[simp]

theorem ContinuousLinearEquiv.finTwoArrow_apply (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] :

⇑(ContinuousLinearEquiv.finTwoArrow R M) = fun (f : Fin 2 → M) => (f 0, f 1)

def ContinuousLinearEquiv.finTwoArrow (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] :

(Fin 2 → M) ≃L[R] M × M

Continuous linear equivalence between vectors in M² = Fin 2 → M and M × M.

Equations

One or more equations did not get rendered due to their size.

noncomputable def ContinuousLinearMap.inverse {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M] [Module R M] :

(M →L[R] M₂) → M₂ →L[R] M

Introduce a function inverse from M →L[R] M₂ to M₂ →L[R] M, which sends f to f.symm if f is a continuous linear equivalence and to 0 otherwise. This definition is somewhat ad hoc, but one needs a fully (rather than partially) defined inverse function for some purposes, including for calculus.

Equations

ContinuousLinearMap.inverse f = if h : ∃ (e : M ≃L[R] M₂), ↑e = f then ↑(ContinuousLinearEquiv.symm (Classical.choose h)) else 0

@[simp]

theorem ContinuousLinearMap.inverse_equiv {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M] [Module R M] (e : M ≃L[R] M₂) :

ContinuousLinearMap.inverse ↑e = ↑(ContinuousLinearEquiv.symm e)

By definition, if f is invertible then inverse f = f.symm.

@[simp]

theorem ContinuousLinearMap.inverse_non_equiv {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Semiring R] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M] [Module R M] (f : M →L[R] M₂) (h : ¬∃ (e' : M ≃L[R] M₂), ↑e' = f) :

ContinuousLinearMap.inverse f = 0

By definition, if f is not invertible then inverse f = 0.

@[simp]

theorem ContinuousLinearMap.ring_inverse_equiv {R : Type u_1} {M : Type u_2} [TopologicalSpace M] [Ring R] [AddCommGroup M] [Module R M] (e : M ≃L[R] M) :

Ring.inverse ↑e = ContinuousLinearMap.inverse ↑e

theorem ContinuousLinearMap.to_ring_inverse {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [TopologicalSpace M] [TopologicalSpace M₂] [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] (e : M ≃L[R] M₂) (f : M →L[R] M₂) :

ContinuousLinearMap.inverse f = ContinuousLinearMap.comp (Ring.inverse (ContinuousLinearMap.comp (↑(ContinuousLinearEquiv.symm e)) f)) ↑(ContinuousLinearEquiv.symm e)

The function ContinuousLinearEquiv.inverse can be written in terms of Ring.inverse for the ring of self-maps of the domain.

theorem ContinuousLinearMap.ring_inverse_eq_map_inverse {R : Type u_1} {M : Type u_2} [TopologicalSpace M] [Ring R] [AddCommGroup M] [Module R M] :

Ring.inverse = ContinuousLinearMap.inverse

def Submodule.ClosedComplemented {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] (p : Submodule R M) :

A submodule p is called complemented if there exists a continuous projection M →ₗ[R] p.

Equations

Submodule.ClosedComplemented p = ∃ (f : M →L[R] ↥p), ∀ (x : ↥p), f ↑x = x

theorem Submodule.ClosedComplemented.exists_isClosed_isCompl {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {p : Submodule R M} [T1Space ↥p] (h : Submodule.ClosedComplemented p) :

∃ (q : Submodule R M), IsClosed ↑q ∧ IsCompl p q

theorem Submodule.ClosedComplemented.isClosed {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] [TopologicalAddGroup M] [T1Space M] {p : Submodule R M} (h : Submodule.ClosedComplemented p) :

@[simp]

theorem Submodule.closedComplemented_bot {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] :

Submodule.ClosedComplemented ⊥

@[simp]

theorem Submodule.closedComplemented_top {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] :

Submodule.ClosedComplemented ⊤

theorem Submodule.ClosedComplemented.exists_submodule_equiv_prod {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] [TopologicalAddGroup M] {p : Submodule R M} (hp : Submodule.ClosedComplemented p) :

∃ (q : Submodule R M) (e : M ≃L[R] ↥p × ↥q), (∀ (x : ↥p), e ↑x = (x, 0)) ∧ (∀ (y : ↥q), e ↑y = (0, y)) ∧ ∀ (x : ↥p × ↥q), (ContinuousLinearEquiv.symm e) x = ↑x.1 + ↑x.2

If p is a closed complemented submodule, then there exists a submodule q and a continuous linear equivalence M ≃L[R] (p × q) such that e (x : p) = (x, 0), e (y : q) = (0, y), and e.symm x = x.1 + x.2.

In fact, the properties of e imply the properties of e.symm and vice versa, but we provide both for convenience.

theorem ContinuousLinearMap.closedComplemented_ker_of_rightInverse {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommGroup M₂] [Module R M] [Module R M₂] [TopologicalAddGroup M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : Function.RightInverse ⇑f₂ ⇑f₁) :

Submodule.ClosedComplemented (LinearMap.ker f₁)

instance QuotientModule.Quotient.topologicalSpace {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] (S : Submodule R M) :

TopologicalSpace (M ⧸ S)

Equations

QuotientModule.Quotient.topologicalSpace S = inferInstanceAs (TopologicalSpace (Quotient (Submodule.quotientRel S)))

theorem Submodule.isOpenMap_mkQ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] (S : Submodule R M) [TopologicalAddGroup M] :

IsOpenMap ⇑(Submodule.mkQ S)

instance Submodule.topologicalAddGroup_quotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] (S : Submodule R M) [TopologicalAddGroup M] :

TopologicalAddGroup (M ⧸ S)

Equations

⋯ = ⋯

instance Submodule.continuousSMul_quotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] (S : Submodule R M) [TopologicalSpace R] [TopologicalAddGroup M] [ContinuousSMul R M] :

ContinuousSMul R (M ⧸ S)

Equations

⋯ = ⋯

instance Submodule.t3_quotient_of_isClosed {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] (S : Submodule R M) [TopologicalAddGroup M] [IsClosed ↑S] :

T3Space (M ⧸ S)

Equations

⋯ = ⋯