Continuous linear equivalences #
Continuous semilinear / linear / star-linear equivalences between topological modules are denoted
by M ≃SL[σ] M₂
, M ≃L[R] M₂
and M ≃L⋆[R] 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
.
- toFun : M → M₂
- map_add' (x y : M) : (↑self.toLinearEquiv).toFun (x + y) = (↑self.toLinearEquiv).toFun x + (↑self.toLinearEquiv).toFun y
- map_smul' (m : R) (x : M) : (↑self.toLinearEquiv).toFun (m • x) = σ m • (↑self.toLinearEquiv).toFun x
- invFun : M₂ → M
- left_inv : Function.LeftInverse self.invFun (↑self.toLinearEquiv).toFun
- right_inv : Function.RightInverse self.invFun (↑self.toLinearEquiv).toFun
- continuous_toFun : Continuous (↑self.toLinearEquiv).toFun
Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications
M
andM₂
will be topological modules over the topological semiringR
. - continuous_invFun : Continuous self.invFun
Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications
M
andM₂
will be topological modules over the topological semiringR
.
Instances For
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
Instances For
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
Instances For
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
.
Instances
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
Instances For
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
Instances For
A continuous linear equivalence induces a continuous linear map.
Equations
Instances For
Coerce continuous linear equivs to continuous linear maps.
Equations
Equations
A continuous linear equivalence induces a homeomorphism.
Equations
Instances For
An extensionality lemma for R ≃L[R] M
.
The identity map as a continuous linear equivalence.
Equations
Instances For
The inverse of a continuous linear equivalence as a continuous linear equivalence
Equations
Instances For
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
See Note [custom simps projection]
Equations
Instances For
The composition of two continuous linear equivalences as a continuous linear equivalence.
Equations
Instances For
Product of two continuous linear equivalences. The map comes from Equiv.prodCongr
.
Equations
Instances For
Product of modules is commutative up to continuous linear isomorphism.
Equations
Instances For
Create a ContinuousLinearEquiv
from two ContinuousLinearMap
s that are
inverse of each other. See also equivOfInverse'
.
Equations
Instances For
Create a ContinuousLinearEquiv
from two ContinuousLinearMap
s that are
inverse of each other, in the ContinuousLinearMap.comp
sense. See also equivOfInverse
.
Equations
Instances For
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
Instances For
A pair of continuous (semi)linear equivalences generates an equivalence between the spaces of
continuous linear maps. See also ContinuousLinearEquiv.arrowCongr
.
Equations
Instances For
Combine a family of linear equivalences into a linear equivalence of pi
-types.
This is Equiv.piCongrLeft
as a ContinuousLinearEquiv
.
Equations
Instances For
The product over S ⊕ T
of a family of topological modules
is isomorphic (topologically and alegbraically) to the product of
(the product over S
) and (the product over T
).
This is Equiv.sumPiEquivProdPi
as a ContinuousLinearEquiv
.
Equations
Instances For
The product Π t : α, f t
of a family of topological modules is isomorphic
(both topologically and algebraically) to the space f ⬝
when α
only contains ⬝
.
This is Equiv.piUnique
as a ContinuousLinearEquiv
.
Equations
Instances For
Combine a family of continuous linear equivalences into a continuous linear equivalence of pi-types.
Equations
Instances For
Scalar multiplication by a group element as a continuous linear equivalence.
Equations
Instances For
Automorphisms as continuous linear equivalences and as units of the ring of endomorphisms #
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
Instances For
A continuous equivalence from M
to itself determines an invertible continuous linear map.
Equations
Instances For
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
Instances For
Units of a ring as linear automorphisms #
Continuous linear equivalences R ≃L[R] R
are enumerated by Rˣ
.
Equations
Instances For
If ι
has a unique element, then ι → M
is continuously linear equivalent to M
.
Equations
Instances For
Continuous linear equivalence between dependent functions (i : Fin 2) → M i
and M 0 × M 1
.
Equations
Instances For
Continuous linear equivalence between vectors in M² = Fin 2 → M
and M × M
.
Equations
Instances For
Fin.consEquiv
as a continuous linear equivalence.
Equations
Instances For
Fin.cons
in the codomain of continuous linear maps.
Equations
Instances For
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
Instances For
The negation map as a continuous linear equivalence.
Equations
Instances For
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
Instances For
A continuous linear map is invertible if it is the forward direction of a continuous linear equivalence.
Equations
Instances For
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
Instances For
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
.
Alias of ContinuousLinearMap.ringInverse_equiv
.
The function ContinuousLinearEquiv.inverse
can be written in terms of Ring.inverse
for the
ring of self-maps of the domain.
Alias of ContinuousLinearMap.inverse_eq_ringInverse
.
The function ContinuousLinearEquiv.inverse
can be written in terms of Ring.inverse
for the
ring of self-maps of the domain.
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.
The function op
is a continuous linear equivalence.