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

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_symm_apply (R : Type u_1) (α : Type u_2) [Small.{v, u_2} α] [AddCommMonoid α] [TopologicalSpace α] [Semiring R] [Module R α] (a✝ : α) : (continuousLinearEquiv R α).symm a✝ = (AddEquiv.symm (equivShrink α).symm.addEquiv) 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✝