Free independence of subalgebras

Let A be a unital algebra over a commutative semiring R and let φ : A →ₗ[R] R be a linear functional. A family of unital subalgebras B i of A is freely independent with respect to φ if φ (a₁ * ⋯ * aₙ) = 0 whenever n ≥ 1, each aⱼ lies in some B iⱼ and is centred, φ aⱼ = 0, and consecutive labels differ, iⱼ ≠ iⱼ₊₁. Labels that are not adjacent may coincide. In free probability R = ℂ and φ is normalised, φ 1 = 1; here normalisation is a separate hypothesis of the results that use it, and no positivity or traciality is assumed. The definition and basic transport lemmas work over semirings; the centring expansions and their consequences require rings.

A word a₁ ⋯ aₙ is encoded as a list [(i₁, a₁), …, (iₙ, aₙ)] of label–element pairs, whose value is the ordered product of the list of elements.

Over rings, for a normalised functional, every word reduces by merging adjacent letters with equal labels and by centring letters one at a time, to centred alternating words and to shorter words. Hence the subalgebra generated by the family is spanned by 1 and the values of the centred alternating words, on which free functionals vanish. Three consequences are proved: freeness determines a normalised functional on the generated subalgebra from its restrictions to the individual members, freeness is preserved by grouping the members along disjoint sets of labels, and freeness preserves traciality.

Main definitions

• TauCeti.IsFreelyIndependent φ B — the subalgebras B i are freely independent with respect to φ, unfolded by TauCeti.isFreelyIndependent_iff.
• TauCeti.centeredAlternatingProds φ B — the values of the nonempty centred alternating words, with TauCeti.isFreelyIndependent_iff_span_le_ker characterising freeness as the vanishing of φ on their span.

Main results

• TauCeti.IsFreelyIndependent.mono, TauCeti.IsFreelyIndependent.comp and TauCeti.IsFreelyIndependent.map — freeness passes to smaller subalgebras, to subfamilies along injective reindexings, and to images under algebra homomorphisms intertwining the functionals.
• TauCeti.isFreelyIndependent_of_subsingleton — a family with at most one member, in particular the empty family, is free.
• TauCeti.isFreelyIndependent_domRestrict_iff — for a normalised functional, members equal to the scalars may be added to or removed from a free family.
• TauCeti.IsFreelyIndependent.apply_mul_of_ne — the first mixed moment factorises, φ (a * b) = φ a * φ b; TauCeti.IsFreelyIndependent.apply_mul_mul_of_ne and TauCeti.IsFreelyIndependent.apply_mul_mul_mul_of_ne compute the alternating mixed moments of orders three and four.
• TauCeti.IsFreelyIndependent.sub_mul_sub_eq_zero_of_commute — freeness is not classical independence: for commuting letters from distinct members the product of their variances vanishes.
• TauCeti.toSubmodule_iSup_eq_span_insert_one_centeredAlternatingProds — for a normalised functional, 1 and the values of the centred alternating words span the generated subalgebra; TauCeti.IsFreelyIndependent.mem_span_centeredAlternatingProds_iff identifies, for a free family, the span of the latter with the centred elements of the generated subalgebra.
• TauCeti.IsFreelyIndependent.eqOn_iSup — two normalised functionals for which the family is free and which agree on each member agree on the subalgebra the family generates, with TauCeti.IsFreelyIndependent.eq_of_iSup_eq_top the case of a generating family.
• TauCeti.IsFreelyIndependent.iSup_fiber — for a normalised functional and g : ι → κ, the subalgebras generated by the members over the fibres of g are free.
• TauCeti.IsFreelyIndependent.apply_prod_mul_prod — pairing of two centred alternating word products under a normalised functional for which the family is free.
• TauCeti.IsFreelyIndependent.apply_mul_comm_of_mem_iSup and TauCeti.IsFreelyIndependent.apply_mul_comm_of_iSup_eq_top — freeness preserves traciality.

References

• A. Nica, R. Speicher, Lectures on the Combinatorics of Free Probability, Lecture 5.
• D. V. Voiculescu, K. J. Dykema, A. Nica, Free Random Variables, §§1.2–1.5, Proposition 2.5.3.

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

Subalgebras B i of A are freely independent with respect to a linear functional φ if φ (a₁ * ⋯ * aₙ) = 0 for every nonempty word [(i₁, a₁), …, (iₙ, aₙ)] whose consecutive labels are distinct and whose letters satisfy aⱼ ∈ B iⱼ and φ aⱼ = 0. Labels that are not adjacent may coincide.

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

def TauCeti.centeredAlternatingProds {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] (φ : A →ₗ[R] R) (B : ι → Subalgebra R A) : Set A

The values a₁ * ⋯ * aₙ of the nonempty words [(i₁, a₁), …, (iₙ, aₙ)] whose consecutive labels are distinct and whose letters satisfy aⱼ ∈ B iⱼ and φ aⱼ = 0: the values of the centred alternating words, on which a free functional vanishes by definition.

theorem TauCeti.mem_centeredAlternatingProds {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] {φ : A →ₗ[R] R} {B : ι → Subalgebra R A} {p : A} : p ∈ centeredAlternatingProds φ B ↔ ∃ (w : List (ι × A)), w ≠ [] ∧ List.IsChain (fun (x1 x2 : ι) => x1 ≠ x2) (List.map Prod.fst w) ∧ (∀ x ∈ w, x.2 ∈ B x.1) ∧ (∀ x ∈ w, φ x.2 = 0) ∧ (List.map Prod.snd w).prod = p

theorem TauCeti.isFreelyIndependent_iff_span_le_ker {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] {φ : A →ₗ[R] R} {B : ι → Subalgebra R A} : IsFreelyIndependent φ B ↔ Submodule.span R (centeredAlternatingProds φ B) ≤ φ.ker

Freeness says exactly that φ vanishes on the span of the values of the centred alternating words.

theorem TauCeti.isFreelyIndependent_of_subsingleton {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Subsingleton ι] (φ : A →ₗ[R] R) (B : ι → Subalgebra R A) : IsFreelyIndependent φ B

A family with at most one member is free: an alternating word then has a single letter.

theorem TauCeti.IsFreelyIndependent.mono {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] {φ : A →ₗ[R] R} {B C : ι → Subalgebra R A} (h : IsFreelyIndependent φ B) (hCB : ∀ (i : ι), C i ≤ B i) : IsFreelyIndependent φ C

Freeness passes to smaller subalgebras.

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

Freeness passes to subfamilies along an injective reindexing.

theorem TauCeti.IsFreelyIndependent.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 →ₗ[R] R} {B : ι → Subalgebra R A} (h : IsFreelyIndependent φ B) (f : A →ₐ[R] A') {φ' : A' →ₗ[R] R} (hf : φ' ∘ₗ f.toLinearMap = φ) : IsFreelyIndependent φ' fun (i : ι) => Subalgebra.map f (B i)

Freeness is transported along an algebra homomorphism f intertwining the functionals: the images of a free family are free.

theorem TauCeti.IsFreelyIndependent.comap {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} {B' : ι → Subalgebra R A'} (h : IsFreelyIndependent φ' B') (f : A →ₐ[R] A') : IsFreelyIndependent (φ' ∘ₗ f.toLinearMap) fun (i : ι) => Subalgebra.comap f (B' i)

Pulling back a free family and its functional along an algebra homomorphism preserves freeness. The homomorphism need not be injective: letters in its kernel have zero expectation.

theorem TauCeti.isFreelyIndependent_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) {B : ι → Subalgebra R A} {s : Set ι} (hs : ∀ i ∉ s, B i = ⊥) : IsFreelyIndependent φ (s.domRestrict B) ↔ IsFreelyIndependent φ B

For a normalised functional, members of a family equal to the scalars do not affect freeness: if B i = ⊥ for every label outside s, then B is free exactly when its restriction to s is free.

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

The first mixed moment of a free family factorises: for a normalised functional and letters from members with distinct labels, φ (a * b) = φ a * φ b.

theorem TauCeti.IsFreelyIndependent.apply_mul_mul_of_ne {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommRing R] [Ring A] [Algebra R A] {φ : A →ₗ[R] R} {B : ι → Subalgebra R A} (h : IsFreelyIndependent φ B) (hφ : φ 1 = 1) {i j : ι} (hij : i ≠ j) {a b a' : A} (ha : a ∈ B i) (hb : b ∈ B j) (ha' : a' ∈ B i) : φ (a * b * a') = φ (a * a') * φ b

The mixed moment of order three of a free family: for a normalised functional, letters a, a' from one member and b from a member with a different label, φ (a * b * a') = φ (a * a') * φ b.

theorem TauCeti.IsFreelyIndependent.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 →ₗ[R] R} {B : ι → Subalgebra R A} (h : IsFreelyIndependent φ B) (hφ : φ 1 = 1) {i j : ι} (hij : i ≠ j) {a b a' b' : A} (ha : a ∈ B i) (hb : b ∈ B j) (ha' : a' ∈ B i) (hb' : b' ∈ B j) : φ (a * b * a' * b') = φ (a * a') * φ b * φ b' + φ a * φ a' * φ (b * b') - φ a * φ a' * φ b * φ b'

The alternating mixed moment of order four of a free family: for a normalised functional, letters a, a' from one member and b, b' from a member with a different label, φ (a * b * a' * b') = φ (a * a') * φ b * φ b' + φ a * φ a' * φ (b * b') - φ a * φ a' * φ b * φ b'.

For centred a = a' and b = b' it gives φ (a * b * a * b) = 0, whereas φ (a * a * (b * b)) = φ (a * a) * φ (b * b) by IsFreelyIndependent.apply_mul_of_ne; for variance one these are 0 and 1, while for commuting classically independent variables both equal 1.

theorem TauCeti.IsFreelyIndependent.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 →ₗ[R] R} {B : ι → Subalgebra R A} (h : IsFreelyIndependent φ B) (hφ : φ 1 = 1) {i j : ι} (hij : i ≠ j) {a b : A} (ha : a ∈ B i) (hb : b ∈ B j) (hab : Commute a b) : (φ (a * a) - φ a ^ 2) * (φ (b * b) - φ b ^ 2) = 0

Freeness differs from classical independence: if a and b lie in members of a free family with distinct labels and commute, then for a normalised functional the product of their variances φ (a * a) - φ a ^ 2 and φ (b * b) - φ b ^ 2 vanishes; over a ring without zero divisors, such as ℂ, one of them is zero, so commuting variables of nonzero variance are never free.

theorem TauCeti.toSubmodule_iSup_eq_span_insert_one_centeredAlternatingProds {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommRing R] [Ring A] [Algebra R A] {φ : A →ₗ[R] R} (hφ : φ 1 = 1) (B : ι → Subalgebra R A) : Subalgebra.toSubmodule (⨆ (i : ι), B i) = Submodule.span R (insert 1 (centeredAlternatingProds φ B))

For a normalised functional φ, the subalgebra generated by the B i is spanned by 1 and the values of the words alternating between the B i whose letters are centred with respect to φ. No freeness is needed: every word reduces to these by merging adjacent letters with equal labels and by centring letters one at a time.

theorem TauCeti.IsFreelyIndependent.mem_span_centeredAlternatingProds_iff {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommRing R] [Ring A] [Algebra R A] {φ : A →ₗ[R] R} {B : ι → Subalgebra R A} (h : IsFreelyIndependent φ B) (hφ : φ 1 = 1) {x : A} : x ∈ Submodule.span R (centeredAlternatingProds φ B) ↔ x ∈ ⨆ (i : ι), B i ∧ φ x = 0

For a normalised functional for which B is free, the span of the values of the centred alternating words consists of the centred elements of the subalgebra generated by the B i.

theorem TauCeti.IsFreelyIndependent.eqOn_iSup {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommRing R] [Ring A] [Algebra R A] {φ ψ : A →ₗ[R] R} {B : ι → Subalgebra R A} (hφ : φ 1 = 1) (hψ : ψ 1 = 1) (hfφ : IsFreelyIndependent φ B) (hfψ : IsFreelyIndependent ψ B) (h : ∀ (i : ι), Set.EqOn ⇑φ ⇑ψ ↑(B i)) : Set.EqOn ⇑φ ⇑ψ ↑(⨆ (i : ι), B i)

Freeness determines the joint distribution from the individual ones: two normalised functionals for which B is free and which agree on each B i agree on the subalgebra generated by the B i.

theorem TauCeti.IsFreelyIndependent.eq_of_iSup_eq_top {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommRing R] [Ring A] [Algebra R A] {φ ψ : A →ₗ[R] R} {B : ι → Subalgebra R A} (hφ : φ 1 = 1) (hψ : ψ 1 = 1) (hfφ : IsFreelyIndependent φ B) (hfψ : IsFreelyIndependent ψ B) (h : ∀ (i : ι), Set.EqOn ⇑φ ⇑ψ ↑(B i)) (htop : ⨆ (i : ι), B i = ⊤) : φ = ψ

Two normalised functionals for which a generating family B is free and which agree on each B i are equal.

theorem TauCeti.IsFreelyIndependent.iSup_fiber {R : Type u_1} {A : Type u_2} {ι : Type u_4} {κ : Type u_5} [CommRing R] [Ring A] [Algebra R A] {φ : A →ₗ[R] R} {B : ι → Subalgebra R A} (h : IsFreelyIndependent φ B) (hφ : φ 1 = 1) (g : ι → κ) : IsFreelyIndependent φ fun (k : κ) => ⨆ (i : ι), ⨆ (_ : g i = k), B i

Freeness passes to the subalgebras generated by the members over disjoint sets of labels: for a normalised functional and any g : ι → κ, the subalgebras ⨆ (i) (_ : g i = k), B i generated by the members labelled by the fibres of g are free.

theorem TauCeti.IsFreelyIndependent.apply_prod_mul_prod {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommRing R] [Ring A] [Algebra R A] {φ : A →ₗ[R] R} {B : ι → Subalgebra R A} [DecidableEq ι] (h : IsFreelyIndependent φ B) (hφ : φ 1 = 1) (u v : List (ι × A)) (hu : List.IsChain (fun (x1 x2 : ι) => x1 ≠ x2) (List.map Prod.fst u)) (hv : List.IsChain (fun (x1 x2 : ι) => x1 ≠ x2) (List.map Prod.fst v)) (huB : ∀ x ∈ u, x.2 ∈ B x.1) (hvB : ∀ x ∈ v, x.2 ∈ B x.1) (huφ : ∀ x ∈ u, φ x.2 = 0) (hvφ : ∀ x ∈ v, φ x.2 = 0) : φ ((List.map Prod.snd u).prod * (List.map Prod.snd v).prod) = if List.map Prod.fst u.reverse = List.map Prod.fst v then (List.zipWith (fun (x y : ι × A) => φ (x.2 * y.2)) u.reverse v).prod else 0

The product of two centered alternating words has zero expectation unless the reversed label sequence of the first equals the label sequence of the second, in which case the expectation factorizes into the product of expectations of matched letter pairs from the middle outward.

theorem TauCeti.IsFreelyIndependent.apply_mul_comm_of_mem_iSup {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommRing R] [Ring A] [Algebra R A] {φ : A →ₗ[R] R} {B : ι → Subalgebra R A} (h : IsFreelyIndependent φ B) (hφ : φ 1 = 1) (htr : ∀ (i : ι), ∀ a ∈ B i, ∀ b ∈ B i, φ (a * b) = φ (b * a)) {x y : A} (hx : x ∈ ⨆ (i : ι), B i) (hy : y ∈ ⨆ (i : ι), B i) : φ (x * y) = φ (y * x)

Freeness preserves traciality. If a normalized linear functional φ makes B freely independent and restricts to a trace on each subalgebra B i, then φ is tracial on the generated subalgebra ⨆ i, B i.

theorem TauCeti.IsFreelyIndependent.apply_mul_comm_of_iSup_eq_top {R : Type u_1} {A : Type u_2} {ι : Type u_4} [CommRing R] [Ring A] [Algebra R A] {φ : A →ₗ[R] R} {B : ι → Subalgebra R A} (h : IsFreelyIndependent φ B) (hφ : φ 1 = 1) (htr : ∀ (i : ι), ∀ a ∈ B i, ∀ b ∈ B i, φ (a * b) = φ (b * a)) (htop : ⨆ (i : ι), B i = ⊤) (x y : A) : φ (x * y) = φ (y * x)

If a generating family of subalgebras B is freely independent for a normalized functional φ that restricts to a trace on each B i, then φ is tracial on A.