Linear maps of modules with coefficients in a principal ideal domain #

Since a submodule of a free module over a PID is free, certain constructions which are often developed only for vector spaces may be generalised to any module with coefficients in a PID.

This file is a location for such results and exists to avoid making large parts of the linear algebra import hierarchy have to depend on the theory of PIDs.

Main results: #

theorem LinearMap.trace_restrict_eq_of_forall_mem {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R M] [IsDomain R] [IsPrincipalIdealRing R] (p : Submodule R M) (f : M →ₗ[R] M) (hf : ∀ (x : M), f x p) (hf' : optParam (∀ (x : M), x pf x p) fun x x_1 => hf x) :
↑(LinearMap.trace R { x // x p }) (LinearMap.restrict f hf') = ↑(LinearMap.trace R M) f

If a linear endomorphism of a (finite, free) module M takes values in a submodule p ⊆ M, then the trace of its restriction to p is equal to its trace on M.