English
If A has an R-basis b, then the span over R_s of the images of b under localization equals the range of the linear map f that encodes the localization to A_s via IsScalarTower.
Русский
Если у A есть база над R, то замкнутая линейная оболочка образов этой базы в локализации равна образу отображения локализации к A_s через IsScalarTower.
LaTeX
$$$\\operatorname{span}_R\\big( \\mathrm{Set.range}\\big( b.ofIsLocalizedModule R_s S f \\big) \\big) = \\operatorname{LinearMap.range} f$$$
Lean4
theorem ofIsLocalizedModule_span : span R (Set.range (b.ofIsLocalizedModule Rₛ S f)) = LinearMap.range f := by
calc
span R (Set.range (b.ofIsLocalizedModule Rₛ S f))
_ = span R (f '' (Set.range b)) := by congr; ext; simp
_ = map f (span R (Set.range b)) := by rw [Submodule.map_span]
_ = LinearMap.range f := by rw [b.span_eq, Submodule.map_top]
