English
If the algebra map from R to A is surjective, then restricting scalars commutes with span: restrictScalars R (span_A X) = span_R X.
Русский
Если отображение R → A сюръективно, то ограничение скаляров и взятие порождающей линейной оболочки согласуются: restrictScalars R (span_A X) = span_R X.
LaTeX
$$$$\\operatorname{restrictScalars}_R(\\operatorname{span}_A X) = \\operatorname{span}_R X$$$$
Lean4
/-- If `A` is an `R`-algebra such that the induced morphism `R →+* A` is surjective, then the
`R`-module generated by a set `X` equals the `A`-module generated by `X`. -/
theorem restrictScalars_span (hsur : Function.Surjective (algebraMap R A)) (X : Set M) :
restrictScalars R (span A X) = span R X :=
by
refine ((span_le_restrictScalars R A X).antisymm fun m hm => ?_).symm
refine span_induction subset_span (zero_mem _) (fun _ _ _ _ => add_mem) (fun a m _ hm => ?_) hm
obtain ⟨r, rfl⟩ := hsur a
simpa [algebraMap_smul] using smul_mem _ r hm
