Continuous linear equivalences on products of topological modules

Main Definitions

• prodCongr: Equiv.prodCongr as a continuous linear equivalence.
• prodComm: LinearEquiv.prodComm as a continuous linear equivalence.
• prodAssoc: LinearEquiv.prodAssoc as a continuous linear equivalence.
• prodProdProdComm: LinearEquiv.prodProdProdComm as a continuous linear equivalence.
• prodUnique: Equiv.prodUnique as a continuous linear equivalence.
• uniqueProd: Equiv.uniqueProd as a continuous linear equivalence.

def ContinuousLinearEquiv.prodCongr {R : Type u_1} [Semiring R] {M₁ : Type u_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] {M₄ : Type u_5} [TopologicalSpace M₄] [AddCommMonoid 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', continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.prodCongr_apply {R : Type u_1} [Semiring R] {M₁ : Type u_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] {M₄ : Type u_5} [TopologicalSpace M₄] [AddCommMonoid 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)

@[simp]

theorem ContinuousLinearEquiv.coe_prodCongr {R : Type u_1} [Semiring R] {M₁ : Type u_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] {M₄ : Type u_5} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R M₄] (e : M₁ ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) : ↑(e.prodCongr e') = (↑e).prodMap ↑e'

@[simp]

theorem ContinuousLinearEquiv.prodCongr_symm {R : Type u_1} [Semiring R] {M₁ : Type u_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] {M₄ : Type u_5} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R M₄] (e : M₁ ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) : (e.prodCongr e').symm = e.symm.prodCongr e'.symm

def ContinuousLinearEquiv.prodComm (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] : (M₁ × M₂) ≃L[R] M₂ × M₁

Product of topological modules is commutative up to continuous linear isomorphism.

Equations

• ContinuousLinearEquiv.prodComm R M₁ M₂ = { toLinearEquiv := LinearEquiv.prodComm R M₁ M₂, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.prodComm_toLinearEquiv (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] : ↑(prodComm R M₁ M₂) = LinearEquiv.prodComm R M₁ M₂

@[simp]

theorem ContinuousLinearEquiv.prodComm_apply (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (a✝ : M₁ × M₂) : (prodComm R M₁ M₂) a✝ = a✝.swap

@[simp]

theorem ContinuousLinearEquiv.prodComm_symm (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] : (prodComm R M₁ M₂).symm = prodComm R M₂ M₁

theorem ContinuousLinearMap.coprod_comp_prodComm (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] [ContinuousAdd M₃] (f : M₁ →L[R] M₃) (g : M₂ →L[R] M₃) : f.coprod g ∘SL ↑(ContinuousLinearEquiv.prodComm R M₂ M₁) = g.coprod f

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

def ContinuousLinearEquiv.prodAssoc (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R 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 := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.prodAssoc_toLinearEquiv (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] : ↑(prodAssoc R M₁ M₂ M₃) = LinearEquiv.prodAssoc R M₁ M₂ M₃

@[simp]

theorem ContinuousLinearEquiv.coe_prodAssoc (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] : ⇑(prodAssoc R M₁ M₂ M₃) = ⇑(Equiv.prodAssoc M₁ M₂ M₃)

@[simp]

theorem ContinuousLinearEquiv.prodAssoc_apply (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] (p₁ : M₁) (p₂ : M₂) (p₃ : M₃) : (prodAssoc R M₁ M₂ M₃) ((p₁, p₂), p₃) = (p₁, p₂, p₃)

@[simp]

theorem ContinuousLinearEquiv.prodAssoc_symm_apply (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] (p₁ : M₁) (p₂ : M₂) (p₃ : M₃) : (prodAssoc R M₁ M₂ M₃).symm (p₁, p₂, p₃) = ((p₁, p₂), p₃)

def ContinuousLinearEquiv.prodProdProdComm (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] (M₄ : Type u_5) [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R 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 := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.prodProdProdComm_symm (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] (M₄ : Type u_5) [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R M₄] : (prodProdProdComm R M₁ M₂ M₃ M₄).symm = prodProdProdComm R M₁ M₃ M₂ M₄

@[simp]

theorem ContinuousLinearEquiv.prodProdProdComm_toLinearEquiv (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] (M₄ : Type u_5) [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R M₄] : ↑(prodProdProdComm R M₁ M₂ M₃ M₄) = LinearEquiv.prodProdProdComm R M₁ M₂ M₃ M₄

@[simp]

theorem ContinuousLinearEquiv.coe_prodProdProdComm (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] (M₄ : Type u_5) [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R M₄] : ⇑(prodProdProdComm R M₁ M₂ M₃ M₄) = ⇑(Equiv.prodProdProdComm M₁ M₂ M₃ M₄)

@[simp]

theorem ContinuousLinearEquiv.prodProdProdComm_apply (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] (M₄ : Type u_5) [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R M₄] (p₁ : M₁) (p₂ : M₂) (p₃ : M₃) (p₄ : M₄) : (prodProdProdComm R M₁ M₂ M₃ M₄) ((p₁, p₂), p₃, p₄) = ((p₁, p₃), p₂, p₄)

def ContinuousLinearEquiv.prodUnique (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] [Unique M₂] : (M₁ × M₂) ≃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₁ M₂ = { toLinearEquiv := LinearEquiv.prodUnique, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.coe_prodUnique (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] [Unique M₂] : (↑(prodUnique R M₁ M₂)).toEquiv = Equiv.prodUnique M₁ M₂

@[simp]

theorem ContinuousLinearEquiv.prodUnique_apply (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] [Unique M₂] (x : M₁ × M₂) : (prodUnique R M₁ M₂) x = x.1

@[simp]

theorem ContinuousLinearEquiv.prodUnique_symm_apply (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] [Unique M₂] (x : M₁) : (prodUnique R M₁ M₂).symm x = (x, default)

def ContinuousLinearEquiv.uniqueProd (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] [Unique M₂] : (M₂ × 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₁ M₂ = { toLinearEquiv := LinearEquiv.uniqueProd, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.coe_uniqueProd (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] [Unique M₂] : (↑(uniqueProd R M₁ M₂)).toEquiv = Equiv.uniqueProd M₁ M₂

@[simp]

theorem ContinuousLinearEquiv.uniqueProd_apply (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] [Unique M₂] (x : M₂ × M₁) : (uniqueProd R M₁ M₂) x = x.2

@[simp]

theorem ContinuousLinearEquiv.uniqueProd_symm_apply (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] [Unique M₂] (x : M₁) : (uniqueProd R M₁ M₂).symm x = (default, x)