Center of the algebra of linear endomorphisms

If V is an R-module, we say that an endomorphism f : Module.End R V is a homothety with central ratio if there exists a ∈ Set.center R such that f x = a • x for all x. By Module.End.mem_subsemiringCenter_iff, these linear maps constitute the center of Module.End R V. (When R is commutative, we can write f = a • LinearMap.id.)

In what follows, V is assumed to be a free R-module.

• LinearMap.commute_transvections_iff_of_basis: if an endomorphism f : V →ₗ[R] V commutes with every elementary transvections (in a given basis), then it is an homothety with central ratio. (Assumes that the basis is provided and has a non trivial set of indices.)

• LinearMap.exists_eq_smul_id_of_forall_notLinearIndependent: over a commutative ring R which is a domain, an endomorphism f : V →ₗ[R] V of a free domain such that v and f v are not linearly independent, for all v : V, is a homothety.

• LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent: a variant that does not assume that R is commutative. Then the homothety has central ratio.

• LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis: a variant that does not assume that R has the strong rank condition, but requires a basis.

Note. In the noncommutative case, the last two results do not hold when the rank is equal to 1. Indeed, right multiplications with noncentral ratio of the R-module R satisfy the property that f v and v are linearly independent, for all v : V, but they are not left multiplication by some element.

theorem LinearMap.commute_transvections_iff_of_basis {R : Type u_1} {V : Type u_2} [Ring R] [AddCommGroup V] [Module R V] {ι : Type u_3} [Nontrivial ι] (b : Module.Basis ι R V) {f : V →ₗ[R] V} (hcomm : ∀ (i j : ι) (r : R), i ≠ j → Commute f ((b.coord i).transvection (r • b j))) : ∃ (a : ↥(Subring.center R)), f = a • 1

A linear endomorphism of a free module of rank at least 2 that commutes with transvections consists of homotheties with central ratio.

theorem LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis {R : Type u_1} {V : Type u_2} [Ring R] [IsDomain R] [AddCommGroup V] [Module R V] {f : V →ₗ[R] V} {ι : Type u_3} [Nontrivial ι] (b : Module.Basis ι R V) (h : ∀ (v : V), ¬LinearIndependent R ![v, f v]) : ∃ (a : ↥(Subring.center R)), f = a • 1

Over a domain, an endomorphism f of a free module V of rank ≠ 1 such that f v and v are colinear, for all v : V, consists of homotheties with central ratio.

In the commutative case, use LinearMap.exists_eq_smul_id.

This is a variant of LinearMap.exists_mem_center_apply_smul which switches the use StrongRankInduction and finrank for the cardinality of a given basis.

When finrank R V = 1, up to a linear equivalence V ≃ₗ[R] R, then any f is right-multiplication by some a : K, but not necessarily left-multiplication by an element of the center of R.

theorem LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent {R : Type u_1} {V : Type u_2} [Ring R] [IsDomain R] [StrongRankCondition R] [AddCommGroup V] [Module R V] [Module.Free R V] {f : V →ₗ[R] V} (hV1 : Module.finrank R V ≠ 1) (h : ∀ (v : V), ¬LinearIndependent R ![v, f v]) : ∃ (a : ↥(Subring.center R)), f = a • 1

Over a domain R, an endomorphism f of a free module V of rank ≠ 1 such that f v and v are colinear, for all v : V, consists of homotheties with central ratio.

When Rdoes not satisfy StrongRankCondition, use LinearMap.exists_mem_center_apply_eq_smul_of_basis.

When finrank R V = 1, up to a linear equivalence V ≃ₗ[R] R, then any f is right-multiplication by some a : K, but not necessarily left-multiplication by an element of the center of R.

theorem LinearMap.exists_eq_smul_id_of_forall_notLinearIndependent {R : Type u_1} {V : Type u_2} [CommRing R] [IsDomain R] [AddCommGroup V] [Module R V] [Module.Free R V] {f : V →ₗ[R] V} (h : ∀ (v : V), ¬LinearIndependent R ![v, f v]) : ∃ (a : R), f = a • 1

Over a commutative domain, an endomorphism f of a free module V such that f v and v are colinear, for all v : V, consists of homotheties.