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:

• LinearMap.trace_restrict_eq_of_forall_mem

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' : ∀ x ∈ p, f x ∈ p := ⋯) : (trace R ↥p) (f.restrict hf') = (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.