Continuous linear maps #
In this file we define continuous (semi-)linear maps, as semilinear maps between topological
modules which are continuous. The set of continuous semilinear maps between the topological
R₁-module M and R₂-module M₂ with respect to the RingHom σ is denoted by M →SL[σ] M₂.
Plain linear maps are denoted by M →L[R] M₂ and star-linear maps by M →L⋆[R] M₂.
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 M →ₛₗ[σ] M₂ :
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₂
- cont : Continuous (↑self).toFun
Continuous linear maps between modules. We only put the type classes that are necessary for the definition, although in applications
MandM₂will be topological modules over the topological ringR.
Instances For
Continuous linear maps between modules. We only put the type classes that are necessary for the
definition, although in applications M and M₂ will be topological modules over the topological
ring R.
Instances For
Continuous linear maps between modules. We only put the type classes that are necessary for the
definition, although in applications M and M₂ will be topological modules over the topological
ring R.
Instances For
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 F σ M M₂, ContinuousMapClass F M M₂ :
ContinuousSemilinearMapClass F σ M M₂ asserts F is a type of bundled continuous
σ-semilinear maps M → M₂. See also ContinuousLinearMapClass F R M M₂ for the case where
σ is the identity map on R. A map f between an R-module and an S-module over a ring
homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y
and f (c • x) = (σ c) • f x.
Instances
@[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₂]
:
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₂.
Instances For
@[reducible, inline]
abbrev
StrongDual
(R : Type u_1)
[Semiring R]
[TopologicalSpace R]
(M : Type u_2)
[TopologicalSpace M]
[AddCommMonoid M]
[Module R M]
:
Type (max u_1 u_2)
The strong dual of a topological vector space M over a ring R. This is the space of
continuous linear functionals and is equipped with the topology of uniform convergence
on bounded subsets. StrongDual R M is an abbreviation for M →L[R] R.
Instances For
Properties that hold for non-necessarily commutative semirings. #
@[implicit_reducible]
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₂]
:
Coerce continuous linear maps to linear maps.
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 toLinearMap
@[implicit_reducible]
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₂]
:
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₂
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)
:
@[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)
:
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.continuous_toLinearMap
{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
@[simp]
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₂]
[IsUniformAddGroup E₁]
[IsUniformAddGroup E₂]
(f : E₁ →SL[σ₁₂] E₂)
:
@[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 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
theorem
ContinuousLinearMap.toContinuousAddMonoidHom_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 ContinuousAddMonoidHom.toContinuousAddMonoidHom
@[simp]
theorem
ContinuousLinearMap.toContinuousAddMonoidHom_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 g : M₁ →SL[σ₁₂] M₂}
:
↑f = ↑g ↔ f = g
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.
Instances For
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₂)
:
See Note [custom simps projection].
Instances For
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 g : M₁ →SL[σ₁₂] M₂}
(h : ∀ (x : M₁), f x = g x)
:
f = g
theorem
ContinuousLinearMap.ext_iff
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_6}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
{f g : M₁ →SL[σ₁₂] M₂}
:
f = g ↔ ∀ (x : M₁), f x = g 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
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)
:
Copy of a ContinuousLinearMap with a new toFun equal to the old one. Useful to fix
definitional equalities.
Instances For
@[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.range_coeFn_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₂]
:
Set.range DFunLike.coe = {f : M₁ → M₂ | Continuous f} ∩ Set.range DFunLike.coe
theorem
ContinuousLinearMap.range_toLinearMap
{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₂)
:
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 y : M₁)
:
f (x + y) = f x + f y
@[simp]
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
theorem
ContinuousLinearMap.ext_ring
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[TopologicalSpace R₁]
{f g : R₁ →L[R₁] M₁}
(h : f 1 = g 1)
:
f = g
theorem
ContinuousLinearMap.ext_ring_iff
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[TopologicalSpace R₁]
{f g : R₁ →L[R₁] M₁}
:
f = g ↔ f 1 = g 1
@[simp]
theorem
ContinuousLinearMap.apply_val_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 : M₁ →SL[σ₁₂] M₂)
(x : ↥(↑f).ker)
:
f ↑x = 0
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 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 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₁)
:
Under a continuous linear map, the image of the TopologicalClosure of a submodule is
contained in the TopologicalClosure of its image.
theorem
Submodule.topologicalClosure_mem_invtSubmodule
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[TopologicalSpace R₁]
[ContinuousSMul R₁ M₁]
[ContinuousAdd M₁]
{f : M₁ →L[R₁] M₁}
{s : Submodule R₁ M₁}
(hs : s ∈ Module.End.invtSubmodule ↑f)
:
If a continuous linear map stabilizes a submodule, then it stabilizes its topological closure.
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.
@[implicit_reducible]
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}
[DistribSMul S₂ M₂]
[SMulCommClass R₂ S₂ M₂]
[ContinuousConstSMul S₂ M₂]
:
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}
[DistribSMul 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}
[DistribSMul 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}
[DistribSMul 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}
[DistribSMul S₂ M₂]
[SMulCommClass R₂ S₂ M₂]
[ContinuousConstSMul S₂ M₂]
[DistribSMul T₂ M₂]
[SMulCommClass R₂ T₂ M₂]
[ContinuousConstSMul T₂ M₂]
[SMul S₂ T₂]
[IsScalarTower S₂ T₂ M₂]
:
IsScalarTower S₂ T₂ (M₁ →SL[σ₁₂] M₂)
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}
[DistribSMul S₂ M₂]
[SMulCommClass R₂ S₂ M₂]
[ContinuousConstSMul S₂ M₂]
[DistribSMul T₂ M₂]
[SMulCommClass R₂ T₂ M₂]
[ContinuousConstSMul T₂ M₂]
[SMulCommClass S₂ T₂ M₂]
:
SMulCommClass S₂ T₂ (M₁ →SL[σ₁₂] M₂)
@[implicit_reducible]
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₂]
:
@[implicit_reducible]
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₂]
:
The continuous map that is constantly zero.
@[implicit_reducible]
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₂]
:
@[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
@[simp]
theorem
ContinuousLinearMap.toContinuousAddMonoidHom_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
@[implicit_reducible]
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₁]
:
@[implicit_reducible]
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₂]
:
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₁]
:
the identity map as a continuous linear map.
Instances For
@[implicit_reducible]
instance
ContinuousLinearMap.one
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module 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_one
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
:
↑1 = 1
@[simp]
theorem
ContinuousLinearMap.toContinuousAddMonoidHom_id
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
:
↑(ContinuousLinearMap.id R₁ M₁) = ContinuousAddMonoidHom.id M₁
@[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₁)
@[implicit_reducible]
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₂]
:
@[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 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 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 g : M₁ →SL[σ₁₂] M₂)
:
⇑(f + g) = ⇑f + ⇑g
@[simp]
theorem
ContinuousLinearMap.toContinuousAddMonoidHom_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 g : M₁ →SL[σ₁₂] M₂)
:
↑(f + g) = ↑f + ↑g
@[implicit_reducible]
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₂)
@[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₂)
:
Composition of bounded linear maps.
Instances For
Composition of bounded linear maps.
Instances For
@[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₂)
:
@[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
@[simp]
theorem
ContinuousLinearMap.toContinuousAddMonoidHom_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₂)
:
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
theorem
ContinuousLinearMap.leftInverse_of_comp
{R : Type u_9}
{E : Type u_10}
{F : Type u_11}
[Semiring R]
[TopologicalSpace E]
[AddCommMonoid E]
[Module R E]
[TopologicalSpace F]
[AddCommMonoid F]
[Module R F]
{f : E →L[R] F}
{g : F →L[R] E}
(hinv : g.comp f = ContinuousLinearMap.id R E)
:
Function.LeftInverse ⇑g ⇑f
g ∘ f = id as ContinuousLinearMaps implies g ∘ f = id as functions.
theorem
ContinuousLinearMap.rightInverse_of_comp
{R : Type u_9}
{E : Type u_10}
{F : Type u_11}
[Semiring R]
[TopologicalSpace E]
[AddCommMonoid E]
[Module R E]
[TopologicalSpace F]
[AddCommMonoid F]
[Module R F]
{f : E →L[R] F}
{g : F →L[R] E}
(hinv : f.comp g = ContinuousLinearMap.id R F)
:
Function.RightInverse ⇑g ⇑f
f ∘ g = id as ContinuousLinearMaps implies f ∘ g = id as functions.
@[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₂)
:
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₁ f₂ : M₁ →SL[σ₁₂] M₂)
:
@[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₁ g₂ : M₂ →SL[σ₂₃] M₃)
(f : M₁ →SL[σ₁₂] M₂)
:
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₂)
:
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₂)
:
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₂)
:
theorem
ContinuousLinearMap.cancel_left
{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₁ f₂ : M₁ →SL[σ₁₂] M₂}
(hg : Function.Injective ⇑g)
(h : g.comp f₁ = g.comp f₂)
:
f₁ = f₂
@[implicit_reducible]
instance
ContinuousLinearMap.instMul
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
:
theorem
ContinuousLinearMap.mul_def
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
(f 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 g : M₁ →L[R₁] M₁)
:
↑(f * g) = ↑f * ↑g
@[simp]
theorem
ContinuousLinearMap.coe_mul'
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
(f 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 g : M₁ →L[R₁] M₁)
(x : M₁)
:
(f * g) x = f (g x)
@[implicit_reducible]
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₁)
@[simp]
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 : ℕ)
:
@[simp]
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
@[implicit_reducible]
instance
ContinuousLinearMap.instNatCast
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[ContinuousAdd M₁]
:
@[implicit_reducible]
instance
ContinuousLinearMap.semiring
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[ContinuousAdd M₁]
:
def
ContinuousLinearMap.toLinearMapRingHom
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[ContinuousAdd M₁]
:
ContinuousLinearMap.toLinearMap as a RingHom.
Instances For
@[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₁)
:
toLinearMapRingHom self = ↑self
@[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
def
ContinuousLinearMap.homeomorphOfUnit
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
(T : (M₁ →L[R₁] M₁)ˣ)
:
Construct a homeomorphism from an invertible continuous linear map.
Instances For
@[simp]
theorem
ContinuousLinearMap.homeomorphOfUnit_symm_apply
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
(T : (M₁ →L[R₁] M₁)ˣ)
(a : M₁)
:
(homeomorphOfUnit T).symm a = ↑T⁻¹ a
@[simp]
theorem
ContinuousLinearMap.homeomorphOfUnit_apply
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
(T : (M₁ →L[R₁] M₁)ˣ)
(a : M₁)
:
(homeomorphOfUnit T) a = ↑T a
theorem
ContinuousLinearMap.isHomeomorph_of_isUnit
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{T : M₁ →L[R₁] M₁}
(hT : IsUnit T)
:
IsHomeomorph ⇑T
@[implicit_reducible]
instance
ContinuousLinearMap.applyModule
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[ContinuousAdd M₁]
:
The tautological action by M₁ →L[R₁] M₁ on M.
This generalizes Function.End.applyMulAction.
@[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.
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₁
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₁
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₁
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₂]
[T1Space M₂]
(f : M₁ →SL[σ₁₂] M₂)
:
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₂]
{M' : Type u_9}
[UniformSpace M']
[CompleteSpace M']
[AddCommMonoid M']
[Module R₁ M']
[T1Space M₂]
(f : M' →SL[σ₁₂] M₂)
:
IsComplete ↑(↑f).ker
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₂]
{M' : Type u_9}
[UniformSpace M']
[CompleteSpace M']
[AddCommMonoid M']
[Module R₁ M']
[T1Space M₂]
(f : M' →SL[σ₁₂] M₂)
:
CompleteSpace ↥(↑f).ker
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₂]
{M' : Type u_9}
[UniformSpace M']
[CompleteSpace M']
[AddCommMonoid M']
[Module R₁ M']
[T2Space M₂]
(f g : M' →SL[σ₁₂] M₂)
:
CompleteSpace ↥(LinearMap.eqLocus f 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)
:
Restrict codomain of a continuous linear map.
Instances For
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)
:
(↑(f.codRestrict p h)).ker = (↑f).ker
@[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₂)
:
Restrict the codomain of a continuous linear map f to f.range.
Instances For
@[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₁)
:
Submodule.subtype as a ContinuousLinearMap.
Instances For
@[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₁)
:
@[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₁)
:
@[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
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₁)
:
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₁)
:
def
ContinuousLinearMap.smulRight
{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 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₂)
:
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.
Instances For
@[simp]
theorem
ContinuousLinearMap.coe_smulRight
{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 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₂)
:
@[simp]
theorem
ContinuousLinearMap.smulRight_apply
{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 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_zero
{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 R]
[Semiring S]
[Module R M₁]
[Module R M₂]
[Module R S]
[Module S M₂]
[IsScalarTower R S M₂]
[TopologicalSpace S]
[ContinuousSMul S M₂]
(f : M₁ →L[R] S)
:
f.smulRight 0 = 0
@[simp]
theorem
ContinuousLinearMap.zero_smulRight
{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 R]
[Semiring S]
[Module R M₁]
[Module R M₂]
[Module R S]
[Module S M₂]
[IsScalarTower R S M₂]
[TopologicalSpace S]
[ContinuousSMul S M₂]
{x : M₂}
:
smulRight 0 x = 0
theorem
ContinuousLinearMap.smulRight_comp_smulRight
{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₂]
[TopologicalSpace R₁]
[ContinuousSMul R₁ M₂]
{M₃ : Type u_9}
[AddCommMonoid M₃]
[Module R₁ M₃]
[TopologicalSpace M₃]
[ContinuousSMul R₁ M₃]
(f : M₃ →L[R₁] R₁)
(g : M₁ →L[R₁] R₁)
{x : M₂}
{y : M₃}
:
@[deprecated ContinuousLinearMap.smulRight_comp_smulRight (since := "2025-12-18")]
theorem
ContinuousLinearMap.smulRight_comp
{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₂]
[TopologicalSpace R₁]
[ContinuousSMul R₁ M₂]
{M₃ : Type u_9}
[AddCommMonoid M₃]
[Module R₁ M₃]
[TopologicalSpace M₃]
[ContinuousSMul R₁ M₃]
(f : M₃ →L[R₁] R₁)
(g : M₁ →L[R₁] R₁)
{x : M₂}
{y : M₃}
:
theorem
ContinuousLinearMap.range_smulRight_apply
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_6}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
{R : Type u_9}
[DivisionSemiring R]
[Module R M₁]
[Module R M₂]
[TopologicalSpace R]
[ContinuousSMul R M₂]
{f : M₁ →L[R] R}
(hf : f ≠ 0)
(x : M₂)
:
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₁)
:
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.
Instances For
@[simp]
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₁)
:
(toSpanSingleton R₁ x) r = r • x
@[simp]
theorem
ContinuousLinearMap.toSpanSingleton_zero
(R₁ : Type u_1)
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[TopologicalSpace R₁]
[ContinuousSMul R₁ M₁]
:
toSpanSingleton R₁ 0 = 0
theorem
ContinuousLinearMap.toSpanSingleton_apply_one
(R₁ : Type u_1)
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[TopologicalSpace R₁]
[ContinuousSMul R₁ M₁]
(x : M₁)
:
(toSpanSingleton R₁ x) 1 = x
@[deprecated ContinuousLinearMap.toSpanSingleton_apply_one (since := "2025-12-05")]
theorem
ContinuousLinearMap.toSpanSingleton_one
(R₁ : Type u_1)
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[TopologicalSpace R₁]
[ContinuousSMul R₁ M₁]
(x : M₁)
:
(toSpanSingleton R₁ x) 1 = x
@[simp]
theorem
ContinuousLinearMap.toSpanSingleton_apply_map_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₂)
:
toSpanSingleton R₁ (c 1) = c
@[deprecated ContinuousLinearMap.toSpanSingleton_apply_map_one (since := "2025-12-18")]
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₂)
:
toSpanSingleton R₁ (c 1) = c
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 y : M₁)
:
toSpanSingleton R₁ (x + y) = toSpanSingleton R₁ x + 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_9}
[Monoid α]
[DistribMulAction α M₁]
[ContinuousConstSMul α M₁]
[SMulCommClass R₁ α M₁]
(c : α)
(x : M₁)
:
toSpanSingleton R₁ (c • x) = c • toSpanSingleton R₁ x
theorem
ContinuousLinearMap.smulRight_id
(R₁ : Type u_1)
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
[TopologicalSpace R₁]
[ContinuousSMul R₁ M₁]
:
(ContinuousLinearMap.id R₁ R₁).smulRight = toSpanSingleton R₁
theorem
ContinuousLinearMap.smulRight_one_eq_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₁)
:
smulRight 1 x = toSpanSingleton R₁ x
@[deprecated ContinuousLinearMap.smulRight_one_eq_toSpanSingleton (since := "2025-12-05")]
theorem
ContinuousLinearMap.one_smulRight_eq_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₁)
:
smulRight 1 x = toSpanSingleton R₁ x
Alias of ContinuousLinearMap.smulRight_one_eq_toSpanSingleton.
@[simp]
theorem
ContinuousLinearMap.toLinearMap_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₁)
:
↑(toSpanSingleton R₁ x) = LinearMap.toSpanSingleton R₁ M₁ x
theorem
ContinuousLinearMap.comp_toSpanSingleton
{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₂]
[TopologicalSpace R₁]
[ContinuousSMul R₁ M₂]
[ContinuousSMul R₁ M₁]
(f : M₁ →L[R₁] M₂)
(x : M₁)
:
f.comp (toSpanSingleton R₁ x) = toSpanSingleton R₁ (f x)
theorem
ContinuousLinearMap.toSpanSingleton_comp
{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₂]
[TopologicalSpace R₁]
[ContinuousSMul R₁ M₂]
(f : M₁ →L[R₁] R₁)
(g : M₂)
:
(toSpanSingleton R₁ g).comp f = f.smulRight g
@[simp]
theorem
ContinuousLinearMap.toSpanSingleton_inj
{R₁ : Type u_1}
[Semiring R₁]
{M₂ : Type u_6}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₂]
[TopologicalSpace R₁]
[ContinuousSMul R₁ M₂]
{f f' : M₂}
:
toSpanSingleton R₁ f = toSpanSingleton R₁ f' ↔ f = f'
@[deprecated ContinuousLinearMap.toSpanSingleton_inj (since := "2025-12-18")]
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 f' : M₂}
:
toSpanSingleton R₁ f = toSpanSingleton R₁ f' ↔ f = f'
Alias of ContinuousLinearMap.toSpanSingleton_inj.
theorem
ContinuousLinearMap.toSpanSingleton_comp_toSpanSingleton
{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₁}
:
(toSpanSingleton R₁ x).comp (toSpanSingleton R₁ c) = toSpanSingleton R₁ (c • x)
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)
:
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 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 g : M →SL[σ₁₂] M₂)
(x : M)
:
(↑f - ↑g) x = f x - g x
@[implicit_reducible]
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₂}
[IsTopologicalAddGroup M₂]
:
@[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₂}
[IsTopologicalAddGroup M₂]
(f : M →SL[σ₁₂] M₂)
(x : M)
:
@[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₂}
[IsTopologicalAddGroup M₂]
(f : M →SL[σ₁₂] M₂)
:
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₂}
[IsTopologicalAddGroup M₂]
(f : M →SL[σ₁₂] M₂)
:
@[simp]
theorem
ContinuousLinearMap.toContinuousAddMonoidHom_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₂}
[IsTopologicalAddGroup M₂]
(f : M →SL[σ₁₂] M₂)
:
@[implicit_reducible]
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₂}
[IsTopologicalAddGroup M₂]
:
@[implicit_reducible]
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₂}
[IsTopologicalAddGroup M₂]
:
AddCommGroup (M →SL[σ₁₂] M₂)
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₂}
[IsTopologicalAddGroup M₂]
(f 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₂}
[IsTopologicalAddGroup M₂]
(f 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₂}
[IsTopologicalAddGroup M₂]
(f g : M →SL[σ₁₂] M₂)
:
⇑(f - g) = ⇑f - ⇑g
@[simp]
theorem
ContinuousLinearMap.toContinuousAddMonoidHom_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₂}
[IsTopologicalAddGroup M₂]
(f 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 σ₁₂ σ₂₃ σ₁₃]
[IsTopologicalAddGroup M₂]
[IsTopologicalAddGroup M₃]
(g : M₂ →SL[σ₂₃] M₃)
(f : M →SL[σ₁₂] M₂)
:
@[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 σ₁₂ σ₂₃ σ₁₃]
[IsTopologicalAddGroup M₃]
(g : M₂ →SL[σ₂₃] M₃)
(f : M →SL[σ₁₂] M₂)
:
@[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 σ₁₂ σ₂₃ σ₁₃]
[IsTopologicalAddGroup M₂]
[IsTopologicalAddGroup M₃]
(g : M₂ →SL[σ₂₃] M₃)
(f₁ f₂ : M →SL[σ₁₂] M₂)
:
@[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 σ₁₂ σ₂₃ σ₁₃]
[IsTopologicalAddGroup M₃]
(g₁ g₂ : M₂ →SL[σ₂₃] M₃)
(f : M →SL[σ₁₂] M₂)
:
@[implicit_reducible]
instance
ContinuousLinearMap.ring
{R : Type u_1}
[Ring R]
{M : Type u_4}
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
[IsTopologicalAddGroup M]
:
@[simp]
theorem
ContinuousLinearMap.intCast_apply
{R : Type u_1}
[Ring R]
{M : Type u_4}
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
[IsTopologicalAddGroup M]
(z : ℤ)
(m : M)
:
↑z m = z • m
theorem
ContinuousLinearMap.toSpanSingleton_pow
{R : Type u_1}
[Ring R]
[TopologicalSpace R]
[IsTopologicalRing R]
(c : R)
(n : ℕ)
:
toSpanSingleton R c ^ n = toSpanSingleton R (c ^ n)
@[deprecated ContinuousLinearMap.toSpanSingleton_pow (since := "2025-12-18")]
theorem
ContinuousLinearMap.smulRight_one_pow
{R : Type u_1}
[Ring R]
[TopologicalSpace R]
[IsTopologicalRing R]
(c : R)
(n : ℕ)
:
toSpanSingleton R c ^ n = toSpanSingleton R (c ^ n)
Alias of ContinuousLinearMap.toSpanSingleton_pow.
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 σ₁₂ σ₂₁]
[IsTopologicalAddGroup M]
(f₁ : M →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M)
(h : Function.RightInverse ⇑f₂ ⇑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₂.
Instances For
@[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 σ₁₂ σ₂₁]
[IsTopologicalAddGroup 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 σ₁₂ σ₂₁]
[IsTopologicalAddGroup M]
(f₁ : M →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M)
(h : Function.RightInverse ⇑f₂ ⇑f₁)
(x : ↥(↑f₁).ker)
:
(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 σ₁₂ σ₂₁]
[IsTopologicalAddGroup 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 : StrongDual R M)
(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₂)
:
@[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₂)
:
@[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₂)
:
@[implicit_reducible]
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₂)
@[implicit_reducible]
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₃]
:
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₃)
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₃]
:
The coercion from M →L[R] M₂ to M →ₗ[R] M₂, as a linear map.
Instances For
@[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₃)
:
(coeLM S) 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₃]
:
The coercion from M →SL[σ] M₂ to M →ₛₗ[σ] M₂, as a linear map.
Instances For
@[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₃)
:
(coeLMₛₗ σ₁₃) self = ↑self
def
ContinuousLinearMap.toSpanSingletonLE
(R : Type u_1)
(S : Type u_2)
(M : Type u_3)
[Semiring R]
[Semiring S]
[AddCommMonoid M]
[Module R M]
[Module S M]
[SMulCommClass R S M]
[TopologicalSpace M]
[ContinuousAdd M]
[ContinuousConstSMul S M]
[TopologicalSpace R]
[ContinuousSMul R M]
:
ContinuousLinearMap.toSpanSingleton as a linear equivalence.
Instances For
@[simp]
theorem
ContinuousLinearMap.toSpanSingletonLE_symm_apply
(R : Type u_1)
(S : Type u_2)
(M : Type u_3)
[Semiring R]
[Semiring S]
[AddCommMonoid M]
[Module R M]
[Module S M]
[SMulCommClass R S M]
[TopologicalSpace M]
[ContinuousAdd M]
[ContinuousConstSMul S M]
[TopologicalSpace R]
[ContinuousSMul R M]
:
⇑(toSpanSingletonLE R S M).symm = fun (f : R →L[R] M) => f 1
@[simp]
theorem
ContinuousLinearMap.toSpanSingletonLE_apply
(R : Type u_1)
(S : Type u_2)
(M : Type u_3)
[Semiring R]
[Semiring S]
[AddCommMonoid M]
[Module R M]
[Module S M]
[SMulCommClass R S M]
[TopologicalSpace M]
[ContinuousAdd M]
[ContinuousConstSMul S M]
[TopologicalSpace R]
[ContinuousSMul R M]
:
⇑(toSpanSingletonLE R S M) = toSpanSingleton R
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)
:
Given c : E →L[R] S, c.smulRightₗ is the linear map from F to E →L[R] F
sending f to fun e => c e • f. See also ContinuousLinearMap.smulRightL.
Instances For
@[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
@[implicit_reducible]
instance
ContinuousLinearMap.algebra
{R : Type u_1}
{S : Type u_2}
{M : Type u_3}
[Semiring R]
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
[CommSemiring S]
[Module S M]
[SMulCommClass R S M]
[SMul S R]
[IsScalarTower S R M]
[ContinuousConstSMul S M]
[IsTopologicalAddGroup M]
:
@[simp]
theorem
ContinuousLinearMap.algebraMap_apply
{R : Type u_1}
{S : Type u_2}
{M : Type u_3}
[Semiring R]
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
[CommSemiring S]
[Module S M]
[SMulCommClass R S M]
[SMul S R]
[IsScalarTower S R M]
[ContinuousConstSMul S M]
[IsTopologicalAddGroup M]
(r : S)
(m : M)
:
((algebraMap S (M →L[R] M)) r) m = r • m
def
ContinuousLinearMap.restrictScalars
{A : Type u_1}
{M₁ : Type u_2}
{M₂ : Type u_3}
(R : Type u_4)
[Semiring A]
[Semiring R]
[AddCommMonoid M₁]
[Module A M₁]
[Module R M₁]
[TopologicalSpace M₁]
[AddCommMonoid M₂]
[Module A M₂]
[Module R M₂]
[TopologicalSpace M₂]
[LinearMap.CompatibleSMul M₁ M₂ R A]
(f : M₁ →L[A] 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.
Instances For
@[simp]
theorem
ContinuousLinearMap.coe_restrictScalars
{A : Type u_1}
{M₁ : Type u_2}
{M₂ : Type u_3}
{R : Type u_4}
[Semiring A]
[Semiring R]
[AddCommMonoid M₁]
[Module A M₁]
[Module R M₁]
[TopologicalSpace M₁]
[AddCommMonoid M₂]
[Module A M₂]
[Module R M₂]
[TopologicalSpace M₂]
[LinearMap.CompatibleSMul M₁ M₂ R A]
(f : M₁ →L[A] M₂)
:
↑(restrictScalars R f) = ↑R ↑f
@[simp]
theorem
ContinuousLinearMap.coe_restrictScalars'
{A : Type u_1}
{M₁ : Type u_2}
{M₂ : Type u_3}
{R : Type u_4}
[Semiring A]
[Semiring R]
[AddCommMonoid M₁]
[Module A M₁]
[Module R M₁]
[TopologicalSpace M₁]
[AddCommMonoid M₂]
[Module A M₂]
[Module R M₂]
[TopologicalSpace M₂]
[LinearMap.CompatibleSMul M₁ M₂ R A]
(f : M₁ →L[A] M₂)
:
⇑(restrictScalars R f) = ⇑f
@[simp]
theorem
ContinuousLinearMap.toContinuousAddMonoidHom_restrictScalars
{A : Type u_1}
{M₁ : Type u_2}
{M₂ : Type u_3}
{R : Type u_4}
[Semiring A]
[Semiring R]
[AddCommMonoid M₁]
[Module A M₁]
[Module R M₁]
[TopologicalSpace M₁]
[AddCommMonoid M₂]
[Module A M₂]
[Module R M₂]
[TopologicalSpace M₂]
[LinearMap.CompatibleSMul M₁ M₂ R A]
(f : M₁ →L[A] M₂)
:
↑(restrictScalars R f) = ↑f
@[simp]
theorem
ContinuousLinearMap.restrictScalars_zero
{A : Type u_1}
{M₁ : Type u_2}
{M₂ : Type u_3}
{R : Type u_4}
[Semiring A]
[Semiring R]
[AddCommMonoid M₁]
[Module A M₁]
[Module R M₁]
[TopologicalSpace M₁]
[AddCommMonoid M₂]
[Module A M₂]
[Module R M₂]
[TopologicalSpace M₂]
[LinearMap.CompatibleSMul M₁ M₂ R A]
:
restrictScalars R 0 = 0
@[simp]
theorem
ContinuousLinearMap.restrictScalars_add
{A : Type u_1}
{M₁ : Type u_2}
{M₂ : Type u_3}
{R : Type u_4}
[Semiring A]
[Semiring R]
[AddCommMonoid M₁]
[Module A M₁]
[Module R M₁]
[TopologicalSpace M₁]
[AddCommMonoid M₂]
[Module A M₂]
[Module R M₂]
[TopologicalSpace M₂]
[LinearMap.CompatibleSMul M₁ M₂ R A]
[ContinuousAdd M₂]
(f g : M₁ →L[A] M₂)
:
restrictScalars R (f + g) = restrictScalars R f + restrictScalars R g
@[simp]
theorem
ContinuousLinearMap.restrictScalars_smul
{A : Type u_1}
{M₁ : Type u_2}
{M₂ : Type u_3}
{R : Type u_4}
{S : Type u_5}
[Semiring A]
[Semiring R]
[Semiring S]
[AddCommMonoid M₁]
[Module A M₁]
[Module R M₁]
[TopologicalSpace M₁]
[AddCommMonoid M₂]
[Module A M₂]
[Module R M₂]
[TopologicalSpace M₂]
[LinearMap.CompatibleSMul M₁ M₂ R A]
[Module S M₂]
[ContinuousConstSMul S M₂]
[SMulCommClass A S M₂]
[SMulCommClass R S M₂]
(c : S)
(f : M₁ →L[A] M₂)
:
restrictScalars R (c • f) = c • restrictScalars R f
def
ContinuousLinearMap.restrictScalarsₗ
(A : Type u_1)
(M₁ : Type u_2)
(M₂ : Type u_3)
(R : Type u_4)
(S : Type u_5)
[Semiring A]
[Semiring R]
[Semiring S]
[AddCommMonoid M₁]
[Module A M₁]
[Module R M₁]
[TopologicalSpace M₁]
[AddCommMonoid M₂]
[Module A M₂]
[Module R M₂]
[TopologicalSpace M₂]
[LinearMap.CompatibleSMul M₁ M₂ R A]
[Module S M₂]
[ContinuousConstSMul S M₂]
[SMulCommClass A S M₂]
[SMulCommClass R S M₂]
[ContinuousAdd M₂]
:
ContinuousLinearMap.restrictScalars as a LinearMap. See also
ContinuousLinearMap.restrictScalarsL.
Instances For
@[simp]
theorem
ContinuousLinearMap.coe_restrictScalarsₗ
{A : Type u_1}
{M₁ : Type u_2}
{M₂ : Type u_3}
{R : Type u_4}
{S : Type u_5}
[Semiring A]
[Semiring R]
[Semiring S]
[AddCommMonoid M₁]
[Module A M₁]
[Module R M₁]
[TopologicalSpace M₁]
[AddCommMonoid M₂]
[Module A M₂]
[Module R M₂]
[TopologicalSpace M₂]
[LinearMap.CompatibleSMul M₁ M₂ R A]
[Module S M₂]
[ContinuousConstSMul S M₂]
[SMulCommClass A S M₂]
[SMulCommClass R S M₂]
[ContinuousAdd M₂]
:
⇑(restrictScalarsₗ A M₁ M₂ R S) = restrictScalars R
@[simp]
theorem
ContinuousLinearMap.restrictScalars_sub
{A : Type u_1}
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[Ring A]
[Ring R]
[AddCommGroup M₁]
[Module A M₁]
[Module R M₁]
[TopologicalSpace M₁]
[AddCommGroup M₂]
[Module A M₂]
[Module R M₂]
[TopologicalSpace M₂]
[LinearMap.CompatibleSMul M₁ M₂ R A]
[IsTopologicalAddGroup M₂]
(f g : M₁ →L[A] M₂)
:
restrictScalars R (f - g) = restrictScalars R f - restrictScalars R g
@[simp]
theorem
ContinuousLinearMap.restrictScalars_neg
{A : Type u_1}
{R : Type u_2}
{M₁ : Type u_4}
{M₂ : Type u_5}
[Ring A]
[Ring R]
[AddCommGroup M₁]
[Module A M₁]
[Module R M₁]
[TopologicalSpace M₁]
[AddCommGroup M₂]
[Module A M₂]
[Module R M₂]
[TopologicalSpace M₂]
[LinearMap.CompatibleSMul M₁ M₂ R A]
[IsTopologicalAddGroup M₂]
(f : M₁ →L[A] M₂)
:
restrictScalars R (-f) = -restrictScalars R f
def
Submodule.ClosedComplemented
{R : Type u_1}
[Ring R]
{M : Type u_2}
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
(p : Submodule R M)
:
A submodule p is called complemented if there exists a continuous projection M →ₗ[R] p.
Instances For
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)
:
noncomputable def
Submodule.ClosedComplemented.complement
{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)
:
Submodule R M
An arbitrary choice of closed complement of a closed complemented submodule.
Instances For
theorem
Submodule.ClosedComplemented.isClosed_complement
{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)
:
theorem
Submodule.ClosedComplemented.isCompl_complement
{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)
:
IsCompl p h.complement
theorem
Submodule.ClosedComplemented.isClosed
{R : Type u_1}
[Ring R]
{M : Type u_2}
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
[IsTopologicalAddGroup 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]
:
@[simp]
theorem
Submodule.closedComplemented_top
{R : Type u_1}
[Ring R]
{M : Type u_2}
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
:
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₂]
[IsTopologicalAddGroup M]
(f₁ : M →L[R] M₂)
(f₂ : M₂ →L[R] M)
(h : Function.RightInverse ⇑f₂ ⇑f₁)
:
(↑f₁).ker.ClosedComplemented
theorem
ContinuousLinearMap.isIdempotentElem_toLinearMap_iff
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[TopologicalSpace M]
[AddCommMonoid M]
[Module R M]
{f : M →L[R] M}
:
IsIdempotentElem ↑f ↔ IsIdempotentElem f
theorem
ContinuousLinearMap.IsIdempotentElem.toLinearMap
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[TopologicalSpace M]
[AddCommMonoid M]
[Module R M]
{f : M →L[R] M}
:
IsIdempotentElem f → IsIdempotentElem ↑f
Alias of the reverse direction of ContinuousLinearMap.isIdempotentElem_toLinearMap_iff.
theorem
ContinuousLinearMap.IsIdempotentElem.ext_iff
{R : Type u_1}
{M : Type u_2}
[Ring R]
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
{p q : M →L[R] M}
(hp : IsIdempotentElem p)
(hq : IsIdempotentElem q)
:
Idempotent operators are equal iff their range and kernels are.
theorem
ContinuousLinearMap.IsIdempotentElem.ext
{R : Type u_1}
{M : Type u_2}
[Ring R]
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
{p q : M →L[R] M}
(hp : IsIdempotentElem p)
(hq : IsIdempotentElem q)
:
Alias of the reverse direction of ContinuousLinearMap.IsIdempotentElem.ext_iff.
Idempotent operators are equal iff their range and kernels are.
theorem
ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff
{R : Type u_1}
{M : Type u_2}
[Ring R]
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
{f T : M →L[R] M}
(hf : IsIdempotentElem f)
:
(↑f).range ∈ Module.End.invtSubmodule ↑T ↔ f.comp (T.comp f) = T.comp f
range f is invariant under T if and only if f ∘L T ∘L f = T ∘L f,
for idempotent f.
theorem
ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule
{R : Type u_1}
{M : Type u_2}
[Ring R]
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
{f T : M →L[R] M}
(hf : IsIdempotentElem f)
:
f.comp (T.comp f) = T.comp f → (↑f).range ∈ Module.End.invtSubmodule ↑T
Alias of the reverse direction of ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff.
range f is invariant under T if and only if f ∘L T ∘L f = T ∘L f,
for idempotent f.
theorem
ContinuousLinearMap.IsIdempotentElem.conj_eq_of_range_mem_invtSubmodule
{R : Type u_1}
{M : Type u_2}
[Ring R]
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
{f T : M →L[R] M}
(hf : IsIdempotentElem f)
:
(↑f).range ∈ Module.End.invtSubmodule ↑T → f.comp (T.comp f) = T.comp f
Alias of the forward direction of ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff.
range f is invariant under T if and only if f ∘L T ∘L f = T ∘L f,
for idempotent f.
theorem
ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff
{R : Type u_1}
{M : Type u_2}
[Ring R]
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
{f T : M →L[R] M}
(hf : IsIdempotentElem f)
:
(↑f).ker ∈ Module.End.invtSubmodule ↑T ↔ f.comp (T.comp f) = f.comp T
ker f is invariant under T if and only if f ∘L T ∘L f = f ∘L T,
for idempotent f.
theorem
ContinuousLinearMap.IsIdempotentElem.conj_eq_of_ker_mem_invtSubmodule
{R : Type u_1}
{M : Type u_2}
[Ring R]
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
{f T : M →L[R] M}
(hf : IsIdempotentElem f)
:
(↑f).ker ∈ Module.End.invtSubmodule ↑T → f.comp (T.comp f) = f.comp T
Alias of the forward direction of ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff.
ker f is invariant under T if and only if f ∘L T ∘L f = f ∘L T,
for idempotent f.
theorem
ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule
{R : Type u_1}
{M : Type u_2}
[Ring R]
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
{f T : M →L[R] M}
(hf : IsIdempotentElem f)
:
f.comp (T.comp f) = f.comp T → (↑f).ker ∈ Module.End.invtSubmodule ↑T
Alias of the reverse direction of ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff.
ker f is invariant under T if and only if f ∘L T ∘L f = f ∘L T,
for idempotent f.
theorem
ContinuousLinearMap.IsIdempotentElem.commute_iff
{R : Type u_1}
{M : Type u_2}
[Ring R]
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
{f T : M →L[R] M}
(hf : IsIdempotentElem f)
:
Commute f T ↔ (↑f).range ∈ Module.End.invtSubmodule ↑T ∧ (↑f).ker ∈ Module.End.invtSubmodule ↑T
An idempotent operator f commutes with T if and only if
both range f and ker f are invariant under T.
theorem
ContinuousLinearMap.IsIdempotentElem.commute_iff_of_isUnit
{R : Type u_1}
{M : Type u_2}
[Ring R]
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
[IsTopologicalAddGroup M]
{f T : M →L[R] M}
(hT : IsUnit T)
(hf : IsIdempotentElem f)
:
Commute f T ↔ Submodule.map (↑T) (↑f).range = (↑f).range ∧ Submodule.map (↑T) (↑f).ker = (↑f).ker
An idempotent operator f commutes with a unit operator T if and only if
T (range f) = range f and T (ker f) = ker f.
@[deprecated LinearMap.IsIdempotentElem.range_eq_ker (since := "2025-12-27")]
theorem
ContinuousLinearMap.IsIdempotentElem.range_eq_ker
{S : Type u_5}
[Semiring S]
{E : Type u_7}
[AddCommGroup E]
[Module S E]
{p : E →ₗ[S] E}
(hp : IsIdempotentElem p)
:
p.range = (LinearMap.id - p).ker
Alias of LinearMap.IsIdempotentElem.range_eq_ker.
@[deprecated LinearMap.IsIdempotentElem.ker_eq_range (since := "2025-12-27")]
theorem
ContinuousLinearMap.IsIdempotentElem.ker_eq_range
{S : Type u_5}
[Semiring S]
{E : Type u_7}
[AddCommGroup E]
[Module S E]
{p : E →ₗ[S] E}
(hp : IsIdempotentElem p)
:
p.ker = (LinearMap.id - p).range
Alias of LinearMap.IsIdempotentElem.ker_eq_range.
theorem
ContinuousLinearMap.IsIdempotentElem.isClosed_range
{R : Type u_1}
{M : Type u_2}
[Ring R]
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
[IsTopologicalAddGroup M]
[T1Space M]
{p : M →L[R] M}
(hp : IsIdempotentElem p)
:
def
topDualPairing
(𝕜 : Type u_1)
(E : Type u_2)
[CommSemiring 𝕜]
[TopologicalSpace 𝕜]
[ContinuousAdd 𝕜]
[AddCommMonoid E]
[Module 𝕜 E]
[TopologicalSpace E]
[ContinuousConstSMul 𝕜 𝕜]
:
The canonical pairing of a vector space and its topological dual.
Instances For
@[simp]
theorem
topDualPairing_apply
{𝕜 : Type u_1}
{E : Type u_2}
[CommSemiring 𝕜]
[TopologicalSpace 𝕜]
[ContinuousAdd 𝕜]
[AddCommMonoid E]
[Module 𝕜 E]
[TopologicalSpace E]
[ContinuousConstSMul 𝕜 𝕜]
(v : E →L[𝕜] 𝕜)
(x : E)
:
((topDualPairing 𝕜 E) v) x = v x