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] [(nhdsWithin 0 {x : R | IsUnit x}).NeBot] (s : Submodule R M) (hs : (interior ↑s).Nonempty) : 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] [(nhdsWithin 0 {0}ᶜ).NeBot] [NoZeroSMulDivisors R M] (x : M) : (nhdsWithin x {x}ᶜ).NeBot

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) : Submodule R M

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

Equations

• s.topologicalClosure = { toAddSubmonoid := s.topologicalClosure, 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) : ↑s.topologicalClosure = 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 ≤ s.topologicalClosure

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.span R s).topologicalClosure

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 ↑s.topologicalClosure

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) : s.topologicalClosure ≤ 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) : s.topologicalClosure ≤ t.topologicalClosure

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) : s.topologicalClosure = 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 ↔ s.topologicalClosure = ⊤

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 ↥U.topologicalClosure

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' : ∀ (m : R) (x : M), (↑self).toFun (m • x) = σ m • (↑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.

theorem ContinuousLinearMap.cont {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₂] (self : M →SL[σ] M₂) : 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.

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.

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 : Prop

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.

@[reducible, inline]

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₂] : Prop

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.toLinearEquiv).toFun (x + y) = (↑self.toLinearEquiv).toFun x + (↑self.toLinearEquiv).toFun y
• map_smul' : ∀ (m : R) (x : M), (↑self.toLinearEquiv).toFun (m • x) = σ m • (↑self.toLinearEquiv).toFun x
• invFun : M₂ → M
• left_inv : Function.LeftInverse self.invFun (↑self.toLinearEquiv).toFun
• right_inv : Function.RightInverse self.invFun (↑self.toLinearEquiv).toFun
• continuous_toFun : Continuous (↑self.toLinearEquiv).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.

theorem ContinuousLinearEquiv.continuous_toFun {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₂] (self : M ≃SL[σ] M₂) : Continuous (↑self.toLinearEquiv).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.

theorem ContinuousLinearEquiv.continuous_invFun {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₂] (self : M ≃SL[σ] M₂) : 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.

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.

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 : Prop

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.

theorem ContinuousSemilinearEquivClass.map_continuous {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} : ∀ {inst : Semiring R} {inst_1 : Semiring S} {σ : outParam (R →+* S)} {σ' : outParam (S →+* R)} {inst_2 : RingHomInvPair σ σ'} {inst_3 : RingHomInvPair σ' σ} {M : outParam (Type u_4)} {inst_4 : TopologicalSpace M} {inst_5 : AddCommMonoid M} {M₂ : outParam (Type u_5)} {inst_6 : TopologicalSpace M₂} {inst_7 : AddCommMonoid M₂} {inst_8 : Module R M} {inst_9 : Module S M₂} {inst_10 : EquivLike F M M₂} [self : ContinuousSemilinearEquivClass F σ M M₂] (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.

theorem ContinuousSemilinearEquivClass.inv_continuous {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} : ∀ {inst : Semiring R} {inst_1 : Semiring S} {σ : outParam (R →+* S)} {σ' : outParam (S →+* R)} {inst_2 : RingHomInvPair σ σ'} {inst_3 : RingHomInvPair σ' σ} {M : outParam (Type u_4)} {inst_4 : TopologicalSpace M} {inst_5 : AddCommMonoid M} {M₂ : outParam (Type u_5)} {inst_6 : TopologicalSpace M₂} {inst_7 : AddCommMonoid M₂} {inst_8 : Module R M} {inst_9 : Module S M₂} {inst_10 : EquivLike F M M₂} [self : ContinuousSemilinearEquivClass F σ M M₂] (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.

@[reducible, inline]

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₂] : Prop

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 100]

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 = { toFun := (↑(addMonoidHomOfMemClosureRangeCoe f hf)).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₂) [l.NeBot] (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₂) [l.NeBot] (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

@[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_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

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

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

• f.copy f' h = { toLinearMap := (↑f).copy 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) : ⇑(f.copy 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) : f.copy 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

@[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_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.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.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) s.topologicalClosure ≤ (Submodule.map (↑f) s).topologicalClosure

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 : s.topologicalClosure = ⊤) : (Submodule.map (↑f) s).topologicalClosure = ⊤

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.instSMul {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₂] : SMul S₂ (M₁ →SL[σ₁₂] M₂)

Equations

• ContinuousLinearMap.instSMul = { smul := fun (c : S₂) (f : M₁ →SL[σ₁₂] M₂) => { toLinearMap := c • ↑f, cont := ⋯ } }

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 = ⋯.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 = ⋯.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.instNontrivialId {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₂) : ↑(∑ d ∈ t, f d) = ∑ d ∈ t, ↑(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₂) : ⇑(∑ d ∈ t, f d) = ∑ d ∈ t, ⇑(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₁) : (∑ d ∈ t, f d) b = ∑ d ∈ t, (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

• g.comp f = { toLinearMap := (↑g).comp ↑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₂) : ↑(h.comp f) = (↑h).comp ↑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₂) : ⇑(h.comp 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₁) : (g.comp 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₂) : f.comp (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.id R₂ M₂).comp 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₃) : g.comp 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₂) : g.comp (f₁ + f₂) = g.comp f₁ + g.comp 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₂) : (g₁ + g₂).comp f = g₁.comp f + g₂.comp f

theorem ContinuousLinearMap.comp_finset_sum {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 σ₁₂ σ₂₃ σ₁₃] {ι : Type u_9} {s : Finset ι} [ContinuousAdd M₂] [ContinuousAdd M₃] (g : M₂ →SL[σ₂₃] M₃) (f : ι → M₁ →SL[σ₁₂] M₂) : g.comp (∑ i ∈ s, f i) = ∑ i ∈ s, g.comp (f i)

theorem ContinuousLinearMap.finset_sum_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 σ₁₂ σ₂₃ σ₁₃] {ι : Type u_9} {s : Finset ι} [ContinuousAdd M₃] (g : ι → M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) : (∑ i ∈ s, g i).comp f = ∑ i ∈ s, (g i).comp 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₂) : (h.comp g).comp f = h.comp (g.comp 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 = f.comp 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.instNatCast {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] [ContinuousAdd M₁] : NatCast (M₁ →L[R₁] M₁)

Equations

• ContinuousLinearMap.instNatCast = { natCast := fun (n : ℕ) => n • 1 }

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 = 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 = { 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 : ℕ) [n.AtLeastTwo] (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

• f₁.prod f₂ = { toLinearMap := (↑f₁).prod ↑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₃) : ↑(f₁.prod f₂) = (↑f₁).prod ↑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₁) : (f₁.prod 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.id R₁ M₁).prod 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 (f.prod 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

• f.codRestrict 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) : ↑(f.codRestrict 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₁) : ↑((f.codRestrict 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 (f.codRestrict p h) = LinearMap.ker f

@[reducible, inline]

abbrev 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

• f.rangeRestrict = f.codRestrict (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₂) : ↑f.rangeRestrict = (↑f).rangeRestrict

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

• p.subtypeL = { toLinearMap := p.subtype, 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₁) : ↑p.subtypeL = p.subtype

@[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₁) : ⇑p.subtypeL = ⇑p.subtype

@[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) : p.subtypeL 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 p.subtypeL = 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 p.subtypeL = ⊥

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.fst R₁ M₁ M₂).prod (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.fst R₁ M₂ M₃).comp (f.prod 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.snd R₁ M₂ M₃).comp (f.prod 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

• f₁.prodMap f₂ = (f₁.comp (ContinuousLinearMap.fst R₁ M₁ M₃)).prod (f₂.comp (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₄) : ↑(f₁.prodMap f₂) = (↑f₁).prodMap ↑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₄) : ⇑(f₁.prodMap 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

• f₁.coprod f₂ = { toLinearMap := (↑f₁).coprod ↑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₃) : ↑(f₁.coprod f₂) = (↑f₁).coprod ↑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₂) : (f₁.coprod 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 (f₁.coprod 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₃) : f.comp (ContinuousLinearMap.fst R₁ M₁ M₂) + g.comp (ContinuousLinearMap.snd R₁ M₁ M₂) = f.coprod 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.inl R₁ M₁ M'₁).coprod (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

• c.smulRight f = { toLinearMap := (↑c).smulRight f, 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₁} : (c.smulRight 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.smulRight 1 x).comp (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.pi f).comp g = ContinuousLinearMap.pi fun (i : ι) => (f i).comp 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.proj i).comp (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 Pi.compRightL (R : Type u_1) [Semiring R] {ι : Type u_4} (φ : ι → Type u_5) [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {α : Type u_6} (f : α → ι) : ((i : ι) → φ i) →L[R] (i : α) → φ (f i)

Given a function f : α → ι, it induces a continuous linear function by right composition on product types. For f = Subtype.val, this corresponds to forgetting some set of variables.

Equations

• Pi.compRightL R φ f = { toFun := fun (v : (i : ι) → φ i) (i : α) => v (f i), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem Pi.compRightL_apply (R : Type u_1) [Semiring R] {ι : Type u_4} (φ : ι → Type u_5) [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {α : Type u_6} (f : α → ι) (v : (i : ι) → φ i) (i : α) : (Pi.compRightL R φ f) v i = v (f 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 (f.prod g) = (LinearMap.range f).prod (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₃) : (LinearMap.ker f).prod (LinearMap.ker g) ≤ LinearMap.ker (f.coprod 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 (f.coprod g) = (LinearMap.ker f).prod (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 = 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₂) : g.comp (-f) = -g.comp 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₂) : (-g).comp f = -g.comp 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₂) : g.comp (f₁ - f₂) = g.comp f₁ - g.comp 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₂) : (g₁ - g₂).comp f = g₁.comp f - g₂.comp 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 = 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

• f₁.projKerOfRightInverse f₂ h = (ContinuousLinearMap.id R M - f₂.comp f₁).codRestrict (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) : ↑((f₁.projKerOfRightInverse 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₁)) : (f₁.projKerOfRightInverse 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₂) : (f₁.projKerOfRightInverse 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) : IsOpenMap ⇑f

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₂) : (c • h).comp f = c • h.comp 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₂) : hₗ.comp (c • fₗ) = c • hₗ.comp 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₂) : h.comp (c • f) = σ₂₃ c • h.comp 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 = f.1.prod 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 ↔ f.comp (ContinuousLinearMap.inl R M N₂) = g.comp (ContinuousLinearMap.inl R M N₂) ∧ f.comp (ContinuousLinearMap.inr R M N₂) = g.comp (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 : f.comp (ContinuousLinearMap.inl R M N₂) = g.comp (ContinuousLinearMap.inl R M N₂)) (hr : f.comp (ContinuousLinearMap.inr R M N₂) = g.comp (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₃} [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

• ContinuousLinearMap.prodₗ S = { toFun := ContinuousLinearMap.prodEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := ContinuousLinearMap.prodEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }

@[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 = { 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ₛₗ σ₁₃ = { 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

• c.smulRightₗ = { toFun := c.smulRight, 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) : ⇑c.smulRightₗ = c.smulRight

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 = { 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_5} [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 = { toLinearMap := ↑e.toLinearEquiv, 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_5} [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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] : EquivLike (M₁ ≃SL[σ₁₂] M₂) M₁ M₂

Equations

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

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_5} [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_5} [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_5} [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_5} [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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] : Function.Injective ContinuousLinearEquiv.toLinearEquiv

theorem ContinuousLinearEquiv.ext_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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {f : M₁ ≃SL[σ₁₂] M₂} {g : M₁ ≃SL[σ₁₂] M₂} : f = g ↔ ⇑f = ⇑g

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_5} [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_5} [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_5} [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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) : M₁ ≃ₜ M₂

A continuous linear equivalence induces a homeomorphism.

Equations

• e.toHomeomorph = { toEquiv := e.toEquiv, 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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) : ⇑e.toHomeomorph = ⇑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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) : IsOpenMap ⇑e

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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {α : Type u_8} [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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {α : Type u_8} [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₁ = { toLinearEquiv := LinearEquiv.refl R₁ M₁, 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_5} [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

• e.symm = { toLinearEquiv := e.symm, 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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) : e.symm.toLinearEquiv = e.symm

@[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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) : e.toHomeomorph.symm = e.symm.toHomeomorph

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_5} [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_5} [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 = ⇑h.symm

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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (x : M₁) : Filter.map (⇑e.symm) (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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_6} [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

• e₁.trans e₂ = { toLinearEquiv := e₁.trans e₂.toLinearEquiv, 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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_6} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] (e₁ : M₁ ≃SL[σ₁₂] M₂) (e₂ : M₂ ≃SL[σ₂₃] M₃) : (e₁.trans e₂).toLinearEquiv = e₁.trans e₂.toLinearEquiv

def ContinuousLinearEquiv.prod {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_5} [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₃] [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

• e.prod e' = { toLinearEquiv := e.prod e'.toLinearEquiv, 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_5} [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₃] [Module R₁ M₄] (e : M₁ ≃L[R₁] M₂) (e' : M₃ ≃L[R₁] M₄) (x : M₁ × M₃) : (e.prod 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_5} [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₃] [Module R₁ M₄] (e : M₁ ≃L[R₁] M₂) (e' : M₃ ≃L[R₁] M₄) : ↑(e.prod e') = (↑e).prodMap ↑e'

theorem ContinuousLinearEquiv.prod_symm {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_5} [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₃] [Module R₁ M₄] (e : M₁ ≃L[R₁] M₂) (e' : M₃ ≃L[R₁] M₄) : (e.prod e').symm = e.symm.prod e'.symm

@[simp]

theorem ContinuousLinearEquiv.prodComm_toLinearEquiv (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₂] : (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_5) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] : ∀ (a : M₁ × M₂), (ContinuousLinearEquiv.prodComm R₁ M₁ M₂) a = a.swap

def ContinuousLinearEquiv.prodComm (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₂] : (M₁ × M₂) ≃L[R₁] M₂ × M₁

Product of modules is commutative up to continuous linear isomorphism.

Equations

• ContinuousLinearEquiv.prodComm R₁ M₁ M₂ = { toLinearEquiv := LinearEquiv.prodComm R₁ M₁ M₂, 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_5) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] : (ContinuousLinearEquiv.prodComm R₁ M₁ M₂).symm = 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_5} [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_5} [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_5} [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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_6} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] (e₁ : M₁ ≃SL[σ₁₂] M₂) (e₂ : M₂ ≃SL[σ₂₃] M₃) (c : M₁) : (e₁.trans 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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (c : M₂) : e (e.symm 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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (b : M₁) : e.symm (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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_6} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] (e₁ : M₂ ≃SL[σ₂₁] M₁) (e₂ : M₃ ≃SL[σ₃₂] M₂) (c : M₁) : (e₂.trans e₁).symm c = e₂.symm (e₁.symm 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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₁) : ⇑e.symm '' (⇑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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₂) : ⇑e '' (⇑e.symm '' 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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] {M₃ : Type u_6} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] (f : M₁ ≃SL[σ₁₂] M₂) (f' : M₂ ≃SL[σ₂₃] M₃) : (↑f').comp ↑f = ↑(f.trans 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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) : (↑e).comp ↑e.symm = 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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) : (↑e.symm).comp ↑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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) : ⇑e.symm ∘ ⇑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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) : ⇑e ∘ ⇑e.symm = 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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) : e.symm.symm = e

@[simp]

theorem ContinuousLinearEquiv.refl_symm {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] : (ContinuousLinearEquiv.refl R₁ M₁).symm = 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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (x : M₁) : e.symm.symm 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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) {x : M₂} {y : M₁} : e.symm 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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) {x : M₂} {y : M₁} : y = e.symm 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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₁) : ⇑e '' s = ⇑e.symm ⁻¹' 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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₂) : ⇑e.symm '' 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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₂) : ⇑e.symm ⁻¹' (⇑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_5} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₁) : ⇑e ⁻¹' (⇑e.symm ⁻¹' s) = s

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

@[deprecated ContinuousLinearEquiv.isUniformEmbedding]

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

Alias of ContinuousLinearEquiv.isUniformEmbedding.

theorem LinearEquiv.isUniformEmbedding {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {E₁ : Type u_8} {E₂ : Type u_9} [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 ⇑e.symm) : IsUniformEmbedding ⇑e

@[deprecated LinearEquiv.isUniformEmbedding]

theorem LinearEquiv.uniformEmbedding {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {E₁ : Type u_8} {E₂ : Type u_9} [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 ⇑e.symm) : IsUniformEmbedding ⇑e

Alias of LinearEquiv.isUniformEmbedding.

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_5} [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₂ = { 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_5} [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_5} [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.equivOfInverse f₁ f₂ h₁ h₂).symm = 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_9, 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 = { toLinearEquiv := ULift.moduleEquiv, 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_5} [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₃] {R₄ : Type u_8} [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₃) : (e₁₂.arrowCongrEquiv e₄₃).symm f = (↑e₄₃.symm).comp (f.comp ↑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_5} [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₃] {R₄ : Type u_8} [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₄) : (e₁₂.arrowCongrEquiv e₄₃) f = (↑e₄₃).comp (f.comp ↑e₁₂.symm)

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_5} [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₃] {R₄ : Type u_8} [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

• e.skewProd e' f = { toLinearEquiv := e.skewProd e'.toLinearEquiv ↑f, 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₃) : (e.skewProd 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₄) : (e.skewProd e' f).symm x = (e.symm x.1, e'.symm (x.2 - f (e.symm 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)ˣ) : M ≃L[R] M

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

Equations

• ContinuousLinearEquiv.ofUnit f = { toFun := ⇑↑f, map_add' := ⋯, map_smul' := ⋯, invFun := ⇑f.inv, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

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

• f.toUnit = { val := ↑f, inv := ↑f.symm, 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 = { 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.unitsEquivAut R) u).symm 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

• ContinuousLinearEquiv.equivOfRightInverse f₁ f₂ h = ContinuousLinearEquiv.equivOfInverse (f₁.prod (f₁.projKerOfRightInverse f₂ h)) (f₂.coprod (LinearMap.ker f₁).subtypeL) ⋯ ⋯

@[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.equivOfRightInverse f₁ f₂ h).symm 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 = { 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.funUnique ι R M).symm = Function.const ι

@[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.piFinTwo R M).symm = fun (p : M 0 × M 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)

@[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)

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 = { toLinearEquiv := LinearEquiv.piFinTwo R M, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[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)

@[simp]

theorem ContinuousLinearEquiv.finTwoArrow_symm_apply (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] : ⇑(ContinuousLinearEquiv.finTwoArrow R M).symm = fun (x : M × M) => ![x.1, x.2]

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

• ContinuousLinearEquiv.finTwoArrow R M = { toLinearEquiv := LinearEquiv.finTwoArrow R M, continuous_toFun := ⋯, continuous_invFun := ⋯ }

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

• f.inverse = if h : ∃ (e : M ≃L[R] M₂), ↑e = f then ↑(Classical.choose h).symm 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₂) : (↑e).inverse = ↑e.symm

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) : f.inverse = 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 = (↑e).inverse

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₂) : f.inverse = (Ring.inverse ((↑e.symm).comp f)).comp ↑e.symm

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) : Prop

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

Equations

• p.ClosedComplemented = ∃ (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 : p.ClosedComplemented) : ∃ (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 : p.ClosedComplemented) : IsClosed ↑p

@[simp]

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

@[simp]

theorem Submodule.closedComplemented_top {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] : ⊤.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 : p.ClosedComplemented) : ∃ (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), e.symm 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₁) : (LinearMap.ker f₁).ClosedComplemented

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 S.quotientRel))

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) [ContinuousAdd M] : IsOpenMap ⇑S.mkQ

theorem Submodule.isOpenQuotientMap_mkQ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] (S : Submodule R M) [ContinuousAdd M] : IsOpenQuotientMap ⇑S.mkQ

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

• ⋯ = ⋯

@[simp]

theorem MulOpposite.opContinuousLinearEquiv_apply (R : Type u_1) [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] [TopologicalSpace M] : ∀ (a : M), (MulOpposite.opContinuousLinearEquiv R) a = MulOpposite.op a

@[simp]

theorem MulOpposite.opContinuousLinearEquiv_symm_apply (R : Type u_1) [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] [TopologicalSpace M] : ∀ (a : Mᵐᵒᵖ), (MulOpposite.opContinuousLinearEquiv R).symm a = MulOpposite.unop a

def MulOpposite.opContinuousLinearEquiv (R : Type u_1) [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] [TopologicalSpace M] : M ≃L[R] Mᵐᵒᵖ

The function op is a continuous linear equivalence.

Equations

• MulOpposite.opContinuousLinearEquiv R = { toLinearEquiv := MulOpposite.opLinearEquiv R, continuous_toFun := ⋯, continuous_invFun := ⋯ }