Orthogonal nonzero idempotents are linearly independent

Let k be a ring whose multiplication cancels (IsCancelMulZero, so in particular any integral domain), let A be a ring that is a torsion-free k-module -- no nonzero scalar annihilates a nonzero element -- on which k acts compatibly with multiplication (IsScalarTower k A A, as for any k-algebra), and let e : ι → A be a family of pairwise orthogonal idempotents, none of them zero. Then the eᵢ are linearly independent over k: multiplying a vanishing combination ∑ᵢ gᵢ • eᵢ = 0 by e_j kills every term but the j-th, which orthogonality and idempotence leave as g_j • e_j = 0.

Mathlib has orthogonal families of idempotents (OrthogonalIdempotents, in Mathlib/RingTheory/Idempotents.lean) and the ring-theoretic decompositions they generate, but records nothing about their linear independence, which is what makes a complete orthogonal family of the right size a basis.

Main results

• OrthogonalIdempotents.linearIndependent: a family of pairwise orthogonal nonzero idempotents is linearly independent.
• OrthogonalIdempotents.linearIndependent_sigma: cornerwise linearly independent families form one linearly independent family.

theorem OrthogonalIdempotents.linearIndependent {k : Type u_1} {A : Type u_2} {ι : Type u_3} [Ring k] [IsCancelMulZero k] [Ring A] [Module k A] [IsScalarTower k A A] [Module.IsTorsionFree k A] {e : ι → A} (he : OrthogonalIdempotents e) (he₀ : ∀ (i : ι), e i ≠ 0) : LinearIndependent k e

A family of pairwise orthogonal nonzero idempotents of a ring A is linearly independent over a ring k with cancellative multiplication, provided A is a torsion-free k-module on which k acts compatibly with multiplication (for example, a torsion-free k-algebra).

theorem OrthogonalIdempotents.mul_mul_eq_ite {A : Type u_1} {ι : Type u_2} [Semiring A] {e : ι → A} (he : OrthogonalIdempotents e) {α : ι → ι → Type u_3} (f : (i j : ι) → α i j → A) (hl : ∀ (i j : ι) (a : α i j), e j * f i j a = f i j a) (hr : ∀ (i j : ι) (a : α i j), f i j a * e i = f i j a) {i j i' j' : ι} (a : α i j) [Decidable (j' = j ∧ i' = i)] : e j' * f i j a * e i' = if j' = j ∧ i' = i then f i j a else 0

Cutting an element of the (j, i)-corner by two members of an orthogonal family keeps it exactly when those members are e j and e i, and kills it otherwise.

theorem OrthogonalIdempotents.linearIndependent_sigma {k : Type u_1} {A : Type u_2} {ι : Type u_3} [Ring k] [Ring A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] {e : ι → A} (he : OrthogonalIdempotents e) {α : ι → ι → Type u_4} (f : (i j : ι) → α i j → A) (hl : ∀ (i j : ι) (a : α i j), e j * f i j a = f i j a) (hr : ∀ (i j : ι) (a : α i j), f i j a * e i = f i j a) (hind : ∀ (i j : ι), LinearIndependent k (f i j)) : LinearIndependent k fun (a : (i : ι) × (j : ι) × α i j) => f a.fst a.snd.fst a.snd.snd

If each family in the (j, i)-corner is linearly independent, their union over all pairs of orthogonal idempotents is linearly independent.