Commutation with homotopy projectors, 1 - a • u and finite sums

An element of a ring commuting with u also commutes with 1 - a • u, for any scalar a acting compatibly with the multiplication. For an operator u, 1 - a • u is the operator whose generalised kernel at a zero a of the Fredholm determinant of u carries the Riesz projector.

Each member of a pairwise commuting finite family commutes with the family's sum, so it preserves the eigenvalue equations of that sum.

A square-zero differential commutes with any element e satisfying a homotopy identity d * h + h * d = 1 - e.

Main results

• Commute.one_sub_smul_left, Commute.one_sub_smul_right: commutation with 1 - a • u.
• TauCeti.commute_of_sq_zero_of_homotopy: commutation of a square-zero differential with its homotopy projector.
• Finset.sum_smul_smul_eq_smul_smul: if the sum of a pairwise commuting family scales x by μ, it scales p a • x by μ for each member p a. The vector p a • x may be zero.

theorem Commute.one_sub_smul_left {R : Type u_1} {A : Type u_2} [Ring A] [SMul R A] [IsScalarTower R A A] [SMulCommClass R A A] {u x : A} (h : Commute u x) (a : R) : Commute (1 - a • u) x

An element commuting with u commutes with 1 - a • u, on the left.

theorem Commute.one_sub_smul_right {R : Type u_1} {A : Type u_2} [Ring A] [SMul R A] [IsScalarTower R A A] [SMulCommClass R A A] {u x : A} (h : Commute x u) (a : R) : Commute x (1 - a • u)

An element commuting with u commutes with 1 - a • u, on the right.

theorem TauCeti.commute_of_sq_zero_of_homotopy {A : Type u_1} [Ring A] {d h e : A} (hd : d * d = 0) (hdh : d * h + h * d = 1 - e) : Commute d e

A square-zero differential commutes with an element satisfying its contracting homotopy identity. Thus contraction constructions can derive this compatibility rather than requiring it separately from callers. No idempotence assumption on that element is needed.

theorem Finset.sum_smul_smul_eq_smul_smul {K : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_4} [Semiring A] [MulAction A M] [SMul K M] [SMulCommClass A K M] (s : Finset ι) (p : ι → A) (hcomm : (↑s).Pairwise fun (i j : ι) => Commute (p i) (p j)) {a : ι} (ha : a ∈ s) {x : M} {μ : K} (heigen : (∑ i ∈ s, p i) • x = μ • x) : (∑ i ∈ s, p i) • p a • x = μ • p a • x

If the sum of a pairwise commuting family scales x by μ, it also scales p a • x by μ for each member p a of the family, since p a commutes with the sum.