# 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₂`.

source
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 `M` and `M₂` will be topological modules over the topological semiring `R`.

- 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` and `M₂` will be topological modules over the topological semiring `R`.

Instances For

source
def «term_≃SL[_]_» :
Lean.TrailingParserDescr

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.

Instances For

source
def «term_≃L[_]_» :
Lean.TrailingParserDescr

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.

Instances For

source
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₂ :
Prop

`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_add (f : F) (a b : M) : f (a + b) = f a + f b
- map_smulₛₗ (f : F) (r : R) (x : M) : f (r • x) = σ r • f x
- map_continuous (f : F) : Continuous ⇑f

  `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`.

- inv_continuous (f : F) : Continuous (EquivLike.inv f)

  `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`.

Instances

source
@[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₂] :
Prop

`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₂

Instances For

source
@[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₂
source
@[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₂
source
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) :
↥(⨅ i ∈ J, LinearMap.ker (proj i)) ≃L[R] (i : ↑I) → φ ↑i

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 := ⋯ }

Instances For

source
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₂) :
M₁ →SL[σ₁₂] M₂

A continuous linear equivalence induces a continuous linear map.

Equations

- ↑e = { toLinearMap := ↑e.toLinearEquiv, cont := ⋯ }

Instances For

source
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₂] :
Coe (M₁ ≃SL[σ₁₂] M₂) (M₁ →SL[σ₁₂] M₂)

Coerce continuous linear equivs to continuous linear maps.

Equations

- ContinuousLinearEquiv.ContinuousLinearMap.coe = { coe := ContinuousLinearEquiv.toContinuousLinearMap }

source
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₂] :
EquivLike (M₁ ≃SL[σ₁₂] M₂) M₁ M₂
Equations

- One or more equations did not get rendered due to their size.

source
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₂
source
@[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) :
⇑{ toLinearEquiv := e, continuous_toFun := a, continuous_invFun := b } = ⇑e
source
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₁) :
↑e b = e b
source
@[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₂) :
⇑f.toLinearEquiv = ⇑f
source
@[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₂) :
⇑↑e = ⇑e
source
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₂] :
Function.Injective toLinearEquiv
source
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) :
f = g
source
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₂} :
f = g ↔ ⇑f = ⇑g
source
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₂] :
Function.Injective toContinuousLinearMap
source
@[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₂} :
↑e = ↑e' ↔ e = e'
source
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₂) :
M₁ ≃ₜ M₂

A continuous linear equivalence induces a homeomorphism.

Equations

- e.toHomeomorph = { toEquiv := e.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source
@[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₂) :
⇑e.toHomeomorph = ⇑e
source
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
source
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₁) :
⇑e '' closure s = closure (⇑e '' s)
source
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₂) :
⇑e ⁻¹' closure s = closure (⇑e ⁻¹' s)
source
@[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₁} :
IsClosed (⇑e '' s) ↔ IsClosed s
source
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₁) :
Filter.map (⇑e) (nhds x) = nhds (e x)
source
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₂) :
e 0 = 0
source
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₁) :
e (x + y) = e x + e y
source
@[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₁) :
e (c • x) = σ₁₂ c • e x
source
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₁) :
e (c • x) = c • e x
source
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₁} :
e x = 0 ↔ x = 0
source
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
source
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
source
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
source
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
source
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 α} :
ContinuousOn (⇑e ∘ f) s ↔ ContinuousOn f s
source
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₁} :
Continuous (⇑e ∘ f) ↔ Continuous f
source
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) :
f = g

An extensionality lemma for `R ≃L[R] M`.

source
def ContinuousLinearEquiv.refl (R₁ : Type u_1) [Semiring R₁] (M₁ : Type u_4) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :
M₁ ≃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 := ⋯ }

Instances For

source
@[simp]
theorem ContinuousLinearEquiv.refl_apply (R₁ : Type u_1) [Semiring R₁] (M₁ : Type u_4) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] (x : M₁) :
(ContinuousLinearEquiv.refl R₁ M₁) x = x
source
@[simp]
theorem ContinuousLinearEquiv.coe_refl {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :
↑(ContinuousLinearEquiv.refl R₁ M₁) = ContinuousLinearMap.id R₁ M₁
source
@[simp]
theorem ContinuousLinearEquiv.coe_refl' {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :
⇑(ContinuousLinearEquiv.refl R₁ M₁) = id
source
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₂) :
M₂ ≃SL[σ₂₁] M₁

The inverse of a continuous linear equivalence as a continuous linear equivalence

Equations

- e.symm = { toLinearEquiv := e.symm, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source
@[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₂) :
e.symm.toLinearEquiv = e.symm
source
@[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₂) :
e.symm.toLinearEquiv = e.symm

Alias of `ContinuousLinearEquiv.toLinearEquiv_symm`.

source
@[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₂) :
⇑e.symm = ⇑e.symm
source
@[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₂) :
e.symm.toHomeomorph = e.toHomeomorph.symm
source
@[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₂) :
e.toHomeomorph.symm = e.symm.toHomeomorph
source
@[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₂) :
⇑e.toHomeomorph.symm = ⇑e.symm
source
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

- ContinuousLinearEquiv.Simps.apply h = ⇑h

Instances For

source
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

- ContinuousLinearEquiv.Simps.symm_apply h = ⇑h.symm

Instances For

source
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₁) :
Filter.map (⇑e.symm) (nhds (e x)) = nhds x
source
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₃) :
M₁ ≃SL[σ₁₃] M₃

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 := ⋯ }

Instances For

source
@[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₃) :
(e₁.trans e₂).toLinearEquiv = e₁.trans e₂.toLinearEquiv
source
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₄) :
(M₁ × M₃) ≃L[R₁] M₂ × M₄

Product of two continuous linear equivalences. The map comes from `Equiv.prodCongr`.

Equations

- e.prodCongr e' = { toLinearEquiv := e.prodCongr e'.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source
@[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₄) :
(M₁ × M₃) ≃L[R₁] M₂ × M₄

Alias of `ContinuousLinearEquiv.prodCongr`.

Product of two continuous linear equivalences. The map comes from `Equiv.prodCongr`.

Equations

- @ContinuousLinearEquiv.prod = @ContinuousLinearEquiv.prodCongr

Instances For

source
@[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₃) :
(e.prodCongr e') x = (e x.1, e' x.2)
source
@[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₃) :
(e.prodCongr e') x = (e x.1, e' x.2)

Alias of `ContinuousLinearEquiv.prodCongr_apply`.

source
@[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₄) :
↑(e.prodCongr e') = (↑e).prodMap ↑e'
source
@[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₄) :
↑(e.prodCongr e') = (↑e).prodMap ↑e'

Alias of `ContinuousLinearEquiv.coe_prodCongr`.

source
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₄) :
(e.prodCongr e').symm = e.symm.prodCongr e'.symm
source
@[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₄) :
(e.prodCongr e').symm = e.symm.prodCongr e'.symm

Alias of `ContinuousLinearEquiv.prodCongr_symm`.

source
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₂] :
(M₁ × M₂) ≃L[R₁] M₂ × M₁

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 := ⋯ }

Instances For

source
@[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₂) :
(prodComm R₁ M₁ M₂) a✝ = a✝.swap
source
@[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₂] :
(prodComm R₁ M₁ M₂).toLinearEquiv = LinearEquiv.prodComm R₁ M₁ M₂
source
@[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₂] :
(prodComm R₁ M₁ M₂).symm = prodComm R₁ M₂ M₁
source
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₃] :
((M₁ × M₂) × M₃) ≃L[R] M₁ × M₂ × M₃

The product of topological modules is associative up to continuous linear isomorphism. This is `LinearEquiv.prodAssoc` prodAssoc as a continuous linear equivalence.

Equations

- ContinuousLinearEquiv.prodAssoc R M₁ M₂ M₃ = { toLinearEquiv := LinearEquiv.prodAssoc R M₁ M₂ M₃, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source
@[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₃] :
(prodAssoc R M₁ M₂ M₃).toLinearEquiv = LinearEquiv.prodAssoc R M₁ M₂ M₃
source
@[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₃] :
⇑(prodAssoc R M₁ M₂ M₃) = ⇑(Equiv.prodAssoc M₁ M₂ M₃)
source
@[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₃) :
(prodAssoc R M₁ M₂ M₃) ((p₁, p₂), p₃) = (p₁, p₂, p₃)
source
@[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₃) :
(prodAssoc R M₁ M₂ M₃).symm (p₁, p₂, p₃) = ((p₁, p₂), p₃)
source
def ContinuousLinearEquiv.prodProdProdComm (R : Type u_8) (M₁ : Type u_9) (M₂ : Type u_10) (M₃ : Type u_11) (M₄ : Type u_12) [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] [TopologicalSpace M₁] [TopologicalSpace M₂] [TopologicalSpace M₃] [TopologicalSpace M₄] :
((M₁ × M₂) × M₃ × M₄) ≃L[R] (M₁ × M₃) × M₂ × M₄

The product of topological modules is four-way commutative up to continuous linear isomorphism. This is `LinearEquiv.prodProdProdComm` prodAssoc as a continuous linear equivalence.

Equations

- ContinuousLinearEquiv.prodProdProdComm R M₁ M₂ M₃ M₄ = { toLinearEquiv := LinearEquiv.prodProdProdComm R M₁ M₂ M₃ M₄, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source
@[simp]
theorem ContinuousLinearEquiv.prodProdProdComm_symm (R : Type u_8) (M₁ : Type u_9) (M₂ : Type u_10) (M₃ : Type u_11) (M₄ : Type u_12) [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] [TopologicalSpace M₁] [TopologicalSpace M₂] [TopologicalSpace M₃] [TopologicalSpace M₄] :
(prodProdProdComm R M₁ M₂ M₃ M₄).symm = prodProdProdComm R M₁ M₃ M₂ M₄
source
@[simp]
theorem ContinuousLinearEquiv.prodProdProdComm_toLinearEquiv (R : Type u_8) (M₁ : Type u_9) (M₂ : Type u_10) (M₃ : Type u_11) (M₄ : Type u_12) [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] [TopologicalSpace M₁] [TopologicalSpace M₂] [TopologicalSpace M₃] [TopologicalSpace M₄] :
(prodProdProdComm R M₁ M₂ M₃ M₄).toLinearEquiv = LinearEquiv.prodProdProdComm R M₁ M₂ M₃ M₄
source
@[simp]
theorem ContinuousLinearEquiv.coe_prodProdProdComm (R : Type u_8) (M₁ : Type u_9) (M₂ : Type u_10) (M₃ : Type u_11) (M₄ : Type u_12) [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] [TopologicalSpace M₁] [TopologicalSpace M₂] [TopologicalSpace M₃] [TopologicalSpace M₄] :
⇑(prodProdProdComm R M₁ M₂ M₃ M₄) = ⇑(Equiv.prodProdProdComm M₁ M₂ M₃ M₄)
source
@[simp]
theorem ContinuousLinearEquiv.prodProdProdComm_apply (R : Type u_8) (M₁ : Type u_9) (M₂ : Type u_10) (M₃ : Type u_11) (M₄ : Type u_12) [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] [TopologicalSpace M₁] [TopologicalSpace M₂] [TopologicalSpace M₃] [TopologicalSpace M₄] (p₁ : M₁) (p₂ : M₂) (p₃ : M₃) (p₄ : M₄) :
(prodProdProdComm R M₁ M₂ M₃ M₄) ((p₁, p₂), p₃, p₄) = ((p₁, p₃), p₂, p₄)
source
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] :
(M × N) ≃L[R] M

The natural equivalence `M × N ≃L[R] M` for any `Unique` type `N`. This is `Equiv.prodUnique` as a continuous linear equivalence.

Equations

- ContinuousLinearEquiv.prodUnique R M N = { toLinearEquiv := LinearEquiv.prodUnique, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source
@[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] :
(prodUnique R M N).toEquiv = Equiv.prodUnique M N
source
@[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) :
(prodUnique R M N) x = x.1
source
@[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) :
(prodUnique R M N).symm x = (x, default)
source
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] :
(N × M) ≃L[R] M

The natural equivalence `N × M ≃L[R] M` for any `Unique` type `N`. This is `Equiv.uniqueProd` as a continuous linear equivalence.

Equations

- ContinuousLinearEquiv.uniqueProd R M N = { toLinearEquiv := LinearEquiv.uniqueProd, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source
@[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] :
(uniqueProd R M N).toEquiv = Equiv.uniqueProd M N
source
@[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) :
(uniqueProd R M N) x = x.2
source
@[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) :
(uniqueProd R M N).symm x = (default, x)
source
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₂) :
Function.Bijective ⇑e
source
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₂) :
Function.Injective ⇑e
source
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₂) :
Function.Surjective ⇑e
source
@[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₁) :
(e₁.trans e₂) c = e₂ (e₁ c)
source
@[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₂) :
e (e.symm c) = c
source
@[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₁) :
e.symm (e b) = b
source
@[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₁) :
(e₂.trans e₁).symm c = e₂.symm (e₁.symm c)
source
@[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₁) :
⇑e.symm '' (⇑e '' s) = s
source
@[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₂) :
⇑e '' (⇑e.symm '' s) = s
source
@[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₃) :
(↑f').comp ↑f = ↑(f.trans f')
source
@[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₂) :
(↑e).comp ↑e.symm = ContinuousLinearMap.id R₂ M₂
source
@[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₂) :
(↑e.symm).comp ↑e = ContinuousLinearMap.id R₁ M₁
source
@[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₂) :
⇑e.symm ∘ ⇑e = id
source
@[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₂) :
⇑e ∘ ⇑e.symm = id
source
@[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₂) :
e.symm.symm = e
source
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₂] :
Function.Bijective ContinuousLinearEquiv.symm
source
@[simp]
theorem ContinuousLinearEquiv.refl_symm {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :
(ContinuousLinearEquiv.refl R₁ M₁).symm = ContinuousLinearEquiv.refl R₁ M₁
source
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₁) :
e.symm.symm x = e x
source
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₁} :
e.symm x = y ↔ x = e y
source
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₁} :
y = e.symm x ↔ e y = x
source
theorem ContinuousLinearEquiv.image_eq_preimage_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₂) (s : Set M₁) :
⇑e '' s = ⇑e.symm ⁻¹' s
source
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₂) :
⇑e.symm '' s = ⇑e ⁻¹' s
source
@[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₂) :
⇑e.symm ⁻¹' (⇑e ⁻¹' s) = s
source
@[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₁) :
⇑e ⁻¹' (⇑e.symm ⁻¹' s) = s
source
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₂) :
IsUniformEmbedding ⇑e
source
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) :
IsUniformEmbedding ⇑e
source
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₁) :
M₁ ≃SL[σ₁₂] M₂

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 := ⋯ }

Instances For

source
@[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₁) :
(equivOfInverse f₁ f₂ h₁ h₂) x = f₁ x
source
@[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₁) :
(equivOfInverse f₁ f₂ h₁ h₂).symm = equivOfInverse f₂ f₁ h₂ h₁
source
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₁) :
M₁ ≃SL[σ₁₂] M₂

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₂ ⋯ ⋯

Instances For

source
@[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₁) :
(equivOfInverse' f₁ f₂ h₁ h₂) x = f₁ x
source
@[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₁) :
(equivOfInverse' f₁ f₂ h₁ h₂).symm = equivOfInverse' f₂ f₁ h₂ h₁

The inverse of `equivOfInverse'` is obtained by swapping the order of its parameters.

source
instance ContinuousLinearEquiv.automorphismGroup {R₁ : Type u_1} [Semiring R₁] (M₁ : Type u_4) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :
Group (M₁ ≃L[R₁] M₁)

The continuous linear equivalences from `M` to itself form a group under composition.

Equations

- One or more equations did not get rendered due to their size.

source
def ContinuousLinearEquiv.ulift {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] :
ULift.{u_9, u_4} M₁ ≃L[R₁] M₁

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 := ⋯ }

Instances For

source
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₃) :
(M₁ →SL[σ₁₄] M₄) ≃ (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

- One or more equations did not get rendered due to their size.

Instances For

source
@[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₃) :
(e₁₂.arrowCongrEquiv e₄₃).symm f = (↑e₄₃.symm).comp (f.comp ↑e₁₂)
source
@[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₄) :
(e₁₂.arrowCongrEquiv e₄₃) f = (↑e₄₃).comp (f.comp ↑e₁₂.symm)
source
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 : ι' ≃ ι) :
((i' : ι') → φ (e i')) ≃L[R] (i : ι) → φ i

Combine a family of linear equivalences into a linear equivalence of `pi`-types. This is `Equiv.piCongrLeft` as a `ContinuousLinearEquiv`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
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)] :
((st : S ⊕ T) → A st) ≃L[R] ((s : S) → A (Sum.inl s)) × ((t : T) → A (Sum.inr t))

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

- ContinuousLinearEquiv.sumPiEquivProdPi R S T A = { toLinearEquiv := LinearEquiv.sumPiEquivProdPi R S T A, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source
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)] :
((t : α) → f t) ≃L[R] f default

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

- ContinuousLinearEquiv.piUnique R f = { toLinearEquiv := LinearEquiv.piUnique R f, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source
@[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)] :
⇑(piUnique R f) = fun (f : (i : α) → f i) => f default
source
@[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)] :
⇑(piUnique R f).symm = uniqueElim
source
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) :
((i : ι) → M i) ≃L[R₁] (i : ι) → N i

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 := ⋯ }

Instances For

source
@[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 : ι) :
(piCongrRight f) m i = (f i) (m i)
source
@[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 : ι) :
(piCongrRight f).symm n i = (f i).symm (n i)
source
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₁] :
G →* M₁ ≃L[R₁] M₁

Scalar multiplication by a group element as a continuous linear equivalence.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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₁) :
(smulLeft g) a✝ = g • a✝
source
@[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) :
(smulLeft g).toLinearEquiv = DistribMulAction.toLinearEquiv R₁ M₁ g

### 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`.

source
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)ˣ) :
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 := ⋯ }

Instances For

source
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) :
(M →L[R] M)ˣ

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 := ⋯ }

Instances For

source
def ContinuousLinearEquiv.unitsEquiv (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] :
(M →L[R] M)ˣ ≃* M ≃L[R] 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

- ContinuousLinearEquiv.unitsEquiv R M = { toFun := ContinuousLinearEquiv.ofUnit, invFun := ContinuousLinearEquiv.toUnit, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

source
@[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) :
((unitsEquiv R M) f) x = ↑f x

### Units of a ring as linear automorphisms #

source
def ContinuousLinearEquiv.unitsEquivAut (R : Type u_1) [Semiring R] [TopologicalSpace R] [ContinuousMul R] :
R ˣ ≃ R ≃L[R] R

Continuous linear equivalences `R ≃L[R] R` are enumerated by `Rˣ`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem ContinuousLinearEquiv.unitsEquivAut_apply {R : Type u_1} [Semiring R] [TopologicalSpace R] [ContinuousMul R] (u : R ˣ) (x : R) :
((unitsEquivAut R) u) x = x * ↑u
source
@[simp]
theorem ContinuousLinearEquiv.unitsEquivAut_apply_symm {R : Type u_1} [Semiring R] [TopologicalSpace R] [ContinuousMul R] (u : R ˣ) (x : R) :
((unitsEquivAut R) u).symm x = x * ↑u⁻¹
source
@[simp]
theorem ContinuousLinearEquiv.unitsEquivAut_symm_apply {R : Type u_1} [Semiring R] [TopologicalSpace R] [ContinuousMul R] (e : R ≃L[R] R) :
↑((unitsEquivAut R).symm e) = e 1
source
def ContinuousLinearEquiv.funUnique (ι : Type u_1) (R : Type u_2) (M : Type u_3) [Unique ι] [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] :
(ι → M) ≃L[R] M

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 := ⋯ }

Instances For

source
@[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] :
⇑(funUnique ι R M) = Function.eval default
source
@[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] :
⇑(funUnique ι R M).symm = Function.const ι
source
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)] :
((i : Fin 2) → M i) ≃L[R] M 0 × M 1

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 := ⋯ }

Instances For

source
@[simp]
theorem ContinuousLinearEquiv.piFinTwo_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)] :
⇑(piFinTwo R M) = fun (f : (i : Fin 2) → M i) => (f 0, f 1)
source
@[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)] :
⇑(piFinTwo R M).symm = fun (p : M 0 × M 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
source
def ContinuousLinearEquiv.finTwoArrow (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] :
(Fin 2 → M) ≃L[R] M × M

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 := ⋯ }

Instances For

source
@[simp]
theorem ContinuousLinearEquiv.finTwoArrow_symm_apply (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] :
⇑(finTwoArrow R M).symm = fun (x : M × M) => ![x.1, x.2]
source
@[simp]
theorem ContinuousLinearEquiv.finTwoArrow_apply (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] :
⇑(finTwoArrow R M) = fun (f : Fin 2 → M) => (f 0, f 1)
source
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)] :
(M 0 × ((i : Fin n) → M i.succ)) ≃L[R] (i : Fin n.succ) → M i

`Fin.consEquiv` as a continuous linear equivalence.

Equations

- Fin.consEquivL R M = { toLinearEquiv := Fin.consLinearEquiv R M, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source
@[simp]
theorem Fin.consEquivL_apply {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)] (a✝ : M 0 × ((i : Fin n) → M i.succ)) (i : Fin (n + 1)) :
(consEquivL R M) a✝ i = cons a✝.1 a✝.2 i
source
@[simp]
theorem Fin.consEquivL_symm_apply {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)] (a✝ : (i : Fin (n + 1)) → M i) :
(consEquivL R M).symm a✝ = (a✝ 0, tail a✝)
source
@[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) :
N →L[R] (i : Fin n.succ) → M i

`Fin.cons` in the codomain of continuous linear maps.

Equations

- f.finCons fs = (↑(Fin.consEquivL R M)).comp (f.prod fs)

Instances For

source
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₄) :
(M × M₃) ≃L[R] M₂ × 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

- e.skewProd e' f = { toLinearEquiv := e.skewProd e'.toLinearEquiv ↑f, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source
@[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₃) :
(e.skewProd e' f) x = (e x.1, e' x.2 + f x.1)
source
@[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₄) :
(e.skewProd e' f).symm x = (e.symm x.1, e'.symm (x.2 - f (e.symm x.1)))
source
def ContinuousLinearEquiv.neg (R : Type u_1) [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] [ContinuousNeg M] :
M ≃L[R] M

The negation map as a continuous linear equivalence.

Equations

- ContinuousLinearEquiv.neg R = { toLinearEquiv := LinearEquiv.neg R, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source
@[simp]
theorem ContinuousLinearEquiv.coe_neg {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] [ContinuousNeg M] :
⇑(neg R) = -id
source
@[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) :
(neg R) x = -x
source
@[simp]
theorem ContinuousLinearEquiv.symm_neg {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] [ContinuousNeg M] :
(neg R).symm = neg R
source
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) :
e (x - y) = e x - e y
source
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) :
e (-x) = -e x
source
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₁) :
M ≃L[R] M₂ × ↥(LinearMap.ker 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

- ContinuousLinearEquiv.equivOfRightInverse f₁ f₂ h = ContinuousLinearEquiv.equivOfInverse (f₁.prod (f₁.projKerOfRightInverse f₂ h)) (f₂.coprod (LinearMap.ker f₁).subtypeL) ⋯ ⋯

Instances For

source
@[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) :
((equivOfRightInverse f₁ f₂ h) x).1 = f₁ x
source
@[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) :
↑((equivOfRightInverse f₁ f₂ h) x).2 = x - f₂ (f₁ x)
source
@[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₁)) :
(equivOfRightInverse f₁ f₂ h).symm y = f₂ y.1 + ↑y.2
source
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₂) :
Prop

A continuous linear map is invertible if it is the forward direction of a continuous linear equivalence.

Equations

- f.IsInvertible = ∃ (A : M ≃L[R] M₂), ↑A = f

Instances For

source
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₂] :
(M →L[R] M₂) → M₂ →L[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

- f.inverse = if h : f.IsInvertible then ↑(Classical.choose h).symm else 0

Instances For

source
@[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
source
@[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₂) :
(↑e).inverse = ↑e.symm

By definition, if `f` is invertible then `inverse f = f.symm`.

source
@[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) :
f.inverse = 0

By definition, if `f` is not invertible then `inverse f = 0`.

source
@[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₂] :
IsInvertible 0 ↔ Subsingleton M ∧ Subsingleton M₂
source
@[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₂] :
inverse 0 = 0
source
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
source
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 = ContinuousLinearMap.id R M₂) (hg : g.comp f = ContinuousLinearMap.id R M) :
f.IsInvertible
source
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 = ContinuousLinearMap.id R M₂) (hg : g.comp f = ContinuousLinearMap.id R M) :
f.inverse = g
source
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) :
f.inverse y = x ↔ y = f x
source
@[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₂} :
((↑e).comp f).IsInvertible ↔ f.IsInvertible
source
@[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₂} :
(f.comp ↑e).IsInvertible ↔ f.IsInvertible
source
@[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₂} :
((↑e).comp f).inverse = f.inverse.comp ↑e.symm
source
@[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₂} :
(f.comp ↑e).inverse = (↑e.symm).comp f.inverse
source
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) :
(g.comp f).inverse = f.inverse.comp g.inverse
source
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) :
(g.comp f).inverse v = f.inverse (g.inverse v)
source
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) :
(g.comp f).inverse = f.inverse.comp g.inverse
source
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) :
(g.comp f).inverse v = f.inverse (g.inverse v)
source
@[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) :
Ring.inverse ↑e = (↑e).inverse
source
@[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) :
Ring.inverse ↑e = (↑e).inverse

Alias of `ContinuousLinearMap.ringInverse_equiv`.

source
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₂) :
f.inverse = (Ring.inverse ((↑e.symm).comp f)).comp ↑e.symm

The function `ContinuousLinearEquiv.inverse` can be written in terms of `Ring.inverse` for the ring of self-maps of the domain.

source
@[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₂) :
f.inverse = (Ring.inverse ((↑e.symm).comp f)).comp ↑e.symm

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.

source
theorem ContinuousLinearMap.ringInverse_eq_inverse {R : Type u_1} {M : Type u_2} [TopologicalSpace M] [Semiring R] [AddCommMonoid M] [Module R M] :
Ring.inverse = inverse
source
@[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] :
Ring.inverse = inverse

Alias of `ContinuousLinearMap.ringInverse_eq_inverse`.

source
@[simp]
theorem ContinuousLinearMap.inverse_id {R : Type u_1} {M : Type u_2} [TopologicalSpace M] [Semiring R] [AddCommMonoid M] [Module R M] :
(ContinuousLinearMap.id R M).inverse = ContinuousLinearMap.id R M
source
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) :
(f.coprod g).comp ↑(ContinuousLinearEquiv.prodComm R M₃ M₂) = g.coprod f

Composition of a map on a product with the exchange of the product factors

source
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) :
∃ (q : Submodule R M) (e : M ≃L[R] ↥p × ↥q), (∀ (x : ↥p), e ↑x = (x, 0)) ∧ (∀ (y : ↥q), e ↑y = (0, y)) ∧ ∀ (x : ↥p × ↥q), e.symm x = ↑x.1 + ↑x.2

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.

source
def MulOpposite.opContinuousLinearEquiv (R : Type u_1) [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] [TopologicalSpace M] :
M ≃L[R] M ᵐᵒᵖ

The function `op` is a continuous linear equivalence.

Equations

- MulOpposite.opContinuousLinearEquiv R = { toLinearEquiv := MulOpposite.opLinearEquiv R, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source
@[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 ᵐᵒᵖ) :
(opContinuousLinearEquiv R).symm a✝ = unop a✝
source
@[simp]
theorem MulOpposite.opContinuousLinearEquiv_apply (R : Type u_1) [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] [TopologicalSpace M] (a✝ : M) :
(opContinuousLinearEquiv R) a✝ = op a✝