English
For a polynomial law f : M →ₚₗ[R] N, ground(f) denotes the associated function M → N; ground is the evaluation of f as a function on elements of M.
Русский
Для полиномального закона f : M →ₚₗ[R] N грунтовая карта ground(f) обозначает соответствующую функцию M → N; ground — это применение f как функции к элементам M.
LaTeX
$$$\\text{ground}(f) : M \\to N \\quad\\text{is defined by}\\quad \\text{ground}(f)(m) = (\\text{TensorProduct.lid } R\\ N)\\left(f^{\\mathrm{toFun'}}(R, 1 \\otimes m)\\right).$$$
Lean4
/-- The map `M → N` associated with a `f : M →ₚₗ[R] N` (essentially, `f.toFun' R`) -/
def ground : M → N :=
(TensorProduct.lid R N) ∘ (f.toFun' R) ∘ (TensorProduct.lid R M).symm
