Projections onto invariant subspaces

theorem Orthogonalization.Blocks.starProjection_commute_of_invariant' {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (W : Submodule ℂ E) [W.HasOrthogonalProjection] {x : E →L[ℂ] E} (hx : ∀ v ∈ W, x v ∈ W) (hx' : ∀ v ∈ W, (star x) v ∈ W) : Commute x W.starProjection

The projection onto a subspace invariant under a *-closed set of operators commutes with them (general form, for any subspace admitting an orthogonal projection).

theorem Orthogonalization.Blocks.starProjection_commute_of_invariant {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (W : Submodule ℂ E) {x : E →L[ℂ] E} (hx : ∀ v ∈ W, x v ∈ W) (hx' : ∀ v ∈ W, (star x) v ∈ W) : Commute x W.starProjection

The projection onto a subspace invariant under a *-closed set of operators commutes with them.

Amplification x ↦ x ⊕ ⋯ ⊕ x on the block space L^ι

noncomputable def Orthogonalization.Blocks.ampl {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] (ι : Type u_2) [Fintype ι] [DecidableEq ι] (x : L →L[ℂ] L) : FinDim.BlockSpace L ι →L[ℂ] FinDim.BlockSpace L ι

The amplification x ⊕ ⋯ ⊕ x of an operator x on L to L^ι.

Equations

• Orthogonalization.Blocks.ampl ι x = Orthogonalization.FinDim.blockProj fun (x_1 : ι) => x

theorem Orthogonalization.Blocks.ampl_apply_coord {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (x : L →L[ℂ] L) (w : FinDim.BlockSpace L ι) (j : ι) : ((ampl ι x) w).ofLp j = x (w.ofLp j)

theorem Orthogonalization.Blocks.proj_ampl {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (x : L →L[ℂ] L) (k : ι) (w : FinDim.BlockSpace L ι) : (FinDim.proj k) ((ampl ι x) w) = x ((FinDim.proj k) w)

theorem Orthogonalization.Blocks.ampl_embed {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (x : L →L[ℂ] L) (k : ι) (v : L) : (ampl ι x) ((FinDim.embed k) v) = (FinDim.embed k) (x v)

theorem Orthogonalization.Blocks.ampl_mul {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (x y : L →L[ℂ] L) : ampl ι (x * y) = ampl ι x * ampl ι y

theorem Orthogonalization.Blocks.ampl_one {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] {ι : Type u_2} [Fintype ι] [DecidableEq ι] : ampl ι 1 = 1

theorem Orthogonalization.Blocks.ampl_add {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (x y : L →L[ℂ] L) : ampl ι (x + y) = ampl ι x + ampl ι y

theorem Orthogonalization.Blocks.ampl_smul {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (c : ℂ) (x : L →L[ℂ] L) : ampl ι (c • x) = c • ampl ι x

theorem Orthogonalization.Blocks.ampl_star {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (x : L →L[ℂ] L) : ampl ι (star x) = star (ampl ι x)

noncomputable def Orthogonalization.Blocks.amplAt {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (ξ : FinDim.BlockSpace L ι) : (L →L[ℂ] L) →ₗ[ℂ] FinDim.BlockSpace L ι

x ↦ ampl ι x ξ, as a linear map.

Equations

• Orthogonalization.Blocks.amplAt ξ = { toFun := fun (x : L →L[ℂ] L) => (Orthogonalization.Blocks.ampl ι x) ξ, map_add' := ⋯, map_smul' := ⋯ }

theorem Orthogonalization.Blocks.amplAt_apply {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (ξ : FinDim.BlockSpace L ι) (x : L →L[ℂ] L) : (amplAt ξ) x = (ampl ι x) ξ

Blocks of an operator on L^ι

noncomputable def Orthogonalization.Blocks.blockEntry {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] {ι : Type u_2} [DecidableEq ι] (X : FinDim.BlockSpace L ι →L[ℂ] FinDim.BlockSpace L ι) (k l : ι) : L →L[ℂ] L

The (k, l) block proj k ∘ X ∘ embed l of an operator X on L^ι.

Equations

• Orthogonalization.Blocks.blockEntry X k l = Orthogonalization.FinDim.proj k ∘SL X ∘SL Orthogonalization.FinDim.embed l

theorem Orthogonalization.Blocks.blockEntry_apply {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] {ι : Type u_2} [DecidableEq ι] (X : FinDim.BlockSpace L ι →L[ℂ] FinDim.BlockSpace L ι) (k l : ι) (v : L) : (blockEntry X k l) v = (FinDim.proj k) (X ((FinDim.embed l) v))

theorem Orthogonalization.Blocks.apply_coord_eq_sum_blockEntry {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (X : FinDim.BlockSpace L ι →L[ℂ] FinDim.BlockSpace L ι) (w : FinDim.BlockSpace L ι) (k : ι) : (X w).ofLp k = ∑ l : ι, (blockEntry X k l) (w.ofLp l)

Coordinate k of X w is ∑ l, X_{kl} (w l).

theorem Orthogonalization.Blocks.blockEntry_mem_centralizer {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {s : Set (L →L[ℂ] L)} {X : FinDim.BlockSpace L ι →L[ℂ] FinDim.BlockSpace L ι} (hX : ∀ y ∈ s, Commute (ampl ι y) X) (k l : ι) : blockEntry X k l ∈ s.centralizer

If X commutes with the amplification of every y ∈ s, its blocks lie in the centralizer of s.

theorem Orthogonalization.Blocks.commute_ampl_of_blockEntry {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {X : FinDim.BlockSpace L ι →L[ℂ] FinDim.BlockSpace L ι} {T : L →L[ℂ] L} (h : ∀ (k l : ι), Commute T (blockEntry X k l)) : Commute (ampl ι T) X

Conversely, an operator commuting with all the blocks of X has its amplification commuting with X.

The bicommutant theorem

theorem Orthogonalization.Blocks.mem_of_mem_centralizer_centralizer_aux {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (A : StarSubalgebra ℂ (L →L[ℂ] L)) (b : Module.Basis ι ℂ L) {T : L →L[ℂ] L} (hT : T ∈ (↑A).centralizer.centralizer) : T ∈ A

The bicommutant theorem, for an arbitrary finite basis b of L.

theorem Orthogonalization.Blocks.mem_of_mem_centralizer_centralizer {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] (A : StarSubalgebra ℂ (L →L[ℂ] L)) {T : L →L[ℂ] L} (hT : T ∈ (↑A).centralizer.centralizer) : T ∈ A

Bicommutant theorem (membership form): A'' ⊆ A for a unital *-subalgebra A of B(L), L finite-dimensional.

theorem Orthogonalization.Blocks.centralizer_centralizer_coe {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] (A : StarSubalgebra ℂ (L →L[ℂ] L)) : (↑A).centralizer.centralizer = ↑A

Bicommutant theorem: A'' = A for a unital *-subalgebra A of B(L), L finite-dimensional.

Schur's lemma

def Orthogonalization.Blocks.IsIrreducible {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] (A : StarSubalgebra ℂ (L →L[ℂ] L)) : Prop

A acts irreducibly on L: every A-invariant subspace is trivial.

Equations

• Orthogonalization.Blocks.IsIrreducible A = ∀ (W : Submodule ℂ L), (∀ x ∈ A, ∀ v ∈ W, x v ∈ W) → W = ⊥ ∨ W = ⊤

theorem Orthogonalization.Blocks.exists_hasEigenvalue {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] [Nontrivial L] (S : L →L[ℂ] L) : ∃ (c : ℂ), Module.End.HasEigenvalue (↑S) c

Every operator on a nontrivial finite-dimensional complex space has an eigenvalue.

theorem Orthogonalization.Blocks.star_mem_centralizer {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] (A : StarSubalgebra ℂ (L →L[ℂ] L)) {S : L →L[ℂ] L} (hS : S ∈ (↑A).centralizer) : star S ∈ (↑A).centralizer

The centralizer of a *-subalgebra is closed under star.

theorem Orthogonalization.Blocks.exists_eq_smul_one_of_mem_centralizer {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] (A : StarSubalgebra ℂ (L →L[ℂ] L)) (hA : IsIrreducible A) {S : L →L[ℂ] L} (hS : S ∈ (↑A).centralizer) : ∃ (c : ℂ), S = c • 1

Schur's lemma: the commutant of an irreducible *-subalgebra is ℂ·1.

Irreducible *-subalgebras are everything

theorem Orthogonalization.Blocks.mem_of_isIrreducible {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] (A : StarSubalgebra ℂ (L →L[ℂ] L)) (hA : IsIrreducible A) (T : L →L[ℂ] L) : T ∈ A

An irreducible *-subalgebra of B(L) contains every operator.

theorem Orthogonalization.Blocks.eq_top_of_isIrreducible {L : Type u_1} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [FiniteDimensional ℂ L] (A : StarSubalgebra ℂ (L →L[ℂ] L)) (hA : IsIrreducible A) : A = ⊤

An irreducible *-subalgebra of B(L) is all of B(L).