The closure-space homeomorphism induced by an orthogonality equivalence

NormedSpace.geometricStructureHomeomorphOfBirkhoffJames

def

Statement

Let and be normed spaces over real-or-complex scalar fields and , and let be a bijection preserving and reflecting their Birkhoff–James orthogonality relations. Define the induced closure-space homeomorphism

\Phi_e:S_{\mathbb K}(E)\longrightarrow S_{\mathbb L}(F), \qquad \Phi_e(I)=e(I),

with inverse . Here is a direct image and is a preimage. Well-definedness and closure preservation are supplied by the separately cited transport theorems.

Definition

Let and be normed spaces over real-or-complex scalar fields and , respectively; the fields may differ. Define

x\perp_{\mathbb K}y \quad\Longleftrightarrow\quad \|x\|\leq\|x+ay\|\text{ for every }a\in\mathbb K.

The same formula with defines orthogonality on . Let be a bijection such that, for every ,

e(x)\perp_{\mathbb L}e(y)\quad\Longleftrightarrow\quad x\perp_{\mathbb K}y.

Here is the geometric point set on which the induced map acts. Write for the continuous -linear dual and . For a nonempty maximal proper real convex face of , put

\begin{aligned} \Sigma_{\mathbb K}(M)&=\{f\in E^*: \|f\|\leq1,\ f|_M=1\},\\ I_{\mathbb K}(M)&=\bigcup_{f\in\Sigma_{\mathbb K}(M)}\ker f. \end{aligned}

Here means for every .

A face is a convex subset containing both endpoints of each segment in the ball whose interior meets it; maximality is among proper convex faces. The set consists of the resulting subsets , with equal subsets regarded as the same point. Its closure is

\begin{gathered} c_E(\mathscr A)=\left\{I\in S_{\mathbb K}(E):\bigcap_{J\in\mathscr A}J\subseteq I\right\},\\ \mathscr A\subseteq S_{\mathbb K}(E). \end{gathered}

The empty intersection is . Define and by the same formulas for . Define the point map by

\Phi_e:S_{\mathbb K}(E)\longrightarrow S_{\mathbb L}(F), \qquad \Phi_e(I)=e(I).

Its inverse sends to , the preimage under .

The geometric-point transport theorem makes this point map well-defined; the same theorem for the inverse bijection supplies the inverse. The incidence identity and hull–kernel closure-transport theorem supply its homeomorphism structure.

Assumptions

The spaces are normed, with no completeness or nontriviality assumption. Their real-or-complex scalar fields may differ. The given bijection preserves and reflects the displayed ordered orthogonality relation for every pair of vectors; additivity, homogeneity and norm continuity are not assumed.

Conclusion

The output is the specified point bijection , together with closure continuity of it and its inverse. Its underlying map and inverse are exactly those displayed above. A closure-space homeomorphism is a bijection continuous in both directions for the given closure operators; the operators need not be topological closures. The cited transport theorem supplies the identity

\Phi_e\bigl(c_E(\mathscr A)\bigr) =c_F\bigl(\Phi_e(\mathscr A)\bigr) \qquad(\mathscr A\subseteq S_{\mathbb K}(E)).

Main citations

Geometric points remain geometric under the given bijection: NormedSpace.image_mem_geometricStructureFamily.
The point equivalence and its incidence identity: NormedSpace.geometricStructureEquivOfBirkhoffJames and NormedSpace.mem_geometricStructureEquivOfBirkhoffJames.
Incidence-preserving equivalences commute with hull–kernel closure: ClosureSpace.HullKernel.image_closure. The following homeomorphOfMemIff definition packages this theorem.
The geometric point family and closure; maximal proper real convex faces.
Closure continuity and closure-space homeomorphisms and the homeomorphism structure.

Lean source signature (exact)

The construction uses the scalar, space and bijection hypotheses reproduced separately below.

def geometricStructureHomeomorphOfBirkhoffJames :
    ClosureSpace.Homeomorph (geometricStructureClosure 𝕜 E) (geometricStructureClosure 𝕝 F) :=
  ClosureSpace.HullKernel.homeomorphOfMemIff
    (univ_notMem_geometricStructureFamily 𝕜 E) (univ_notMem_geometricStructureFamily 𝕝 F)
    e (geometricStructureEquivOfBirkhoffJames 𝕜 𝕝 e h)
    (mem_geometricStructureEquivOfBirkhoffJames 𝕜 𝕝 e h)

Back to the reading-guide item

In the source	Mathematical meaning
Scalar fields and normed spaces`variable (𝕜 : Type v) (𝕝 : Type z) [RCLike 𝕜] [RCLike 𝕝] variable {E : Type u} {F : Type w} variable [NormedAddCommGroup E] [NormedSpace 𝕜 E] variable [NormedAddCommGroup F] [NormedSpace 𝕝 F]`Fixed source	The fields may each be real or complex. The spaces carry their respective norms and scalar actions; neither completeness nor nontriviality is required.
Bijection and orthogonality`variable (e : E ≃ F) variable (h : ∀ x y : E, BirkhoffJamesOrthogonal 𝕝 (e x) (e y) ↔ BirkhoffJamesOrthogonal 𝕜 x y) include h`Fixed source	The given set bijection preserves and reflects Birkhoff–James orthogonality for every ordered pair. The included hypothesis is the same used in this construction; linearity of is not assumed.
Two closure spaces`def geometricStructureHomeomorphOfBirkhoffJames : ClosureSpace.Homeomorph (geometricStructureClosure 𝕜 E) (geometricStructureClosure 𝕝 F) :=`Fixed source	The result is a homeomorphism from to . These two complete closure arguments specify its domain and codomain.
Point map and incidence input`ClosureSpace.HullKernel.homeomorphOfMemIff (univ_notMem_geometricStructureFamily 𝕜 E) (univ_notMem_geometricStructureFamily 𝕝 F) e (geometricStructureEquivOfBirkhoffJames 𝕜 𝕝 e h) (mem_geometricStructureEquivOfBirkhoffJames 𝕜 𝕝 e h)`Fixed source	The constructor receives the properness of both geometric families, the ambient bijection , the point bijection , and the incidence identity . These are the same maps as in the Statement.
Forward and inverse point maps`def geometricStructureEquivOfBirkhoffJames : GeometricStructureSpace 𝕜 E ≃ GeometricStructureSpace 𝕝 F where toFun I := ⟨e '' I.val, image_mem_geometricStructureFamily 𝕜 𝕝 e h I.property⟩ invFun J := ⟨e.symm '' J.val, image_mem_geometricStructureFamily 𝕝 𝕜 e.symm (birkhoffJamesOrthogonal_symm_equiv 𝕜 𝕝 e h) J.property⟩`Fixed source	The underlying point map is . Its inverse sends to ; the image under the inverse bijection in the code is this same preimage. The cited geometric-point transport result supplies membership in the target family.
Homeomorphism fields`structure Homeomorph (c : ClosureSpace α) (d : ClosureSpace β) extends α ≃ β where continuous_toFun : c.Continuous d toFun continuous_invFun : d.Continuous c invFun`Fixed source	The bundle contains one bijection and continuity of that map and its inverse. Applied here, the two conditions are $\Phi_e(c_E(\mathscr A))\subseteq c_F(\Phi_e(\mathscr A)),$ $\Phi_e^{-1}(c_F(\mathscr B))\subseteq c_E(\Phi_e^{-1}(\mathscr B))$ for every and .
Closure continuity`def Continuous (c : ClosureSpace α) (d : ClosureSpace β) (f : α → β) : Prop := ∀ s : Set α, f '' c.closure s ⊆ d.closure (f '' s)`Fixed source	Continuity of a map means $r(c_Y(E))\subseteq c_Z(r(E))\qquad(E\subseteq Y).$ In the preceding row this is used first for , then for its same inverse.

Exact surrounding source context (separate excerpts)

The surrounding declarations below are from the ambient source declarations; their mathematical meaning is included in the guide above.

variable (𝕜 : Type v) (𝕝 : Type z) [RCLike 𝕜] [RCLike 𝕝]
variable {E : Type u} {F : Type w}
variable [NormedAddCommGroup E] [NormedSpace 𝕜 E]
variable [NormedAddCommGroup F] [NormedSpace 𝕝 F]
variable (e : E ≃ F)
variable (h : ∀ x y : E, BirkhoffJamesOrthogonal 𝕝 (e x) (e y) ↔
  BirkhoffJamesOrthogonal 𝕜 x y)
include h

Back to the reading-guide item

Read exact source with highlighted declaration · Raw UTF-8 source · LFH Companion ·

Technical documentation