Transport of a Hilbert space along an isomorphism of RCLike fields

RCLike is an open class, but it has exactly two models: RCLike.I_eq_zero_or_im_I_eq_one says every RCLike field is isomorphic to ℝ or to ℂ. A theorem proved at those two fields is therefore true at every RCLike field — but only after the statement has been carried across the isomorphism, and that is what this file does.

The design is one transport, used twice. RCLikeIso 𝕜 𝕂 is a field isomorphism fixing the reals and I; RCLikeIso.real and RCLikeIso.complex build the two instances from Mathlib's RCLike.realRingEquiv and RCLike.complexRingEquiv.

ScalarTransport e E is E with the 𝕂-structure its 𝕜-structure induces through e. The type, the additive group, the topology and the norm are unchanged; only the scalar action and the field the inner product takes values in move. So most of what follows is a bijection between two spellings of the same object, and the transported object is equal to the original wherever that makes sense:

object	transport	preserved
Submodule 𝕜 E	ScalarTransport.submodule	the carrier, ᗮ, Module.rank
E →L[𝕜] F	ScalarTransport.clm	the function, ‖·‖, adjoint, IsSelfAdjoint
Submodule.starProjection	—	it is the transported projection
E →ₗ.[𝕜] F	ScalarTransport.pmap	the domain, the function, adjoint, IsSelfAdjoint

Nothing here is specific to any application: it is the general statement that a Hilbert space over an RCLike field is a Hilbert space over ℝ or ℂ, in a way that carries the operator theory with it.

Why not restriction of scalars

InnerProductSpace.rclikeToReal restricts a 𝕜-space to ℝ. That is a different construction and it does not answer this question: over a complex-like 𝕜 it halves the scalars, doubling Module.rank and changing the singular-value sequence of an operator. The transport here changes no ranks, because it changes no scalars — it renames the field.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: none. Written directly here, 2026-09-01, because the Palomar Section 2 Challenge needs its four theorems at an arbitrary RCLike field and the development's endpoints are stated at ℝ and ℂ.
• Extraction class: new. It depends on nothing outside Mathlib, and is the reason the two capability classes ContinuousLinearMap.HasMinMaxLowerBoundEverywhere and TauCeti.DavisKahan.Sylvester.HasUnboundedSylvesterKyFan stopped being hypotheses.
• Namespace: TauCeti, per ForTauCeti/README.md section 2.
• @[expose] on ten definitional carriers, each measured load-bearing by deleting the attribute and reading the compiler's complaint.
• Original authors / copyright: Jon Crall, Claude Opus 5; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none.

structure TauCeti.RCLikeIso (𝕜 : Type u) (𝕂 : Type w) [RCLike 𝕜] [RCLike 𝕂] : Type (max u w)

An isomorphism of RCLike fields fixing the reals and I.

• toRingEquiv : 𝕜 ≃+* 𝕂

  The underlying ring equivalence.

• map_ofReal (r : ℝ) : self.toRingEquiv ↑r = ↑r
• map_I : self.toRingEquiv RCLike.I = RCLike.I

@[instance_reducible]

instance TauCeti.RCLikeIso.instCoeFunForall {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] : CoeFun (RCLikeIso 𝕜 𝕂) fun (x : RCLikeIso 𝕜 𝕂) => 𝕜 → 𝕂

The isomorphism acts as a function.

Equations

• TauCeti.RCLikeIso.instCoeFunForall = { coe := fun (e : TauCeti.RCLikeIso 𝕜 𝕂) => ⇑e.toRingEquiv }

def TauCeti.RCLikeIso.symm {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] (e : RCLikeIso 𝕜 𝕂) : RCLikeIso 𝕂 𝕜

Reverse an isomorphism of RCLike fields.

Equations

• e.symm = { toRingEquiv := e.toRingEquiv.symm, map_ofReal := ⋯, map_I := ⋯ }

noncomputable def TauCeti.RCLikeIso.real {𝕜 : Type u} [RCLike 𝕜] (h : RCLike.I = 0) : RCLikeIso 𝕜 ℝ

When I = 0 the field is ℝ.

Equations

• TauCeti.RCLikeIso.real h = { toRingEquiv := RCLike.realRingEquiv h, map_ofReal := ⋯, map_I := ⋯ }

noncomputable def TauCeti.RCLikeIso.complex {𝕜 : Type u} [RCLike 𝕜] (h : RCLike.im RCLike.I = 1) : RCLikeIso 𝕜 ℂ

When im I = 1 the field is ℂ.

Equations

• TauCeti.RCLikeIso.complex h = { toRingEquiv := RCLike.complexRingEquiv h, map_ofReal := ⋯, map_I := ⋯ }

theorem TauCeti.RCLikeIso.apply_eq {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] (e : RCLikeIso 𝕜 𝕂) (x : 𝕜) : e.toRingEquiv x = ↑(RCLike.re x) + ↑(RCLike.im x) * RCLike.I

The isomorphism is determined by its action on the real and imaginary parts.

@[simp]

theorem TauCeti.RCLikeIso.re_map {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] (e : RCLikeIso 𝕜 𝕂) (x : 𝕜) : RCLike.re (e.toRingEquiv x) = RCLike.re x

The isomorphism preserves real parts.

theorem TauCeti.RCLikeIso.im_I_map {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] (e : RCLikeIso 𝕜 𝕂) : RCLike.im RCLike.I = RCLike.im RCLike.I

I vanishes on one side exactly when it vanishes on the other.

@[simp]

theorem TauCeti.RCLikeIso.im_map {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] (e : RCLikeIso 𝕜 𝕂) (x : 𝕜) : RCLike.im (e.toRingEquiv x) = RCLike.im x

The isomorphism preserves imaginary parts.

@[simp]

theorem TauCeti.RCLikeIso.norm_map {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] (e : RCLikeIso 𝕜 𝕂) (x : 𝕜) : ‖e.toRingEquiv x‖ = ‖x‖

The isomorphism preserves norms.

@[simp]

theorem TauCeti.RCLikeIso.map_conj {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] (e : RCLikeIso 𝕜 𝕂) (x : 𝕜) : e.toRingEquiv ((starRingEnd 𝕜) x) = (starRingEnd 𝕂) (e.toRingEquiv x)

The isomorphism commutes with conjugation.

theorem TauCeti.RCLikeIso.norm_symm_map' {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] (e : RCLikeIso 𝕜 𝕂) (c : 𝕂) : ‖e.toRingEquiv.symm c‖ = ‖c‖

The inverse preserves norms.

theorem TauCeti.RCLikeIso.isometry {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] (e : RCLikeIso 𝕜 𝕂) : Isometry ⇑e.toRingEquiv

The isomorphism is an isometry.

noncomputable def TauCeti.RCLikeIso.homeomorph {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] (e : RCLikeIso 𝕜 𝕂) : 𝕜 ≃ₜ 𝕂

The field isomorphism is a homeomorphism.

Equations

• e.homeomorph = { toEquiv := e.toRingEquiv.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.RCLikeIso.coe_homeomorph {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] (e : RCLikeIso 𝕜 𝕂) : ⇑e.homeomorph = ⇑e.toRingEquiv

The homeomorphism is the isomorphism.

theorem TauCeti.RCLikeIso.norm_symm_map {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] (e : RCLikeIso 𝕜 𝕂) (c : 𝕂) : ‖e.toRingEquiv.symm c‖ = ‖c‖

The inverse preserves norms.

def TauCeti.ScalarTransport {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] (_e : RCLikeIso 𝕜 𝕂) (E : Type v) : Type v

E, carrying the 𝕂-Hilbert structure its 𝕜-structure induces through e.

The type, the additive group, the topology and the norm are unchanged; only the scalar action and the inner product's field of values move.

Equations

• TauCeti.ScalarTransport _e E = E

def TauCeti.ScalarTransport.of {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} (x : E) : ScalarTransport e E

The identity, as the passage from E to its transport.

Equations

• TauCeti.ScalarTransport.of x = x

def TauCeti.ScalarTransport.out {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} (x : ScalarTransport e E) : E

The identity, as the passage back.

Equations

• x.out = x

@[simp]

theorem TauCeti.ScalarTransport.of_out {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} (x : ScalarTransport e E) : of x.out = x

of and out are mutually inverse.

@[simp]

theorem TauCeti.ScalarTransport.out_of {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} (x : E) : (of x).out = x

of and out are mutually inverse.

@[instance_reducible]

instance TauCeti.ScalarTransport.instNormedAddCommGroup {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] : NormedAddCommGroup (ScalarTransport e E)

The transport does not touch the additive normed structure.

Equations

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

@[instance_reducible]

instance TauCeti.ScalarTransport.instModule {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : Module 𝕂 (ScalarTransport e E)

Scalars act through e⁻¹.

Equations

• TauCeti.ScalarTransport.instModule = Module.compHom E ↑e.toRingEquiv.symm

theorem TauCeti.ScalarTransport.smul_def {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (c : 𝕂) (x : ScalarTransport e E) : c • x = of (e.toRingEquiv.symm c • x.out)

Scalars act through e⁻¹.

@[instance_reducible]

noncomputable instance TauCeti.ScalarTransport.instNormedSpace {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : NormedSpace 𝕂 (ScalarTransport e E)

and isometrically, because e is.

Equations

• TauCeti.ScalarTransport.instNormedSpace = { toModule := TauCeti.ScalarTransport.instModule, norm_smul_le := ⋯ }

@[instance_reducible]

noncomputable instance TauCeti.ScalarTransport.instInnerProductSpace {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : InnerProductSpace 𝕂 (ScalarTransport e E)

The inner product is the original, carried across e.

Equations

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

instance TauCeti.ScalarTransport.instCompleteSpace {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [CompleteSpace E] : CompleteSpace (ScalarTransport e E)

Completeness is a fact about the metric, which is unchanged.

@[simp]

theorem TauCeti.ScalarTransport.norm_of {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] (x : E) : ‖of x‖ = ‖x‖

The transport does not change the norm.

@[simp]

theorem TauCeti.ScalarTransport.inner_of {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) : inner 𝕂 (of x) (of y) = e.toRingEquiv (inner 𝕜 x y)

The transported inner product is the original, carried across e.

@[simp]

theorem TauCeti.ScalarTransport.ofReal_smul_of {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (r : ℝ) (x : E) : ↑r • of x = of (↑r • x)

A real scalar acts the same on both sides.

theorem TauCeti.ScalarTransport.re_inner_of {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) : RCLike.re (inner 𝕂 (of x) (of y)) = RCLike.re (inner 𝕜 x y)

and its real part is literally unchanged.

Subspaces

def TauCeti.ScalarTransport.submodule {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (S : Submodule 𝕜 E) : Submodule 𝕂 (ScalarTransport e E)

A 𝕜-subspace of E, as a 𝕂-subspace of the transport, with the same carrier.

Equations

• TauCeti.ScalarTransport.submodule S = { carrier := {x : TauCeti.ScalarTransport e E | x.out ∈ S}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem TauCeti.ScalarTransport.mem_submodule {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {S : Submodule 𝕜 E} {x : ScalarTransport e E} : x ∈ submodule S ↔ x.out ∈ S

Membership in a transported subspace is membership in the original.

def TauCeti.ScalarTransport.submoduleSymm {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (S : Submodule 𝕂 (ScalarTransport e E)) : Submodule 𝕜 E

and back again.

Equations

• TauCeti.ScalarTransport.submoduleSymm S = { carrier := {x : E | TauCeti.ScalarTransport.of x ∈ S}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem TauCeti.ScalarTransport.mem_submoduleSymm {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {S : Submodule 𝕂 (ScalarTransport e E)} {x : E} : x ∈ submoduleSymm S ↔ of x ∈ S

Membership in a subspace read back is membership in the original.

@[simp]

theorem TauCeti.ScalarTransport.submoduleSymm_submodule {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (S : Submodule 𝕜 E) : submoduleSymm (submodule S) = S

The two directions are mutually inverse.

@[simp]

theorem TauCeti.ScalarTransport.submodule_submoduleSymm {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (S : Submodule 𝕂 (ScalarTransport e E)) : submodule (submoduleSymm S) = S

The two directions are mutually inverse.

@[simp]

theorem TauCeti.ScalarTransport.submodule_orthogonal {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (S : Submodule 𝕜 E) : (submodule S)ᗮ = submodule Sᗮ

The transport preserves orthogonal complements.

Bounded operators

def TauCeti.ScalarTransport.clm {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) : ScalarTransport e E →L[𝕂] ScalarTransport e F

A 𝕜-linear continuous map, as a 𝕂-linear one on the transports.

Equations

• TauCeti.ScalarTransport.clm T = { toFun := fun (x : TauCeti.ScalarTransport e E) => TauCeti.ScalarTransport.of (T x.out), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem TauCeti.ScalarTransport.clm_apply {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) (x : E) : (clm T) (of x) = of (T x)

The transported operator is the original function.

@[simp]

theorem TauCeti.ScalarTransport.clm_sub {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T R : E →L[𝕜] F) : clm (T - R) = clm T - clm R

The transport of operators is subtractive: it does not change the functions.

@[simp]

theorem TauCeti.ScalarTransport.clm_norm {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) : ‖clm T‖ = ‖T‖

and has the same operator norm.

def TauCeti.ScalarTransport.clmEquiv {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] : (E →L[𝕜] F) ≃ (ScalarTransport e E →L[𝕂] ScalarTransport e F)

The transport of a bounded operator is a bijection onto the 𝕂-operators.

Equations

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

Rank

def TauCeti.ScalarTransport.addEquiv {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] : E ≃+ ScalarTransport e E

The additive identity E ≃+ ScalarTransport e E.

Equations

• TauCeti.ScalarTransport.addEquiv = { toFun := TauCeti.ScalarTransport.of, invFun := TauCeti.ScalarTransport.out, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

theorem TauCeti.ScalarTransport.addEquiv_smul {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (r : 𝕜) (x : E) : addEquiv (r • x) = e.toRingEquiv r • addEquiv x

The additive identity intertwines the two scalar actions through e.

theorem TauCeti.ScalarTransport.rank_eq {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (S : Submodule 𝕜 E) : Module.rank 𝕜 ↥S = Module.rank 𝕂 ↥(submodule S)

Rank is unchanged by the transport: the scalar action is the same up to e.

theorem TauCeti.ScalarTransport.rank_clm_eq {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) : (↑(clm T)).rank = (↑T).rank

Hence the rank of a transported map.

Orthogonal projections

instance TauCeti.ScalarTransport.hasOrthogonalProjection {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (S : Submodule 𝕜 E) [S.HasOrthogonalProjection] : (submodule S).HasOrthogonalProjection

A transported subspace inherits its orthogonal projection.

theorem TauCeti.ScalarTransport.starProjection_of {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (S : Submodule 𝕜 E) [S.HasOrthogonalProjection] (x : E) : (submodule S).starProjection (of x) = of (S.starProjection x)

and the projection is the original projection.

@[simp]

theorem TauCeti.ScalarTransport.starProjection_clm {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (S : Submodule 𝕜 E) [S.HasOrthogonalProjection] : (submodule S).starProjection = clm S.starProjection

The transported projection is the transport of the projection.

Adjoints

@[simp]

theorem TauCeti.ScalarTransport.adjoint_clm {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (T : E →L[𝕜] F) : ContinuousLinearMap.adjoint (clm T) = clm (ContinuousLinearMap.adjoint T)

The adjoint of a transported operator is the transport of its adjoint.

theorem TauCeti.ScalarTransport.isSelfAdjoint_clm_iff {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} : IsSelfAdjoint (clm T) ↔ IsSelfAdjoint T

Self-adjointness is preserved and reflected by the transport.

Partial maps

def TauCeti.ScalarTransport.domainOut {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] F) (x : ↥(submodule A.domain)) : ↥A.domain

A point of the transported domain, read back in A.domain.

Equations

• TauCeti.ScalarTransport.domainOut A x = ⟨(↑x).out, ⋯⟩

def TauCeti.ScalarTransport.pmap {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] F) : ScalarTransport e E →ₗ.[𝕂] ScalarTransport e F

A 𝕜-linear partial map, as a 𝕂-linear one on the transports: the same domain and the same function.

Equations

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

@[simp]

theorem TauCeti.ScalarTransport.pmap_domain {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] F) : (pmap A).domain = submodule A.domain

The transported partial map has the transported domain.

@[simp]

theorem TauCeti.ScalarTransport.pmap_apply {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] F) (x : ↥(pmap A).domain) : ↑(pmap A) x = of (↑A (domainOut A x))

and the original function.

theorem TauCeti.ScalarTransport.dense_pmap_domain_iff {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] F) : Dense ↑(pmap A).domain ↔ Dense ↑A.domain

Density of the domain is unchanged: the carrier and the topology are.

theorem TauCeti.ScalarTransport.mem_pmap_adjointDomain_iff {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] F) (y : ScalarTransport e F) : y ∈ (pmap A).adjointDomain ↔ y.out ∈ A.adjointDomain

The transported adjoint domain is the original one, because e is a homeomorphism.

@[simp]

theorem TauCeti.ScalarTransport.pmap_adjointDomain {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] F) : (pmap A).adjointDomain = submodule A.adjointDomain

The transported adjoint domain is the transport of the adjoint domain.

theorem TauCeti.ScalarTransport.pmap_injective {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] : Function.Injective pmap

The transport of partial maps is injective.

theorem TauCeti.ScalarTransport.pmap_adjoint {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] (e : RCLikeIso 𝕜 𝕂) {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v'} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] (A : E →ₗ.[𝕜] F) (hA : Dense ↑A.domain) : (pmap A).adjoint = pmap A.adjoint

The adjoint of a transported partial map is the transport of its adjoint.

theorem TauCeti.ScalarTransport.isSelfAdjoint_pmap_iff {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] (e : RCLikeIso 𝕜 𝕂) {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →ₗ.[𝕜] E} : IsSelfAdjoint (pmap A) ↔ IsSelfAdjoint A

Self-adjointness is preserved and reflected by the transport.