lift_symm_apply_apply — Mathlib

English

For φ a unitization algebra homomorphism, lifting followed by taking the inverse yields the original on A: lift.symm φ a = φ a.

Русский

Для гомоморфизма φ, восстанавливающего по единичизации, получаемое обратное отображение возвращает исходное на A: lift.symm φ a = φ a.

LaTeX

$$$\mathrm{lift}^{-1}(φ)(a) = φ(a)$ for all a ∈ A.$$

Lean4

theorem lift_symm_apply_apply (φ : Unitization R A →ₐ[R] C) (a : A) : Unitization.lift.symm φ a = φ a :=
  rfl

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