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
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₂.
Equations
- ContinuousLinearMapClass F R M M₂ = 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.
Equations
- StrongDual R M = (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.
Equations
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₂]
:
@[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₂}
:
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₂]
:
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₂]
:
@[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₂}
:
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
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].
Equations
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)
:
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₂}
:
@[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₂)
:
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)
:
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)
:
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₂]
:
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₂)
:
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₁)
:
@[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₁)
:
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₁)
:
@[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₁)
:
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)
:
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₁}
:
@[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)
:
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)
:
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 = ⊤)
:
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₁)
:
@[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₂)
:
@[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₂)
:
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₂]
:
Equations
- ContinuousLinearMap.mulAction = { toSMul := ContinuousLinearMap.instSMul, mul_smul := ⋯, one_smul := ⋯ }
@[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₂]
:
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₂]
:
@[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₁)
:
@[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₂]
:
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₂]
:
@[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₂]
:
@[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₁]
:
Equations
@[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₂]
:
Equations
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.
Equations
- ContinuousLinearMap.id R₁ M₁ = { toLinearMap := LinearMap.id, cont := ⋯ }
Instances For
@[implicit_reducible]
instance
ContinuousLinearMap.one
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module 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₁]
:
theorem
ContinuousLinearMap.id_apply
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
(x : M₁)
:
@[simp]
theorem
ContinuousLinearMap.coe_id
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
:
@[simp]
theorem
ContinuousLinearMap.coe_id'
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
:
@[simp]
theorem
ContinuousLinearMap.coe_one
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
:
@[simp]
theorem
ContinuousLinearMap.toContinuousAddMonoidHom_id
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ 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₁}
:
@[simp]
theorem
ContinuousLinearMap.one_apply
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
(x : M₁)
:
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₁)
:
@[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₂)
:
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₂)
:
@[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₂)
:
@[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₂)
Equations
- One or more equations did not get rendered due to their size.
@[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₂)
:
@[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₂)
:
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₁)
:
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.
Equations
- One or more equations did not get rendered due to their size.
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₂)
:
@[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₁)
:
@[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₂)
:
@[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₂)
:
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₃)
:
@[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₂)
:
@[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₂)
:
@[implicit_reducible]
instance
ContinuousLinearMap.instMul
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
:
Equations
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₁)
:
@[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₁)
:
@[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₁)
:
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₁)
:
@[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₁)
Equations
- One or more equations did not get rendered due to their size.
@[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 : ℕ)
:
@[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₁]
:
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- ContinuousLinearMap.toLinearMapRingHom = { toFun := ContinuousLinearMap.toLinearMap, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
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₁)
:
@[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₁)
:
@[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₁)
:
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.
Equations
- ContinuousLinearMap.homeomorphOfUnit T = { toFun := ⇑↑T, invFun := ⇑↑T⁻¹, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
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₁)
:
@[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₁)
:
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₁)
:
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.
Equations
- f.codRestrict p h = { toLinearMap := LinearMap.codRestrict p (↑f) h, cont := ⋯ }
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)
:
@[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₁)
:
@[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)
:
@[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.
Equations
- f.rangeRestrict = f.codRestrict (↑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₂)
:
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)
:
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₁}
:
@[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)
:
@[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₂}
:
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.
Equations
- ContinuousLinearMap.toSpanSingleton R₁ x = { toLinearMap := LinearMap.toSpanSingleton R₁ M₁ x, cont := ⋯ }
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₁)
:
@[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₁]
:
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₁)
:
@[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₁)
:
@[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₂)
:
@[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₂)
:
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₁)
:
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₁)
:
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₁]
:
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₁)
:
@[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₁)
:
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₁)
:
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₁)
:
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₂)
:
@[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₂}
:
@[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₂}
:
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₁}
:
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)
:
@[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)
:
@[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₂)
Equations
- One or more equations did not get rendered due to their size.
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)
:
@[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₂)
:
@[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₂)
:
@[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₂)
:
@[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]
:
Equations
- One or more equations did not get rendered due to their size.
@[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)
:
theorem
ContinuousLinearMap.toSpanSingleton_pow
{R : Type u_1}
[Ring R]
[TopologicalSpace R]
[IsTopologicalRing R]
(c : R)
(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 : ℕ)
:
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₂.
Equations
- f₁.projKerOfRightInverse f₂ h = (ContinuousLinearMap.id R M - f₂.comp f₁).codRestrict (↑f₁).ker ⋯
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)
:
@[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)
:
@[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₂)
:
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₂)
Equations
- ContinuousLinearMap.distribMulAction = { toMulAction := ContinuousLinearMap.mulAction, smul_zero := ⋯, smul_add := ⋯ }
@[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₃]
:
Equations
- ContinuousLinearMap.module = { toDistribMulAction := ContinuousLinearMap.distribMulAction, add_smul := ⋯, zero_smul := ⋯ }
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.
Equations
- ContinuousLinearMap.coeLM S = { toFun := ContinuousLinearMap.toLinearMap, map_add' := ⋯, map_smul' := ⋯ }
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₃)
:
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.
Equations
- ContinuousLinearMap.coeLMₛₗ σ₁₃ = { toFun := ContinuousLinearMap.toLinearMap, map_add' := ⋯, map_smul' := ⋯ }
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₃)
:
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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]
:
@[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]
:
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.
Equations
- c.smulRightₗ = { toFun := c.smulRight, map_add' := ⋯, map_smul' := ⋯ }
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)
:
@[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]
:
Equations
@[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)
:
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.
Equations
- ContinuousLinearMap.restrictScalars R f = { toLinearMap := ↑R ↑f, cont := ⋯ }
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₂)
:
@[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₂)
:
@[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₂)
:
@[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]
:
@[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₂)
:
@[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₂)
:
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.
Equations
- ContinuousLinearMap.restrictScalarsₗ A M₁ M₂ R S = { toFun := ContinuousLinearMap.restrictScalars R, map_add' := ⋯, map_smul' := ⋯ }
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₂]
:
@[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₂)
:
@[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₂)
:
def
Submodule.ClosedComplemented
{R : Type u_1}
[Ring R]
{M : Type u_2}
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
(p : Submodule R M)
:
A submodule p is called complemented if there exists a continuous projection M →ₗ[R] p.
Equations
- p.ClosedComplemented = ∃ (f : M →L[R] ↥p), ∀ (x : ↥p), f ↑x = x
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.
Equations
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}
:
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)
:
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)
:
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.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)
:
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.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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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.
Equations
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)
: