lift_unique — Mathlib

English

For any algebra hom g, lift R (g ∘ ι_R) = g, i.e., lift is a left-inverse to evaluation on ι_R.

Русский

Для любого гомоморфизма g выполняется lift R (g ∘ ι_R) = g; lift является левосторонним обратным к взятию значения на ι_R.

LaTeX

$$$\mathrm{lift}\_R((g\,:\ FreeAlgebra(R,X) \to_A A) \circ \iota_R) = g$$$

Lean4

@[simp]
theorem lift_unique (f : X → A) (g : FreeAlgebra R X →ₐ[R] A) : (g : FreeAlgebra R X → A) ∘ ι R = f ↔ g = lift R f :=
  by
  rw [← (lift R).symm_apply_eq, lift]
  rfl

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