lift_symm_apply

Mathlib.Algebra.FreeAlgebra

URI: https://scilib.ai/kg/mathlib#FreeAlgebra.lift_symm_apply

English

The inverse of lift sends an R-algebra homomorphism F to F ∘ ι_R.

Русский

Обратный к lift гомоморфизм F отправляет F на F ∘ ι_R.

LaTeX

$$$\mathrm{lift}\_R^{-1} (F) = F \circ \iota_R$$$

Lean4

@[simp]
theorem lift_symm_apply (F : FreeAlgebra R X →ₐ[R] A) : (lift R).symm F = F ∘ ι R :=
  by
  rw [lift]
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru