Theorems · Theorem · ring theory

LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis

∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [IsDomain R] [inst_2 : AddCommGroup V] [inst_3 : Module R V]
  {f : V →ₗ[R] V} {ι : Type u_3} [Nontrivial ι] (b : Module.Basis ι R V),
  (∀ (v : V), ¬LinearIndependent R ![v, f v]) → ∃ a, f = a • 1

Over a domain, an endomorphism f of a free module V of rank ≠ 1 such that f v and v are collinear, 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 of 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 : R, but not necessarily left-multiplication by an element of the center of R.

Defined in

Mathlib.LinearAlgebra.Center

Cited by

1 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingIsDomainAddCommGroupModuleNontrivial