free_hom_ext — Mathlib

English

A homomorphism from the free R-module on X to M is completely determined by its values on the generators X; i.e., morphisms from free(X) to M are in bijection with functions X → M.

Русский

Гомоморфизм от свободного модуля свободного множества X в M определяется значениями на генераторах X; гомоморфизмы из свободного(X) в M эквивалентны функциям X → M.

LaTeX

$$$\mathrm{Hom}(\mathrm{Free}(R,X),M) \cong X \to M$$$

Lean4

@[ext 1200]
theorem free_hom_ext {X : Type u} {M : ModuleCat.{u} R} {f g : (free R).obj X ⟶ M}
    (h : ∀ (x : X), f (freeMk x) = g (freeMk x)) : f = g :=
  ModuleCat.hom_ext (Finsupp.lhom_ext' (fun x ↦ LinearMap.ext_ring (h x)))

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