The spectrum survives complexification

For a real Hilbert space E, complexify : (E →L[ℝ] E) → (Eℂ →L[ℂ] Eℂ) is an injective unital ⋆-algebra map (complexifyStarAlgHom). This file proves that it also reflects invertibility, and deduces that it preserves the real spectrum on the nose:

• isUnit_complexify_iff : IsUnit (complexify T) ↔ IsUnit T;
• spectrum_complexify : spectrum ℝ (complexify T) = spectrum ℝ T;
• mem_spectrum_complexify_iff : the real points of the complex spectrum.

The two halves of the first statement are asymmetric:

• forward is formal — a unital ring map carries units to units;
• backward is the content — an inverse of complexify T must be shown to come from a real operator, and realify is that operator. The proof does not need the usual "the inverse of a conjugation-fixed operator is conjugation-fixed" argument: evaluating both unit equations at ofReal x and taking real parts gives the two real identities directly.

Which real algebra structure

spectrum ℝ on Eℂ →L[ℂ] Eℂ is taken with respect to the scoped complexOperatorRealAlgebra (Algebra.complexToReal), the one the real continuous functional calculus of Complexification/FunctionalCalculus.lean is registered against. A globally available second real structure, ContinuousLinearMap.algebra, exists on the same type and is only propositionally equal to it, so a consumer of spectrum_complexify must have this namespace's scope open. See algebraMap_complexOperator.

Provenance

The mathematics is moved, not restated, from TauCeti.DavisKahan.Experimental.Foundation. RealComplexification in DavisKahan/SpectralTheory/Complexification/Spectrum.lean, which depended on nothing in the paper library and is where this argument was first proved. That module still carries its own copies in its own namespace; re-grounding it on these is separate, mechanical work. A third copy, in DavisKahan/Experimental/MathAhead/ HiddenFoundations/RealSylvesterDescent.lean, was deleted with that staging file on 2026-08-27.

theorem TauCeti.RealComplexification.isUnit_complexify_of_isUnit {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {T : E →L[ℝ] E} (h : IsUnit T) : IsUnit (complexify T)

Complexification is a unital ring map, so it carries units to units.

theorem TauCeti.RealComplexification.isUnit_of_isUnit_complexify {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {T : E →L[ℝ] E} (h : IsUnit (complexify T)) : IsUnit T

Complexification reflects invertibility.

The inverse of complexify T restricts to an inverse of T: realify of it works on both sides, because evaluating each unit equation at ofReal x and taking real parts gives exactly the two real identities.

theorem TauCeti.RealComplexification.isUnit_complexify_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {T : E →L[ℝ] E} : IsUnit (complexify T) ↔ IsUnit T

Invertibility is preserved and reflected by complexification.

theorem TauCeti.RealComplexification.mem_spectrum_complexify_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : E →L[ℝ] E) (r : ℝ) : ↑r ∈ spectrum ℂ (complexify T) ↔ r ∈ spectrum ℝ T

The real points of the complex spectrum survive complexification.

theorem TauCeti.RealComplexification.spectrum_complexify {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : E →L[ℝ] E) : spectrum ℝ (complexify T) = spectrum ℝ T

The real spectrum survives complexification, as an equality of subsets of ℝ.

This is the statement that lets the real continuous functional calculus of the complexified algebra be read as a calculus for the real operator: the two symbol algebras C(spectrum ℝ T, ℝ) and C(spectrum ℝ (complexify T), ℝ) are the same object.