English
Base-change of a submodule p equals the span of its image under the canonical map into A ⊗ M.
Русский
Расширение по основанию подмодуля p равно порождению образа p в A ⊗ M.
LaTeX
$$$$ p.baseChange A = \\operatorname{span}_A( p.map(\\mathrm{TensorProduct.mk}\; R\\; A\\; M\\; 1) ). $$$$
Lean4
theorem baseChange_eq_span : p.baseChange A = span A (p.map (TensorProduct.mk R A M 1)) :=
by
refine le_antisymm ?_ ?_
· rw [baseChange, LinearMap.range_le_iff_comap, eq_top_iff, ←
span_eq_top_of_span_eq_top R A _ (span_tmul_eq_top R ..), span_le]
refine fun _ ⟨a, m, h⟩ ↦ ?_
rw [← h, SetLike.mem_coe, mem_comap, LinearMap.baseChange_tmul, ← mul_one a, ← smul_eq_mul, ← smul_tmul']
exact smul_mem _ a (subset_span ⟨m, m.2, rfl⟩)
· refine span_le.2 fun _ ⟨m, hm, h⟩ ↦ h ▸ ⟨1 ⊗ₜ[R] ⟨m, hm⟩, rfl⟩
