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₂.
structure
ContinuousLinearEquiv
{R : Type u_1}
{S : Type u_2}
[Semiring R]
[Semiring S]
(σ : R →+* S)
{σ' : S →+* R}
[RingHomInvPair σ σ']
[RingHomInvPair σ' σ]
(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 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
MandM₂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
MandM₂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
class
ContinuousSemilinearEquivClass
(F : Type u_1)
{R : outParam (Type u_2)}
{S : outParam (Type u_3)}
[Semiring R]
[Semiring S]
(σ : outParam (R →+* S))
{σ' : outParam (S →+* R)}
[RingHomInvPair σ σ']
[RingHomInvPair σ' σ]
(M : outParam (Type u_4))
[TopologicalSpace M]
[AddCommMonoid M]
(M₂ : outParam (Type u_5))
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R M]
[Module S M₂]
[EquivLike F M M₂]
extends SemilinearEquivClass F σ M M₂ :
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₂assertsFis a type of bundled continuousσ-semilinear equivsM → M₂. See alsoContinuousLinearEquivClass F R M M₂for the case whereσis the identity map onR. A mapfbetween anR-module and anS-module over a ring homomorphismσ : R →+* Sis semilinear if it satisfies the two propertiesf (x + y) = f x + f yandf (c • x) = (σ c) • f x. - inv_continuous (f : F) : Continuous (EquivLike.inv f)
ContinuousSemilinearEquivClass F σ M M₂assertsFis a type of bundled continuousσ-semilinear equivsM → M₂. See alsoContinuousLinearEquivClass F R M M₂for the case whereσis the identity map onR. A mapfbetween anR-module and anS-module over a ring homomorphismσ : R →+* Sis semilinear if it satisfies the two propertiesf (x + y) = f x + f yandf (c • x) = (σ c) • f x.
Instances
@[reducible, inline]
abbrev
ContinuousLinearEquivClass
(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₂]
[EquivLike F M M₂]
:
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
@[instance 100]
instance
ContinuousSemilinearEquivClass.continuousSemilinearMapClass
(F : Type u_1)
{R : Type u_2}
{S : Type u_3}
[Semiring R]
[Semiring S]
(σ : R →+* S)
{σ' : S →+* R}
[RingHomInvPair σ σ']
[RingHomInvPair σ' σ]
(M : Type u_4)
[TopologicalSpace M]
[AddCommMonoid M]
(M₂ : Type u_5)
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R M]
[Module S M₂]
[EquivLike F M M₂]
[s : ContinuousSemilinearEquivClass F σ M M₂]
:
ContinuousSemilinearMapClass F σ M M₂
@[instance 100]
instance
ContinuousSemilinearEquivClass.instHomeomorphClass
(F : Type u_1)
{R : Type u_2}
{S : Type u_3}
[Semiring R]
[Semiring S]
(σ : R →+* S)
{σ' : S →+* R}
[RingHomInvPair σ σ']
[RingHomInvPair σ' σ]
(M : Type u_4)
[TopologicalSpace M]
[AddCommMonoid M]
(M₂ : Type u_5)
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R M]
[Module S M₂]
[EquivLike F M M₂]
[s : ContinuousSemilinearEquivClass F σ M M₂]
:
HomeomorphClass F M M₂
def
ContinuousLinearMap.iInfKerProjEquiv
(R : Type u_1)
[Semiring R]
{ι : Type u_4}
(φ : ι → Type u_5)
[(i : ι) → TopologicalSpace (φ i)]
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
{I J : Set ι}
[DecidablePred fun (i : ι) => i ∈ I]
(hd : Disjoint I J)
(hu : Set.univ ⊆ I ∪ J)
:
If I and J are complementary index sets, the product of the kernels of the Jth projections
of φ is linearly equivalent to the product over I.
Equations
Instances For
def
ContinuousLinearEquiv.toContinuousLinearMap
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
A continuous linear equivalence induces a continuous linear map.
Equations
Instances For
instance
ContinuousLinearEquiv.ContinuousLinearMap.coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
:
Coerce continuous linear equivs to continuous linear maps.
Equations
instance
ContinuousLinearEquiv.equivLike
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
:
Equations
instance
ContinuousLinearEquiv.continuousSemilinearEquivClass
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
:
ContinuousSemilinearEquivClass (M₁ ≃SL[σ₁₂] M₂) σ₁₂ M₁ M₂
@[simp]
theorem
ContinuousLinearEquiv.coe_mk
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃ₛₗ[σ₁₂] M₂)
(a : Continuous (↑e).toFun)
(b : Continuous e.invFun)
:
theorem
ContinuousLinearEquiv.coe_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(b : M₁)
:
@[simp]
theorem
ContinuousLinearEquiv.coe_toLinearEquiv
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(f : M₁ ≃SL[σ₁₂] M₂)
:
@[simp]
theorem
ContinuousLinearEquiv.coe_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
theorem
ContinuousLinearEquiv.toLinearEquiv_injective
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
:
theorem
ContinuousLinearEquiv.ext
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
{f g : M₁ ≃SL[σ₁₂] M₂}
(h : ⇑f = ⇑g)
:
theorem
ContinuousLinearEquiv.ext_iff
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
{f g : M₁ ≃SL[σ₁₂] M₂}
:
theorem
ContinuousLinearEquiv.coe_injective
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
:
@[simp]
theorem
ContinuousLinearEquiv.coe_inj
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
{e e' : M₁ ≃SL[σ₁₂] M₂}
:
def
ContinuousLinearEquiv.toHomeomorph
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
A continuous linear equivalence induces a homeomorphism.
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.coe_toHomeomorph
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
theorem
ContinuousLinearEquiv.isOpenMap
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
IsOpenMap ⇑e
theorem
ContinuousLinearEquiv.image_closure
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : Set M₁)
:
theorem
ContinuousLinearEquiv.preimage_closure
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : Set M₂)
:
@[simp]
theorem
ContinuousLinearEquiv.isClosed_image
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{s : Set M₁}
:
theorem
ContinuousLinearEquiv.map_nhds_eq
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(x : M₁)
:
theorem
ContinuousLinearEquiv.map_zero
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
theorem
ContinuousLinearEquiv.map_add
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(x y : M₁)
:
@[simp]
theorem
ContinuousLinearEquiv.map_smulₛₗ
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(c : R₁)
(x : M₁)
:
theorem
ContinuousLinearEquiv.map_smul
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₁ M₂]
(e : M₁ ≃L[R₁] M₂)
(c : R₁)
(x : M₁)
:
theorem
ContinuousLinearEquiv.map_eq_zero_iff
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{x : M₁}
:
theorem
ContinuousLinearEquiv.continuous
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
Continuous ⇑e
theorem
ContinuousLinearEquiv.continuousOn
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{s : Set M₁}
:
ContinuousOn (⇑e) s
theorem
ContinuousLinearEquiv.continuousAt
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{x : M₁}
:
ContinuousAt (⇑e) x
theorem
ContinuousLinearEquiv.continuousWithinAt
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{s : Set M₁}
{x : M₁}
:
ContinuousWithinAt (⇑e) s x
theorem
ContinuousLinearEquiv.comp_continuousOn_iff
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
{α : Type u_8}
[TopologicalSpace α]
(e : M₁ ≃SL[σ₁₂] M₂)
{f : α → M₁}
{s : Set α}
:
theorem
ContinuousLinearEquiv.comp_continuous_iff
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
{α : Type u_8}
[TopologicalSpace α]
(e : M₁ ≃SL[σ₁₂] M₂)
{f : α → M₁}
:
theorem
ContinuousLinearEquiv.ext₁
{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)
:
An extensionality lemma for R ≃L[R] M.
def
ContinuousLinearEquiv.refl
(R₁ : Type u_1)
[Semiring R₁]
(M₁ : Type u_4)
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
:
The identity map as a continuous linear equivalence.
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.refl_apply
(R₁ : Type u_1)
[Semiring R₁]
(M₁ : Type u_4)
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
(x : M₁)
:
@[simp]
theorem
ContinuousLinearEquiv.coe_refl
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
:
@[simp]
theorem
ContinuousLinearEquiv.coe_refl'
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
:
def
ContinuousLinearEquiv.symm
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
The inverse of a continuous linear equivalence as a continuous linear equivalence
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.toLinearEquiv_symm
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
@[deprecated ContinuousLinearEquiv.toLinearEquiv_symm (since := "2025-06-08")]
theorem
ContinuousLinearEquiv.symm_toLinearEquiv
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
Alias of ContinuousLinearEquiv.toLinearEquiv_symm.
@[simp]
theorem
ContinuousLinearEquiv.coe_symm_toLinearEquiv
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
@[simp]
theorem
ContinuousLinearEquiv.toHomeomorph_symm
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
@[deprecated "use instead `toHomeomorph_symm`, in the reverse direction" (since := "2025-06-08")]
theorem
ContinuousLinearEquiv.symm_toHomeomorph
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
@[simp]
theorem
ContinuousLinearEquiv.coe_symm_toHomeomorph
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
def
ContinuousLinearEquiv.Simps.apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[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
ContinuousLinearEquiv.Simps.symm_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(h : M₁ ≃SL[σ₁₂] M₂)
:
M₂ → M₁
See Note [custom simps projection]
Equations
Instances For
theorem
ContinuousLinearEquiv.symm_map_nhds_eq
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(x : M₁)
:
def
ContinuousLinearEquiv.trans
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[Semiring R₁]
[Semiring R₂]
[Semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[RingHomInvPair σ₂₃ σ₃₂]
[RingHomInvPair σ₃₂ σ₂₃]
{σ₁₃ : R₁ →+* R₃}
{σ₃₁ : R₃ →+* R₁}
[RingHomInvPair σ₁₃ σ₃₁]
[RingHomInvPair σ₃₁ σ₁₃]
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
{M₃ : Type u_6}
[TopologicalSpace M₃]
[AddCommMonoid M₃]
[Module R₁ M₁]
[Module R₂ M₂]
[Module R₃ M₃]
(e₁ : M₁ ≃SL[σ₁₂] M₂)
(e₂ : M₂ ≃SL[σ₂₃] M₃)
:
The composition of two continuous linear equivalences as a continuous linear equivalence.
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.trans_toLinearEquiv
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[Semiring R₁]
[Semiring R₂]
[Semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[RingHomInvPair σ₂₃ σ₃₂]
[RingHomInvPair σ₃₂ σ₂₃]
{σ₁₃ : R₁ →+* R₃}
{σ₃₁ : R₃ →+* R₁}
[RingHomInvPair σ₁₃ σ₃₁]
[RingHomInvPair σ₃₁ σ₁₃]
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
{M₃ : Type u_6}
[TopologicalSpace M₃]
[AddCommMonoid M₃]
[Module R₁ M₁]
[Module R₂ M₂]
[Module R₃ M₃]
(e₁ : M₁ ≃SL[σ₁₂] M₂)
(e₂ : M₂ ≃SL[σ₂₃] M₃)
:
def
ContinuousLinearEquiv.prodCongr
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[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₃]
[Module R₁ M₄]
(e : M₁ ≃L[R₁] M₂)
(e' : M₃ ≃L[R₁] M₄)
:
Product of two continuous linear equivalences. The map comes from Equiv.prodCongr.
Equations
Instances For
@[deprecated ContinuousLinearEquiv.prodCongr (since := "2025-06-06")]
def
ContinuousLinearEquiv.prod
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[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₃]
[Module R₁ M₄]
(e : M₁ ≃L[R₁] M₂)
(e' : M₃ ≃L[R₁] M₄)
:
Alias of ContinuousLinearEquiv.prodCongr.
Product of two continuous linear equivalences. The map comes from Equiv.prodCongr.
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.prodCongr_apply
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[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₃]
[Module R₁ M₄]
(e : M₁ ≃L[R₁] M₂)
(e' : M₃ ≃L[R₁] M₄)
(x : M₁ × M₃)
:
@[deprecated ContinuousLinearEquiv.prodCongr_apply (since := "2025-06-06")]
theorem
ContinuousLinearEquiv.prod_apply
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[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₃]
[Module R₁ M₄]
(e : M₁ ≃L[R₁] M₂)
(e' : M₃ ≃L[R₁] M₄)
(x : M₁ × M₃)
:
Alias of ContinuousLinearEquiv.prodCongr_apply.
@[simp]
theorem
ContinuousLinearEquiv.coe_prodCongr
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[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₃]
[Module R₁ M₄]
(e : M₁ ≃L[R₁] M₂)
(e' : M₃ ≃L[R₁] M₄)
:
@[deprecated ContinuousLinearEquiv.coe_prodCongr (since := "2025-06-06")]
theorem
ContinuousLinearEquiv.coe_prod
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[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₃]
[Module R₁ M₄]
(e : M₁ ≃L[R₁] M₂)
(e' : M₃ ≃L[R₁] M₄)
:
Alias of ContinuousLinearEquiv.coe_prodCongr.
theorem
ContinuousLinearEquiv.prodCongr_symm
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[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₃]
[Module R₁ M₄]
(e : M₁ ≃L[R₁] M₂)
(e' : M₃ ≃L[R₁] M₄)
:
@[deprecated ContinuousLinearEquiv.prodCongr_symm (since := "2025-06-06")]
theorem
ContinuousLinearEquiv.prod_symm
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[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₃]
[Module R₁ M₄]
(e : M₁ ≃L[R₁] M₂)
(e' : M₃ ≃L[R₁] M₄)
:
Alias of ContinuousLinearEquiv.prodCongr_symm.
def
ContinuousLinearEquiv.prodComm
(R₁ : Type u_1)
[Semiring R₁]
(M₁ : Type u_4)
[TopologicalSpace M₁]
[AddCommMonoid M₁]
(M₂ : Type u_5)
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₁ M₂]
:
Product of modules is commutative up to continuous linear isomorphism.
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.prodComm_apply
(R₁ : Type u_1)
[Semiring R₁]
(M₁ : Type u_4)
[TopologicalSpace M₁]
[AddCommMonoid M₁]
(M₂ : Type u_5)
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₁ M₂]
(a✝ : M₁ × M₂)
:
@[simp]
theorem
ContinuousLinearEquiv.prodComm_toLinearEquiv
(R₁ : Type u_1)
[Semiring R₁]
(M₁ : Type u_4)
[TopologicalSpace M₁]
[AddCommMonoid M₁]
(M₂ : Type u_5)
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₁ M₂]
:
@[simp]
theorem
ContinuousLinearEquiv.prodComm_symm
(R₁ : Type u_1)
[Semiring R₁]
(M₁ : Type u_4)
[TopologicalSpace M₁]
[AddCommMonoid M₁]
(M₂ : Type u_5)
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₁ M₂]
:
def
ContinuousLinearEquiv.prodAssoc
(R : Type u_8)
(M₁ : Type u_9)
(M₂ : Type u_10)
(M₃ : Type u_11)
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M₁]
[Module R M₂]
[Module R M₃]
[TopologicalSpace M₁]
[TopologicalSpace M₂]
[TopologicalSpace M₃]
:
The product of topological modules is associative up to continuous linear isomorphism.
This is LinearEquiv.prodAssoc prodAssoc as a continuous linear equivalence.
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.prodAssoc_toLinearEquiv
(R : Type u_8)
(M₁ : Type u_9)
(M₂ : Type u_10)
(M₃ : Type u_11)
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M₁]
[Module R M₂]
[Module R M₃]
[TopologicalSpace M₁]
[TopologicalSpace M₂]
[TopologicalSpace M₃]
:
@[simp]
theorem
ContinuousLinearEquiv.coe_prodAssoc
(R : Type u_8)
(M₁ : Type u_9)
(M₂ : Type u_10)
(M₃ : Type u_11)
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M₁]
[Module R M₂]
[Module R M₃]
[TopologicalSpace M₁]
[TopologicalSpace M₂]
[TopologicalSpace M₃]
:
@[simp]
theorem
ContinuousLinearEquiv.prodAssoc_apply
(R : Type u_8)
(M₁ : Type u_9)
(M₂ : Type u_10)
(M₃ : Type u_11)
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M₁]
[Module R M₂]
[Module R M₃]
[TopologicalSpace M₁]
[TopologicalSpace M₂]
[TopologicalSpace M₃]
(p₁ : M₁)
(p₂ : M₂)
(p₃ : M₃)
:
@[simp]
theorem
ContinuousLinearEquiv.prodAssoc_symm_apply
(R : Type u_8)
(M₁ : Type u_9)
(M₂ : Type u_10)
(M₃ : Type u_11)
[Semiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[Module R M₁]
[Module R M₂]
[Module R M₃]
[TopologicalSpace M₁]
[TopologicalSpace M₂]
[TopologicalSpace M₃]
(p₁ : M₁)
(p₂ : M₂)
(p₃ : M₃)
:
def
ContinuousLinearEquiv.prodUnique
(R : Type u_8)
(M : Type u_9)
(N : Type u_10)
[Semiring R]
[TopologicalSpace M]
[AddCommMonoid M]
[TopologicalSpace N]
[AddCommMonoid N]
[Unique N]
[Module R M]
[Module R N]
:
The natural equivalence M × N ≃L[R] M for any Unique type N.
This is Equiv.prodUnique as a continuous linear equivalence.
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.coe_prodUnique
(R : Type u_8)
(M : Type u_9)
(N : Type u_10)
[Semiring R]
[TopologicalSpace M]
[AddCommMonoid M]
[TopologicalSpace N]
[AddCommMonoid N]
[Unique N]
[Module R M]
[Module R N]
:
@[simp]
theorem
ContinuousLinearEquiv.prodUnique_apply
(R : Type u_8)
(M : Type u_9)
(N : Type u_10)
[Semiring R]
[TopologicalSpace M]
[AddCommMonoid M]
[TopologicalSpace N]
[AddCommMonoid N]
[Unique N]
[Module R M]
[Module R N]
(x : M × N)
:
@[simp]
theorem
ContinuousLinearEquiv.prodUnique_symm_apply
(R : Type u_8)
(M : Type u_9)
(N : Type u_10)
[Semiring R]
[TopologicalSpace M]
[AddCommMonoid M]
[TopologicalSpace N]
[AddCommMonoid N]
[Unique N]
[Module R M]
[Module R N]
(x : M)
:
def
ContinuousLinearEquiv.uniqueProd
(R : Type u_8)
(M : Type u_9)
(N : Type u_10)
[Semiring R]
[TopologicalSpace M]
[AddCommMonoid M]
[TopologicalSpace N]
[AddCommMonoid N]
[Unique N]
[Module R M]
[Module R N]
:
The natural equivalence N × M ≃L[R] M for any Unique type N.
This is Equiv.uniqueProd as a continuous linear equivalence.
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.coe_uniqueProd
(R : Type u_8)
(M : Type u_9)
(N : Type u_10)
[Semiring R]
[TopologicalSpace M]
[AddCommMonoid M]
[TopologicalSpace N]
[AddCommMonoid N]
[Unique N]
[Module R M]
[Module R N]
:
@[simp]
theorem
ContinuousLinearEquiv.uniqueProd_apply
(R : Type u_8)
(M : Type u_9)
(N : Type u_10)
[Semiring R]
[TopologicalSpace M]
[AddCommMonoid M]
[TopologicalSpace N]
[AddCommMonoid N]
[Unique N]
[Module R M]
[Module R N]
(x : N × M)
:
@[simp]
theorem
ContinuousLinearEquiv.uniqueProd_symm_apply
(R : Type u_8)
(M : Type u_9)
(N : Type u_10)
[Semiring R]
[TopologicalSpace M]
[AddCommMonoid M]
[TopologicalSpace N]
[AddCommMonoid N]
[Unique N]
[Module R M]
[Module R N]
(x : M)
:
theorem
ContinuousLinearEquiv.bijective
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
theorem
ContinuousLinearEquiv.injective
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
theorem
ContinuousLinearEquiv.surjective
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
@[simp]
theorem
ContinuousLinearEquiv.trans_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[Semiring R₁]
[Semiring R₂]
[Semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[RingHomInvPair σ₂₃ σ₃₂]
[RingHomInvPair σ₃₂ σ₂₃]
{σ₁₃ : R₁ →+* R₃}
{σ₃₁ : R₃ →+* R₁}
[RingHomInvPair σ₁₃ σ₃₁]
[RingHomInvPair σ₃₁ σ₁₃]
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
{M₃ : Type u_6}
[TopologicalSpace M₃]
[AddCommMonoid M₃]
[Module R₁ M₁]
[Module R₂ M₂]
[Module R₃ M₃]
(e₁ : M₁ ≃SL[σ₁₂] M₂)
(e₂ : M₂ ≃SL[σ₂₃] M₃)
(c : M₁)
:
@[simp]
theorem
ContinuousLinearEquiv.apply_symm_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(c : M₂)
:
@[simp]
theorem
ContinuousLinearEquiv.symm_apply_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(b : M₁)
:
@[simp]
theorem
ContinuousLinearEquiv.symm_trans_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[Semiring R₁]
[Semiring R₂]
[Semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[RingHomInvPair σ₂₃ σ₃₂]
[RingHomInvPair σ₃₂ σ₂₃]
{σ₁₃ : R₁ →+* R₃}
{σ₃₁ : R₃ →+* R₁}
[RingHomInvPair σ₁₃ σ₃₁]
[RingHomInvPair σ₃₁ σ₁₃]
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
{M₃ : Type u_6}
[TopologicalSpace M₃]
[AddCommMonoid M₃]
[Module R₁ M₁]
[Module R₂ M₂]
[Module R₃ M₃]
(e₁ : M₂ ≃SL[σ₂₁] M₁)
(e₂ : M₃ ≃SL[σ₃₂] M₂)
(c : M₁)
:
@[simp]
theorem
ContinuousLinearEquiv.symm_image_image
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : Set M₁)
:
@[simp]
theorem
ContinuousLinearEquiv.image_symm_image
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : Set M₂)
:
@[simp]
theorem
ContinuousLinearEquiv.comp_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[Semiring R₁]
[Semiring R₂]
[Semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[RingHomInvPair σ₂₃ σ₃₂]
[RingHomInvPair σ₃₂ σ₂₃]
{σ₁₃ : R₁ →+* R₃}
{σ₃₁ : R₃ →+* R₁}
[RingHomInvPair σ₁₃ σ₃₁]
[RingHomInvPair σ₃₁ σ₁₃]
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
{M₃ : Type u_6}
[TopologicalSpace M₃]
[AddCommMonoid M₃]
[Module R₁ M₁]
[Module R₂ M₂]
[Module R₃ M₃]
(f : M₁ ≃SL[σ₁₂] M₂)
(f' : M₂ ≃SL[σ₂₃] M₃)
:
@[simp]
theorem
ContinuousLinearEquiv.coe_comp_coe_symm
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
@[simp]
theorem
ContinuousLinearEquiv.coe_symm_comp_coe
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
@[simp]
theorem
ContinuousLinearEquiv.symm_comp_self
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
@[simp]
theorem
ContinuousLinearEquiv.self_comp_symm
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
@[simp]
theorem
ContinuousLinearEquiv.symm_symm
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
:
theorem
ContinuousLinearEquiv.symm_bijective
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
:
@[simp]
theorem
ContinuousLinearEquiv.refl_symm
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
:
theorem
ContinuousLinearEquiv.symm_symm_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(x : M₁)
:
theorem
ContinuousLinearEquiv.symm_apply_eq
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{x : M₂}
{y : M₁}
:
theorem
ContinuousLinearEquiv.eq_symm_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
{x : M₂}
{y : M₁}
:
theorem
ContinuousLinearEquiv.image_eq_preimage
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : Set M₁)
:
theorem
ContinuousLinearEquiv.image_symm_eq_preimage
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : Set M₂)
:
@[simp]
theorem
ContinuousLinearEquiv.symm_preimage_preimage
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : Set M₂)
:
@[simp]
theorem
ContinuousLinearEquiv.preimage_symm_preimage
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(e : M₁ ≃SL[σ₁₂] M₂)
(s : Set M₁)
:
theorem
ContinuousLinearEquiv.isUniformEmbedding
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{E₁ : Type u_8}
{E₂ : Type u_9}
[UniformSpace E₁]
[UniformSpace E₂]
[AddCommGroup E₁]
[AddCommGroup E₂]
[Module R₁ E₁]
[Module R₂ E₂]
[IsUniformAddGroup E₁]
[IsUniformAddGroup E₂]
(e : E₁ ≃SL[σ₁₂] E₂)
:
theorem
LinearEquiv.isUniformEmbedding
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{E₁ : Type u_8}
{E₂ : Type u_9}
[UniformSpace E₁]
[UniformSpace E₂]
[AddCommGroup E₁]
[AddCommGroup E₂]
[Module R₁ E₁]
[Module R₂ E₂]
[IsUniformAddGroup E₁]
[IsUniformAddGroup E₂]
(e : E₁ ≃ₛₗ[σ₁₂] E₂)
(h₁ : Continuous ⇑e)
(h₂ : Continuous ⇑e.symm)
:
def
ContinuousLinearEquiv.equivOfInverse
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(f₁ : M₁ →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M₁)
(h₁ : Function.LeftInverse ⇑f₂ ⇑f₁)
(h₂ : Function.RightInverse ⇑f₂ ⇑f₁)
:
Create a ContinuousLinearEquiv from two ContinuousLinearMaps that are
inverse of each other. See also equivOfInverse'.
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.equivOfInverse_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(f₁ : M₁ →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M₁)
(h₁ : Function.LeftInverse ⇑f₂ ⇑f₁)
(h₂ : Function.RightInverse ⇑f₂ ⇑f₁)
(x : M₁)
:
@[simp]
theorem
ContinuousLinearEquiv.symm_equivOfInverse
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(f₁ : M₁ →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M₁)
(h₁ : Function.LeftInverse ⇑f₂ ⇑f₁)
(h₂ : Function.RightInverse ⇑f₂ ⇑f₁)
:
def
ContinuousLinearEquiv.equivOfInverse'
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(f₁ : M₁ →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M₁)
(h₁ : f₁.comp f₂ = ContinuousLinearMap.id R₂ M₂)
(h₂ : f₂.comp f₁ = ContinuousLinearMap.id R₁ M₁)
:
Create a ContinuousLinearEquiv from two ContinuousLinearMaps that are
inverse of each other, in the ContinuousLinearMap.comp sense. See also equivOfInverse.
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.equivOfInverse'_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(f₁ : M₁ →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M₁)
(h₁ : f₁.comp f₂ = ContinuousLinearMap.id R₂ M₂)
(h₂ : f₂.comp f₁ = ContinuousLinearMap.id R₁ M₁)
(x : M₁)
:
@[simp]
theorem
ContinuousLinearEquiv.symm_equivOfInverse'
{R₁ : Type u_1}
{R₂ : Type u_2}
[Semiring R₁]
[Semiring R₂]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[TopologicalSpace M₂]
[AddCommMonoid M₂]
[Module R₁ M₁]
[Module R₂ M₂]
(f₁ : M₁ →SL[σ₁₂] M₂)
(f₂ : M₂ →SL[σ₂₁] M₁)
(h₁ : f₁.comp f₂ = ContinuousLinearMap.id R₂ M₂)
(h₂ : f₂.comp f₁ = ContinuousLinearMap.id R₁ M₁)
:
The inverse of equivOfInverse' is obtained by swapping the order of its parameters.
instance
ContinuousLinearEquiv.automorphismGroup
{R₁ : Type u_1}
[Semiring R₁]
(M₁ : Type u_4)
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
:
The continuous linear equivalences from M to itself form a group under composition.
Equations
def
ContinuousLinearEquiv.ulift
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
:
The continuous linear equivalence between ULift M₁ and M₁.
This is a continuous version of ULift.moduleEquiv.
Equations
Instances For
def
ContinuousLinearEquiv.arrowCongrEquiv
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[Semiring R₁]
[Semiring R₂]
[Semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[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₃]
{R₄ : Type u_8}
[Semiring R₄]
[Module R₄ M₄]
{σ₃₄ : R₃ →+* R₄}
{σ₄₃ : R₄ →+* R₃}
[RingHomInvPair σ₃₄ σ₄₃]
[RingHomInvPair σ₄₃ σ₃₄]
{σ₂₄ : R₂ →+* R₄}
{σ₁₄ : R₁ →+* R₄}
[RingHomCompTriple σ₂₁ σ₁₄ σ₂₄]
[RingHomCompTriple σ₂₄ σ₄₃ σ₂₃]
[RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
(e₁₂ : M₁ ≃SL[σ₁₂] M₂)
(e₄₃ : M₄ ≃SL[σ₄₃] M₃)
:
A pair of continuous (semi)linear equivalences generates an equivalence between the spaces of
continuous linear maps. See also ContinuousLinearEquiv.arrowCongr.
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.arrowCongrEquiv_symm_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[Semiring R₁]
[Semiring R₂]
[Semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[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₃]
{R₄ : Type u_8}
[Semiring R₄]
[Module R₄ M₄]
{σ₃₄ : R₃ →+* R₄}
{σ₄₃ : R₄ →+* R₃}
[RingHomInvPair σ₃₄ σ₄₃]
[RingHomInvPair σ₄₃ σ₃₄]
{σ₂₄ : R₂ →+* R₄}
{σ₁₄ : R₁ →+* R₄}
[RingHomCompTriple σ₂₁ σ₁₄ σ₂₄]
[RingHomCompTriple σ₂₄ σ₄₃ σ₂₃]
[RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
(e₁₂ : M₁ ≃SL[σ₁₂] M₂)
(e₄₃ : M₄ ≃SL[σ₄₃] M₃)
(f : M₂ →SL[σ₂₃] M₃)
:
@[simp]
theorem
ContinuousLinearEquiv.arrowCongrEquiv_apply
{R₁ : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
[Semiring R₁]
[Semiring R₂]
[Semiring R₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₁ : R₂ →+* R₁}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
{M₂ : Type u_5}
[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₃]
{R₄ : Type u_8}
[Semiring R₄]
[Module R₄ M₄]
{σ₃₄ : R₃ →+* R₄}
{σ₄₃ : R₄ →+* R₃}
[RingHomInvPair σ₃₄ σ₄₃]
[RingHomInvPair σ₄₃ σ₃₄]
{σ₂₄ : R₂ →+* R₄}
{σ₁₄ : R₁ →+* R₄}
[RingHomCompTriple σ₂₁ σ₁₄ σ₂₄]
[RingHomCompTriple σ₂₄ σ₄₃ σ₂₃]
[RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
(e₁₂ : M₁ ≃SL[σ₁₂] M₂)
(e₄₃ : M₄ ≃SL[σ₄₃] M₃)
(f : M₁ →SL[σ₁₄] M₄)
:
def
ContinuousLinearEquiv.piCongrLeft
(R : Type u_9)
[Semiring R]
{ι : Type u_10}
{ι' : Type u_11}
(φ : ι → Type u_12)
[(i : ι) → AddCommMonoid (φ i)]
[(i : ι) → Module R (φ i)]
[(i : ι) → TopologicalSpace (φ i)]
(e : ι' ≃ ι)
:
Combine a family of linear equivalences into a linear equivalence of pi-types.
This is Equiv.piCongrLeft as a ContinuousLinearEquiv.
Equations
Instances For
def
ContinuousLinearEquiv.sumPiEquivProdPi
(R : Type u_9)
[Semiring R]
(S : Type u_10)
(T : Type u_11)
(A : S ⊕ T → Type u_12)
[(st : S ⊕ T) → AddCommMonoid (A st)]
[(st : S ⊕ T) → Module R (A st)]
[(st : S ⊕ T) → TopologicalSpace (A st)]
:
The product over S ⊕ T of a family of topological modules
is isomorphic (topologically and algebraically) to the product of
(the product over S) and (the product over T).
This is Equiv.sumPiEquivProdPi as a ContinuousLinearEquiv.
Equations
Instances For
def
ContinuousLinearEquiv.piUnique
{α : Type u_9}
[Unique α]
(R : Type u_10)
[Semiring R]
(f : α → Type u_11)
[(x : α) → AddCommMonoid (f x)]
[(x : α) → Module R (f x)]
[(x : α) → TopologicalSpace (f x)]
:
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
@[simp]
theorem
ContinuousLinearEquiv.piUnique_symm_apply
{α : Type u_9}
[Unique α]
(R : Type u_10)
[Semiring R]
(f : α → Type u_11)
[(x : α) → AddCommMonoid (f x)]
[(x : α) → Module R (f x)]
[(x : α) → TopologicalSpace (f x)]
:
@[simp]
theorem
ContinuousLinearEquiv.piUnique_apply
{α : Type u_9}
[Unique α]
(R : Type u_10)
[Semiring R]
(f : α → Type u_11)
[(x : α) → AddCommMonoid (f x)]
[(x : α) → Module R (f x)]
[(x : α) → TopologicalSpace (f x)]
:
def
ContinuousLinearEquiv.piCongrRight
{R₁ : Type u_1}
[Semiring R₁]
{ι : Type u_9}
{M : ι → Type u_10}
[(i : ι) → TopologicalSpace (M i)]
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R₁ (M i)]
{N : ι → Type u_11}
[(i : ι) → TopologicalSpace (N i)]
[(i : ι) → AddCommMonoid (N i)]
[(i : ι) → Module R₁ (N i)]
(f : (i : ι) → M i ≃L[R₁] N i)
:
Combine a family of continuous linear equivalences into a continuous linear equivalence of pi-types.
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.piCongrRight_apply
{R₁ : Type u_1}
[Semiring R₁]
{ι : Type u_9}
{M : ι → Type u_10}
[(i : ι) → TopologicalSpace (M i)]
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R₁ (M i)]
{N : ι → Type u_11}
[(i : ι) → TopologicalSpace (N i)]
[(i : ι) → AddCommMonoid (N i)]
[(i : ι) → Module R₁ (N i)]
(f : (i : ι) → M i ≃L[R₁] N i)
(m : (i : ι) → M i)
(i : ι)
:
@[simp]
theorem
ContinuousLinearEquiv.piCongrRight_symm_apply
{R₁ : Type u_1}
[Semiring R₁]
{ι : Type u_9}
{M : ι → Type u_10}
[(i : ι) → TopologicalSpace (M i)]
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R₁ (M i)]
{N : ι → Type u_11}
[(i : ι) → TopologicalSpace (N i)]
[(i : ι) → AddCommMonoid (N i)]
[(i : ι) → Module R₁ (N i)]
(f : (i : ι) → M i ≃L[R₁] N i)
(n : (i : ι) → N i)
(i : ι)
:
def
ContinuousLinearEquiv.smulLeft
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{G : Type u_9}
[Group G]
[DistribMulAction G M₁]
[ContinuousConstSMul G M₁]
[SMulCommClass G R₁ M₁]
:
Scalar multiplication by a group element as a continuous linear equivalence.
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.smulLeft_apply_toLinearEquiv
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{G : Type u_9}
[Group G]
[DistribMulAction G M₁]
[ContinuousConstSMul G M₁]
[SMulCommClass G R₁ M₁]
(g : G)
:
@[simp]
theorem
ContinuousLinearEquiv.smulLeft_apply_apply
{R₁ : Type u_1}
[Semiring R₁]
{M₁ : Type u_4}
[TopologicalSpace M₁]
[AddCommMonoid M₁]
[Module R₁ M₁]
{G : Type u_9}
[Group G]
[DistribMulAction G M₁]
[ContinuousConstSMul G M₁]
[SMulCommClass G R₁ M₁]
(g : G)
(a✝ : M₁)
:
Automorphisms as continuous linear equivalences and as units of the ring of endomorphisms #
The next theorems cover the identification between M ≃L[R] Mand the group of units of the ring
M →L[R] M.
def
ContinuousLinearEquiv.ofUnit
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[TopologicalSpace M]
(f : (M →L[R] M)ˣ)
:
An invertible continuous linear map f determines a continuous equivalence from M to itself.
Equations
Instances For
def
ContinuousLinearEquiv.toUnit
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[TopologicalSpace M]
(f : M ≃L[R] M)
:
A continuous equivalence from M to itself determines an invertible continuous linear map.
Equations
Instances For
def
ContinuousLinearEquiv.unitsEquiv
(R : Type u_1)
(M : Type u_2)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[TopologicalSpace M]
:
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
@[simp]
theorem
ContinuousLinearEquiv.unitsEquiv_apply
(R : Type u_1)
(M : Type u_2)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[TopologicalSpace M]
(f : (M →L[R] M)ˣ)
(x : M)
:
Units of a ring as linear automorphisms #
def
ContinuousLinearEquiv.unitsEquivAut
(R : Type u_1)
[Semiring R]
[TopologicalSpace R]
[ContinuousMul R]
:
Continuous linear equivalences R ≃L[R] R are enumerated by Rˣ.
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.unitsEquivAut_apply
{R : Type u_1}
[Semiring R]
[TopologicalSpace R]
[ContinuousMul R]
(u : Rˣ)
(x : R)
:
@[simp]
theorem
ContinuousLinearEquiv.unitsEquivAut_apply_symm
{R : Type u_1}
[Semiring R]
[TopologicalSpace R]
[ContinuousMul R]
(u : Rˣ)
(x : R)
:
@[simp]
theorem
ContinuousLinearEquiv.unitsEquivAut_symm_apply
{R : Type u_1}
[Semiring R]
[TopologicalSpace R]
[ContinuousMul R]
(e : R ≃L[R] R)
:
def
ContinuousLinearEquiv.funUnique
(ι : Type u_1)
(R : Type u_2)
(M : Type u_3)
[Unique ι]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[TopologicalSpace M]
:
If ι has a unique element, then ι → M is continuously linear equivalent to M.
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.coe_funUnique
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[Unique ι]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[TopologicalSpace M]
:
@[simp]
theorem
ContinuousLinearEquiv.coe_funUnique_symm
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[Unique ι]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[TopologicalSpace M]
:
def
ContinuousLinearEquiv.piFinTwo
(R : Type u_2)
[Semiring R]
(M : Fin 2 → Type u_4)
[(i : Fin 2) → AddCommMonoid (M i)]
[(i : Fin 2) → Module R (M i)]
[(i : Fin 2) → TopologicalSpace (M i)]
:
Continuous linear equivalence between dependent functions (i : Fin 2) → M i and M 0 × M 1.
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.piFinTwo_symm_apply
(R : Type u_2)
[Semiring R]
(M : Fin 2 → Type u_4)
[(i : Fin 2) → AddCommMonoid (M i)]
[(i : Fin 2) → Module R (M i)]
[(i : Fin 2) → TopologicalSpace (M i)]
:
def
ContinuousLinearEquiv.finTwoArrow
(R : Type u_2)
(M : Type u_3)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[TopologicalSpace M]
:
Continuous linear equivalence between vectors in M² = Fin 2 → M and M × M.
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.finTwoArrow_symm_apply
(R : Type u_2)
(M : Type u_3)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[TopologicalSpace M]
:
@[simp]
theorem
ContinuousLinearEquiv.finTwoArrow_apply
(R : Type u_2)
(M : Type u_3)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[TopologicalSpace M]
:
def
Fin.consEquivL
{n : ℕ}
(R : Type u_4)
(M : Fin n.succ → Type u_5)
[Semiring R]
[(i : Fin n.succ) → AddCommMonoid (M i)]
[(i : Fin n.succ) → Module R (M i)]
[(i : Fin n.succ) → TopologicalSpace (M i)]
:
Fin.consEquiv as a continuous linear equivalence.
Equations
Instances For
@[simp]
@[reducible, inline]
abbrev
ContinuousLinearMap.finCons
{n : ℕ}
{R : Type u_4}
{M : Fin n.succ → Type u_5}
{N : Type u_6}
[Semiring R]
[(i : Fin n.succ) → AddCommMonoid (M i)]
[(i : Fin n.succ) → Module R (M i)]
[(i : Fin n.succ) → TopologicalSpace (M i)]
[AddCommMonoid N]
[Module R N]
[TopologicalSpace N]
(f : N →L[R] M 0)
(fs : N →L[R] (i : Fin n) → M i.succ)
:
Fin.cons in the codomain of continuous linear maps.
Equations
Instances For
def
ContinuousLinearEquiv.skewProd
{R : Type u_1}
[Semiring R]
{M : Type u_2}
[TopologicalSpace M]
[AddCommGroup M]
{M₂ : Type u_3}
[TopologicalSpace M₂]
[AddCommGroup M₂]
{M₃ : Type u_4}
[TopologicalSpace M₃]
[AddCommGroup M₃]
{M₄ : Type u_5}
[TopologicalSpace M₄]
[AddCommGroup M₄]
[Module R M]
[Module R M₂]
[Module R M₃]
[Module R M₄]
[IsTopologicalAddGroup M₄]
(e : M ≃L[R] M₂)
(e' : M₃ ≃L[R] M₄)
(f : M →L[R] M₄)
:
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
@[simp]
theorem
ContinuousLinearEquiv.skewProd_apply
{R : Type u_1}
[Semiring R]
{M : Type u_2}
[TopologicalSpace M]
[AddCommGroup M]
{M₂ : Type u_3}
[TopologicalSpace M₂]
[AddCommGroup M₂]
{M₃ : Type u_4}
[TopologicalSpace M₃]
[AddCommGroup M₃]
{M₄ : Type u_5}
[TopologicalSpace M₄]
[AddCommGroup M₄]
[Module R M]
[Module R M₂]
[Module R M₃]
[Module R M₄]
[IsTopologicalAddGroup M₄]
(e : M ≃L[R] M₂)
(e' : M₃ ≃L[R] M₄)
(f : M →L[R] M₄)
(x : M × M₃)
:
@[simp]
theorem
ContinuousLinearEquiv.skewProd_symm_apply
{R : Type u_1}
[Semiring R]
{M : Type u_2}
[TopologicalSpace M]
[AddCommGroup M]
{M₂ : Type u_3}
[TopologicalSpace M₂]
[AddCommGroup M₂]
{M₃ : Type u_4}
[TopologicalSpace M₃]
[AddCommGroup M₃]
{M₄ : Type u_5}
[TopologicalSpace M₄]
[AddCommGroup M₄]
[Module R M]
[Module R M₂]
[Module R M₃]
[Module R M₄]
[IsTopologicalAddGroup M₄]
(e : M ≃L[R] M₂)
(e' : M₃ ≃L[R] M₄)
(f : M →L[R] M₄)
(x : M₂ × M₄)
:
def
ContinuousLinearEquiv.neg
(R : Type u_1)
[Semiring R]
{M : Type u_2}
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
[ContinuousNeg M]
:
The negation map as a continuous linear equivalence.
Equations
Instances For
@[simp]
theorem
ContinuousLinearEquiv.coe_neg
{R : Type u_1}
[Semiring R]
{M : Type u_2}
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
[ContinuousNeg M]
:
@[simp]
theorem
ContinuousLinearEquiv.neg_apply
{R : Type u_1}
[Semiring R]
{M : Type u_2}
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
[ContinuousNeg M]
(x : M)
:
@[simp]
theorem
ContinuousLinearEquiv.symm_neg
{R : Type u_1}
[Semiring R]
{M : Type u_2}
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
[ContinuousNeg M]
:
theorem
ContinuousLinearEquiv.map_sub
{R : Type u_1}
[Ring R]
{R₂ : Type u_2}
[Ring R₂]
{M : Type u_3}
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
{M₂ : Type u_4}
[TopologicalSpace M₂]
[AddCommGroup M₂]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
(e : M ≃SL[σ₁₂] M₂)
(x y : M)
:
theorem
ContinuousLinearEquiv.map_neg
{R : Type u_1}
[Ring R]
{R₂ : Type u_2}
[Ring R₂]
{M : Type u_3}
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
{M₂ : Type u_4}
[TopologicalSpace M₂]
[AddCommGroup M₂]
[Module R₂ M₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
(e : M ≃SL[σ₁₂] M₂)
(x : M)
:
def
ContinuousLinearEquiv.equivOfRightInverse
{R : Type u_1}
[Ring R]
{M : Type u_3}
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
{M₂ : Type u_4}
[TopologicalSpace M₂]
[AddCommGroup M₂]
[Module R M₂]
[IsTopologicalAddGroup M]
(f₁ : M →L[R] M₂)
(f₂ : M₂ →L[R] M)
(h : Function.RightInverse ⇑f₂ ⇑f₁)
:
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
@[simp]
theorem
ContinuousLinearEquiv.fst_equivOfRightInverse
{R : Type u_1}
[Ring R]
{M : Type u_3}
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
{M₂ : Type u_4}
[TopologicalSpace M₂]
[AddCommGroup M₂]
[Module R M₂]
[IsTopologicalAddGroup M]
(f₁ : M →L[R] M₂)
(f₂ : M₂ →L[R] M)
(h : Function.RightInverse ⇑f₂ ⇑f₁)
(x : M)
:
@[simp]
theorem
ContinuousLinearEquiv.snd_equivOfRightInverse
{R : Type u_1}
[Ring R]
{M : Type u_3}
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
{M₂ : Type u_4}
[TopologicalSpace M₂]
[AddCommGroup M₂]
[Module R M₂]
[IsTopologicalAddGroup M]
(f₁ : M →L[R] M₂)
(f₂ : M₂ →L[R] M)
(h : Function.RightInverse ⇑f₂ ⇑f₁)
(x : M)
:
@[simp]
theorem
ContinuousLinearEquiv.equivOfRightInverse_symm_apply
{R : Type u_1}
[Ring R]
{M : Type u_3}
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
{M₂ : Type u_4}
[TopologicalSpace M₂]
[AddCommGroup M₂]
[Module R M₂]
[IsTopologicalAddGroup M]
(f₁ : M →L[R] M₂)
(f₂ : M₂ →L[R] M)
(h : Function.RightInverse ⇑f₂ ⇑f₁)
(y : M₂ × ↥(LinearMap.ker f₁))
:
def
ContinuousLinearMap.IsInvertible
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[TopologicalSpace M]
[TopologicalSpace M₂]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
(f : M →L[R] M₂)
:
A continuous linear map is invertible if it is the forward direction of a continuous linear equivalence.
Equations
Instances For
noncomputable def
ContinuousLinearMap.inverse
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[TopologicalSpace M]
[TopologicalSpace M₂]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
:
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
@[simp]
theorem
ContinuousLinearMap.isInvertible_equiv
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[TopologicalSpace M]
[TopologicalSpace M₂]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
{f : M ≃L[R] M₂}
:
(↑f).IsInvertible
@[simp]
theorem
ContinuousLinearMap.inverse_equiv
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[TopologicalSpace M]
[TopologicalSpace M₂]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
(e : M ≃L[R] M₂)
:
@[simp]
theorem
ContinuousLinearMap.inverse_of_not_isInvertible
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[TopologicalSpace M]
[TopologicalSpace M₂]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
{f : M →L[R] M₂}
(hf : ¬f.IsInvertible)
:
By definition, if f is not invertible then inverse f = 0.
@[simp]
theorem
ContinuousLinearMap.isInvertible_zero_iff
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[TopologicalSpace M]
[TopologicalSpace M₂]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
:
@[simp]
theorem
ContinuousLinearMap.inverse_zero
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[TopologicalSpace M]
[TopologicalSpace M₂]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
:
theorem
ContinuousLinearMap.IsInvertible.comp
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
{M₃ : Type u_4}
[TopologicalSpace M]
[TopologicalSpace M₂]
[TopologicalSpace M₃]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid M₃]
[Module R M₃]
{g : M₂ →L[R] M₃}
{f : M →L[R] M₂}
(hg : g.IsInvertible)
(hf : f.IsInvertible)
:
(g.comp f).IsInvertible
theorem
ContinuousLinearMap.IsInvertible.of_inverse
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[TopologicalSpace M]
[TopologicalSpace M₂]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
{f : M →L[R] M₂}
{g : M₂ →L[R] M}
(hf : f.comp g = id R M₂)
(hg : g.comp f = id R M)
:
theorem
ContinuousLinearMap.inverse_eq
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[TopologicalSpace M]
[TopologicalSpace M₂]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
{f : M →L[R] M₂}
{g : M₂ →L[R] M}
(hf : f.comp g = id R M₂)
(hg : g.comp f = id R M)
:
theorem
ContinuousLinearMap.IsInvertible.inverse_apply_eq
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[TopologicalSpace M]
[TopologicalSpace M₂]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
{f : M →L[R] M₂}
{x : M}
{y : M₂}
(hf : f.IsInvertible)
:
@[simp]
theorem
ContinuousLinearMap.isInvertible_equiv_comp
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
{M₃ : Type u_4}
[TopologicalSpace M]
[TopologicalSpace M₂]
[TopologicalSpace M₃]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid M₃]
[Module R M₃]
{e : M₂ ≃L[R] M₃}
{f : M →L[R] M₂}
:
@[simp]
theorem
ContinuousLinearMap.isInvertible_comp_equiv
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
{M₃ : Type u_4}
[TopologicalSpace M]
[TopologicalSpace M₂]
[TopologicalSpace M₃]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid M₃]
[Module R M₃]
{e : M₃ ≃L[R] M}
{f : M →L[R] M₂}
:
@[simp]
theorem
ContinuousLinearMap.inverse_equiv_comp
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
{M₃ : Type u_4}
[TopologicalSpace M]
[TopologicalSpace M₂]
[TopologicalSpace M₃]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid M₃]
[Module R M₃]
{e : M₂ ≃L[R] M₃}
{f : M →L[R] M₂}
:
@[simp]
theorem
ContinuousLinearMap.inverse_comp_equiv
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
{M₃ : Type u_4}
[TopologicalSpace M]
[TopologicalSpace M₂]
[TopologicalSpace M₃]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid M₃]
[Module R M₃]
{e : M₃ ≃L[R] M}
{f : M →L[R] M₂}
:
theorem
ContinuousLinearMap.IsInvertible.inverse_comp_of_left
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
{M₃ : Type u_4}
[TopologicalSpace M]
[TopologicalSpace M₂]
[TopologicalSpace M₃]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid M₃]
[Module R M₃]
{g : M₂ →L[R] M₃}
{f : M →L[R] M₂}
(hg : g.IsInvertible)
:
theorem
ContinuousLinearMap.IsInvertible.inverse_comp_apply_of_left
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
{M₃ : Type u_4}
[TopologicalSpace M]
[TopologicalSpace M₂]
[TopologicalSpace M₃]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid M₃]
[Module R M₃]
{g : M₂ →L[R] M₃}
{f : M →L[R] M₂}
{v : M₃}
(hg : g.IsInvertible)
:
theorem
ContinuousLinearMap.IsInvertible.inverse_comp_of_right
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
{M₃ : Type u_4}
[TopologicalSpace M]
[TopologicalSpace M₂]
[TopologicalSpace M₃]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid M₃]
[Module R M₃]
{g : M₂ →L[R] M₃}
{f : M →L[R] M₂}
(hf : f.IsInvertible)
:
theorem
ContinuousLinearMap.IsInvertible.inverse_comp_apply_of_right
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
{M₃ : Type u_4}
[TopologicalSpace M]
[TopologicalSpace M₂]
[TopologicalSpace M₃]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid M₃]
[Module R M₃]
{g : M₂ →L[R] M₃}
{f : M →L[R] M₂}
{v : M₃}
(hf : f.IsInvertible)
:
@[simp]
theorem
ContinuousLinearMap.ringInverse_equiv
{R : Type u_1}
{M : Type u_2}
[TopologicalSpace M]
[Semiring R]
[AddCommMonoid M]
[Module R M]
(e : M ≃L[R] M)
:
@[deprecated ContinuousLinearMap.ringInverse_equiv (since := "2025-04-22")]
theorem
ContinuousLinearMap.ring_inverse_equiv
{R : Type u_1}
{M : Type u_2}
[TopologicalSpace M]
[Semiring R]
[AddCommMonoid M]
[Module R M]
(e : M ≃L[R] M)
:
Alias of ContinuousLinearMap.ringInverse_equiv.
theorem
ContinuousLinearMap.inverse_eq_ringInverse
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[TopologicalSpace M]
[TopologicalSpace M₂]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
(e : M ≃L[R] M₂)
(f : M →L[R] M₂)
:
The function ContinuousLinearEquiv.inverse can be written in terms of Ring.inverse for the
ring of self-maps of the domain.
@[deprecated ContinuousLinearMap.inverse_eq_ringInverse (since := "2025-04-22")]
theorem
ContinuousLinearMap.to_ring_inverse
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[TopologicalSpace M]
[TopologicalSpace M₂]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
(e : M ≃L[R] M₂)
(f : M →L[R] M₂)
:
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.
theorem
ContinuousLinearMap.ringInverse_eq_inverse
{R : Type u_1}
{M : Type u_2}
[TopologicalSpace M]
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
@[deprecated ContinuousLinearMap.ringInverse_eq_inverse (since := "2025-04-22")]
theorem
ContinuousLinearMap.ring_inverse_eq_map_inverse
{R : Type u_1}
{M : Type u_2}
[TopologicalSpace M]
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
@[simp]
theorem
ContinuousLinearMap.inverse_id
{R : Type u_1}
{M : Type u_2}
[TopologicalSpace M]
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
theorem
ContinuousLinearMap.coprod_comp_prodComm
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
{M₃ : Type u_4}
[TopologicalSpace M]
[TopologicalSpace M₂]
[TopologicalSpace M₃]
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
[AddCommMonoid M₃]
[Module R M₃]
[ContinuousAdd M]
(f : M₂ →L[R] M)
(g : M₃ →L[R] M)
:
Composition of a map on a product with the exchange of the product factors
theorem
Submodule.ClosedComplemented.exists_submodule_equiv_prod
{R : Type u_1}
[Ring R]
{M : Type u_2}
[TopologicalSpace M]
[AddCommGroup M]
[Module R M]
[IsTopologicalAddGroup M]
{p : Submodule R M}
(hp : p.ClosedComplemented)
:
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.
def
MulOpposite.opContinuousLinearEquiv
(R : Type u_1)
[Semiring R]
{M : Type u_2}
[AddCommMonoid M]
[Module R M]
[TopologicalSpace M]
:
The function op is a continuous linear equivalence.
Equations
Instances For
@[simp]
theorem
MulOpposite.opContinuousLinearEquiv_apply
(R : Type u_1)
[Semiring R]
{M : Type u_2}
[AddCommMonoid M]
[Module R M]
[TopologicalSpace M]
(a✝ : M)
:
@[simp]
theorem
MulOpposite.opContinuousLinearEquiv_symm_apply
(R : Type u_1)
[Semiring R]
{M : Type u_2}
[AddCommMonoid M]
[Module R M]
[TopologicalSpace M]
(a✝ : Mᵐᵒᵖ)
: