Vanishing of a family fixed by a matrix

A family y : n → P in a module over a ring A satisfying yᵢ = ∑ⱼ Bᵢⱼ • yⱼ is exactly a fixed point of the Matrix n n A-action on n → P, so it is killed by 1 - B. If 1 - B is a unit, y vanishes.

This is pure algebra: no topology, and A need not be commutative. It is stated here rather than beside the topological criteria that produce IsUnit (1 - B), so that consumers do not have to import a ring theory they do not use — in particular it applies where P is an abstract subquotient with no topology of its own.

Main results

• TauCeti.eq_zero_of_isUnit_one_sub_of_forall_eq_sum_smul: a family fixed by B vanishes as soon as 1 - B is a unit.

References

• [S. Bosch, U. Güntzer and R. Remmert, Non-Archimedean Analysis][bosch-guntzer-remmert], §3.7.2/1, where this is the algebraic engine behind closedness of finitely generated submodules.

theorem TauCeti.eq_zero_of_isUnit_one_sub_of_forall_eq_sum_smul {A : Type u_1} [Ring A] {n : Type u_2} [Fintype n] [DecidableEq n] {P : Type u_3} [AddCommGroup P] [Module A P] {B : Matrix n n A} (hU : IsUnit (1 - B)) {y : n → P} (hy : ∀ (i : n), y i = ∑ j : n, B i j • y j) : y = 0

Nakayama once 1 - B is known to be a unit. A family with yᵢ = ∑ⱼ Bᵢⱼ • yⱼ is killed by 1 - B under the Matrix n n A-action on n → P, so invertibility of 1 - B forces y = 0.

Nothing topological appears: P carries no topology, and A is an arbitrary ring — the matrix action needs no commutativity.