The Kalton--Peck rank-parity obstruction

This file exposes the project-level definitions and the main rank-parity and hyperplane obstruction theorems.

@[reducible, inline]

abbrev KaltonPeck.StrongSymplecticForm (X : Type u_1) [NormedAddCommGroup X] [NormedSpace ℝ X] : Type u_1

A strong continuous alternating form on a real normed space.

Equations

• KaltonPeck.StrongSymplecticForm X = KaltonPeck.Support.StrongSymplecticForm X

@[reducible, inline]

abbrev KaltonPeck.StrongSymplecticForm.toDual {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (ω : StrongSymplecticForm X) : X ≃L[ℝ] StrongDual ℝ X

The continuous linear equivalence induced by the strong symplectic form.

Equations

• ω.toDual = ω.toDual

@[reducible, inline]

abbrev KaltonPeck.StrongSymplecticForm.alternating {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (ω : StrongSymplecticForm X) (x : X) : (ω.toDual x) x = 0

The form vanishes on the diagonal.

Equations

• ⋯ = ⋯

@[reducible, inline]

noncomputable abbrev KaltonPeck.transpose {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : X →L[ℝ] Y) : StrongDual ℝ Y →L[ℝ] StrongDual ℝ X

The transpose of a bounded linear map between real normed spaces.

Equations

• KaltonPeck.transpose T = KaltonPeck.Support.transpose T

@[reducible, inline]

noncomputable abbrev KaltonPeck.StrongSymplecticForm.adjoint {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (ω : StrongSymplecticForm X) (T : X →L[ℝ] X) : X →L[ℝ] X

The adjoint of a bounded operator with respect to a strong symplectic form.

Equations

• ω.adjoint T = KaltonPeck.Support.StrongSymplecticForm.adjoint ω T

@[reducible, inline]

abbrev KaltonPeck.IsFredholm {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : X →L[ℝ] Y) : Prop

A bounded linear map is Fredholm when it has finite-dimensional kernel, closed range, and finite-dimensional cokernel.

Equations

• KaltonPeck.IsFredholm T = KaltonPeck.Support.IsFredholm T

@[reducible, inline]

abbrev KaltonPeck.HasFiniteRank {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : X →L[ℝ] Y) : Prop

A bounded linear map has finite rank when its algebraic range is finite-dimensional.

Equations

• KaltonPeck.HasFiniteRank T = KaltonPeck.Support.HasFiniteRank T

@[reducible, inline]

noncomputable abbrev KaltonPeck.operatorRank {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : X →L[ℝ] Y) : ℕ

The rank of a bounded linear map, used when its range is finite-dimensional.

Equations

• KaltonPeck.operatorRank T = KaltonPeck.Support.operatorRank T

@[reducible, inline]

noncomputable abbrev KaltonPeck.nullity {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : X →L[ℝ] Y) : ℕ

The dimension of the kernel of a bounded linear map, used when the kernel is finite-dimensional.

Equations

• KaltonPeck.nullity T = KaltonPeck.Support.nullity T

@[reducible, inline]

abbrev KaltonPeck.IsComplexStructure {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (J : X →L[ℝ] X) : Prop

A complex structure on a real normed space is a bounded operator squaring to -I.

Equations

• KaltonPeck.IsComplexStructure J = KaltonPeck.Support.IsComplexStructure J

@[reducible, inline]

abbrev KaltonPeck.IsHyperplane {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (H : Submodule ℝ X) : Prop

A closed codimension-one linear subspace.

Equations

• KaltonPeck.IsHyperplane H = KaltonPeck.Support.IsHyperplane H

@[reducible, inline]

abbrev KaltonPeck.IsSquareSummable (x : ℕ → ℝ) : Prop

A real sequence is square-summable.

Equations

• KaltonPeck.IsSquareSummable x = KaltonPeck.Support.IsSquareSummable x

@[reducible, inline]

noncomputable abbrev KaltonPeck.l2Norm (x : ℕ → ℝ) : ℝ

The usual ℓ₂ norm, defined on all real sequences and used on square-summable ones.

Equations

• KaltonPeck.l2Norm x = KaltonPeck.Support.l2Norm x

@[reducible, inline]

noncomputable abbrev KaltonPeck.centralizer (x : ℕ → ℝ) (n : ℕ) : ℝ

The Kalton--Peck centralizer, with Lean's Real.log 0 = 0 supplying the zero convention.

Equations

• KaltonPeck.centralizer x n = KaltonPeck.Support.centralizer x n

@[reducible, inline]

abbrev KaltonPeck.IsAdmissiblePair (p : (ℕ → ℝ) × (ℕ → ℝ)) : Prop

The admissible coordinate pairs in the usual real Kalton--Peck presentation.

Equations

• KaltonPeck.IsAdmissiblePair p = KaltonPeck.Support.IsAdmissiblePair p

@[reducible, inline]

noncomputable abbrev KaltonPeck.kaltonPeckQuasiNorm (p : (ℕ → ℝ) × (ℕ → ℝ)) : ℝ

The standard quasi-norm used to present the real Kalton--Peck space.

Equations

• KaltonPeck.kaltonPeckQuasiNorm p = KaltonPeck.Support.kaltonPeckQuasiNorm p

@[reducible, inline]

abbrev KaltonPeck.RealKaltonPeckPresentation (X : Type u_1) [NormedAddCommGroup X] [NormedSpace ℝ X] : Type u_1

A real Banach space carrying the standard Kalton--Peck coordinate presentation.

Equations

• KaltonPeck.RealKaltonPeckPresentation X = KaltonPeck.Support.RealKaltonPeckPresentation X

@[reducible, inline]

abbrev KaltonPeck.RealKaltonPeckPresentation.coordinates {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : RealKaltonPeckPresentation X) : X →ₗ[ℝ] (ℕ → ℝ) × (ℕ → ℝ)

Linear coordinates identifying the space with the admissible Kalton--Peck pairs.

Equations

• p.coordinates = p.coordinates

theorem KaltonPeck.RealKaltonPeckPresentation.coordinates_injective {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : RealKaltonPeckPresentation X) : Function.Injective ⇑p.coordinates

The coordinate map is injective.

theorem KaltonPeck.RealKaltonPeckPresentation.coordinates_mem {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : RealKaltonPeckPresentation X) (z : X) : IsAdmissiblePair (p.coordinates z)

Every coordinate pair is admissible.

theorem KaltonPeck.RealKaltonPeckPresentation.coordinates_surjective {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : RealKaltonPeckPresentation X) (q : (ℕ → ℝ) × (ℕ → ℝ)) : IsAdmissiblePair q → ∃ (z : X), p.coordinates z = q

Every admissible coordinate pair is represented by a vector.

theorem KaltonPeck.RealKaltonPeckPresentation.norm_equivalent {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : RealKaltonPeckPresentation X) : ∃ (c : ℝ) (C : ℝ), 0 < c ∧ 0 < C ∧ ∀ (z : X), c * kaltonPeckQuasiNorm (p.coordinates z) ≤ ‖z‖ ∧ ‖z‖ ≤ C * kaltonPeckQuasiNorm (p.coordinates z)

The coordinate quasi-norm and the norm of the space are equivalent.

theorem KaltonPeck.rankParityGeneral {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (ω : StrongSymplecticForm X) (T : X →L[ℝ] X) (hFredholm : IsFredholm (1 + ω.adjoint T * T)) (hFiniteRank : HasFiniteRank (T ^ 2 + 1)) : operatorRank (T ^ 2 + 1) ≡ nullity (1 + ω.adjoint T * T) [MOD 2]

theorem KaltonPeck.rankParityZ2 {Z₂ : Type u_1} [NormedAddCommGroup Z₂] [NormedSpace ℝ Z₂] [CompleteSpace Z₂] (_hZ₂ : RealKaltonPeckPresentation Z₂) (T : Z₂ →L[ℝ] Z₂) (hFiniteRank : HasFiniteRank (T ^ 2 + 1)) : Even (operatorRank (T ^ 2 + 1))

theorem KaltonPeck.noHyperplaneComplexStructure {Z₂ : Type u_1} [NormedAddCommGroup Z₂] [NormedSpace ℝ Z₂] [CompleteSpace Z₂] (_hZ₂ : RealKaltonPeckPresentation Z₂) (H : Submodule ℝ Z₂) : IsHyperplane H → ¬∃ (J : ↥H →L[ℝ] ↥H), IsComplexStructure J