Continuous linear maps #
In this file we define the type of continuous (semi)linear maps between topological modules that are continuous, and endow it with its algebraic structure.
Later files endow it with a topological structure, see the docstring of
Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean.
Main definitions #
ContinuousLinearMapis the type of (semi)linear maps between two topological modules that are continuous. It is denoted byM →L[R] Nin theR-linear case,M →SL[σ] Nin theσ-semilinear case, andM →L⋆[R] Nin the conjugate-linear (antilinear) case.StrongDual R Mis an abbreviation forM →L[R] R, the type of continuousR-linear forms onM. As a vector space, it is often called the "topological dual ofM". We use the name "strong dual" because it will (in later files) be endowed with the strong-dual topology, namely the topology of uniform convergence on bounded subsets.ContinuousLinearMap.addCommMonoid,ContinuousLinearMap.module,... : the algebraic structures onM →SL[σ] N.
Notation #
M →L[R] N: the type ofR-linear continuous maps fromMtoN;M →SL[σ] N: the type ofσ-semilinear continuous maps fromMtoN;M →L⋆[σ] N: the type of conjugate-linear (antilinear) continuous maps fromMtoN;f ∘L g: the composition of two continuous linear maps;f ∘SL g: the composition of two continuous semilinear maps.
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.mk_id
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
:
@[simp]
theorem
ContinuousLinearMap.mk_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.instAddMonoid
{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₂]
:
Equations
- One or more equations did not get rendered due to their size.
@[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
- ContinuousLinearMap.addCommMonoid = { toAddMonoid := ContinuousLinearMap.instAddMonoid, add_comm := ⋯ }
@[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 continuous linear maps.
Instances For
Composition of continuous linear maps.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Composition of continuous 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 ∘SL 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 ∘SL 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_finsetSum
{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₂)
:
@[deprecated ContinuousLinearMap.comp_finsetSum (since := "2026-04-08")]
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₂)
:
Alias of ContinuousLinearMap.comp_finsetSum.
theorem
ContinuousLinearMap.finsetSum_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₂)
:
@[deprecated ContinuousLinearMap.finsetSum_comp (since := "2026-04-08")]
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₂)
:
Alias of ContinuousLinearMap.finsetSum_comp.
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 ∘SL f₁ = g ∘SL f₂)
:
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)
:
@[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_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_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₁)
:
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.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.
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.lcomp
{R : Type u_1}
{U : Type u_2}
{V : Type u_3}
(W : Type u_4)
[CommSemiring R]
[AddCommMonoid U]
[Module R U]
[TopologicalSpace U]
[AddCommMonoid V]
[Module R V]
[TopologicalSpace V]
[AddCommMonoid W]
[Module R W]
[TopologicalSpace W]
[ContinuousAdd W]
[ContinuousConstSMul R W]
(f : U →L[R] V)
:
Composition of continuous linear maps, as a linear map. Compare LinearMap.lcomp.
Equations
Instances For
@[simp]
theorem
ContinuousLinearMap.lcomp_apply
{R : Type u_1}
{U : Type u_2}
{V : Type u_3}
(W : Type u_4)
[CommSemiring R]
[AddCommMonoid U]
[Module R U]
[TopologicalSpace U]
[AddCommMonoid V]
[Module R V]
[TopologicalSpace V]
[AddCommMonoid W]
[Module R W]
[TopologicalSpace W]
[ContinuousAdd W]
[ContinuousConstSMul R W]
(f : U →L[R] V)
(l : V →L[R] W)
:
def
ContinuousLinearMap.llcomp
(R : Type u_1)
(U : Type u_2)
(V : Type u_3)
(W : Type u_4)
[CommSemiring R]
[AddCommMonoid U]
[Module R U]
[TopologicalSpace U]
[AddCommMonoid V]
[Module R V]
[TopologicalSpace V]
[ContinuousAdd V]
[ContinuousConstSMul R V]
[AddCommMonoid W]
[Module R W]
[TopologicalSpace W]
[ContinuousAdd W]
[ContinuousConstSMul R W]
:
Composition of continuous linear maps, as a bilinear map. Compare LinearMap.llcomp.
Equations
- ContinuousLinearMap.llcomp R U V W = { toFun := fun (l : U →L[R] V) => ContinuousLinearMap.lcomp W l, map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[simp]
theorem
ContinuousLinearMap.llcomp_apply
(R : Type u_1)
(U : Type u_2)
(V : Type u_3)
(W : Type u_4)
[CommSemiring R]
[AddCommMonoid U]
[Module R U]
[TopologicalSpace U]
[AddCommMonoid V]
[Module R V]
[TopologicalSpace V]
[ContinuousAdd V]
[ContinuousConstSMul R V]
[AddCommMonoid W]
[Module R W]
[TopologicalSpace W]
[ContinuousAdd W]
[ContinuousConstSMul R W]
(l : U →L[R] V)
:
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. See
ContinuousLinearMap.toSpanSingletonLIE for the isometric version
and ContinuousLinearMap.toSpanSingletonCLE for the continuous version.
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
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)
: