Peirce projections in alternative algebras

Let c be an idempotent in a unital alternative algebra and put c₀ = c and c₁ = 1 - c. This file constructs the four Peirce projections

x ↦ (cᵢ * x) * cⱼ.

The projections are complete, idempotent, and pairwise orthogonal. This is the linear-algebraic core of the singular Peirce decomposition [GPR, Exc. 14.12]. The range of the (i, j) projection is the Peirce component Aᵢⱼ.

Main definitions

• IsAlternative.peirceIdempotent: the complementary idempotents c and 1 - c.
• IsAlternative.peirceProjection: the four Peirce projections.
• IsAlternative.peirceComponent: their ranges.

Main results

• IsAlternative.peirceProjection_idem: each Peirce projection is idempotent.
• IsAlternative.peirceProjection_comp_eq_zero: distinct Peirce projections are orthogonal.
• IsAlternative.sum_peirceProjection_apply: the four projections sum to the identity.
• IsAlternative.mul_mem_peirceComponent_of_opposite: opposite off-diagonal components multiply into a diagonal component.
• IsAlternative.mul_mem_peirceComponent_swap: one off-diagonal component squares into the opposite component.
• IsAlternative.finite_peirceComponent, IsAlternative.projective_peirceComponent: Peirce components inherit finite projectivity from the ambient module.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, Exc. 14.12.

def IsAlternative.peirceIdempotent {A : Type v} [NonAssocRing A] (c : A) : Bool → A

The two complementary idempotents attached to c, indexed by Bool. The index false denotes c, and true denotes 1 - c.

Equations

• IsAlternative.peirceIdempotent c false = c
• IsAlternative.peirceIdempotent c true = 1 - c

@[simp]

theorem IsAlternative.peirceIdempotent_false {A : Type v} [NonAssocRing A] (c : A) : peirceIdempotent c false = c

@[simp]

theorem IsAlternative.peirceIdempotent_true {A : Type v} [NonAssocRing A] (c : A) : peirceIdempotent c true = 1 - c

theorem IsAlternative.peirceIdempotent_mul_self {A : Type v} [NonAssocRing A] {c : A} (hc : c * c = c) (i : Bool) : peirceIdempotent c i * peirceIdempotent c i = peirceIdempotent c i

Both elements of the complementary pair attached to an idempotent are idempotent.

theorem IsAlternative.peirceIdempotent_mul_eq_zero {A : Type v} [NonAssocRing A] {c : A} (hc : c * c = c) {i j : Bool} (hij : i ≠ j) : peirceIdempotent c i * peirceIdempotent c j = 0

Distinct elements of the complementary pair multiply to zero.

def IsAlternative.peirceLeftProjection {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] (c : A) (i : Bool) : A →ₗ[R] A

Multiplication on the left by one of the two complementary idempotents.

Equations

• IsAlternative.peirceLeftProjection c i = LinearMap.mulLeft R (IsAlternative.peirceIdempotent c i)

def IsAlternative.peirceRightProjection {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [IsScalarTower R A A] (c : A) (j : Bool) : A →ₗ[R] A

Multiplication on the right by one of the two complementary idempotents.

Equations

• IsAlternative.peirceRightProjection c j = LinearMap.mulRight R (IsAlternative.peirceIdempotent c j)

def IsAlternative.peirceProjection {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (c : A) (i j : Bool) : A →ₗ[R] A

The (i, j) Peirce projection x ↦ (cᵢ * x) * cⱼ.

Equations

• IsAlternative.peirceProjection c i j = IsAlternative.peirceRightProjection c j ∘ₗ IsAlternative.peirceLeftProjection c i

@[simp]

theorem IsAlternative.peirceLeftProjection_apply {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] (c x : A) (i : Bool) : (peirceLeftProjection c i) x = peirceIdempotent c i * x

@[simp]

theorem IsAlternative.peirceRightProjection_apply {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [IsScalarTower R A A] (c x : A) (j : Bool) : (peirceRightProjection c j) x = x * peirceIdempotent c j

@[simp]

theorem IsAlternative.peirceProjection_apply {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (c x : A) (i j : Bool) : (peirceProjection c i j) x = peirceIdempotent c i * x * peirceIdempotent c j

theorem IsAlternative.peirce_associate {A : Type v} [NonAssocRing A] [IsAlternative A] (c x : A) (i j : Bool) : peirceIdempotent c i * x * peirceIdempotent c j = peirceIdempotent c i * (x * peirceIdempotent c j)

The two complementary idempotents associate across an arbitrary middle element. This is the flexible law, expanded linearly when either idempotent is 1 - c.

theorem IsAlternative.peirce_left_associate {A : Type v} [NonAssocRing A] [IsAlternative A] (c x : A) (i j : Bool) : peirceIdempotent c i * (peirceIdempotent c j * x) = peirceIdempotent c i * peirceIdempotent c j * x

Two complementary left multiplications associate.

theorem IsAlternative.peirce_right_associate {A : Type v} [NonAssocRing A] [IsAlternative A] (c x : A) (i j : Bool) : x * peirceIdempotent c i * peirceIdempotent c j = x * (peirceIdempotent c i * peirceIdempotent c j)

Two complementary right multiplications associate.

theorem IsAlternative.peirceProjection_idem {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsAlternative A] {c : A} (hc : c * c = c) (i j : Bool) : peirceProjection c i j ∘ₗ peirceProjection c i j = peirceProjection c i j

Each Peirce projection is idempotent.

theorem IsAlternative.peirceProjection_comp_eq_zero_of_left {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsAlternative A] {c : A} (hc : c * c = c) {i j k l : Bool} (hik : i ≠ k) : peirceProjection c i j ∘ₗ peirceProjection c k l = 0

Peirce projections with distinct left indices have zero composite.

theorem IsAlternative.peirceProjection_comp_eq_zero_of_right {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsAlternative A] {c : A} (hc : c * c = c) {i j k l : Bool} (hjl : j ≠ l) : peirceProjection c i j ∘ₗ peirceProjection c k l = 0

Peirce projections with distinct right indices have zero composite.

theorem IsAlternative.peirceProjection_comp_eq_zero {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsAlternative A] {c : A} (hc : c * c = c) {i j k l : Bool} (h : (i, j) ≠ (k, l)) : peirceProjection c i j ∘ₗ peirceProjection c k l = 0

Distinct Peirce projections are pairwise orthogonal.

theorem IsAlternative.sum_peirceProjection_apply {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (c x : A) : (peirceProjection c false false) x + (peirceProjection c false true) x + (peirceProjection c true false) x + (peirceProjection c true true) x = x

The four Peirce projections decompose every element.

def IsAlternative.peirceComponent {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (c : A) (i j : Bool) : Submodule R A

The (i, j) Peirce component is the range of the corresponding projection.

Equations

• IsAlternative.peirceComponent c i j = (IsAlternative.peirceProjection c i j).range

theorem IsAlternative.mem_peirceComponent_iff {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsAlternative A] {c : A} (hc : c * c = c) {x : A} (i j : Bool) : x ∈ peirceComponent c i j ↔ (peirceProjection c i j) x = x

An element belongs to a Peirce component exactly when its projection is itself.

theorem IsAlternative.mem_peirceComponent_iff_mul_eq {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsAlternative A] {c : A} (hc : c * c = c) {x : A} (i j : Bool) : x ∈ peirceComponent c i j ↔ peirceIdempotent c i * x = x ∧ x * peirceIdempotent c j = x

The intrinsic characterization of a Peirce component: x lies in Aᵢⱼ exactly when cᵢ * x = x = x * cⱼ [GPR, Exc. 14.12].

theorem IsAlternative.peirceIdempotent_mem_peirceComponent {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsAlternative A] {c : A} (hc : c * c = c) (i : Bool) : peirceIdempotent c i ∈ peirceComponent c i i

Each complementary idempotent belongs to its diagonal Peirce component.

theorem IsAlternative.peirceIdempotent_mul_of_mem {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsAlternative A] {c : A} (hc : c * c = c) {x : A} {k l : Bool} (hx : x ∈ peirceComponent c k l) (i : Bool) : peirceIdempotent c i * x = if i = k then x else 0

A complementary idempotent acts on the left of a Peirce component by either the identity or zero, according to its left index.

theorem IsAlternative.mul_peirceIdempotent_of_mem {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsAlternative A] {c : A} (hc : c * c = c) {x : A} {k l : Bool} (hx : x ∈ peirceComponent c k l) (j : Bool) : x * peirceIdempotent c j = if j = l then x else 0

A complementary idempotent acts on the right of a Peirce component by either the identity or zero, according to its right index.

theorem IsAlternative.mul_mem_peirceComponent_of_opposite {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsAlternative A] {c : A} (hc : c * c = c) {x y : A} {i j : Bool} (hij : i ≠ j) (hx : x ∈ peirceComponent c i j) (hy : y ∈ peirceComponent c j i) : x * y ∈ peirceComponent c i i

Opposite off-diagonal Peirce components multiply into the corresponding diagonal component: Aᵢⱼ Aⱼᵢ ⊆ Aᵢᵢ for i ≠ j [GPR, Exc. 14.12].

theorem IsAlternative.mul_mem_peirceComponent_swap {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsAlternative A] {c : A} (hc : c * c = c) {x y : A} {i j : Bool} (hij : i ≠ j) (hx : x ∈ peirceComponent c i j) (hy : y ∈ peirceComponent c i j) : x * y ∈ peirceComponent c j i

Multiplying two elements of one off-diagonal Peirce component lands in the opposite component: Aᵢⱼ Aᵢⱼ ⊆ Aⱼᵢ for i ≠ j [GPR, Exc. 14.12].

theorem IsAlternative.peirceProjection_apply_of_mem {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsAlternative A] {c : A} (hc : c * c = c) {i j k l : Bool} (x : ↥(peirceComponent c k l)) : (peirceProjection c i j) ↑x = ↑(if (i, j) = (k, l) then x else 0)

A Peirce projection acts as the identity on its component and as zero on every other component.

def IsAlternative.peirceDecompose {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (c : A) : A →ₗ[R] (p : Bool × Bool) → ↥(peirceComponent c p.1 p.2)

The map sending an element to its four Peirce components.

Equations

• IsAlternative.peirceDecompose c = { toFun := fun (x : A) (p : Bool × Bool) => ⟨(IsAlternative.peirceProjection c p.1 p.2) x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

def IsAlternative.peirceRecombine {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (c : A) : ((p : Bool × Bool) → ↥(peirceComponent c p.1 p.2)) →ₗ[R] A

Sum the four coordinates in a family of Peirce components.

Equations

• IsAlternative.peirceRecombine c = { toFun := fun (x : (p : Bool × Bool) → ↥(IsAlternative.peirceComponent c p.1 p.2)) => ∑ p : Bool × Bool, ↑(x p), map_add' := ⋯, map_smul' := ⋯ }

theorem IsAlternative.peirceRecombine_decompose {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {c : A} (x : A) : (peirceRecombine c) ((peirceDecompose c) x) = x

Recombining the Peirce coordinates of an element returns that element.

theorem IsAlternative.peirceDecompose_recombine {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsAlternative A] {c : A} (hc : c * c = c) (x : (p : Bool × Bool) → ↥(peirceComponent c p.1 p.2)) : (peirceDecompose c) ((peirceRecombine c) x) = x

Decomposing a sum of Peirce coordinates returns the original coordinates.

def IsAlternative.peirceDecomposition {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsAlternative A] {c : A} (hc : c * c = c) : A ≃ₗ[R] (p : Bool × Bool) → ↥(peirceComponent c p.1 p.2)

The singular Peirce decomposition of an alternative algebra [GPR, Exc. 14.12].

Equations

• IsAlternative.peirceDecomposition hc = { toLinearMap := IsAlternative.peirceDecompose c, invFun := ⇑(IsAlternative.peirceRecombine c), left_inv := ⋯, right_inv := ⋯ }

theorem IsAlternative.finite_peirceComponent {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [Module.Finite R A] {c : A} (i j : Bool) : Module.Finite R ↥(peirceComponent c i j)

A Peirce component is finite when the ambient module is finite: it is the image of a projection.

theorem IsAlternative.projective_peirceComponent {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsAlternative A] [Module.Projective R A] {c : A} (hc : c * c = c) (i j : Bool) : Module.Projective R ↥(peirceComponent c i j)

A Peirce component is projective when the ambient module is projective: its projection splits the inclusion.