Peirce decomposition at an elementary idempotent

This file specializes the singular Peirce decomposition [GPR, Exc. 14.12] to an elementary idempotent in a multiplicative conic alternative algebra. It proves [GPR, Exc. 19.35(1)--(6)]: the diagonal components, existence of Peirce coordinates, and the coordinate formulas for the norm, polar form, trace, and conjugation. Under regularity it also proves that the two off-diagonal components are in duality under the polar form, and it constructs the alternating trace trilinear form at the end of the exercise. GPR 19.11 supplies regularity for a constant-rank composition algebra of rank other than one.

Main results

• ConicAlgebra.IsElementaryIdempotent.eq_trace_smul_peirceIdempotent: an element of a diagonal Peirce component is its trace times the corresponding idempotent.
• ConicAlgebra.IsElementaryIdempotent.peirceComponent_same: Cᵢᵢ = k cᵢ.
• ConicAlgebra.IsElementaryIdempotent.norm_peirceElement: the norm formula (3).
• ConicAlgebra.IsElementaryIdempotent.polar_peirceElement: the polar formula (4).
• ConicAlgebra.IsElementaryIdempotent.trace_peirceElement: the trace formula (5).
• ConicAlgebra.IsElementaryIdempotent.conj_peirceElement: the conjugation formula (6).
• ConicAlgebra.IsElementaryIdempotent.mul_add_mul_eq_zero_of_mem_peirceComponent: multiplication within an off-diagonal component is alternating.
• ConicAlgebra.IsElementaryIdempotent.mul_eq_neg_polar_smul_peirceIdempotent: the product of opposite off-diagonal components.
• ConicAlgebra.IsElementaryIdempotent.offDiagonalDuality: the duality C₁₂ ≃ C₂₁* when the norm is regular.
• ConicAlgebra.IsElementaryIdempotent.isLocallyFreeRankOne_offDiagonal: in rank four the off-diagonal components are line bundles, the rank count in GPR 22.13.
• ConicAlgebra.IsElementaryIdempotent.mul_eq_zero_of_mem_offDiagonal_of_rankAtStalk_eq_four: multiplication within either off-diagonal component vanishes in rank four.
• ConicAlgebra.IsElementaryIdempotent.peirceTraceAlternating: the alternating form (x, y, z) ↦ t((xy)z) on either off-diagonal component.

The duality theorem is stated with the regularity it consumes; its composition-algebra corollary uses GPR 19.11 under a constant-rank hypothesis. The hyperbolic presentation assembled from these coordinates is in Composition/Reduced/Hyperbolic.lean, and the rank-four twisted-matrix classification is in Composition/Reduced/TwistedMatrix.lean.

References

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

theorem ConicAlgebra.IsElementaryIdempotent.peirceIdempotent {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (i : Bool) : C.IsElementaryIdempotent (IsAlternative.peirceIdempotent c i)

Each member of the complementary pair attached to an elementary idempotent is elementary.

theorem ConicAlgebra.IsElementaryIdempotent.eq_trace_smul_peirceIdempotent {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) {x : A} {i : Bool} (hx : x ∈ IsAlternative.peirceComponent c i i) : x = C.trace x • IsAlternative.peirceIdempotent c i

An element of a diagonal Peirce component is its trace times the corresponding elementary idempotent [GPR, Exc. 19.35(1)].

theorem ConicAlgebra.IsElementaryIdempotent.peirceComponent_same {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) (i : Bool) : IsAlternative.peirceComponent c i i = k ∙ IsAlternative.peirceIdempotent c i

The diagonal Peirce component Cᵢᵢ is the scalar line k cᵢ [GPR, Exc. 19.35(1)].

def ConicAlgebra.IsElementaryIdempotent.diagonalEquiv {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) (i : Bool) : k ≃ₗ[k] ↥(IsAlternative.peirceComponent c i i)

A diagonal Peirce component at an elementary idempotent is linearly equivalent to the base ring, by a ↦ a cᵢ; the inverse is the trace [GPR, Exc. 19.35(1)].

Equations

• One or more equations did not get rendered due to their size.

theorem ConicAlgebra.IsElementaryIdempotent.conj_peirceIdempotent {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (i : Bool) : C.conj (IsAlternative.peirceIdempotent c i) = IsAlternative.peirceIdempotent c !i

Conjugation exchanges the two complementary idempotents.

theorem ConicAlgebra.IsElementaryIdempotent.norm_eq_zero_of_mem_peirceComponent {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) {x : A} {i j : Bool} (hx : x ∈ IsAlternative.peirceComponent c i j) : C.norm x = 0

Every Peirce component is totally singular for the quadratic norm: each of its elements has norm zero.

theorem ConicAlgebra.IsElementaryIdempotent.polar_eq_zero_of_mem_peirceComponent_of_left_eq {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) {x y : A} {i j l : Bool} (hx : x ∈ IsAlternative.peirceComponent c i j) (hy : y ∈ IsAlternative.peirceComponent c i l) : QuadraticMap.polar (⇑C.norm) x y = 0

Peirce components with the same left index are mutually orthogonal for the polar form.

theorem ConicAlgebra.IsElementaryIdempotent.polar_eq_zero_of_mem_peirceComponent_of_right_eq {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) {x y : A} {i m j : Bool} (hx : x ∈ IsAlternative.peirceComponent c i j) (hy : y ∈ IsAlternative.peirceComponent c m j) : QuadraticMap.polar (⇑C.norm) x y = 0

Peirce components with the same right index are mutually orthogonal for the polar form.

theorem ConicAlgebra.IsElementaryIdempotent.trace_eq_zero_of_mem_peirceComponent {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) {x : A} {i j : Bool} (hij : i ≠ j) (hx : x ∈ IsAlternative.peirceComponent c i j) : C.trace x = 0

An off-diagonal Peirce component has trace zero.

theorem ConicAlgebra.IsElementaryIdempotent.mul_self_eq_zero_of_mem_peirceComponent {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) {x : A} {i j : Bool} (hij : i ≠ j) (hx : x ∈ IsAlternative.peirceComponent c i j) : x * x = 0

Every element of an off-diagonal Peirce component has square zero.

theorem ConicAlgebra.IsElementaryIdempotent.mul_add_mul_eq_zero_of_mem_peirceComponent {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) {x y : A} {i j : Bool} (hij : i ≠ j) (hx : x ∈ IsAlternative.peirceComponent c i j) (hy : y ∈ IsAlternative.peirceComponent c i j) : x * y + y * x = 0

Multiplication restricted to one off-diagonal Peirce component is alternating: x * y + y * x = 0 [GPR, Exc. 14.12]. This is the linearization of the square-zero rule and does not divide by 2.

theorem ConicAlgebra.IsElementaryIdempotent.mul_eq_neg_mul_of_mem_peirceComponent {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) {x y : A} {i j : Bool} (hij : i ≠ j) (hx : x ∈ IsAlternative.peirceComponent c i j) (hy : y ∈ IsAlternative.peirceComponent c i j) : x * y = -(y * x)

Products in one off-diagonal Peirce component anticommute [GPR, Exc. 14.12]. This formulation is valid in characteristic 2, where the negation may be invisible.

theorem ConicAlgebra.IsElementaryIdempotent.mul_eq_neg_polar_smul_peirceIdempotent {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) {x y : A} {i j : Bool} (hij : i ≠ j) (hx : x ∈ IsAlternative.peirceComponent c i j) (hy : y ∈ IsAlternative.peirceComponent c j i) : x * y = -QuadraticMap.polar (⇑C.norm) x y • IsAlternative.peirceIdempotent c i

The product of elements in opposite off-diagonal Peirce components is their negative polar pairing times the corresponding diagonal idempotent [GPR, Exc. 14.12, Exc. 19.35]: xy = -n(x, y)cᵢ for x ∈ Cᵢⱼ and y ∈ Cⱼᵢ.

theorem ConicAlgebra.IsElementaryIdempotent.trace_mul_mul_self_left {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) {i j : Bool} (hij : i ≠ j) (x y : ↥(IsAlternative.peirceComponent c i j)) : C.trace (↑x * ↑x * ↑y) = 0

The Peirce trace trilinear form vanishes when its first two arguments agree.

theorem ConicAlgebra.IsElementaryIdempotent.trace_mul_mul_self_right {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) {i j : Bool} (hij : i ≠ j) (x y : ↥(IsAlternative.peirceComponent c i j)) : C.trace (↑x * ↑y * ↑y) = 0

The Peirce trace trilinear form vanishes when its last two arguments agree.

theorem ConicAlgebra.IsElementaryIdempotent.trace_mul_mul_self_outer {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) {i j : Bool} (hij : i ≠ j) (x y : ↥(IsAlternative.peirceComponent c i j)) : C.trace (↑x * ↑y * ↑x) = 0

The Peirce trace trilinear form vanishes when its outside arguments agree.

def ConicAlgebra.IsElementaryIdempotent.peirceTraceTrilinear {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] (C : ConicAlgebra k A) (c : A) (i j : Bool) : MultilinearMap k (fun (x : Fin 3) => ↥(IsAlternative.peirceComponent c i j)) k

The trilinear form (x, y, z) ↦ t((xy)z) on a Peirce component.

Equations

• ConicAlgebra.IsElementaryIdempotent.peirceTraceTrilinear C c i j = MultilinearMap.mk' (fun (x : Fin 3 → ↥(IsAlternative.peirceComponent c i j)) => C.trace (↑(x 0) * ↑(x 1) * ↑(x 2))) ⋯ ⋯

@[simp]

theorem ConicAlgebra.IsElementaryIdempotent.peirceTraceTrilinear_apply {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] (C : ConicAlgebra k A) (c : A) (i j : Bool) (x : Fin 3 → ↥(IsAlternative.peirceComponent c i j)) : (peirceTraceTrilinear C c i j) x = C.trace (↑(x 0) * ↑(x 1) * ↑(x 2))

def ConicAlgebra.IsElementaryIdempotent.peirceTraceAlternating {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) {i j : Bool} (hij : i ≠ j) : ↥(IsAlternative.peirceComponent c i j) [⋀^Fin 3]→ₗ[k] k

The alternating trilinear form on an off-diagonal Peirce component at the end of [GPR, Exc. 19.35].

Equations

• hc.peirceTraceAlternating hmul hij = { toMultilinearMap := ConicAlgebra.IsElementaryIdempotent.peirceTraceTrilinear C c i j, map_eq_zero_of_eq' := ⋯ }

@[simp]

theorem ConicAlgebra.IsElementaryIdempotent.peirceTraceAlternating_apply {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) {i j : Bool} (hij : i ≠ j) (x : Fin 3 → ↥(IsAlternative.peirceComponent c i j)) : (hc.peirceTraceAlternating hmul hij) x = C.trace (↑(x 0) * ↑(x 1) * ↑(x 2))

def ConicAlgebra.IsElementaryIdempotent.peirceElement {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] (c : A) (a₁ a₂ : k) (x₁₂ : ↥(IsAlternative.peirceComponent c false true)) (x₂₁ : ↥(IsAlternative.peirceComponent c true false)) : A

The element with Peirce coordinates (a₁, x₁₂, x₂₁, a₂) relative to an elementary idempotent c; see [GPR, Exc. 19.35(2)].

Equations

• ConicAlgebra.IsElementaryIdempotent.peirceElement c a₁ a₂ x₁₂ x₂₁ = a₁ • IsAlternative.peirceIdempotent c false + ↑x₁₂ + ↑x₂₁ + a₂ • IsAlternative.peirceIdempotent c true

theorem ConicAlgebra.IsElementaryIdempotent.peirceProjection_peirceElement {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (a₁ a₂ : k) (x₁₂ : ↥(IsAlternative.peirceComponent c false true)) (x₂₁ : ↥(IsAlternative.peirceComponent c true false)) (i j : Bool) : (IsAlternative.peirceProjection c i j) (peirceElement c a₁ a₂ x₁₂ x₂₁) = if (i, j) = (false, false) then a₁ • IsAlternative.peirceIdempotent c false else if (i, j) = (false, true) then ↑x₁₂ else if (i, j) = (true, false) then ↑x₂₁ else a₂ • IsAlternative.peirceIdempotent c true

The four projections recover the corresponding Peirce coordinates.

theorem ConicAlgebra.IsElementaryIdempotent.exists_eq_peirceElement {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) (x : A) : ∃ (a₁ : k) (a₂ : k) (x₁₂ : ↥(IsAlternative.peirceComponent c false true)) (x₂₁ : ↥(IsAlternative.peirceComponent c true false)), x = peirceElement c a₁ a₂ x₁₂ x₂₁

Every element has Peirce coordinates as in [GPR, Exc. 19.35(2)].

theorem ConicAlgebra.IsElementaryIdempotent.norm_peirceElement {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) (a₁ a₂ : k) (x₁₂ : ↥(IsAlternative.peirceComponent c false true)) (x₂₁ : ↥(IsAlternative.peirceComponent c true false)) : C.norm (peirceElement c a₁ a₂ x₁₂ x₂₁) = a₁ * a₂ + QuadraticMap.polar ⇑C.norm ↑x₁₂ ↑x₂₁

The norm in Peirce coordinates [GPR, Exc. 19.35(3)].

theorem ConicAlgebra.IsElementaryIdempotent.polar_peirceElement {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) (a₁ a₂ b₁ b₂ : k) (x₁₂ y₁₂ : ↥(IsAlternative.peirceComponent c false true)) (x₂₁ y₂₁ : ↥(IsAlternative.peirceComponent c true false)) : QuadraticMap.polar (⇑C.norm) (peirceElement c a₁ a₂ x₁₂ x₂₁) (peirceElement c b₁ b₂ y₁₂ y₂₁) = a₁ * b₂ + a₂ * b₁ + QuadraticMap.polar ⇑C.norm ↑x₁₂ ↑y₂₁ + QuadraticMap.polar ⇑C.norm ↑x₂₁ ↑y₁₂

The polar form in Peirce coordinates [GPR, Exc. 19.35(4)].

theorem ConicAlgebra.IsElementaryIdempotent.trace_peirceElement {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) (a₁ a₂ : k) (x₁₂ : ↥(IsAlternative.peirceComponent c false true)) (x₂₁ : ↥(IsAlternative.peirceComponent c true false)) : C.trace (peirceElement c a₁ a₂ x₁₂ x₂₁) = a₁ + a₂

The trace in Peirce coordinates [GPR, Exc. 19.35(5)].

theorem ConicAlgebra.IsElementaryIdempotent.conj_peirceElement {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) (a₁ a₂ : k) (x₁₂ : ↥(IsAlternative.peirceComponent c false true)) (x₂₁ : ↥(IsAlternative.peirceComponent c true false)) : C.conj (peirceElement c a₁ a₂ x₁₂ x₂₁) = peirceElement c a₂ a₁ (-x₁₂) (-x₂₁)

Conjugation in Peirce coordinates [GPR, Exc. 19.35(6)]: it exchanges the diagonal coefficients and negates the off-diagonal components.

def ConicAlgebra.IsElementaryIdempotent.offDiagonalPairing {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] (C : ConicAlgebra k A) (c : A) : ↥(IsAlternative.peirceComponent c false true) →ₗ[k] Module.Dual k ↥(IsAlternative.peirceComponent c true false)

The polar pairing from C₁₂ to the dual of C₂₁.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConicAlgebra.IsElementaryIdempotent.offDiagonalPairing_apply {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] (C : ConicAlgebra k A) (c : A) (x : ↥(IsAlternative.peirceComponent c false true)) (y : ↥(IsAlternative.peirceComponent c true false)) : ((offDiagonalPairing C c) x) y = QuadraticMap.polar ⇑C.norm ↑x ↑y

theorem ConicAlgebra.IsElementaryIdempotent.bijective_offDiagonalPairing {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) (hreg : C.norm.IsGPRRegular) : Function.Bijective ⇑(offDiagonalPairing C c)

Under regularity, the off-diagonal Peirce components are in duality under the polar form, as in [GPR, Exc. 19.35].

noncomputable def ConicAlgebra.IsElementaryIdempotent.offDiagonalDuality {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) (hreg : C.norm.IsGPRRegular) : ↥(IsAlternative.peirceComponent c false true) ≃ₗ[k] Module.Dual k ↥(IsAlternative.peirceComponent c true false)

The linear equivalence expressing the duality between C₁₂ and C₂₁ [GPR, Exc. 19.35].

Equations

• hc.offDiagonalDuality hmul hreg = LinearEquiv.ofBijective (ConicAlgebra.IsElementaryIdempotent.offDiagonalPairing C c) ⋯

theorem ConicAlgebra.IsElementaryIdempotent.rankAtStalk_offDiagonal_eq_one {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} [Module.Finite k A] [Module.Projective k A] (hc : C.IsElementaryIdempotent c) (hmul : C.IsMultiplicative) (hreg : C.norm.IsGPRRegular) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) (i : Bool) : Module.rankAtStalk ↥(IsAlternative.peirceComponent c i !i) = 1

The rank count in GPR 22.13. At an elementary idempotent in a constant-rank-four composition algebra with regular norm, both off-diagonal Peirce components have constant rank one. Thus each is a line bundle.

theorem ConicAlgebra.IsElementaryIdempotent.isLocallyFreeRankOne_offDiagonal {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} [Module.Finite k A] [Module.Projective k A] (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) (i : Bool) : Module.IsLocallyFreeRankOne k ↥(IsAlternative.peirceComponent c i !i)

The line-bundle step in GPR 22.13. In a rank-four composition algebra with an elementary idempotent, each off-diagonal Peirce component is finite projective of constant rank one. The regularity needed for the duality and rank count is supplied by GPR 19.11.

theorem ConicAlgebra.IsElementaryIdempotent.mul_eq_zero_of_mem_offDiagonal_of_rankAtStalk_eq_four {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} [Module.Finite k A] [Module.Projective k A] (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) {x y : A} {i j : Bool} (hij : i ≠ j) (hx : x ∈ IsAlternative.peirceComponent c i j) (hy : y ∈ IsAlternative.peirceComponent c i j) : x * y = 0

The vanishing product needed in GPR 22.13. In a rank-four composition algebra, multiplication of any two elements in the same off-diagonal Peirce component is zero. The component is a line bundle, and its internal multiplication is alternating because every element squares to zero.

theorem ConicAlgebra.IsElementaryIdempotent.mul_peirceElement_of_rankAtStalk_eq_four {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} [Module.Finite k A] [Module.Projective k A] (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) (a₁ a₂ b₁ b₂ : k) (x₁₂ y₁₂ : ↥(IsAlternative.peirceComponent c false true)) (x₂₁ y₂₁ : ↥(IsAlternative.peirceComponent c true false)) : peirceElement c a₁ a₂ x₁₂ x₂₁ * peirceElement c b₁ b₂ y₁₂ y₂₁ = peirceElement c (a₁ * b₁ - QuadraticMap.polar ⇑C.norm ↑x₁₂ ↑y₂₁) (a₂ * b₂ - QuadraticMap.polar ⇑C.norm ↑y₁₂ ↑x₂₁) (a₁ • y₁₂ + b₂ • x₁₂) (b₁ • x₂₁ + a₂ • y₂₁)

The complete Peirce-coordinate multiplication formula in rank four, the multiplication table used in the converse half of GPR 22.13.

noncomputable def ConicAlgebra.IsElementaryIdempotent.offDiagonalDualityOfIsComposition {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] {C : ConicAlgebra k A} {c : A} [Module.Finite k A] [Module.Projective k A] (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition) {r : ℕ} (hrank : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => r) (hr : r ≠ 1) : ↥(IsAlternative.peirceComponent c false true) ≃ₗ[k] Module.Dual k ↥(IsAlternative.peirceComponent c true false)

For a constant-rank composition algebra of rank other than one, C₁₂ and C₂₁ are in duality under the polar form [GPR, Exc. 19.35]. Regularity is supplied by GPR 19.11.

Equations

• hc.offDiagonalDualityOfIsComposition hcomp hrank hr = hc.offDiagonalDuality ⋯ ⋯