Elements acting trivially on projective space

An element of a group acting linearly on a vector space fixes every projective point exactly when its linear action is scalar. This criterion identifies the kernel of projective actions of matrix subgroups without any finite-dimensionality assumption.

The argument generalizes the scalarity step in Mathlib's Projectivization.SL_mulAction_ker, using LinearMap.exists_eq_smul_id_of_forall_notLinearIndependent.

theorem TauCeti.Projectivization.forall_smul_eq_iff_exists_smul {G : Type u_1} {K : Type u_2} {V : Type u_3} [Group G] [Field K] [AddCommGroup V] [Module K V] [DistribMulAction G V] [SMulCommClass G K V] (g : G) : (∀ (p : Projectivization K V), g • p = p) ↔ ∃ (c : K), ∀ (v : V), g • v = c • v

A linear group element fixes every line if and only if it acts by a single scalar on the whole vector space. The statement also allows the zero vector space.