freeMap — Mathlib

English

The morphism of presheaves of R-modules free I ⟶ free J induced by a map f: I → J.

Русский

Гомоморфизм прешейфов модулей R, свободный по множеству I, в свободный по J определяется картой f: I → J.

LaTeX

$$$\mathrm{freeMap} : \mathrm{free}(R,I) \to \mathrm{free}(R,J)$$$

Lean4

/-- The morphism of presheaves of `R`-modules `free I ⟶ free J` induced by
a map `f : I → J`. -/
noncomputable def freeMap : free (R := R) I ⟶ free J :=
  (freeHomEquiv _).symm (fun i ↦ freeSection (f i))

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