Functionals normalised at a vector

A functional f with f x = 1 splits a module into the line through x and the kernel of f. This file records the projection id - f(·) • x that this splitting defines, and the dimension count for the trace of ker f on a subspace on which f does not vanish.

Main results

• Module.Dual.ker_id_sub_smulRight: if f x = 1, the kernel of id - f(·) • x is the line through x.
• Module.Dual.finrank_ker_inf_add_one: if f does not vanish on a finite-dimensional subspace U, then ker f ⊓ U has codimension one in U. This is the relative form of Mathlib's Module.Dual.finrank_ker_add_one_of_ne_zero.

@[simp]

theorem Module.Dual.ker_id_sub_smulRight {K : Type u_1} {V : Type u_2} [Semiring K] [AddCommGroup V] [Module K V] (f : Dual K V) {x : V} (hfx : f x = 1) : (LinearMap.id - LinearMap.smulRight f x).ker = K ∙ x

If f x = 1, the kernel of id - f(·) • x is the line through x.

theorem Module.Dual.finrank_ker_inf_add_one {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {f : Dual K V} {U : Submodule K V} [FiniteDimensional K ↥U] (hU : ¬U ≤ LinearMap.ker f) : finrank K ↥(LinearMap.ker f ⊓ U) + 1 = finrank K ↥U

If a functional f does not vanish on a finite-dimensional subspace U, then ker f ⊓ U has codimension one in U.