English
There is a natural linear map structure on C^n(I,N; I', V) given by the pointwise evaluation, i.e., f ↦ f(p) is linear for each p, and this extends to a linear map on the whole ContMDiffMap space.
Русский
Естественно линейное отображение на C^n(I,N; I', V), заданное точечной оценкой: f↦f(p) линейно по f и по каждому p, переходящее к линейному отображению на всём пространстве.
LaTeX
$$$C^n(I,N;I',V)\to V$ via $f\mapsto f(p)$ is linear for each fixed p.$$
Lean4
/-- For a manifold `N` and a `C^n` homomorphism `φ` between `C^n` rings `R'`, `R''`, the
'left-composition-by-`φ`' ring homomorphism from `C^n⟮I, N; I', R'⟯` to `C^n⟮I, N; I'', R''⟯`. -/
def compLeftRingHom {R' : Type*} [Ring R'] [TopologicalSpace R'] [ChartedSpace H' R'] [ContMDiffRing I' n R']
{R'' : Type*} [Ring R''] [TopologicalSpace R''] [ChartedSpace H'' R''] [ContMDiffRing I'' n R''] (φ : R' →+* R'')
(hφ : ContMDiff I' I'' n φ) : C^n⟮I, N; I', R'⟯ →+* C^n⟮I, N; I'', R''⟯ :=
{ ContMDiffMap.compLeftMonoidHom I N φ.toMonoidHom hφ, ContMDiffMap.compLeftAddMonoidHom I N φ.toAddMonoidHom hφ with
toFun := fun f => ⟨φ ∘ f, hφ.comp f.contMDiff⟩ }
