English
If f is a base change, then every R-linear map M → Q factors uniquely through f as an S-linear map N → Q, using a canonical lift.
Русский
Если f — базовое изменение, то любой линейный отображение M → Q разлагается через f в единственном виде как S-линейное отображение N → Q, через каноническое поднятие.
LaTeX
$$$ \text{lift } g : N \to_S Q \;\;\text{with} \; (g'.restrictScalars R).comp f = g$$$
Lean4
/-- Suppose `f : M →ₗ[R] N` is the base change of `M` along `R → S`. Then any `R`-linear map from
`M` to an `S`-module factors through `f`. -/
noncomputable nonrec def lift (g : M →ₗ[R] Q) : N →ₗ[S] Q :=
{ h.lift (((Algebra.linearMap S <| Module.End S (M →ₗ[R] Q)).flip g).restrictScalars R) with
map_smul' := fun r x =>
by
let F := ((Algebra.linearMap S <| Module.End S (M →ₗ[R] Q)).flip g).restrictScalars R
have hF : ∀ (s : S) (m : M), h.lift F (s • f m) = s • g m := h.lift_eq F
change h.lift F (r • x) = r • h.lift F x
induction x using h.inductionOn with
| zero => rw [smul_zero, map_zero, smul_zero]
| tmul s m =>
change h.lift F (r • s • f m) = r • h.lift F (s • f m)
rw [← mul_smul, hF, hF, mul_smul]
| add x₁ x₂ e₁ e₂ => rw [map_add, smul_add, map_add, smul_add, e₁, e₂] }
