lift_map_single — Mathlib

English

There is a natural equivalence between morphisms from the free R-module on X to M and functions X → M: ((free R).obj X ⟶ M) ≃ (X → M).

Русский

Существует естественная эквивалентность между морфизмами от свободного R-модуля на X в M и функциями X → M: ((free R).obj X ⟶ M) ≃ (X → M).

LaTeX

$$$\mathrm{freeHomEquiv}: ((\mathrm{free}(R).obj X \to M) \simeq (X \to M))$$$

Lean4

theorem lift_map_single (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) (r : R) : (lift R F).map (single f r) = r • F.map f := by simp

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