Free independence of elements

A family of elements in a unital algebra is freely independent when the unital subalgebras generated by the individual elements are freely independent. This file connects that definition to the two forms used in computations: centred alternating polynomial evaluations and the subalgebras generated by groups of variables.

The polynomial test is valid in a possibly noncommutative ambient algebra: a polynomial in one element is evaluated using the central R-algebra structure. For a normalised functional, scalar variables can be inserted or removed, and freeness determines the functional on the algebra generated by the whole family from its one-variable polynomial moments. The definition, polynomial test, basic transport lemmas and removal of scalar variables work over a commutative semiring; the mixed-moment, grouping and uniqueness results use rings.

References

• A. Nica, R. Speicher, Lectures on the Combinatorics of Free Probability, Lecture 5.

def TauCeti.IsFreelyIndependentElements {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] (φ : A →ₗ[R] R) (a : ι → A) : Prop

Elements a i are freely independent with respect to φ when the unital subalgebras generated by the individual elements are freely independent.

theorem TauCeti.isFreelyIndependentElements_iff {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] {a : ι → A} {φ : A →ₗ[R] R} : IsFreelyIndependentElements φ a ↔ IsFreelyIndependent φ fun (i : ι) => R[a i]

Free independence of elements, restated as free independence of their generated unital subalgebras.

theorem TauCeti.isFreelyIndependentElements_iff_polynomial {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] {a : ι → A} {φ : A →ₗ[R] R} : IsFreelyIndependentElements φ a ↔ ∀ (w : List (ι × Polynomial R)), w ≠ [] → List.IsChain (fun (x1 x2 : ι) => x1 ≠ x2) (List.map Prod.fst w) → (∀ x ∈ w, φ ((Polynomial.aeval (a x.1)) x.2) = 0) → φ (List.map (fun (x : ι × Polynomial R) => (Polynomial.aeval (a x.1)) x.2) w).prod = 0

Elements are freely independent exactly when every nonempty centred polynomial word with alternating labels has zero expectation.

theorem TauCeti.IsFreelyIndependentElements.comp {R : Type u_1} {A : Type u_2} {ι : Type u_4} {κ : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] {a : ι → A} {φ : A →ₗ[R] R} (h : IsFreelyIndependentElements φ a) {e : κ → ι} (he : Function.Injective e) : IsFreelyIndependentElements φ (a ∘ e)

A subfamily of a freely independent family, selected by an injective reindexing, is freely independent.

theorem TauCeti.IsFreelyIndependentElements.map {R : Type u_1} {A : Type u_2} {A' : Type u_3} {ι : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring A'] [Algebra R A'] {a : ι → A} {φ : A →ₗ[R] R} (h : IsFreelyIndependentElements φ a) (f : A →ₐ[R] A') {φ' : A' →ₗ[R] R} (hf : φ' ∘ₗ f.toLinearMap = φ) : IsFreelyIndependentElements φ' (⇑f ∘ a)

An algebra homomorphism intertwining two functionals sends freely independent elements to freely independent elements.

theorem TauCeti.isFreelyIndependentElements_map_iff {R : Type u_1} {A : Type u_2} {A' : Type u_3} {ι : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring A'] [Algebra R A'] (φ' : A' →ₗ[R] R) (f : A →ₐ[R] A') (a : ι → A) : IsFreelyIndependentElements φ' (⇑f ∘ a) ↔ IsFreelyIndependentElements (φ' ∘ₗ f.toLinearMap) a

Free independence of elements can be tested after applying an algebra homomorphism, provided that the functional is pulled back along the same homomorphism. Injectivity is not required.

theorem TauCeti.isFreelyIndependentElements_of_subsingleton {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Subsingleton ι] (φ : A →ₗ[R] R) (a : ι → A) : IsFreelyIndependentElements φ a

Every family indexed by a subsingleton type is freely independent.

theorem TauCeti.isFreelyIndependentElements_domRestrict_iff {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] {φ : A →ₗ[R] R} (hφ : φ 1 = 1) {a : ι → A} {s : Set ι} (hs : ∀ i ∉ s, ∃ (r : R), a i = (algebraMap R A) r) : IsFreelyIndependentElements φ (s.domRestrict a) ↔ IsFreelyIndependentElements φ a

For a normalised functional, scalar-valued members can be added to or removed from a family without changing free independence.

theorem TauCeti.IsFreelyIndependentElements.apply_mul_of_ne {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommRing R] [Ring A] [Algebra R A] {a : ι → A} {φ : A →ₗ[R] R} (h : IsFreelyIndependentElements φ a) (hφ : φ 1 = 1) {i j : ι} (hij : i ≠ j) : φ (a i * a j) = φ (a i) * φ (a j)

The first mixed moment of two distinct freely independent elements factorises.

theorem TauCeti.IsFreelyIndependentElements.apply_mul_mul_of_ne {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommRing R] [Ring A] [Algebra R A] {a : ι → A} {φ : A →ₗ[R] R} (h : IsFreelyIndependentElements φ a) (hφ : φ 1 = 1) {i j : ι} (hij : i ≠ j) : φ (a i * a j * a i) = φ (a i * a i) * φ (a j)

The alternating mixed moment of order three of two distinct freely independent elements: φ (a i * a j * a i) = φ (a i * a i) * φ (a j).

theorem TauCeti.IsFreelyIndependentElements.apply_mul_mul_mul_of_ne {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommRing R] [Ring A] [Algebra R A] {a : ι → A} {φ : A →ₗ[R] R} (h : IsFreelyIndependentElements φ a) (hφ : φ 1 = 1) {i j : ι} (hij : i ≠ j) : φ (a i * a j * a i * a j) = φ (a i * a i) * φ (a j) ^ 2 + φ (a i) ^ 2 * φ (a j * a j) - φ (a i) ^ 2 * φ (a j) ^ 2

The alternating mixed moment of order four of two distinct freely independent elements: φ (a i * a j * a i * a j) = φ (a i * a i) * φ (a j) ^ 2 + φ (a i) ^ 2 * φ (a j * a j) - φ (a i) ^ 2 * φ (a j) ^ 2. For centred elements it vanishes.

theorem TauCeti.IsFreelyIndependentElements.sub_mul_sub_eq_zero_of_commute {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommRing R] [Ring A] [Algebra R A] {a : ι → A} {φ : A →ₗ[R] R} (h : IsFreelyIndependentElements φ a) (hφ : φ 1 = 1) {i j : ι} (hij : i ≠ j) (hcomm : Commute (a i) (a j)) : (φ (a i * a i) - φ (a i) ^ 2) * (φ (a j * a j) - φ (a j) ^ 2) = 0

Two distinct freely independent elements that commute have variances φ (a i * a i) - φ (a i) ^ 2 and φ (a j * a j) - φ (a j) ^ 2 with vanishing product.

theorem TauCeti.IsFreelyIndependentElements.adjoin_image_fiber {R : Type u_1} {A : Type u_2} {ι : Type u_4} {κ : Type u_5} [CommRing R] [Ring A] [Algebra R A] {a : ι → A} {φ : A →ₗ[R] R} (h : IsFreelyIndependentElements φ a) (hφ : φ 1 = 1) (g : ι → κ) : IsFreelyIndependent φ fun (k : κ) => Algebra.adjoin R (a '' g ⁻¹' {k})

Grouping freely independent variables along the fibres of a map gives freely independent generated subalgebras.

theorem TauCeti.IsFreelyIndependentElements.eqOn_adjoin_range {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommRing R] [Ring A] [Algebra R A] {a : ι → A} {φ ψ : A →ₗ[R] R} (hφ : φ 1 = 1) (hψ : ψ 1 = 1) (hfφ : IsFreelyIndependentElements φ a) (hfψ : IsFreelyIndependentElements ψ a) (hmom : ∀ (i : ι) (p : Polynomial R), φ ((Polynomial.aeval (a i)) p) = ψ ((Polynomial.aeval (a i)) p)) : Set.EqOn ⇑φ ⇑ψ ↑(Algebra.adjoin R (Set.range a))

If two normalised functionals make a family free and have the same one-variable polynomial moments, they agree on the unital algebra generated by the family.

theorem TauCeti.IsFreelyIndependentElements.eq_of_adjoin_range_eq_top {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommRing R] [Ring A] [Algebra R A] {a : ι → A} {φ ψ : A →ₗ[R] R} (hφ : φ 1 = 1) (hψ : ψ 1 = 1) (hfφ : IsFreelyIndependentElements φ a) (hfψ : IsFreelyIndependentElements ψ a) (hmom : ∀ (i : ι) (p : Polynomial R), φ ((Polynomial.aeval (a i)) p) = ψ ((Polynomial.aeval (a i)) p)) (htop : Algebra.adjoin R (Set.range a) = ⊤) : φ = ψ

If freely independent elements generate the ambient algebra, their one-variable polynomial moments determine the functional.