English
Given a basis b of M, an auxiliary semiring S and a function f: ι → M', there is a linear map constr b S f: M → M' defined by combining f with the coordinates of x in basis b.
Русский
С данным базисом b модуля M, над семирингом S и функцией f: ι → M' существует линейное отображение constr b S f: M → M', задаваемое как линейная комбинация значений f по координатам x в базисе b.
LaTeX
$$$\\mathrm{constr}\, b\\ S\\ f : M \\to M',\\; (\\mathrm{constr}\\, b\\ S\\ f)(x) = \\sum_{i \\in ι} (b.\\mathrm{repr}\\, x)(i) \\cdot f(i).$$$
Lean4
/-- Construct a linear map given the value at the basis, called `Basis.constr b S f` where `b` is
a basis, `f` is the value of the linear map over the elements of the basis, and `S` is an
extra semiring (typically `S = R` or `S = ℕ`).
This definition is parameterized over an extra `Semiring S`,
such that `SMulCommClass R S M'` holds.
If `R` is commutative, you can set `S := R`; if `R` is not commutative,
you can recover an `AddEquiv` by setting `S := ℕ`.
See library note [bundled maps over different rings].
-/
def constr : (ι → M') ≃ₗ[S] M →ₗ[R] M'
where
toFun f := (Finsupp.linearCombination R id).comp <| Finsupp.lmapDomain R R f ∘ₗ ↑b.repr
invFun f i := f (b i)
left_inv
f := by
ext
simp
right_inv
f := by
refine b.ext fun i => ?_
simp
map_add' f
g := by
refine b.ext fun i => ?_
simp
map_smul' c
f := by
refine b.ext fun i => ?_
simp
