English
IsBaseChange S f expresses that the base change of M along R → S via f is realized by a universal tensor-product condition, i.e., the map s ⊗ m ↦ s f(m) exhibits N as the base change of M to S.
Русский
IsBaseChange S f означает, что базовое изменение M вдоль R → S, реализуется через универсальное тензорное условие, то есть отображение s ⊗ m ↦ s f(m) характеризует N как базовое изменение M к S.
LaTeX
$$$ IsBaseChange(S,f) := IsTensorProduct\left( ((\mathrm{Algebra.linearMap} S (\mathrm{Module.End} S (M \to_R N))).flip f).restrictScalars R \right)$$$
Lean4
/-- Given an `R`-algebra `S` and an `R`-module `M`, an `S`-module `N` together with a map
`f : M →ₗ[R] N` is the base change of `M` to `S` if the map `S × M → N, (s, m) ↦ s • f m` is the
tensor product. -/
def IsBaseChange : Prop :=
IsTensorProduct (((Algebra.linearMap S <| Module.End S (M →ₗ[R] N)).flip f).restrictScalars R)
