The joint eigenspaces of two commuting involutions

For two commuting involutions P₀, P₁ of a finite-dimensional space over a field of characteristic zero and signs ε₀, ε₁ = ±1, the operator ¼ (1 + ε₀P₀)(1 + ε₁P₁) is a projection onto the joint eigenspace {P₀ = ε₀, P₁ = ε₁}, so its trace is the dimension of that space: dim = ¼ [dim V + ε₀ tr P₀ + ε₁ tr P₁ + ε₀ε₁ tr (P₀P₁)] (the parity count of Proposition 3 of «What the Higgs Potential Cannot See»).

Main results

• LinearMap.isProj_jointProj: ¼ (1 + ε₀P₀)(1 + ε₁P₁) projects onto the joint eigenspace.
• LinearMap.finrank_joint_eigenspace: the dimension formula.

References

• C. Marín, What the Higgs Potential Cannot See: Bulk Matter That Cannot Help Select a Boundary Condition (Part V), Zenodo (2026), doi:10.5281/zenodo.21727095, Proposition prop:three.

noncomputable def LinearMap.jointProj {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (P₀ P₁ : V →ₗ[K] V) (ε₀ ε₁ : K) : V →ₗ[K] V

The projector ¼ (1 + ε₀P₀)(1 + ε₁P₁) onto the joint eigenspace {P₀ = ε₀, P₁ = ε₁} of two commuting involutions (ε₀, ε₁ = ±1).

Equations

• P₀.jointProj P₁ ε₀ ε₁ = 4⁻¹ • ((1 + ε₀ • P₀) * (1 + ε₁ • P₁))

theorem LinearMap.isProj_jointProj {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [CharZero K] (P₀ P₁ : V →ₗ[K] V) (h₀ : P₀ * P₀ = 1) (h₁ : P₁ * P₁ = 1) (hc : P₀ * P₁ = P₁ * P₀) {ε₀ ε₁ : K} (hε₀ : ε₀ = 1 ∨ ε₀ = -1) (hε₁ : ε₁ = 1 ∨ ε₁ = -1) : IsProj ((P₀ - ε₀ • 1).ker ⊓ (P₁ - ε₁ • 1).ker) (P₀.jointProj P₁ ε₀ ε₁)

theorem LinearMap.finrank_joint_eigenspace {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [CharZero K] [FiniteDimensional K V] (P₀ P₁ : V →ₗ[K] V) (h₀ : P₀ * P₀ = 1) (h₁ : P₁ * P₁ = 1) (hc : P₀ * P₁ = P₁ * P₀) {ε₀ ε₁ : K} (hε₀ : ε₀ = 1 ∨ ε₀ = -1) (hε₁ : ε₁ = 1 ∨ ε₁ = -1) : ↑(Module.finrank K ↥((P₀ - ε₀ • 1).ker ⊓ (P₁ - ε₁ • 1).ker)) = (↑(Module.finrank K V) + ε₀ * (trace K V) P₀ + ε₁ * (trace K V) P₁ + ε₀ * ε₁ * (trace K V) (P₀ * P₁)) / 4

Proposition 3 of ghu-higgs-cannot-see, in general form: for two commuting involutions P₀, P₁ of a finite-dimensional space over a field of characteristic zero and signs ε₀, ε₁ = ±1, the joint eigenspace {P₀ = ε₀, P₁ = ε₁} has dimension ¼ [dim + ε₀ tr P₀ + ε₁ tr P₁ + ε₀ε₁ tr (P₀P₁)].