Nondegeneracy of the trace pairing #
This file records that the trace pairing on the endomorphisms of a finite free module is nondegenerate.
Main result #
TauCeti.LinearMap.ext_iff_trace_mul_right: two endomorphisms are equal exactly when their products with every endomorphism have equal trace.TauCeti.LinearMap.eq_zero_of_trace_mul_eq_zero: the corresponding zero criterion.
theorem
TauCeti.LinearMap.ext_iff_trace_mul_right
{K : Type u_1}
{V : Type u_2}
[CommSemiring K]
[AddCommMonoid V]
[Module K V]
[Module.Free K V]
[Module.Finite K V]
(f g : Module.End K V)
:
The trace pairing on the endomorphisms of a finite free module over a commutative semiring is nondegenerate.
theorem
TauCeti.LinearMap.eq_zero_of_trace_mul_eq_zero
{K : Type u_1}
{V : Type u_2}
[CommSemiring K]
[AddCommMonoid V]
[Module K V]
[Module.Free K V]
[Module.Finite K V]
(f : Module.End K V)
(h : ∀ (g : Module.End K V), (LinearMap.trace K V) (f * g) = 0)
:
An endomorphism whose product with every endomorphism has zero trace is zero.