Transfer topological algebraic structures across AddEquivs or ContinuousLinearEquivs

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 AddEquiv.continuousLinearEquiv (R : Type u_1) {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [TopologicalSpace β] [AddCommMonoid β] [Semiring R] [Module R β] (e : α ≃+ β) : α ≃L[R] β

An additive 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

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

@[simp]

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

@[deprecated AddEquiv.continuousLinearEquiv (since := "2026-08-10")]

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

Alias of AddEquiv.continuousLinearEquiv.

---

An additive 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 = AddEquiv.continuousLinearEquiv

@[deprecated AddEquiv.toLinearEquiv_continuousLinearEquiv (since := "2026-08-10")]

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

Alias of AddEquiv.toLinearEquiv_continuousLinearEquiv.

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

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

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

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

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 α = AddEquiv.continuousLinearEquiv R Shrink.addEquiv

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

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