The diagonal operators of the invertible endomorphisms span all of them

A V-endomorphism f acts on the tensor power ⨂[K] (_ : ι), V diagonally, by f^{⊗ι} = PiTensorProduct.map (fun _ ↦ f). These diagonal operators are not closed under addition, so the span of the ones coming from invertible f is not visibly all of the span of them all. Over an infinite field and for a finite-dimensional V the two spans nonetheless coincide (PiTensorProduct.span_range_map_const_units_eq_span_range_map_const), because the invertible endomorphisms are Zariski dense. That is what lets the general linear group replace the whole endomorphism algebra in Schur-Weyl duality, where the commutant of the symmetric-group action is the span of the diagonal operators and one wants it to be the image of K[GL(V)].

The argument

A vector of a vector space lies in a subspace as soon as every functional vanishing on the subspace kills it (Subspace.forall_mem_dualAnnihilator_apply_eq_zero_iff). So fix a functional φ on End (⨂[K] (_ : ι), V) vanishing on the span of the invertible diagonal operators. Composing φ with PiTensorProduct.mapMultilinear, which is multilinear in the family of endomorphisms, and with the matrix-to-endomorphism isomorphism attached to a basis, produces a multilinear form Θ in ι matrix arguments whose diagonal is Θ (Y, …, Y) = φ (Y^{⊗ι}). That diagonal vanishes on the invertible matrices, hence identically, by MultilinearMap.apply_const_eq_zero_of_eq_zero_on_gl.

Main results

• PiTensorProduct.map_const_mem_span_range_map_const_units: the diagonal operator of an endomorphism is a combination of the diagonal operators of the invertible ones.
• PiTensorProduct.span_range_map_const_units_eq_span_range_map_const: consequently the two spans agree.

theorem PiTensorProduct.map_const_mem_span_range_map_const_units {K : Type u} {V : Type v} {ι : Type w} [Field K] [Infinite K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Finite ι] (f : V →ₗ[K] V) : (map fun (x : ι) => f) ∈ Submodule.span K (Set.range fun (u : (V →ₗ[K] V)ˣ) => map fun (x : ι) => ↑u)

The diagonal operator of an endomorphism is a combination of the diagonal operators of the invertible ones, over an infinite field and for a finite-dimensional V.

theorem PiTensorProduct.span_range_map_const_units_eq_span_range_map_const {K : Type u} {V : Type v} {ι : Type w} [Field K] [Infinite K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Finite ι] : Submodule.span K (Set.range fun (u : (V →ₗ[K] V)ˣ) => map fun (x : ι) => ↑u) = Submodule.span K (Set.range fun (f : V →ₗ[K] V) => map fun (x : ι) => f)

The diagonal operators of the invertible endomorphisms span the same subspace as all the diagonal operators, over an infinite field and for a finite-dimensional V.