Transfer topological algebraic structures across Equivs

In this file, we construct a continuous linear equivalence α ≃L[R] β from an equivalence α ≃ β, where the continuous R-module structure on α is the one obtained by transporting an R-module structure on β back along e. We also specialize this construction to Shrink α.

This continues the pattern set in Mathlib/Algebra/Module/TransferInstance.lean.

def Equiv.continuousLinearEquiv (R : Type u_1) {α : Type u_2} {β : Type u_3} [TopologicalSpace β] [AddCommMonoid β] [Semiring R] [Module R β] (e : α ≃ β) : α ≃L[R] β

An equivalence e : α ≃ β gives a continuous linear equivalence α ≃L[R] β where the continuous R-module structure on α is the one obtained by transporting an R-module structure on β back along e.

This is e.linearEquiv as a continuous linear equivalence.

Equations

• Equiv.continuousLinearEquiv R e = { toLinearEquiv := Equiv.linearEquiv R e, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem Equiv.toLinearEquiv_continuousLinearEquiv {R : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] [AddCommMonoid β] [Semiring R] [Module R β] (e : α ≃ β) : (continuousLinearEquiv R e).toLinearEquiv = linearEquiv R e

theorem ContinuousMulEquiv.isTopologicalGroup {α : Type u_2} {β : Type u_3} [TopologicalSpace β] [Group β] [IsTopologicalGroup β] [TopologicalSpace α] [Group α] (e : α ≃ₜ* β) : IsTopologicalGroup α

Given a continuous additive equivalence e : α ≃ₜ+ β, if β is a topological additive group, then so is α.

theorem ContinuousAddEquiv.isTopologicalAddGroup {α : Type u_2} {β : Type u_3} [TopologicalSpace β] [AddGroup β] [IsTopologicalAddGroup β] [TopologicalSpace α] [AddGroup α] (e : α ≃ₜ+ β) : IsTopologicalAddGroup α

theorem ContinuousLinearEquiv.continuousSMul {R : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring R] [TopologicalSpace β] [AddCommGroup β] [Module R β] [TopologicalSpace R] [ContinuousSMul R β] [TopologicalSpace α] [AddCommGroup α] [Module R α] (e : α ≃L[R] β) : ContinuousSMul R α

Given a continuous linear equivalence e : α ≃L[R] β, if scalar multiplication on β is continuous, then so is it for α.

noncomputable def Shrink.continuousLinearEquiv (R : Type u_1) (α : Type u_2) [Small.{v, u_2} α] [AddCommMonoid α] [TopologicalSpace α] [Semiring R] [Module R α] : Shrink.{v, u_2} α ≃L[R] α

Shrinking α to a smaller universe preserves the continuous module structure.

Equations

• Shrink.continuousLinearEquiv R α = Equiv.continuousLinearEquiv R (equivShrink α).symm

@[simp]

theorem Shrink.continuousLinearEquiv_apply (R : Type u_1) (α : Type u_2) [Small.{v, u_2} α] [AddCommMonoid α] [TopologicalSpace α] [Semiring R] [Module R α] (a✝ : Shrink.{v, u_2} α) : (continuousLinearEquiv R α) a✝ = (equivShrink α).symm a✝

@[simp]

theorem Shrink.continuousLinearEquiv_symm_apply (R : Type u_1) (α : Type u_2) [Small.{v, u_2} α] [AddCommMonoid α] [TopologicalSpace α] [Semiring R] [Module R α] (a✝ : α) : (continuousLinearEquiv R α).symm a✝ = (equivShrink α) a✝