freeMap_map — Mathlib

English

Let R be a ring and X, Y be topological spaces (viewed as objects in TopCat). For a continuous map f: X → Y and any finitely supported function v: X → R, the induced map on the free R-module of X coincides with pushing the domain along f: (freeMap R f)(v) = Finsupp.mapDomain f v.

Русский

Пусть R — кольцо, X, Y — топологические пространства. Для непрерывного отображения f: X → Y и любого v ∈ X →₀ R выполнение на свободном модуле над X даёт ту же функцию, что и перенос области по f: (freeMap R f)(v) = Finsupp.mapDomain f v.

LaTeX

$$$ (freeMap \, R \, f)(v) = \mathrm{Finsupp.mapDomain}(f)(v). $$$

Lean4

theorem freeMap_map {X Y : TopCat} (f : X ⟶ Y) (v : X →₀ R) :
    (freeMap R f : (X →₀ R) → (Y →₀ R)) v = Finsupp.mapDomain f.hom v :=
  rfl

Похожие утверждения