Functionals that annihilate their own argument

A linear form φ : M → R is self-annihilating if φ x • x = 0 for every x. On a finitely generated projective module this forces φ = 0.

Over a free module the reason is immediate: a basis vector e has φ e • e = 0, and a basis vector is not killed by any nonzero scalar. Over a projective module it is false pointwise — φ x • x = 0 says only that φ x annihilates x — and what rescues it is that the hypothesis is required for every x, so it survives base change and can be checked after localizing at each maximal ideal, where the module is free.

This is the mechanism behind GPR 16.14(b): an identity of the shape c(x) • x = d(x) • 1, which is what flexibility gives in a conic algebra, collapses to c = 0 as soon as the algebra is projective — see CompositionAlgebras/Conic/Projective.lean.

Main results

• LinearMap.eq_zero_of_smul_self_eq_zero_of_free : the free case.
• LinearMap.eq_zero_of_smul_self_eq_zero : the finitely generated projective case.

Implementation notes

The projective case is proved by base change to Localization.AtPrime 𝔪 rather than by localizing the module: LinearMap.baseChange and TensorProduct.induction_on are enough, and the hypothesis transfers to S ⊗[R] M in two steps — its linearization φ u • v + φ v • u = 0 is bi-additive and so reduces to pure tensors, and the hypothesis itself then follows from the linearization by induction. This is the same two-step shape as the degree-two identity in CompositionAlgebras/Conic/BaseChange.lean.

theorem LinearMap.smul_add_smul_eq_zero_of_smul_self_eq_zero {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {φ : M →ₗ[R] R} (h : ∀ (x : M), φ x • x = 0) (u v : M) : φ u • v + φ v • u = 0

The linearization of φ x • x = 0.

theorem LinearMap.eq_zero_of_smul_self_eq_zero_of_free {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Free R M] (φ : M →ₗ[R] R) (h : ∀ (x : M), φ x • x = 0) : φ = 0

A self-annihilating functional on a free module is zero. A basis vector is killed by no nonzero scalar.

theorem LinearMap.smul_add_smul_baseChange_eq_zero {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {S : Type u_1} [CommRing S] [Algebra R S] {φ : M →ₗ[R] R} (h : ∀ (x : M), φ x • x = 0) (z w : TensorProduct R S M) : ((Module.Dual.baseChange S) φ) z • w + ((Module.Dual.baseChange S) φ) w • z = 0

The linearized hypothesis transfers to the base change: it is bi-additive, so it is enough to check it on pure tensors.

theorem LinearMap.smul_self_baseChange_eq_zero {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] {S : Type u_1} [CommRing S] [Algebra R S] {φ : M →ₗ[R] R} (h : ∀ (x : M), φ x • x = 0) (z : TensorProduct R S M) : ((Module.Dual.baseChange S) φ) z • z = 0

Self-annihilation transfers to the base change.

theorem LinearMap.eq_zero_of_smul_self_eq_zero {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Projective R M] (φ : M →ₗ[R] R) (h : ∀ (x : M), φ x • x = 0) : φ = 0

A self-annihilating functional on a finitely generated projective module is zero.

Base change to Localization.AtPrime 𝔪 preserves the hypothesis, and there the module is free, so the base-changed functional vanishes; hence φ x dies in every localization, hence is 0.