lift_comp_inlHom — Mathlib

English

The lifted map when restricted to the base A recovers the original algebra map f.

Русский

Лифтованный отображение при ограничении к A восстанавливает исходное отображение f.

LaTeX

$$$ (\text{lift } fe) \circ (\text{inlAlgHom } R A A) = fe.1 $$$

Lean4

@[simp]
theorem lift_comp_inlHom (fe : { _fe : (A →ₐ[R] B) × B // _ }) : (lift fe).comp (inlAlgHom R A A) = fe.val.1 :=
  AlgHom.ext <| lift_apply_inl fe

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