Kernels after extension of scalars

Mathlib's Submodule.baseChange extends a submodule of M to an A-submodule of A ⊗[R] M, and LinearMap.baseChange extends a linear map. For a general map the two constructions satisfy only the containment (ker f).baseChange A ≤ ker (f.baseChange A); it is an equality when A is flat over R. This file records that case and the other case in which it is an equality: the kernel of a surjective map is computed correctly after extending scalars along an arbitrary coefficient algebra, flat or not.

That is the form wanted when the map is a quotient map, where the kernel of the extension is to be identified with the extension of the submodule quotiented by.

Main results

• LinearMap.ker_baseChange_of_flat: over a flat coefficient algebra, the kernel of an extended linear map is the extension of its kernel.
• LinearMap.ker_baseChange_of_surjective: for a surjective map the kernel of an extended linear map is the extension of its kernel, with no hypothesis on the coefficient algebra.

References

• [N. Bourbaki, Algebra I, Chapters 1-3][bourbaki1989], Chapter II, §3, n°6, for the exactness properties of the tensor product.

theorem LinearMap.ker_baseChange_of_flat {R : Type u} (A : Type v) {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Ring A] [Algebra R A] [Module.Flat R A] (f : M →ₗ[R] N) : (baseChange A f).ker = Submodule.baseChange A f.ker

Over a flat coefficient algebra, extension of scalars commutes with kernels.

theorem LinearMap.ker_baseChange_of_surjective {R : Type u} (A : Type v) {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Ring A] [Algebra R A] (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) : (baseChange A f).ker = Submodule.baseChange A f.ker

Extension of scalars commutes with the kernel of a surjective map, with no hypothesis on the coefficient algebra. Dropping surjectivity, the same equality holds when A is flat over R, which is LinearMap.ker_baseChange_of_flat.