Theory of topological modules and continuous linear maps. #
We use the class ContinuousSMul
for topological (semi) modules and topological vector spaces.
In this file we define continuous (semi-)linear maps, as semilinear maps between topological
modules which are continuous. The set of continuous semilinear maps between the topological
R₁
-module M
and R₂
-module M₂
with respect to the RingHom
σ
is denoted by M →SL[σ] M₂
.
Plain linear maps are denoted by M →L[R] M₂
and star-linear maps by M →L⋆[R] M₂
.
The corresponding notation for equivalences is M ≃SL[σ] M₂
, M ≃L[R] M₂
and M ≃L⋆[R] M₂
.
If M
is a topological module over R
and 0
is a limit of invertible elements of R
, then
⊤
is the only submodule of M
with a nonempty interior.
This is the case, e.g., if R
is a nontrivially normed field.
Let R
be a topological ring such that zero is not an isolated point (e.g., a nontrivially
normed field, see NormedField.punctured_nhds_neBot
). Let M
be a nontrivial module over R
such that c • x = 0
implies c = 0 ∨ x = 0
. Then M
has no isolated points. We formulate this
using NeBot (𝓝[≠] x)
.
This lemma is not an instance because Lean would need to find [ContinuousSMul ?m_1 M]
with
unknown ?m_1
. We register this as an instance for R = ℝ
in Real.punctured_nhds_module_neBot
.
One can also use haveI := Module.punctured_nhds_neBot R M
in a proof.
The span of a separable subset with respect to a separable scalar ring is again separable.
Equations
- ⋯ = ⋯
The (topological-space) closure of a submodule of a topological R
-module M
is itself
a submodule.
Equations
- s.topologicalClosure = { toAddSubmonoid := s.topologicalClosure, smul_mem' := ⋯ }
The topological closure of a closed submodule s
is equal to s
.
A subspace is dense iff its topological closure is the entire space.
Equations
- ⋯ = ⋯
A maximal proper subspace of a topological module (i.e a Submodule
satisfying IsCoatom
)
is either closed or dense.
Continuous linear maps between modules. We only put the type classes that are necessary for the
definition, although in applications M
and M₂
will be topological modules over the topological
ring R
.
Instances For
- ContinuousLinearEquiv.ContinuousLinearMap.coe
- ContinuousLinearMap.LinearMap.coe
- ContinuousLinearMap.add
- ContinuousLinearMap.addCommGroup
- ContinuousLinearMap.addCommMonoid
- ContinuousLinearMap.algebra
- ContinuousLinearMap.applyFaithfulSMul
- ContinuousLinearMap.applyModule
- ContinuousLinearMap.applySMulCommClass
- ContinuousLinearMap.applySMulCommClass'
- ContinuousLinearMap.continuousConstSMul
- ContinuousLinearMap.continuousConstSMul_apply
- ContinuousLinearMap.continuousSMul
- ContinuousLinearMap.continuousSemilinearMapClass
- ContinuousLinearMap.distribMulAction
- ContinuousLinearMap.funLike
- ContinuousLinearMap.hasOpNorm
- ContinuousLinearMap.inhabited
- ContinuousLinearMap.instBorelSpace
- ContinuousLinearMap.instCompleteSpace
- ContinuousLinearMap.instCompleteSpace_1
- ContinuousLinearMap.instContinuousEvalConst
- ContinuousLinearMap.instMeasurableSpace
- ContinuousLinearMap.instMul
- ContinuousLinearMap.instNatCast
- ContinuousLinearMap.instNontrivialId
- ContinuousLinearMap.instSMul
- ContinuousLinearMap.instT2Space
- ContinuousLinearMap.isCentralScalar
- ContinuousLinearMap.isScalarTower
- ContinuousLinearMap.module
- ContinuousLinearMap.monoidWithZero
- ContinuousLinearMap.mulAction
- ContinuousLinearMap.neg
- ContinuousLinearMap.normOneClass
- ContinuousLinearMap.one
- ContinuousLinearMap.ring
- ContinuousLinearMap.semiring
- ContinuousLinearMap.smulCommClass
- ContinuousLinearMap.sub
- ContinuousLinearMap.toNormedAddCommGroup
- ContinuousLinearMap.toNormedAlgebra
- ContinuousLinearMap.toNormedRing
- ContinuousLinearMap.toNormedSpace
- ContinuousLinearMap.toPseudoMetricSpace
- ContinuousLinearMap.toSemiNormedRing
- ContinuousLinearMap.toSeminormedAddCommGroup
- ContinuousLinearMap.topologicalAddGroup
- ContinuousLinearMap.topologicalSpace
- ContinuousLinearMap.uniformAddGroup
- ContinuousLinearMap.uniformContinuousConstSMul
- ContinuousLinearMap.uniformSpace
- ContinuousLinearMap.uniqueOfLeft
- ContinuousLinearMap.uniqueOfRight
- ContinuousLinearMap.zero
- LinearIsometryEquiv.instCoeTCContinuousLinearMap
- LinearMap.canLiftContinuousLinearMap
- instFiniteDimensionalContinuousLinearMapId
- instSecondCountableTopologyContinuousLinearMapIdOfFiniteDimensional
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
.
Continuous linear maps between modules. We only put the type classes that are necessary for the
definition, although in applications M
and M₂
will be topological modules over the topological
ring R
.
Equations
- One or more equations did not get rendered due to their size.
Continuous linear maps between modules. We only put the type classes that are necessary for the
definition, although in applications M
and M₂
will be topological modules over the topological
ring R
.
Equations
- One or more equations did not get rendered due to their size.
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
.
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₂
Continuous linear equivalences between modules. We only put the type classes that are necessary
for the definition, although in applications M
and M₂
will be topological modules over the
topological semiring R
.
Continuous linear equivalences between modules. We only put the type classes that are necessary
for the definition, although in applications M
and M₂
will be topological modules over the
topological semiring R
.
Continuous linear equivalences between modules. We only put the type classes that are necessary
for the definition, although in applications M
and M₂
will be topological modules over the
topological semiring R
.
Continuous linear equivalences between modules. We only put the type classes that are necessary
for the definition, although in applications M
and M₂
will be topological modules over the
topological semiring R
.
Equations
- One or more equations did not get rendered due to their size.
Continuous linear equivalences between modules. We only put the type classes that are necessary
for the definition, although in applications M
and M₂
will be topological modules over the
topological semiring R
.
Equations
- One or more equations did not get rendered due to their size.
ContinuousSemilinearEquivClass F σ M M₂
asserts F
is a type of bundled continuous
σ
-semilinear equivs M → M₂
. See also ContinuousLinearEquivClass F R M M₂
for the case
where σ
is the identity map on R
. A map f
between an R
-module and an S
-module over a ring
homomorphism σ : R →+* S
is semilinear if it satisfies the two properties f (x + y) = f x + f y
and f (c • x) = (σ c) • f x
.
- map_continuous : ∀ (f : F), Continuous ⇑f
ContinuousSemilinearEquivClass F σ M M₂
assertsF
is a type of bundled continuousσ
-semilinear equivsM → M₂
. See alsoContinuousLinearEquivClass F R M M₂
for the case whereσ
is the identity map onR
. A mapf
between anR
-module and anS
-module over a ring homomorphismσ : R →+* S
is semilinear if it satisfies the two propertiesf (x + y) = f x + f y
andf (c • x) = (σ c) • f x
. - inv_continuous : ∀ (f : F), Continuous (EquivLike.inv f)
ContinuousSemilinearEquivClass F σ M M₂
assertsF
is a type of bundled continuousσ
-semilinear equivsM → M₂
. See alsoContinuousLinearEquivClass F R M M₂
for the case whereσ
is the identity map onR
. A mapf
between anR
-module and anS
-module over a ring homomorphismσ : R →+* S
is semilinear if it satisfies the two propertiesf (x + y) = f x + f y
andf (c • x) = (σ c) • f x
.
ContinuousSemilinearEquivClass F σ M M₂
asserts F
is a type of bundled continuous
σ
-semilinear equivs M → M₂
. See also ContinuousLinearEquivClass F R M M₂
for the case
where σ
is the identity map on R
. A map f
between an R
-module and an S
-module over a ring
homomorphism σ : R →+* S
is semilinear if it satisfies the two properties f (x + y) = f x + f y
and f (c • x) = (σ c) • f x
.
ContinuousSemilinearEquivClass F σ M M₂
asserts F
is a type of bundled continuous
σ
-semilinear equivs M → M₂
. See also ContinuousLinearEquivClass F R M M₂
for the case
where σ
is the identity map on R
. A map f
between an R
-module and an S
-module over a ring
homomorphism σ : R →+* S
is semilinear if it satisfies the two properties f (x + y) = f x + f y
and f (c • x) = (σ c) • f x
.
ContinuousLinearEquivClass F σ M M₂
asserts F
is a type of bundled continuous
R
-linear equivs M → M₂
. This is an abbreviation for
ContinuousSemilinearEquivClass F (RingHom.id R) M M₂
.
Equations
- ContinuousLinearEquivClass F R M M₂ = ContinuousSemilinearEquivClass F (RingHom.id R) M M₂
Equations
- ⋯ = ⋯
Constructs a bundled linear map from a function and a proof that this function belongs to the closure of the set of linear maps.
Equations
- linearMapOfMemClosureRangeCoe f hf = { toFun := (↑(addMonoidHomOfMemClosureRangeCoe f hf)).toFun, map_add' := ⋯, map_smul' := ⋯ }
Construct a bundled linear map from a pointwise limit of linear maps
Equations
- linearMapOfTendsto f g h = linearMapOfMemClosureRangeCoe f ⋯
Properties that hold for non-necessarily commutative semirings. #
Coerce continuous linear maps to linear maps.
Equations
- ContinuousLinearMap.LinearMap.coe = { coe := ContinuousLinearMap.toLinearMap }
Equations
- ⋯ = ⋯
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
See Note [custom simps projection].
Equations
Copy of a ContinuousLinearMap
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Equations
- f.copy f' h = { toLinearMap := (↑f).copy f' h, cont := ⋯ }
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.
If the submodule generated by a set s
is dense in the ambient module, then two continuous
linear maps equal on s
are equal.
Under a continuous linear map, the image of the TopologicalClosure
of a submodule is
contained in the TopologicalClosure
of its image.
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.
Equations
- ContinuousLinearMap.mulAction = MulAction.mk ⋯ ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The continuous map that is constantly zero.
Equations
- ContinuousLinearMap.zero = { zero := { toLinearMap := 0, cont := ⋯ } }
Equations
- ContinuousLinearMap.inhabited = { default := 0 }
Equations
- ContinuousLinearMap.uniqueOfLeft = ⋯.unique
Equations
- ContinuousLinearMap.uniqueOfRight = ⋯.unique
the identity map as a continuous linear map.
Equations
- ContinuousLinearMap.id R₁ M₁ = { toLinearMap := LinearMap.id, cont := ⋯ }
Equations
- ContinuousLinearMap.one = { one := ContinuousLinearMap.id R₁ M₁ }
Equations
- ⋯ = ⋯
Equations
- ContinuousLinearMap.addCommMonoid = AddCommMonoid.mk ⋯
Composition of bounded linear maps.
Equations
- g.comp f = { toLinearMap := (↑g).comp ↑f, cont := ⋯ }
Composition of bounded linear maps.
Equations
- One or more equations did not get rendered due to their size.
Equations
- ContinuousLinearMap.instMul = { mul := ContinuousLinearMap.comp }
Equations
- ContinuousLinearMap.monoidWithZero = MonoidWithZero.mk ⋯ ⋯
Equations
- ContinuousLinearMap.semiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯
ContinuousLinearMap.toLinearMap
as a RingHom
.
Equations
- ContinuousLinearMap.toLinearMapRingHom = { toFun := ContinuousLinearMap.toLinearMap, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
The tautological action by M₁ →L[R₁] M₁
on M
.
This generalizes Function.End.applyMulAction
.
Equations
- ContinuousLinearMap.applyModule = Module.compHom M₁ ContinuousLinearMap.toLinearMapRingHom
ContinuousLinearMap.applyModule
is faithful.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The cartesian product of two bounded linear maps, as a bounded linear map.
Equations
- f₁.prod f₂ = { toLinearMap := (↑f₁).prod ↑f₂, cont := ⋯ }
The left injection into a product is a continuous linear map.
Equations
- ContinuousLinearMap.inl R₁ M₁ M₂ = (ContinuousLinearMap.id R₁ M₁).prod 0
The right injection into a product is a continuous linear map.
Equations
- ContinuousLinearMap.inr R₁ M₁ M₂ = ContinuousLinearMap.prod 0 (ContinuousLinearMap.id R₁ M₂)
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Restrict codomain of a continuous linear map.
Equations
- f.codRestrict p h = { toLinearMap := LinearMap.codRestrict p (↑f) h, cont := ⋯ }
Restrict the codomain of a continuous linear map f
to f.range
.
Equations
- f.rangeRestrict = f.codRestrict (LinearMap.range f) ⋯
Submodule.subtype
as a ContinuousLinearMap
.
Equations
- p.subtypeL = { toLinearMap := p.subtype, cont := ⋯ }
Prod.fst
as a ContinuousLinearMap
.
Equations
- ContinuousLinearMap.fst R₁ M₁ M₂ = { toLinearMap := LinearMap.fst R₁ M₁ M₂, cont := ⋯ }
Prod.snd
as a ContinuousLinearMap
.
Equations
- ContinuousLinearMap.snd R₁ M₁ M₂ = { toLinearMap := LinearMap.snd R₁ M₁ M₂, cont := ⋯ }
Prod.map
of two continuous linear maps.
Equations
- f₁.prodMap f₂ = (f₁.comp (ContinuousLinearMap.fst R₁ M₁ M₃)).prod (f₂.comp (ContinuousLinearMap.snd R₁ M₁ M₃))
The continuous linear map given by (x, y) ↦ f₁ x + f₂ y
.
Equations
- f₁.coprod f₂ = { toLinearMap := (↑f₁).coprod ↑f₂, cont := ⋯ }
The linear map fun x => c x • f
. Associates to a scalar-valued linear map and an element of
M₂
the M₂
-valued linear map obtained by multiplying the two (a.k.a. tensoring by M₂
).
See also ContinuousLinearMap.smulRightₗ
and ContinuousLinearMap.smulRightL
.
Equations
- c.smulRight f = { toLinearMap := (↑c).smulRight f, cont := ⋯ }
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 := ⋯ }
A special case of to_span_singleton_smul'
for when R
is commutative.
pi
construction for continuous linear functions. From a family of continuous linear functions
it produces a continuous linear function into a family of topological modules.
Equations
- ContinuousLinearMap.pi f = { toLinearMap := LinearMap.pi fun (i : ι) => ↑(f i), cont := ⋯ }
The projections from a family of topological modules are continuous linear maps.
Equations
- ContinuousLinearMap.proj i = { toLinearMap := LinearMap.proj i, cont := ⋯ }
Given a function f : α → ι
, it induces a continuous linear function by right composition on
product types. For f = Subtype.val
, this corresponds to forgetting some set of variables.
Equations
- Pi.compRightL R φ f = { toFun := fun (v : (i : ι) → φ i) (i : α) => v (f i), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
If I
and J
are complementary index sets, the product of the kernels of the J
th projections
of φ
is linearly equivalent to the product over I
.
Equations
- ContinuousLinearMap.iInfKerProjEquiv R φ hd hu = { toLinearEquiv := LinearMap.iInfKerProjEquiv R φ hd hu, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Equations
- ContinuousLinearMap.addCommGroup = AddCommGroup.mk ⋯
Given a right inverse f₂ : M₂ →L[R] M
to f₁ : M →L[R] M₂
,
projKerOfRightInverse f₁ f₂ h
is the projection M →L[R] LinearMap.ker f₁
along
LinearMap.range f₂
.
Equations
- f₁.projKerOfRightInverse f₂ h = (ContinuousLinearMap.id R M - f₂.comp f₁).codRestrict (LinearMap.ker f₁) ⋯
A nonzero continuous linear functional is open.
Equations
- ContinuousLinearMap.distribMulAction = DistribMulAction.mk ⋯ ⋯
ContinuousLinearMap.prod
as an Equiv
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- ⋯ = ⋯
ContinuousLinearMap.prod
as a LinearEquiv
.
Equations
- ContinuousLinearMap.prodₗ S = { toFun := ContinuousLinearMap.prodEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := ContinuousLinearMap.prodEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }
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' := ⋯ }
The coercion from M →SL[σ] M₂
to M →ₛₗ[σ] M₂
, as a linear map.
Equations
- ContinuousLinearMap.coeLMₛₗ σ₁₃ = { toFun := ContinuousLinearMap.toLinearMap, map_add' := ⋯, map_smul' := ⋯ }
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' := ⋯ }
Equations
- ContinuousLinearMap.algebra = Algebra.ofModule ⋯ ⋯
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 := ⋯ }
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' := ⋯ }
A continuous linear equivalence induces a continuous linear map.
Equations
- ↑e = { toLinearMap := ↑e.toLinearEquiv, cont := ⋯ }
Coerce continuous linear equivs to continuous linear maps.
Equations
- ContinuousLinearEquiv.ContinuousLinearMap.coe = { coe := ContinuousLinearEquiv.toContinuousLinearMap }
Equations
- One or more equations did not get rendered due to their size.
Equations
- ⋯ = ⋯
A continuous linear equivalence induces a homeomorphism.
Equations
- e.toHomeomorph = { toEquiv := e.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
An extensionality lemma for R ≃L[R] M
.
The identity map as a continuous linear equivalence.
Equations
- ContinuousLinearEquiv.refl R₁ M₁ = { toLinearEquiv := LinearEquiv.refl R₁ M₁, continuous_toFun := ⋯, continuous_invFun := ⋯ }
The inverse of a continuous linear equivalence as a continuous linear equivalence
Equations
- e.symm = { toLinearEquiv := e.symm, continuous_toFun := ⋯, continuous_invFun := ⋯ }
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
See Note [custom simps projection]
Equations
- ContinuousLinearEquiv.Simps.symm_apply h = ⇑h.symm
The composition of two continuous linear equivalences as a continuous linear equivalence.
Equations
- e₁.trans e₂ = { toLinearEquiv := e₁.trans e₂.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Product of two continuous linear equivalences. The map comes from Equiv.prodCongr
.
Equations
- e.prod e' = { toLinearEquiv := e.prod e'.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Product of modules is commutative up to continuous linear isomorphism.
Equations
- ContinuousLinearEquiv.prodComm R₁ M₁ M₂ = { toLinearEquiv := LinearEquiv.prodComm R₁ M₁ M₂, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Alias of ContinuousLinearEquiv.isUniformEmbedding
.
Alias of LinearEquiv.isUniformEmbedding
.
Create a ContinuousLinearEquiv
from two ContinuousLinearMap
s that are
inverse of each other. See also equivOfInverse'
.
Equations
- ContinuousLinearEquiv.equivOfInverse f₁ f₂ h₁ h₂ = { toLinearMap := ↑f₁, invFun := ⇑f₂, left_inv := h₁, right_inv := h₂, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Create a ContinuousLinearEquiv
from two ContinuousLinearMap
s that are
inverse of each other, in the ContinuousLinearMap.comp
sense. See also equivOfInverse
.
Equations
- ContinuousLinearEquiv.equivOfInverse' f₁ f₂ h₁ h₂ = ContinuousLinearEquiv.equivOfInverse f₁ f₂ ⋯ ⋯
The inverse of equivOfInverse'
is obtained by swapping the order of its parameters.
The continuous linear equivalences from M
to itself form a group under composition.
Equations
The continuous linear equivalence between ULift M₁
and M₁
.
This is a continuous version of ULift.moduleEquiv
.
Equations
- ContinuousLinearEquiv.ulift = { toLinearEquiv := ULift.moduleEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
A pair of continuous (semi)linear equivalences generates an equivalence between the spaces of
continuous linear maps. See also ContinuousLinearEquiv.arrowCongr
.
Equations
- One or more equations did not get rendered due to their size.
Combine a family of continuous linear equivalences into a continuous linear equivalence of pi-types.
Equations
- ContinuousLinearEquiv.piCongrRight f = { toLinearEquiv := LinearEquiv.piCongrRight fun (i : ι) => ↑(f i), continuous_toFun := ⋯, continuous_invFun := ⋯ }
Equivalence given by a block lower diagonal matrix. e
and e'
are diagonal square blocks,
and f
is a rectangular block below the diagonal.
Equations
- e.skewProd e' f = { toLinearEquiv := e.skewProd e'.toLinearEquiv ↑f, continuous_toFun := ⋯, continuous_invFun := ⋯ }
The negation map as a continuous linear equivalence.
Equations
- ContinuousLinearEquiv.neg R = { toLinearEquiv := LinearEquiv.neg R, continuous_toFun := ⋯, continuous_invFun := ⋯ }
The next theorems cover the identification between M ≃L[R] M
and the group of units of the ring
M →L[R] M
.
An invertible continuous linear map f
determines a continuous equivalence from M
to itself.
Equations
- ContinuousLinearEquiv.ofUnit f = { toFun := ⇑↑f, map_add' := ⋯, map_smul' := ⋯, invFun := ⇑f.inv, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
A continuous equivalence from M
to itself determines an invertible continuous linear map.
Equations
- f.toUnit = { val := ↑f, inv := ↑f.symm, val_inv := ⋯, inv_val := ⋯ }
The units of the algebra of continuous R
-linear endomorphisms of M
is multiplicatively
equivalent to the type of continuous linear equivalences between M
and itself.
Equations
- ContinuousLinearEquiv.unitsEquiv R M = { toFun := ContinuousLinearEquiv.ofUnit, invFun := ContinuousLinearEquiv.toUnit, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
Continuous linear equivalences R ≃L[R] R
are enumerated by Rˣ
.
Equations
- One or more equations did not get rendered due to their size.
A pair of continuous linear maps such that f₁ ∘ f₂ = id
generates a continuous
linear equivalence e
between M
and M₂ × f₁.ker
such that (e x).2 = x
for x ∈ f₁.ker
,
(e x).1 = f₁ x
, and (e (f₂ y)).2 = 0
. The map is given by e x = (f₁ x, x - f₂ (f₁ x))
.
Equations
- ContinuousLinearEquiv.equivOfRightInverse f₁ f₂ h = ContinuousLinearEquiv.equivOfInverse (f₁.prod (f₁.projKerOfRightInverse f₂ h)) (f₂.coprod (LinearMap.ker f₁).subtypeL) ⋯ ⋯
If ι
has a unique element, then ι → M
is continuously linear equivalent to M
.
Equations
- ContinuousLinearEquiv.funUnique ι R M = { toLinearEquiv := LinearEquiv.funUnique ι R M, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Continuous linear equivalence between dependent functions (i : Fin 2) → M i
and M 0 × M 1
.
Equations
- ContinuousLinearEquiv.piFinTwo R M = { toLinearEquiv := LinearEquiv.piFinTwo R M, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Continuous linear equivalence between vectors in M² = Fin 2 → M
and M × M
.
Equations
- ContinuousLinearEquiv.finTwoArrow R M = { toLinearEquiv := LinearEquiv.finTwoArrow R M, continuous_toFun := ⋯, continuous_invFun := ⋯ }
A continuous linear map is invertible if it is the forward direction of a continuous linear equivalence.
Introduce a function inverse
from M →L[R] M₂
to M₂ →L[R] M
, which sends f
to f.symm
if
f
is a continuous linear equivalence and to 0
otherwise. This definition is somewhat ad hoc,
but one needs a fully (rather than partially) defined inverse function for some purposes, including
for calculus.
Equations
- f.inverse = if h : f.IsInvertible then ↑(Classical.choose h).symm else 0
By definition, if f
is not invertible then inverse f = 0
.
Alias of ContinuousLinearMap.inverse_of_not_isInvertible
.
By definition, if f
is not invertible then inverse f = 0
.
The function ContinuousLinearEquiv.inverse
can be written in terms of Ring.inverse
for the
ring of self-maps of the domain.
A submodule p
is called complemented if there exists a continuous projection M →ₗ[R] p
.
If p
is a closed complemented submodule,
then there exists a submodule q
and a continuous linear equivalence M ≃L[R] (p × q)
such that
e (x : p) = (x, 0)
, e (y : q) = (0, y)
, and e.symm x = x.1 + x.2
.
In fact, the properties of e
imply the properties of e.symm
and vice versa,
but we provide both for convenience.
Equations
- QuotientModule.Quotient.topologicalSpace S = inferInstanceAs (TopologicalSpace (Quotient S.quotientRel))
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The function op
is a continuous linear equivalence.
Equations
- MulOpposite.opContinuousLinearEquiv R = { toLinearEquiv := MulOpposite.opLinearEquiv R, continuous_toFun := ⋯, continuous_invFun := ⋯ }