Closed hyperplane images force semilinear regularity

LinearEquiv.regularity_of_isClosed_image_hyperplane

theorem

Derives scalar regularity and bounded invertibility from closed images of closed hyperplanes.

Statement

Let be complex Banach spaces, with infinite-dimensional. Let be a field automorphism and an algebraic -semilinear equivalence: is bijective and

T(x+x')=Tx+Tx',\qquad T(cx)=\sigma(c)Tx. \tag{1}

Suppose that is closed in for every closed complex hyperplane . Then is the identity or complex conjugation. The same and its inverse are continuous, and there exist real constants such that

\|Tx\|\le C\|x\|\quad(x\in X),\qquad \|T^{-1}y\|\le D\|y\|\quad(y\in Y). \tag{2}

The scalar alternative and both continuity assertions hold together with this one pair of bounds.

Assumptions

Here a closed complex hyperplane is a closed complex-linear subspace of codimension one. The assumption requires its image under to be closed.

Both and are Banach spaces; only is required to be infinite dimensional. No separability, Hilbert-space structure, or initial continuity or boundedness of , , or is assumed.

Conclusion

The given semilinear equivalence is complex-linear or conjugate-linear and is boundedly invertible. The conclusion includes continuity of and and one pair of positive constants satisfying both estimates (2). It does not require those constants to be optimal or equal.

Main citations

The closed-hyperplane regularity theorem gives the scalar alternative, both continuity assertions and both bounds. In the same file, scalar continuity, continuity of the equivalence and its inverse, and positive norm bounds are stated separately.

Lean source signature (exact)

The declaration prefix below is a contiguous source excerpt, ending before its proof assignment.

theorem regularity_of_isClosed_image_hyperplane
    (T : LinearEquiv σ.toRingHom (σ' := σ.symm.toRingHom) X Y) (hX : ¬ FiniteDimensional ℂ X)
    (hclosed : ∀ M : Submodule ℂ X, IsCoatom M → IsClosed (M : Set X) →
      IsClosed (T '' (M : Set X))) :
    (σ = RingEquiv.refl ℂ ∨ σ = starRingAut (R := ℂ)) ∧
      Continuous T ∧ Continuous T.symm ∧
      ∃ C D : ℝ, 0 < C ∧ 0 < D ∧
        (∀ x, ‖T x‖ ≤ C * ‖x‖) ∧ (∀ y, ‖T.symm y‖ ≤ D * ‖y‖)

In the source	Mathematical meaning
Exact declaration`X`, `Y`, their normed-space instances, and `[CompleteSpace X] [CompleteSpace Y]`	The complex Banach spaces .
Exact declaration`{σ : ℂ ≃+* ℂ}`	A field automorphism , not assumed continuous.
Exact declaration`T : LinearEquiv σ.toRingHom (σ' := σ.symm.toRingHom) X Y`	The additive bijection with ; its inverse satisfies .
Exact declaration`hX : ¬ FiniteDimensional ℂ X`	.
Exact declaration`M : Submodule ℂ X`	A complex-linear subspace . This part alone does not require closedness.
Exact declaration`IsCoatom M`	: is a complex hyperplane.
Exact declaration`IsClosed (M : Set X)`	is closed in . Together with the preceding condition, this specifies a closed complex hyperplane.
Exact declaration`hclosed`, ending in `IsClosed (T '' (M : Set X))`	is closed in for every closed complex hyperplane .
Exact declaration`σ = RingEquiv.refl ℂ ∨ σ = starRingAut (R := ℂ)`	or for every .
Exact declaration`Continuous T ∧ Continuous T.symm`	Both and are norm-continuous.
Exact declaration`∃ C D : ℝ, 0 < C ∧ 0 < D ∧ ...`	There are such that for every , and for every , as in (2).
The two local Exact declaration`RingHomInvPair` instances	and ; no assumption is made.

The literal signature above is the declaration prefix through line 298, ending before the proof assignment. The full declaration occupies lines 291–302; the comment at 304–305 belongs to the next theorem. The ambient variables and completeness assumptions are quoted separately below.

Exact surrounding source context (separate excerpts)

Source lines 35–39:

universe u v
variable {X : Type u} {Y : Type v}
variable [NormedAddCommGroup X] [NormedSpace ℂ X]
variable [NormedAddCommGroup Y] [NormedSpace ℂ Y]
variable {σ : ℂ ≃+* ℂ}

Source lines 41–44:

local instance (σ : ℂ ≃+* ℂ) : RingHomInvPair σ.toRingHom σ.symm.toRingHom :=
  RingHomInvPair.of_ringEquiv σ
local instance (σ : ℂ ≃+* ℂ) : RingHomInvPair σ.symm.toRingHom σ.toRingHom :=
  RingHomInvPair.of_ringEquiv_symm σ

Source lines 237–237:

variable [CompleteSpace X] [CompleteSpace Y]

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

Technical documentation