lift_comp_iso — Mathlib

English

Equivalent formulation of the universal property: there exists a unique l with l ∘ f = g.

Русский

Эквивалентная формулировка универсального свойства: существует единственный l, удовлетворяющий l ∘ f = g.

LaTeX

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

Lean4

@[simp]
theorem lift_comp_iso (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x)) :
    IsLocalizedModule.lift S f g h ∘ₗ iso S f = LocalizedModule.lift S g h :=
  LinearMap.ext fun x ↦ lift_iso S f g h x

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