English
Let i: M' → M and k: P' → P be linear maps over S, with k injective, and f: M → P a linear map over R such that f(i(m)) lies in the range of k for all m ∈ M'. Then there exists a linear lift restrictScalarsRange i k hk f hf : M' → P' with k ∘ restrictScalarsRange i k hk f hf = f ∘ i. In particular, for every m ∈ M', k(restrictScalarsRange i k hk f hf m) = f(i(m)).
Русский
Пусть i: M' → M и k: P' → P — линейные отображения над S, причём k вводит инъективно, и f: M → P — линейное отображение над R, такое что f(i(m)) принадлежит образу k для всех m ∈ M'. Тогда существует линеаризованное восхождение restrictScalarsRange i k hk f hf: M' → P' такое, что k ∘ restrictScalarsRange i k hk f hf = f ∘ i. В частности, для каждого m ∈ M' выполняется k(restrictScalarsRange i k hk f hf m) = f(i(m)).
LaTeX
$$$k\circ (restrictScalarsRange\\ i\\ k\\ hk\\ f\\ hf) = f\\circ i,$ for all m\in M', \quad k(restrictScalarsRange i k hk f hf\, m) = f(i(m)).$$
Lean4
@[simp]
theorem restrictScalarsRange_apply (m : M') : k (restrictScalarsRange i k hk f hf m) = f (i m) :=
by
have : k (restrictScalarsRange i k hk f hf m) = (k ∘ₗ ((f.restrictScalars S).comp i).codLift k hk hf) m := rfl
rw [this, comp_codLift, comp_apply, restrictScalars_apply]
