linearMap_ext — Mathlib

English

Auxiliary form of the universal property statement providing the equivalence with lift.

Русский

Вспомогательная форма универсального свойства, связывающая c lift.

LaTeX

$$$$ \exists! l : M' \to M'', \; l \circ f = g. $$$$

Lean4

theorem linearMap_ext {N N'} [AddCommMonoid N] [Module R N] [AddCommMonoid N'] [Module R N'] (f' : N →ₗ[R] N')
    [IsLocalizedModule S f'] ⦃g g' : M' →ₗ[R] N'⦄ (h : g ∘ₗ f = g' ∘ₗ f) : g = g' :=
  (is_universal S f _ <| map_units f').unique h rfl

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