ι_comp_lift — Mathlib

English

There is a unique algebra hom g with given action on ι_R, namely g = lift R f when g ∘ ι_R = f.

Русский

Существует единственный алгебра-гомоморфизм g с заданным действием на ι_R: g = lift R f, если g ∘ ι_R = f.

LaTeX

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

Lean4

@[simp]
theorem ι_comp_lift (f : X → A) : (lift R f : FreeAlgebra R X → A) ∘ ι R = f :=
  by
  ext
  rw [Function.comp_apply, ι_def, lift]
  rfl

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