The trace of an algebra endomorphism

Let S be a commutative A-algebra and σ : S →ₐ[A] S an algebra endomorphism, viewed as an A-linear endomorphism of S. Twisting σ by multiplication gives the linear functional z ↦ trace (σ ∘ m_z) on S. Since σ ∘ m_y = m_{σ y} ∘ σ, cyclicity of the trace shows that this functional takes the same value on x * σ y and on x * y, so it vanishes on the ideal generated by the elements σ y - y.

Evaluating at a scalar a lying in that ideal gives a * trace σ = 0. For the automorphism σ ≠ 1 of a finite Galois extension of fields one may take a = 1, recovering the classical fact that σ has trace zero, so the extension is the regular representation of its Galois group on the level of characters. The point of the statement over a ring is that it applies before passing to fraction fields: over a domain A, any nonzero scalar a with algebraMap A S a a multiple of σ y - y forces trace σ = 0.

Main statements

• AlgHom.trace_toLinearMap_comp_mulLeft_mul_sub: trace (σ ∘ m_{x (σ y - y)}) = 0.
• AlgHom.mul_trace_toLinearMap_eq_zero_of_mem_span: if algebraMap A S a lies in the ideal generated by σ y - y, then a * trace σ = 0.

theorem AlgHom.trace_toLinearMap_comp_mulLeft_mul_sub {A : Type u_1} {S : Type u_2} [CommRing A] [CommRing S] [Algebra A S] (σ : S →ₐ[A] S) (x y : S) : (LinearMap.trace A S) (σ.toLinearMap ∘ₗ LinearMap.mulLeft A (x * (σ y - y))) = 0

The functional z ↦ trace (σ ∘ m_z) vanishes on multiples of σ y - y: cyclicity of the trace and σ ∘ m_y = m_{σ y} ∘ σ give trace (σ ∘ m_{x σ y}) = trace (σ ∘ m_{x y}). No freeness or finiteness of S over A is needed; otherwise the trace is zero by definition.

theorem AlgHom.mul_trace_toLinearMap_eq_zero_of_mem_span {A : Type u_1} {S : Type u_2} [CommRing A] [CommRing S] [Algebra A S] (σ : S →ₐ[A] S) {a : A} {y : S} (h : (algebraMap A S) a ∈ Ideal.span {σ y - y}) : a * (LinearMap.trace A S) σ.toLinearMap = 0

If a scalar a maps into the ideal generated by σ y - y, then a annihilates the trace of the algebra endomorphism σ. Over a domain A, a nonzero such a forces trace σ = 0.