Continuous linear equivalences

Notation

Continuous semilinear / linear / star-linear equivalences between topological modules are denoted by M ≃SL[σ] M₂, M ≃L[R] M₂ and M ≃L⋆[R] M₂.

Main Definitions

• toHomeomorph is the homeomorphism induced by a continuous (semi)linear equivalence.
• symm is the inverse of a continuous linear equivalence as a continuous linear equivalence.
• equivOfInverse creates a ContinuousLinearEquiv from two ContinuousLinearMaps that are inverse of each other (as functions). See also equivOfInverse' when they're inverse to each other as continuous linear maps.
• ofUnit is the ContinuousLinearEquiv corresponding to a unit in the ring of continuous endomorphisms. See toUnit for the inverse direction.
• ofIsHomeomorph: a linear equivalence that is a homeomorphism is a continuous linear equivalence.

Main Results

• LinearEquiv.isHomeomorph_iff: A linear equivalence between topological modules is a homeomorphism if and only if it is continuous in both directions.

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).toFun (x + y) = (↑↑self).toFun x + (↑↑self).toFun y
• map_smul' (m : R) (x : M) : (↑↑self).toFun (m • x) = σ m • (↑↑self).toFun x
• invFun : M₂ → M
• left_inv : Function.LeftInverse (↑self).invFun (↑↑self).toFun
• right_inv : Function.RightInverse (↑self).invFun (↑↑self).toFun
• continuous_toFun : Continuous (↑↑self).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.

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.

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.

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.

@[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₂

@[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 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, cont := ⋯ }

@[instance_reducible]

instance ContinuousLinearEquiv.instCoeContinuousLinearMap {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.instCoeContinuousLinearMap = { coe := ContinuousLinearEquiv.toContinuousLinearMap }

@[instance_reducible]

instance ContinuousLinearEquiv.instCoeLinearEquiv {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₁ ≃ₛₗ[σ₁₂] M₂)

Equations

• ContinuousLinearEquiv.instCoeLinearEquiv = { coe := ContinuousLinearEquiv.toLinearEquiv }

@[simp]

theorem ContinuousLinearEquiv.toLinearMap_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₂) : ↑↑e = ↑↑e

@[instance_reducible, macro_inline]

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

• ContinuousLinearEquiv.equivLike = { coe := fun (f : M₁ ≃SL[σ₁₂] M₂) => (↑↑f).toFun, inv := fun (f : M₁ ≃SL[σ₁₂] M₂) => (↑f).invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

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) : ⇑{ toLinearEquiv := e, continuous_toFun := a, continuous_invFun := b } = ⇑e

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

@[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 = ⇑f

@[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

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

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

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

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

@[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'

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

@[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

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₁) : ⇑e '' closure s = closure (⇑e '' s)

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)

@[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

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)

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

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

@[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

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

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

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 α} : ContinuousOn (⇑e ∘ f) s ↔ ContinuousOn f s

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

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.

def ContinuousLinearEquiv.toContinuousAddEquiv {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] {M : Type u_8} [TopologicalSpace M] [AddCommMonoid M] [Module R₁ M] (e : M₁ ≃L[R₁] M) : M₁ ≃ₜ+ M

A continuous linear equivalence seen as a ContinuousAddEquiv.

Equations

• e.toContinuousAddEquiv = (↑e).toAddEquiv.toContinuousAddEquiv ⋯

@[simp]

theorem ContinuousLinearEquiv.toContinuousAddEquiv_coe {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] {M : Type u_8} [TopologicalSpace M] [AddCommMonoid M] [Module R₁ M] (e : M₁ ≃L[R₁] M) : ⇑e.toContinuousAddEquiv = ⇑e

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

@[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

@[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₁

@[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

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

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

@[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

@[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

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

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

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

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₂, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[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₂) = (↑e₁).trans ↑e₂

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

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

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

@[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)

@[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

@[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

@[simp]

theorem ContinuousLinearEquiv.symm_trans_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.trans e = ContinuousLinearEquiv.refl R₂ M₂

@[simp]

theorem ContinuousLinearEquiv.self_trans_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.trans e.symm = ContinuousLinearEquiv.refl R₁ 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₁) : (e₂.trans e₁).symm c = e₂.symm (e₁.symm c)

@[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

@[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

@[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' ∘SL ↑f = ↑(f.trans f')

@[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 ∘SL ↑e.symm = ContinuousLinearMap.id R₂ 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₂) : ↑e.symm ∘SL ↑e = ContinuousLinearMap.id R₁ 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₂) : ⇑e.symm ∘ ⇑e = id

@[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

@[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

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

@[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₁

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

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

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

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

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

@[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

@[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

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

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

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 ContinuousLinearMaps that are inverse of each other. See also equivOfInverse'. ToDo: Improve the naming to make it match LinearEquiv.ofLinearMap.

Equations

• ContinuousLinearEquiv.equivOfInverse f₁ f₂ h₁ h₂ = { toLinearMap := ↑f₁, invFun := ⇑f₂, left_inv := h₁, right_inv := h₂, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[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

@[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₁

@[simp]

theorem ContinuousLinearEquiv.toContinuousLinearMap_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₂) = 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₁ ∘SL f₂ = ContinuousLinearMap.id R₂ M₂) (h₂ : f₂ ∘SL f₁ = ContinuousLinearMap.id R₁ M₁) : M₁ ≃SL[σ₁₂] M₂

Create a ContinuousLinearEquiv from two ContinuousLinearMaps that are inverse of each other, in the ContinuousLinearMap.comp sense. See also equivOfInverse. ToDo: Improve the naming to make it match LinearEquiv.ofLinearMap

Equations

• ContinuousLinearEquiv.equivOfInverse' f₁ f₂ h₁ h₂ = ContinuousLinearEquiv.equivOfInverse f₁ f₂ ⋯ ⋯

@[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₁ ∘SL f₂ = ContinuousLinearMap.id R₂ M₂) (h₂ : f₂ ∘SL f₁ = ContinuousLinearMap.id R₁ M₁) (x : M₁) : (equivOfInverse' f₁ f₂ h₁ h₂) x = f₁ x

@[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₁ ∘SL f₂ = ContinuousLinearMap.id R₂ M₂) (h₂ : f₂ ∘SL 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.

@[simp]

theorem ContinuousLinearEquiv.toContinuousLinearMap_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₁ ∘SL f₂ = ContinuousLinearMap.id R₂ M₂) (h₂ : f₂ ∘SL f₁ = ContinuousLinearMap.id R₁ M₁) : ↑(equivOfInverse' f₁ f₂ h₁ h₂) = f₁

theorem ContinuousLinearEquiv.eq_comp_toContinuousLinearMap_symm {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₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] (e₁₂ : M₁ ≃SL[σ₁₂] M₂) [RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] (f : M₂ →SL[σ₂₃] M₃) (g : M₁ →SL[σ₁₃] M₃) : f = g ∘SL ↑e₁₂.symm ↔ f ∘SL ↑e₁₂ = g

theorem ContinuousLinearEquiv.eq_toContinuousLinearMap_symm_comp {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₃] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] {e₁₂ : M₁ ≃SL[σ₁₂] M₂} [RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (f : M₃ →SL[σ₃₁] M₁) (g : M₃ →SL[σ₃₂] M₂) : f = ↑e₁₂.symm ∘SL g ↔ ↑e₁₂ ∘SL f = g

@[instance_reducible]

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.

@[simp]

theorem ContinuousLinearEquiv.toContinuousLinearMap_one {R₁ : Type u_1} [Semiring R₁] (M₁ : Type u_4) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] : ↑1 = 1

@[simp]

theorem ContinuousLinearEquiv.toContinuousLinearMap_mul {R₁ : Type u_1} [Semiring R₁] (M₁ : Type u_4) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R₁ M₁] (e e' : M₁ ≃L[R₁] M₁) : ↑(e * e') = ↑e * ↑e'

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

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

• e₁₂.arrowCongrEquiv e₄₃ = { toFun := fun (f : M₁ →SL[σ₁₄] M₄) => ↑e₄₃ ∘SL f ∘SL ↑e₁₂.symm, invFun := fun (f : M₂ →SL[σ₂₃] M₃) => ↑e₄₃.symm ∘SL f ∘SL ↑e₁₂, left_inv := ⋯, right_inv := ⋯ }

@[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 ∘SL f ∘SL ↑e₁₂

@[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₄₃ ∘SL f ∘SL ↑e₁₂.symm

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 σ₁₃ σ₃₄ σ₁₄] [SMulCommClass R₃ R₃ M₃] [SMulCommClass R₄ R₄ M₄] [ContinuousAdd M₃] [ContinuousConstSMul R₃ M₃] [ContinuousAdd M₄] [ContinuousConstSMul R₄ M₄] (e₁₂ : M₁ ≃SL[σ₁₂] M₂) (e₄₃ : M₄ ≃SL[σ₄₃] M₃) : (M₁ →SL[σ₁₄] M₄) ≃ₛₗ[σ₄₃] M₂ →SL[σ₂₃] M₃

A pair of continuous (semi)linear equivalences generates a linear equivalence between the spaces of continuous linear maps. See also ContinuousLinearEquiv.arrowCongr.

Equations

• e₁₂.arrowCongrEquivₛₗ e₄₃ = { toFun := (e₁₂.arrowCongrEquiv e₄₃).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (e₁₂.arrowCongrEquiv e₄₃).invFun, left_inv := ⋯, right_inv := ⋯ }

@[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 σ₁₃ σ₃₄ σ₁₄] [SMulCommClass R₃ R₃ M₃] [SMulCommClass R₄ R₄ M₄] [ContinuousAdd M₃] [ContinuousConstSMul R₃ M₃] [ContinuousAdd M₄] [ContinuousConstSMul R₄ M₄] (e₁₂ : M₁ ≃SL[σ₁₂] M₂) (e₄₃ : M₄ ≃SL[σ₄₃] M₃) (a✝ : M₁ →SL[σ₁₄] M₄) : (e₁₂.arrowCongrEquivₛₗ e₄₃) a✝ = (e₁₂.arrowCongrEquiv e₄₃).toFun a✝

@[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 σ₁₃ σ₃₄ σ₁₄] [SMulCommClass R₃ R₃ M₃] [SMulCommClass R₄ R₄ M₄] [ContinuousAdd M₃] [ContinuousConstSMul R₃ M₃] [ContinuousAdd M₄] [ContinuousConstSMul R₄ M₄] (e₁₂ : M₁ ≃SL[σ₁₂] M₂) (e₄₃ : M₄ ≃SL[σ₄₃] M₃) (a✝ : M₂ →SL[σ₂₃] M₃) : (e₁₂.arrowCongrEquivₛₗ e₄₃).symm a✝ = (e₁₂.arrowCongrEquiv e₄₃).invFun a✝

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.

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

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.

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

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

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

@[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

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.

@[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

@[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⁻¹

@[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

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' ↑f, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[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)

@[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)))

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

@[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

@[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

@[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

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

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

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₂ × ↥(↑f₁).ker

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 (↑f₁).ker.subtypeL) ⋯ ⋯

@[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

@[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)

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

def ContinuousLinearEquiv.restrictScalars (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [TopologicalSpace M] [LinearMap.CompatibleSMul M M R S] (f : M ≃L[S] M) : M ≃L[R] M

If M is an R-module and S-module and R-module structure is defined by an action of R on S (formally, we have two scalar towers), then any S-linear equivalence on M is an R-linear equivalence.

Equations

• ContinuousLinearEquiv.restrictScalars R f = { toLinearEquiv := LinearEquiv.restrictScalars R ↑f, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.restrictScalars_symm_apply (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [TopologicalSpace M] [LinearMap.CompatibleSMul M M R S] (f : M ≃L[S] M) (a : M) : (restrictScalars R f).symm a = f.symm a

@[simp]

theorem ContinuousLinearEquiv.restrictScalars_toLinearEquiv (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [TopologicalSpace M] [LinearMap.CompatibleSMul M M R S] (f : M ≃L[S] M) : ↑(restrictScalars R f) = LinearEquiv.restrictScalars R ↑f

@[simp]

theorem ContinuousLinearEquiv.restrictScalars_apply (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [TopologicalSpace M] [LinearMap.CompatibleSMul M M R S] (f : M ≃L[S] M) (a : M) : (restrictScalars R f) a = f a

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

@[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✝

@[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✝

@[instance_reducible]

instance ContinuousLinearEquiv.instSMulUnitsId {S : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [TopologicalSpace V] [Module S V] [ContinuousConstSMul S V] [AddCommMonoid W] [Module R W] [TopologicalSpace W] [Module S W] [ContinuousConstSMul S W] [SMulCommClass R S W] [SMul S R] [IsScalarTower S R V] [IsScalarTower S R W] : SMul Sˣ (V ≃L[R] W)

Left scalar multiplication of a unit and a continuous linear equivalence, as a continuous linear equivalence.

Equations

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

@[simp]

theorem ContinuousLinearEquiv.smul_apply {S : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [TopologicalSpace V] [Module S V] [ContinuousConstSMul S V] [AddCommMonoid W] [Module R W] [TopologicalSpace W] [Module S W] [ContinuousConstSMul S W] [SMulCommClass R S W] [SMul S R] [IsScalarTower S R V] [IsScalarTower S R W] (α : Sˣ) (e : V ≃L[R] W) (x : V) : (α • e) x = ↑α • e x

theorem ContinuousLinearEquiv.symm_smul_apply {S : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [TopologicalSpace V] [Module S V] [ContinuousConstSMul S V] [AddCommMonoid W] [Module R W] [TopologicalSpace W] [Module S W] [ContinuousConstSMul S W] [SMulCommClass R S W] [SMul S R] [IsScalarTower S R V] [IsScalarTower S R W] (e : V ≃L[R] W) (α : Sˣ) (x : W) : (α • e).symm x = ↑α⁻¹ • e.symm x

@[simp]

theorem ContinuousLinearEquiv.symm_smul {S : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [TopologicalSpace V] [Module S V] [ContinuousConstSMul S V] [AddCommMonoid W] [Module R W] [TopologicalSpace W] [Module S W] [ContinuousConstSMul S W] [SMulCommClass R S W] [SMul S R] [IsScalarTower S R V] [IsScalarTower S R W] [SMulCommClass R S V] (e : V ≃L[R] W) (α : Sˣ) : (α • e).symm = α⁻¹ • e.symm

@[simp]

theorem ContinuousLinearEquiv.toLinearEquiv_smul {S : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [TopologicalSpace V] [Module S V] [ContinuousConstSMul S V] [AddCommMonoid W] [Module R W] [TopologicalSpace W] [Module S W] [ContinuousConstSMul S W] [SMulCommClass R S W] [SMul S R] [IsScalarTower S R V] [IsScalarTower S R W] (e : V ≃L[R] W) (α : Sˣ) : ↑(α • e) = α • ↑e

theorem ContinuousLinearEquiv.smul_trans {S : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} {G : Type u_5} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [TopologicalSpace V] [Module S V] [ContinuousConstSMul S V] [AddCommMonoid W] [Module R W] [TopologicalSpace W] [Module S W] [ContinuousConstSMul S W] [AddCommMonoid G] [Module R G] [TopologicalSpace G] [Module S G] [ContinuousConstSMul S G] [SMulCommClass R S W] [SMul S R] [IsScalarTower S R V] [IsScalarTower S R W] [SMulCommClass R S V] [IsScalarTower S R G] (α : Sˣ) (e : G ≃L[R] V) (f : V ≃L[R] W) : (α • e).trans f = α • e.trans f

theorem ContinuousLinearEquiv.trans_smul {S : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} {G : Type u_5} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [TopologicalSpace V] [Module S V] [ContinuousConstSMul S V] [AddCommMonoid W] [Module R W] [TopologicalSpace W] [Module S W] [ContinuousConstSMul S W] [AddCommMonoid G] [Module R G] [TopologicalSpace G] [Module S G] [ContinuousConstSMul S G] [SMulCommClass R S W] [SMul S R] [IsScalarTower S R V] [IsScalarTower S R W] [IsScalarTower S R G] (α : Sˣ) (e : G ≃L[R] V) (f : V ≃L[R] W) : e.trans (α • f) = α • e.trans f

def ContinuousLinearEquiv.ofIsHomeomorph {S : Type u_1} [Semiring S] {S₁ : Type u_6} {M : Type u_7} {M₁ : Type u_8} [Semiring S₁] {σ : S →+* S₁} {σ' : S₁ →+* S} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [TopologicalSpace M] [AddCommMonoid M] [Module S M] [TopologicalSpace M₁] [AddCommMonoid M₁] [Module S₁ M₁] (f : M ≃ₛₗ[σ] M₁) (hf : IsHomeomorph ⇑f) : M ≃SL[σ] M₁

A linear equivalence that is a homeomorphism is a continuous linear equivalence.

Equations

• ContinuousLinearEquiv.ofIsHomeomorph f hf = { toLinearEquiv := f, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem ContinuousLinearEquiv.isHomeomorph {S : Type u_1} [Semiring S] {S₁ : Type u_6} {M : Type u_7} {M₁ : Type u_8} [Semiring S₁] {σ : S →+* S₁} {σ' : S₁ →+* S} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [TopologicalSpace M] [AddCommMonoid M] [Module S M] [TopologicalSpace M₁] [AddCommMonoid M₁] [Module S₁ M₁] (f : M ≃SL[σ] M₁) : IsHomeomorph ⇑f

@[simp]

theorem ContinuousLinearEquiv.toLinearEquiv_ofIsHomeomorph {S : Type u_1} [Semiring S] {S₁ : Type u_6} {M : Type u_7} {M₁ : Type u_8} [Semiring S₁] {σ : S →+* S₁} {σ' : S₁ →+* S} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [TopologicalSpace M] [AddCommMonoid M] [Module S M] [TopologicalSpace M₁] [AddCommMonoid M₁] [Module S₁ M₁] {f : M ≃ₛₗ[σ] M₁} (hf : IsHomeomorph ⇑f) : ↑(ofIsHomeomorph f hf) = f

@[deprecated ContinuousLinearEquiv.toLinearEquiv_ofIsHomeomorph (since := "2026-08-12")]

theorem ContinuousLinearEquiv.toLinearquiv_ofIsHomeomorph {S : Type u_1} [Semiring S] {S₁ : Type u_6} {M : Type u_7} {M₁ : Type u_8} [Semiring S₁] {σ : S →+* S₁} {σ' : S₁ →+* S} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [TopologicalSpace M] [AddCommMonoid M] [Module S M] [TopologicalSpace M₁] [AddCommMonoid M₁] [Module S₁ M₁] {f : M ≃ₛₗ[σ] M₁} (hf : IsHomeomorph ⇑f) : ↑(ofIsHomeomorph f hf) = f

Alias of ContinuousLinearEquiv.toLinearEquiv_ofIsHomeomorph.

@[simp]

theorem ContinuousLinearEquiv.coe_ofIsHomeomorph {S : Type u_1} [Semiring S] {S₁ : Type u_6} {M : Type u_7} {M₁ : Type u_8} [Semiring S₁] {σ : S →+* S₁} {σ' : S₁ →+* S} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [TopologicalSpace M] [AddCommMonoid M] [Module S M] [TopologicalSpace M₁] [AddCommMonoid M₁] [Module S₁ M₁] {f : M ≃ₛₗ[σ] M₁} (hf : IsHomeomorph ⇑f) : ⇑(ofIsHomeomorph f hf) = ⇑f

theorem LinearEquiv.isHomeomorph_iff {S : Type u_1} [Semiring S] {S₁ : Type u_6} {M : Type u_7} {M₁ : Type u_8} [Semiring S₁] {σ : S →+* S₁} {σ' : S₁ →+* S} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [TopologicalSpace M] [AddCommMonoid M] [Module S M] [TopologicalSpace M₁] [AddCommMonoid M₁] [Module S₁ M₁] (e : M ≃ₛₗ[σ] M₁) : IsHomeomorph ⇑e ↔ Continuous ⇑e ∧ Continuous ⇑e.symm

A linear equivalence between topological modules is a homeomorphism if and only if it is continuous in both directions.

@[simp]

theorem ContinuousLinearEquiv.toLinearEquiv_inv {R : Type u_2} {V : Type u_3} [Semiring R] [AddCommMonoid V] [Module R V] [TopologicalSpace V] (f : V ≃L[R] V) : ↑f⁻¹ = (↑f)⁻¹

@[simp]

theorem ContinuousLinearEquiv.toLinearEquiv_mul {R : Type u_2} {V : Type u_3} [Semiring R] [AddCommMonoid V] [Module R V] [TopologicalSpace V] (f g : V ≃L[R] V) : ↑(f * g) = ↑f * ↑g

def ContinuousLinearEquiv.toLinearEquivMonoidHom {R : Type u_2} {V : Type u_3} [Semiring R] [AddCommMonoid V] [Module R V] [TopologicalSpace V] : (V ≃L[R] V) →* V ≃ₗ[R] V

ContinuousLinearEquiv.toLinearEquiv as a multiplicative monoid homomorphism MonoidHom.

Equations

• ContinuousLinearEquiv.toLinearEquivMonoidHom = { toFun := ContinuousLinearEquiv.toLinearEquiv, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.toLinearEquivMonoidHom_apply {R : Type u_2} {V : Type u_3} [Semiring R] [AddCommMonoid V] [Module R V] [TopologicalSpace V] (self : V ≃L[R] V) : toLinearEquivMonoidHom self = ↑self

@[simp]

theorem ContinuousLinearEquiv.toLinearEquiv_pow {R : Type u_2} {V : Type u_3} [Semiring R] [AddCommMonoid V] [Module R V] [TopologicalSpace V] (f : V ≃L[R] V) (n : ℕ) : ↑(f ^ n) = ↑f ^ n

@[simp]

theorem ContinuousLinearEquiv.toLinearEquiv_zpow {R : Type u_2} {V : Type u_3} [Semiring R] [AddCommMonoid V] [Module R V] [TopologicalSpace V] (f : V ≃L[R] V) (n : ℤ) : ↑(f ^ n) = ↑f ^ n