lift_comp_ι — Mathlib

English

The left-inverse property of lift ensures that composing with ι_R recovers the original g.

Русский

Свойство левого обратного lift гарантирует, что композиция с ι_R восстанавливает исходный g.

LaTeX

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

Lean4

@[simp]
theorem lift_comp_ι (g : FreeAlgebra R X →ₐ[R] A) : lift R ((g : FreeAlgebra R X → A) ∘ ι R) = g :=
  by
  rw [← lift_symm_apply]
  exact (lift R).apply_symm_apply g

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