Ranges after extension of scalars

If the coefficient algebra is faithfully flat, membership of a vector in the range of a linear map can be checked after extension of scalars. This is the linear-algebraic descent step used when an equation acquires a solution after passing to a larger field.

This builds on Submodule.baseChange from Mathlib/LinearAlgebra/TensorProduct/Tower.lean and lTensor_mkQ and LinearMap.lTensor_range from Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean, as well as Module.FaithfullyFlat.one_tmul_eq_zero_iff from Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean.

Main results

• LinearMap.one_tmul_mem_range_baseChange_iff: a vector belongs to a range exactly when its canonical image belongs to the extended range, for a faithfully flat coefficient algebra.

@[simp]

theorem Submodule.one_tmul_mem_baseChange_iff {R : Type u} {A : Type v} {M : Type w} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module.FaithfullyFlat R A] (p : Submodule R M) (m : M) : 1 ⊗ₜ[R] m ∈ baseChange A p ↔ m ∈ p

Over a faithfully flat coefficient algebra, a vector belongs to a submodule exactly when its canonical image belongs to the extension of that submodule.

theorem LinearMap.one_tmul_mem_range_baseChange_iff {R : Type u} {A : Type v} {M : Type w} {N : Type x} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.FaithfullyFlat R A] (f : M →ₗ[R] N) (y : N) : 1 ⊗ₜ[R] y ∈ (baseChange A f).range ↔ y ∈ f.range

Over a faithfully flat coefficient algebra, a vector belongs to the range of a linear map if and only if its canonical image belongs to the range after extension of scalars.