The idempotents cut out by a square root of one

Let A be an algebra over a commutative ring R in which 2 is invertible, and let ω : A. The element

TauCeti.halfOneAdd R ω = ½ (1 + ω)

and its companion TauCeti.halfOneAdd R (-ω) = ½ (1 - ω) always add up to 1 (TauCeti.halfOneAdd_add_halfOneAdd_neg) and always differ by ω (TauCeti.halfOneAdd_sub_halfOneAdd_neg). As soon as ω * ω = 1 they are moreover orthogonal (TauCeti.halfOneAdd_mul_halfOneAdd_neg) and therefore idempotent (TauCeti.isIdempotentElem_halfOneAdd): a square root of one always cuts out a complementary orthogonal pair of idempotents. The right ideals e₊ A and e₋ A are two-sided, and the resulting decomposition is one of rings, only when the idempotents are central, which is more than this file assumes. If ω commutes with a given element then so do both idempotents (TauCeti.commute_halfOneAdd), and elements written in the form e₊ a + e₋ b then multiply componentwise (TauCeti.halfOneAdd_mul_add_mul).

Nothing here is specific to any one algebra: TauCeti/LinearAlgebra/CliffordAlgebra/OddSplitting.lean runs it on a central odd square root of one in a Clifford algebra, where the two blocks turn out to be copies of the even subalgebra.

Mathlib has IsIdempotentElem and its complement API (IsIdempotentElem.of_mul_add, IsIdempotentElem.one_sub_mul_self), which is what the proofs below consume, but not the passage from a square root of one to the idempotent pair.

Main definitions

• TauCeti.halfOneAdd: the element ½ (1 + ω). No property of ω is built into it, so that the complementary idempotent is literally the same construction applied to -ω.

Main results

• TauCeti.halfOneAdd_add_halfOneAdd_neg, TauCeti.halfOneAdd_sub_halfOneAdd_neg: the pair is complementary, and its difference recovers ω.
• TauCeti.halfOneAdd_mul_halfOneAdd_neg, TauCeti.isIdempotentElem_halfOneAdd: for a square root of one the pair is orthogonal and idempotent.
• TauCeti.halfOneAdd_mul_add_mul: the multiplication rule (e₊ a + e₋ b) (e₊ c + e₋ d) = e₊ (a c) + e₋ (b d), for a and b commuting with ω.

noncomputable def TauCeti.halfOneAdd (R : Type u_1) {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [Invertible 2] (ω : A) : A

The element ½ (1 + ω) of an R-algebra, for 2 invertible in R.

It is idempotent when ω * ω = 1 (TauCeti.isIdempotentElem_halfOneAdd), and then halfOneAdd R (-ω) = ½ (1 - ω) is the complementary idempotent. No property of ω is built into the definition, so that the two idempotents are literally the same construction applied to ω and to -ω.

Equations

• TauCeti.halfOneAdd R ω = ⅟2 • (1 + ω)

theorem TauCeti.halfOneAdd_def (R : Type u_1) {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [Invertible 2] (ω : A) : halfOneAdd R ω = ⅟2 • (1 + ω)

The defining formula for TauCeti.halfOneAdd.

@[simp]

theorem TauCeti.halfOneAdd_add_halfOneAdd_neg (R : Type u_1) {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [Invertible 2] (ω : A) : halfOneAdd R ω + halfOneAdd R (-ω) = 1

The pair is complementary: ½ (1 + ω) + ½ (1 - ω) = 1.

@[simp]

theorem TauCeti.halfOneAdd_sub_halfOneAdd_neg (R : Type u_1) {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [Invertible 2] (ω : A) : halfOneAdd R ω - halfOneAdd R (-ω) = ω

The difference of the pair is ω: ½ (1 + ω) - ½ (1 - ω) = ω. This is what makes ω recoverable from the splitting it induces.

theorem TauCeti.halfOneAdd_neg_eq_one_sub (R : Type u_1) {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [Invertible 2] (ω : A) : halfOneAdd R (-ω) = 1 - halfOneAdd R ω

The companion element is the complement 1 - ½ (1 + ω), the form in which Mathlib's IsIdempotentElem API talks about it.

theorem TauCeti.halfOneAdd_mul_halfOneAdd_neg (R : Type u_1) {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [Invertible 2] {ω : A} (hsq : ω * ω = 1) : halfOneAdd R ω * halfOneAdd R (-ω) = 0

The pair is orthogonal when ω squares to 1: ½ (1 + ω) · ½ (1 - ω) = 0.

theorem TauCeti.isIdempotentElem_halfOneAdd (R : Type u_1) {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [Invertible 2] {ω : A} (hsq : ω * ω = 1) : IsIdempotentElem (halfOneAdd R ω)

½ (1 + ω) is idempotent when ω squares to 1.

theorem TauCeti.isIdempotentElem_halfOneAdd_neg (R : Type u_1) {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [Invertible 2] {ω : A} (hsq : ω * ω = 1) : IsIdempotentElem (halfOneAdd R (-ω))

½ (1 - ω) is idempotent when ω squares to 1; it is the complementary idempotent.

theorem TauCeti.halfOneAdd_neg_mul_halfOneAdd (R : Type u_1) {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [Invertible 2] {ω : A} (hsq : ω * ω = 1) : halfOneAdd R (-ω) * halfOneAdd R ω = 0

The reverse orthogonality ½ (1 - ω) · ½ (1 + ω) = 0, read off the complement.

theorem TauCeti.commute_halfOneAdd (R : Type u_1) {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [Invertible 2] {ω x : A} (h : Commute ω x) : Commute (halfOneAdd R ω) x

The pair inherits commutation from ω. Only commutation with the element at hand is needed, so a central ω gives a central pair.

theorem TauCeti.halfOneAdd_mul_add_mul (R : Type u_1) {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [Invertible 2] {ω : A} (hsq : ω * ω = 1) {a b : A} (ha : Commute ω a) (hb : Commute ω b) (c d : A) : (halfOneAdd R ω * a + halfOneAdd R (-ω) * b) * (halfOneAdd R ω * c + halfOneAdd R (-ω) * d) = halfOneAdd R ω * (a * c) + halfOneAdd R (-ω) * (b * d)

The multiplication rule a splitting rests on: the pair being orthogonal, idempotent and commuting with a and b, elements of the form e₊ a + e₋ b multiply componentwise.